projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 07c4b6c) | patch
Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 31 Aug 2016 22:44:42 +0000 (17:44 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 1 Sep 2016 14:46:59 +0000 (09:46 -0500)
commit2cadfe31cfddaff7eff4cd220273d0bab3d2792d
tree5a519bf9fe2da10e03ec2a4faf167c09ae1792f7tree
parent07c4b6c27aac497c74695dd559adfee0d9e8e83fcommit | diff
Updates to cbqi.  New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
12 files changed:
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/inst_match.cpp 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/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h 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