projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c833e17) | patch
More work on instantiation propagation. Enable external filtering of instantiations...
authorajreynol <andrew.j.reynolds@gmail.com>
Sun, 10 Apr 2016 20:20:33 +0000 (15:20 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Sun, 10 Apr 2016 20:20:41 +0000 (15:20 -0500)
commit5e4ed407978b892e04de00994be535f58fb33257
tree5ff2dfbf18845113c5ea0fa43e8792532498d2ectree
parentc833e176a81eb193462c0efde0c6c2f28c5159fbcommit | diff
More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.
22 files changed:
src/theory/quantifiers/ambqi_builder.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.h diff | blob | history
src/theory/quantifiers/full_model_check.cpp 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_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.cpp diff | blob | history
src/theory/quantifiers/inst_propagator.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/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history