projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7e133db) | patch
Enable counterexample-guided quantifier instantiation by default for quantified logic...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 22 Oct 2015 09:01:05 +0000 (11:01 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 22 Oct 2015 09:01:05 +0000 (11:01 +0200)
commita7a9ba359a2a8a26f20ac8fdf5292c4e0e27c76a
treea62e3c29bb702a2e890b234504bbc121c4da2619tree
parent7e133dbb7c1adf077102d377d1f7eecae1640ee1commit | diff
Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
18 files changed:
src/Makefile.am diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp [new file with mode: 0644] blob
src/theory/quantifiers/ceg_instantiator.h [new file with mode: 0644] blob
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/modes.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress0/bug519.smt2 diff | blob | history
test/regress/regress0/quantifiers/bug291.smt2 diff | blob | history
test/regress/regress0/quantifiers/bug291.smt2.expect diff | blob | history
test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 diff | blob | history