projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 740df59) | patch
refactoring of quantifiers rewriter based on code review from yesterday, refactoring...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 13 Nov 2012 21:16:26 +0000 (21:16 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 13 Nov 2012 21:16:26 +0000 (21:16 +0000)
commit795e5ba8a1138a371409ac9c8e9da78ce652bb94
tree5cc0d5bebbccf87b122b9e1690f27e398b4e8cc0tree
parent740df5937639738a0238312dfb061643e62ba605commit | diff
refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine
14 files changed:
src/theory/arith/theory_arith.h diff | blob | history
src/theory/arith/theory_arith_instantiator.cpp diff | blob | history
src/theory/arith/theory_arith_instantiator.h diff | blob | history
src/theory/datatypes/theory_datatypes_instantiator.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_instantiator.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/theory_uf_instantiator.cpp diff | blob | history
src/theory/uf/theory_uf_instantiator.h diff | blob | history
src/util/sort_inference.cpp diff | blob | history