projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8a43f6c) | patch
Do not eliminate variables only occurring in patterns. Minor improvements to sort...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 10 Nov 2014 14:53:51 +0000 (15:53 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 10 Nov 2014 14:53:51 +0000 (15:53 +0100)
commitbe316870ef337a435d65f46a26f40ef0eab97934
tree24db24b777180ea71d0e9078b7bcf4eff05ae9dctree
parent8a43f6c6aa01f9b27434caf1c5dd9ef6b2dcd963commit | diff
Do not eliminate variables only occurring in patterns.  Minor improvements to sort inference.  Remove unused code.
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp 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/theory_engine.cpp diff | blob | history
src/util/sort_inference.cpp diff | blob | history