projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f2abab) | patch
made datatypes rewrite incorrect selectors to ground term. this feature can be turne...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 9 Oct 2012 17:44:02 +0000 (17:44 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 9 Oct 2012 17:44:02 +0000 (17:44 +0000)
commit680d9e20d412afe24a23dcaf3a4e440bcf208fbe
tree6bac4b3ba212d021cfbb0136c232b149f3d22acctree
parent5f2ababa9d26f94e8438dc1d17b60781fcaa8522commit | diff
made datatypes rewrite incorrect selectors to ground term.  this feature can be turned off by --disable-dt-rewrite-error-sel.  changed regression answer to reflect new default behavior.
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
test/regress/regress0/datatypes/wrong-sel-simp.cvc diff | blob | history