diff options
Diffstat (limited to 'src/theory')
36 files changed, 205 insertions, 60 deletions
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 */ |