projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 97111ec) | patch
cleaned up some of the hacks in the datatypes theory solver, working on using Transit...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Apr 2011 00:49:02 +0000 (00:49 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Apr 2011 00:49:02 +0000 (00:49 +0000)
commitc21ca8353370eb44aa6318e6ee4bffee64197fd8
tree4f67e58bad5c372034c34df2681b818b3c164488tree
parent97111ecb8681838f2d201420cda12ca9fc7184edcommit | diff
cleaned up some of the hacks in the datatypes theory solver, working on using Transitive Closure to detect cycles, added rewrite rule for disinguished ground terms
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/util/trans_closure.cpp diff | blob | history
src/util/trans_closure.h diff | blob | history