projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4479383) | patch
Eliminate raw use of output channel and valuation in quantifiers (#5933)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 22 Feb 2021 23:19:20 +0000 (17:19 -0600)
committerGitHub <noreply@github.com>
Mon, 22 Feb 2021 23:19:20 +0000 (17:19 -0600)
commit13819c4ae33a103b1075e816772a305b16db9157
treef8598d57ac30065091fd2115af2f25cef1673acdtree
parent4479383c2fd8a3b81ab63d66f843b09b5c9d0cd3commit | diff
Eliminate raw use of output channel and valuation in quantifiers (#5933)

This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
28 files changed:
src/theory/inference_id.h diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/cegqi/vts_term_cache.cpp diff | blob | history
src/theory/quantifiers/cegqi/vts_term_cache.h diff | blob | history
src/theory/quantifiers/ematching/ho_trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/ho_trigger.h diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.h diff | blob | history
src/theory/quantifiers/fmf/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis.h diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.h diff | blob | history
src/theory/quantifiers/sygus/cegis_unif.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_unif.h diff | blob | history
src/theory/quantifiers/sygus/sygus_module.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_module.h diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.h diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus_inst.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history