projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c34722f) | patch
Use standard conflict mechanism in quantifiers state (#5822)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Jan 2021 01:24:58 +0000 (19:24 -0600)
committerGitHub <noreply@github.com>
Wed, 27 Jan 2021 01:24:58 +0000 (19:24 -0600)
commit524c2d9f44a7c4297422dd1356fe3dc377166180
tree7cb5988f7d9feb633bb9dace3f272015ddd8300ftree
parentc34722f830b63bc45a38217943f061912990086dcommit | diff
Use standard conflict mechanism in quantifiers state (#5822)

Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck.
23 files changed:
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy.h diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.h diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h diff | blob | history
src/theory/quantifiers/ematching/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.h diff | blob | history
src/theory/quantifiers/fmf/model_builder.cpp diff | blob | history
src/theory/quantifiers/fmf/model_builder.h diff | blob | history
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/sygus/synth_engine.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory_state.cpp diff | blob | history
src/theory/theory_state.h diff | blob | history