projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8936ca3) | patch
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 17 Jun 2013 20:31:28 +0000 (15:31 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 17 Jun 2013 20:31:38 +0000 (15:31 -0500)
commit66ee6c6472264be842f4e80a7106399d7f51d28a
tree55c6adcdcadc41c7b34d46eea7081d8bdc2eb7a0tree
parent8936ca3ab2a1b9e3612e08a73542f7a288ee1df8commit | diff
Make --var-elim-quant true by default.  Add rewrite engine to quantifiers module.
16 files changed:
src/theory/quantifiers/Makefile.am diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_builder.h diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.cpp [new file with mode: 0755] blob
src/theory/quantifiers/rewrite_engine.h [new file with mode: 0755] blob
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/rewriterules/theory_rewriterules_rules.cpp diff | blob | history