projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c603a04) | patch
Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 17 Feb 2016 23:35:56 +0000 (17:35 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 17 Feb 2016 23:35:56 +0000 (17:35 -0600)
commitb0d7ac44fb7be5c56cd0c743114e792a985bb3b7
tree4d5e8de3b66de4af0fe225d594edd78726b8bb1dtree
parentc603a047ac534ed4caafb128b5d333e05e1fd191commit | diff
Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.
17 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.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/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history