diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-26 15:03:23 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-26 15:03:23 -0600 |
commit | c34722f830b63bc45a38217943f061912990086d (patch) | |
tree | 41f5d335973c675cc2f5d6e08df0b350ba10bae9 /src | |
parent | 06e367c39bf080b9a82dea82ebdf8b9fb79409d5 (diff) |
Introduce quantifiers inference manager (#5821)
This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas.
The code for adding lemmas in quantifiers engine will be migrated to this class.
Diffstat (limited to 'src')
37 files changed, 207 insertions, 60 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1f7fc8bac..dbf00409c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -721,6 +721,8 @@ libcvc4_add_sources( theory/quantifiers/quant_util.h theory/quantifiers/quantifiers_attributes.cpp theory/quantifiers/quantifiers_attributes.h + theory/quantifiers/quantifiers_inference_manager.cpp + theory/quantifiers/quantifiers_inference_manager.h theory/quantifiers/quantifiers_modules.cpp theory/quantifiers/quantifiers_modules.h theory/quantifiers/quantifiers_rewriter.cpp diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 539dc1474..980bc1d4b 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -50,8 +50,9 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, } InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe, - QuantifiersState& qs) - : QuantifiersModule(qs, qe), + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index f98ea8549..d4b78d306 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -69,7 +69,9 @@ class InstStrategyCegqi : public QuantifiersModule typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; public: - InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs); + InstStrategyCegqi(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~InstStrategyCegqi(); /** whether to do counterexample-guided instantiation for quantifier q */ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 2b3bb807a..280c8c511 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -86,8 +86,9 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, - QuantifiersState& qs) - : QuantifiersModule(qs, qe), + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_notify(*this), d_uequalityEngine( d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false), diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 79c6f3f29..e45853e12 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -435,7 +435,9 @@ private: //information about ground equivalence classes unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: - ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs); + ConjectureGenerator(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~ConjectureGenerator(); /* needs check */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index d4904ebe8..382cb233f 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -35,8 +35,9 @@ namespace theory { namespace quantifiers { InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, - QuantifiersState& qs) - : QuantifiersModule(qs, qe), + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_instStrategies(), d_isup(), d_i_ag(), diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index f22da6ec1..f5b999cea 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -48,7 +48,9 @@ class InstantiationEngine : public QuantifiersModule { void doInstantiationRound(Theory::Effort effort); public: - InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs); + InstantiationEngine(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~InstantiationEngine(); void presolve() override; bool needsCheck(Theory::Effort e) override; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 51f88ad44..0f17bb04a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -84,8 +84,10 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() return lem; } -BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs) - : QuantifiersModule(qs, qe) +BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe) { } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index ff971bc12..685c07d82 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -161,7 +161,9 @@ private: std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; public: - BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs); + BoundedIntegers(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); virtual ~BoundedIntegers(); void presolve() override; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 8803fdb2c..3849dc2c6 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -35,8 +35,10 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; //Model Engine constructor -ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs) - : QuantifiersModule(qs, qe), +ModelEngine::ModelEngine(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 5616eaf5e..3e212b319 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -43,7 +43,9 @@ private: int d_triedLemmas; int d_totalLemmas; public: - ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs); + ModelEngine(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); virtual ~ModelEngine(); public: diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index c064819fc..1dff5e000 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -34,8 +34,9 @@ namespace quantifiers { InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, RelevantDomain* rd) - : QuantifiersModule(qs, qe), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1) { } void InstStrategyEnum::presolve() diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index a24aeedab..5687624db 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -64,6 +64,7 @@ class InstStrategyEnum : public QuantifiersModule public: InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, RelevantDomain* rd); ~InstStrategyEnum() {} /** Presolve */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 23942ba7e..822c9b323 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1838,8 +1838,9 @@ bool MatchGen::isHandled( TNode n ) { } QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, - QuantifiersState& qs) - : QuantifiersModule(qs, qe), + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst<bool>(true)), d_false(NodeManager::currentNM()->mkConst<bool>(false)), diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index f90f1db18..15b3d119a 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -232,7 +232,9 @@ private: //for equivalence classes bool areMatchDisequal( TNode n1, TNode n2 ); public: - QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs); + QuantConflictFind(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); /** register quantifier */ void registerQuantifier(Node q) override; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 588d4de76..ad65c06cd 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -25,8 +25,10 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs) - : QuantifiersModule(qs, qe), d_added_split(qs.getUserContext()) +QuantDSplit::QuantDSplit(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_added_split(qs.getUserContext()) { } diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 6f9e74fad..76ac1a974 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -49,7 +49,9 @@ class QuantDSplit : public QuantifiersModule { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs); + QuantDSplit(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); /** determine whether this quantified formula will be reduced */ void checkOwnership(Node q) override; /* whether this module needs to check this round */ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index cbaa8bfe6..dcf38eccb 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -23,9 +23,11 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -QuantifiersModule::QuantifiersModule(quantifiers::QuantifiersState& qs, - QuantifiersEngine* qe) - : d_quantEngine(qe), d_qstate(qs) +QuantifiersModule::QuantifiersModule( + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim) { } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 240282d3d..5040bd232 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -21,6 +21,7 @@ #include <map> #include <vector> +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -58,7 +59,9 @@ class QuantifiersModule { }; public: - QuantifiersModule(quantifiers::QuantifiersState& qs, QuantifiersEngine* qe); + QuantifiersModule(quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe); virtual ~QuantifiersModule(){} /** Presolve. * @@ -159,6 +162,8 @@ class QuantifiersModule { QuantifiersEngine* d_quantEngine; /** The state of the quantifiers engine */ quantifiers::QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& d_qim; };/* class QuantifiersModule */ /** Quantifiers utility diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp new file mode 100644 index 000000000..f456dd407 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -0,0 +1,31 @@ +/********************* */ +/*! \file quantifiers_inference_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for quantifiers inference manager + **/ + +#include "theory/quantifiers/quantifiers_inference_manager.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantifiersInferenceManager::QuantifiersInferenceManager( + Theory& t, QuantifiersState& state, ProofNodeManager* pnm) + : InferenceManagerBuffered(t, state, pnm) +{ +} + +QuantifiersInferenceManager::~QuantifiersInferenceManager() {} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h new file mode 100644 index 000000000..f89606d75 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file quantifiers_inference_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for quantifiers inference manager + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H + +#include "theory/inference_manager_buffered.h" +#include "theory/quantifiers/quantifiers_state.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * The quantifiers inference manager. + */ +class QuantifiersInferenceManager : public InferenceManagerBuffered +{ + public: + QuantifiersInferenceManager(Theory& t, + QuantifiersState& state, + ProofNodeManager* pnm); + ~QuantifiersInferenceManager(); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */ diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 719cc3de1..573824b80 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -39,49 +39,50 @@ QuantifiersModules::QuantifiersModules() QuantifiersModules::~QuantifiersModules() {} void QuantifiersModules::initialize(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, std::vector<QuantifiersModule*>& modules) { // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qe, qs)); + d_qcf.reset(new QuantConflictFind(qe, qs, qim)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qe, qs)); + d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new InstantiationEngine(qe, qs)); + d_inst_engine.reset(new InstantiationEngine(qe, qs, qim)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qe, qs)); + d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim)); modules.push_back(d_i_cbqi.get()); qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { - d_synth_e.reset(new SynthEngine(qe, qs)); + d_synth_e.reset(new SynthEngine(qe, qs, qim)); modules.push_back(d_synth_e.get()); } // finite model finding if (options::fmfBound()) { - d_bint.reset(new BoundedIntegers(qe, qs)); + d_bint.reset(new BoundedIntegers(qe, qs, qim)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) { - d_model_engine.reset(new ModelEngine(qe, qs)); + d_model_engine.reset(new ModelEngine(qe, qs, qim)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qe, qs)); + d_qsplit.reset(new QuantDSplit(qe, qs, qim)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) @@ -92,12 +93,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { d_rel_dom.reset(new RelevantDomain(qe)); - d_fs.reset(new InstStrategyEnum(qe, qs, d_rel_dom.get())); + d_fs.reset(new InstStrategyEnum(qe, qs, qim, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qe, qs)); + d_sygus_inst.reset(new SygusInst(qe, qs, qim)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 5aa8cf1d5..ba48cc68b 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -53,6 +53,7 @@ class QuantifiersModules */ void initialize(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, std::vector<QuantifiersModule*>& modules); private: diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 09a6add1c..fc1bda579 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -30,8 +30,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs) - : QuantifiersModule(qs, qe), +SynthEngine::SynthEngine(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_tds(qe->getTermDatabaseSygus()), d_conj(nullptr), d_sqp(qe) diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index e3cf2e47b..63175cf0c 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -33,7 +33,9 @@ class SynthEngine : public QuantifiersModule typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; public: - SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs); + SynthEngine(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~SynthEngine(); /** presolve * diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 210ebb921..728797d85 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -46,9 +46,12 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs) +TermDbSygus::TermDbSygus(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) : d_quantEngine(qe), d_qstate(qs), + d_qim(qim), d_syexp(new SygusExplain(this)), d_ext_rw(new ExtendedRewriter(true)), d_eval(new Evaluator), diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 1bf6b6ca7..ba09c723f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -54,7 +54,9 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r); // TODO :issue #1235 split and document this class class TermDbSygus { public: - TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs); + TermDbSygus(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~TermDbSygus() {} /** Reset this utility */ bool reset(Theory::Effort e); @@ -318,6 +320,8 @@ class TermDbSygus { QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; //------------------------------utilities /** sygus explanation */ diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 12ce544d3..c4c722ab2 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -180,8 +180,10 @@ void addSpecialValues( } // namespace -SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs) - : QuantifiersModule(qs, qe), +SygusInst::SygusInst(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : QuantifiersModule(qs, qim, qe), d_ce_lemma_added(qs.getUserContext()), d_global_terms(qs.getUserContext()), d_notified_assertions(qs.getUserContext()) diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 10363f5a2..4820398be 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -62,7 +62,9 @@ namespace quantifiers { class SygusInst : public QuantifiersModule { public: - SygusInst(QuantifiersEngine* qe, QuantifiersState& qs); + SygusInst(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~SygusInst() = default; bool needsCheck(Theory::Effort e) override; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 047a3cd41..12cdb1b8c 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -33,8 +33,13 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TermDb::TermDb(QuantifiersState& qs, QuantifiersEngine* qe) - : d_quantEngine(qe), d_inactive_map(qs.getSatContext()) +TermDb::TermDb(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersEngine* qe) + : d_quantEngine(qe), + d_qstate(qs), + d_qim(qim), + d_inactive_map(qs.getSatContext()) { d_consistent_ee = true; d_true = NodeManager::currentNM()->mkConst(true); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index afb8d0c0c..c246ea6fc 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -76,7 +76,9 @@ class TermDb : public QuantifiersUtil { typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; public: - TermDb(QuantifiersState& qs, QuantifiersEngine* qe); + TermDb(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersEngine* qe); ~TermDb(); /** presolve (called once per user check-sat) */ void presolve(); @@ -303,6 +305,10 @@ class TermDb : public QuantifiersUtil { private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; + /** The quantifiers state object */ + QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** terms processed */ std::unordered_set< Node, NodeHashFunction > d_processed; /** terms processed */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 808c88b78..d01d6a83f 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -36,7 +36,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TermUtil::TermUtil(QuantifiersEngine* qe) : d_quantEngine(qe) +TermUtil::TermUtil() { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index fb982eea8..4033c888f 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -70,11 +70,8 @@ class TermUtil : public QuantifiersUtil friend class ::CVC4::theory::QuantifiersEngine; friend class Instantiate; - private: - /** reference to the quantifiers engine */ - QuantifiersEngine* d_quantEngine; -public: - TermUtil(QuantifiersEngine * qe); + public: + TermUtil(); ~TermUtil(); /** boolean terms */ Node d_true; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index aaf8f347c..4dd59d12f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -44,7 +44,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, ProofNodeManager* pnm) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), d_qstate(c, u, valuation), - d_qengine(d_qstate, pnm) + d_qim(*this, d_qstate, pnm), + d_qengine(d_qstate, d_qim, pnm) { out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute("qid", this); @@ -60,6 +61,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, } // indicate we are using the quantifiers theory state object d_theoryState = &d_qstate; + // use the inference manager as the official inference manager + d_inferManager = &d_qim; // Set the pointer to the quantifiers engine, which this theory owns. This // pointer will be retreived by TheoryEngine and set to all theories diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 82a588009..8d2366065 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -21,6 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/proof_checker.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" @@ -81,6 +82,8 @@ class TheoryQuantifiers : public Theory { QuantifiersProofRuleChecker d_qChecker; /** The quantifiers state */ QuantifiersState d_qstate; + /** The quantifiers inference manager */ + QuantifiersInferenceManager d_qim; /** The quantifiers engine, which lives here */ QuantifiersEngine d_qengine; };/* class TheoryQuantifiers */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f60bb724f..fa7e50e1c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,9 +30,12 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate, - ProofNodeManager* pnm) +QuantifiersEngine::QuantifiersEngine( + quantifiers::QuantifiersState& qstate, + quantifiers::QuantifiersInferenceManager& qim, + ProofNodeManager* pnm) : d_qstate(qstate), + d_qim(qim), d_te(nullptr), d_decManager(nullptr), d_masterEqualityEngine(nullptr), @@ -40,9 +43,9 @@ QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate, d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), - d_term_util(new quantifiers::TermUtil(this)), + d_term_util(new quantifiers::TermUtil), d_term_canon(new expr::TermCanonize), - d_term_db(new quantifiers::TermDb(qstate, this)), + d_term_db(new quantifiers::TermDb(qstate, qim, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)), @@ -68,7 +71,7 @@ QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate, if (options::sygus() || options::sygusInst()) { // must be constructed here since it is required for datatypes finistInit - d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate)); + d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate, qim)); } d_util.push_back(d_instantiate.get()); @@ -128,7 +131,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, d_masterEqualityEngine = mee; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(this, d_qstate, d_modules); + d_qmodules->initialize(this, d_qstate, d_qim, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7ed183342..5a371ff09 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -31,6 +31,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -61,6 +62,7 @@ class QuantifiersEngine { public: QuantifiersEngine(quantifiers::QuantifiersState& qstate, + quantifiers::QuantifiersInferenceManager& qim, ProofNodeManager* pnm); ~QuantifiersEngine(); //---------------------- external interface @@ -337,6 +339,8 @@ public: private: /** The quantifiers state object */ quantifiers::QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& d_qim; /** Pointer to theory engine object */ TheoryEngine* d_te; /** Reference to the decision manager of the theory engine */ |