diff options
Diffstat (limited to 'src/theory')
54 files changed, 265 insertions, 227 deletions
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 531dd8d21..c91ba419b 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -84,9 +84,10 @@ QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() { } } -QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe) - : QuantifiersModule(qe) { - d_sqc = new CDSkQuantCache(qe->getUserContext()); +QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe) +{ + d_sqc = new CDSkQuantCache(qs.getUserContext()); } QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; } @@ -160,7 +161,8 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) { Assert(!quants.empty()); std::sort( quants.begin(), quants.end() ); - if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){ + if (d_sqc->add(d_qstate.getUserContext(), quants)) + { //partition into connected components if( pconnected && quants.size()>1 ){ Trace("anti-sk-debug") << "Partition into connected components..." << std::endl; diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 93834d7ce..21faa0361 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -32,8 +32,8 @@ namespace theory { namespace quantifiers { class QuantAntiSkolem : public QuantifiersModule { -public: - QuantAntiSkolem( QuantifiersEngine * qe ); + public: + QuantAntiSkolem(QuantifiersEngine* qe, QuantifiersState& qs); virtual ~QuantAntiSkolem(); bool sendAntiSkolemizeLemma( std::vector< Node >& quants, diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 16c7476ab..539dc1474 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -49,12 +49,13 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, return d_parent->rewriteInstantiation(q, terms, inst, doVts); } -InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) - : QuantifiersModule(qe), +InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe, + QuantifiersState& qs) + : QuantifiersModule(qs, qe), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), - d_added_cbqi_lemma(qe->getUserContext()), + d_added_cbqi_lemma(qs.getUserContext()), d_vtsCache(new VtsTermCache(qe)), d_bv_invert(nullptr) { @@ -68,7 +69,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) } if (options::cegqiNestedQE()) { - d_nestedQe.reset(new NestedQe(qe->getUserContext())); + d_nestedQe.reset(new NestedQe(qs.getUserContext())); } } @@ -168,7 +169,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) d_dstrat[q].reset( new DecisionStrategySingleton("CexLiteral", ceLit, - d_quantEngine->getSatContext(), + d_qstate.getSatContext(), d_quantEngine->getValuation())); dlds = d_dstrat[q].get(); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 1860962c7..f98ea8549 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -69,7 +69,7 @@ class InstStrategyCegqi : public QuantifiersModule typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; public: - InstStrategyCegqi(QuantifiersEngine* qe); + InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs); ~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 e13902077..2b3bb807a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -86,11 +86,12 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, - context::Context* c) - : QuantifiersModule(qe), + QuantifiersState& qs) + : QuantifiersModule(qs, qe), d_notify(*this), - d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), - d_ee_conjectures(c), + d_uequalityEngine( + d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false), + d_ee_conjectures(qs.getSatContext()), d_conj_count(0), d_subs_confirmCount(0), d_subs_unkCount(0), @@ -163,7 +164,7 @@ ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bo if( eqc_i!=d_eqc_info.end() ){ return eqc_i->second; }else if( doMake ){ - EqcInfo* ei = new EqcInfo( d_quantEngine->getSatContext() ); + EqcInfo* ei = new EqcInfo(d_qstate.getSatContext()); d_eqc_info[n] = ei; return ei; }else{ diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 0c8106ad5..79c6f3f29 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -433,8 +433,9 @@ private: //information about ground equivalence classes bool d_hasAddedLemma; //flush the waiting conjectures unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); -public: - ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ); + + public: + ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs); ~ConjectureGenerator(); /* needs check */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 7eb5a1378..d4904ebe8 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -34,8 +34,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe) - : QuantifiersModule(qe), +InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, + QuantifiersState& qs) + : QuantifiersModule(qs, 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 9304c84ae..f22da6ec1 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -48,7 +48,7 @@ class InstantiationEngine : public QuantifiersModule { void doInstantiationRound(Theory::Effort effort); public: - InstantiationEngine(QuantifiersEngine* qe); + InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs); ~InstantiationEngine(); void presolve() override; bool needsCheck(Theory::Effort e) override; diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 0b4539d7a..3887c583b 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -33,8 +33,8 @@ namespace theory { namespace quantifiers { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( - context::Context* c, QuantifiersEngine* qe) - : d_qe(qe), d_eqi_counter(c), d_reset_count(0) + QuantifiersState& qs, QuantifiersEngine* qe) + : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0) { } diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index b11dbe033..b82b9ae64 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -21,6 +21,7 @@ #include "context/context.h" #include "expr/node.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quantifiers_state.h" namespace CVC4 { namespace theory { @@ -43,7 +44,7 @@ namespace quantifiers { class EqualityQueryQuantifiersEngine : public EqualityQuery { public: - EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe); + EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe); virtual ~EqualityQueryQuantifiersEngine(); /** reset */ bool reset(Theory::Effort e) override; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index ba91960e1..8f587c09d 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -34,11 +34,11 @@ namespace theory { namespace quantifiers { FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe, - context::Context* c, + QuantifiersState& qs, std::string name) - : TheoryModel(c, name, true), + : TheoryModel(qs.getSatContext(), name, true), d_qe(qe), - d_forall_asserts(c), + d_forall_asserts(qs.getSatContext()), d_forallRlvComputed(false) { } @@ -335,9 +335,11 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) return n.getAttribute(ModelBasisArgAttribute()); } -FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(qe, c, name){ - +FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe, + QuantifiersState& qs, + std::string name) + : FirstOrderModel(qe, qs, name) +{ } FirstOrderModelFmc::~FirstOrderModelFmc() diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index a26401dd1..e4236a95d 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,6 +19,7 @@ #include "context/cdlist.h" #include "expr/attribute.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" @@ -54,7 +55,9 @@ typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute; class FirstOrderModel : public TheoryModel { public: - FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); + FirstOrderModel(QuantifiersEngine* qe, + QuantifiersState& qs, + std::string name); virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } /** assert quantifier */ @@ -198,7 +201,9 @@ class FirstOrderModelFmc : public FirstOrderModel void processInitializeModelForTerm(Node n) override; public: - FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); + FirstOrderModelFmc(QuantifiersEngine* qe, + QuantifiersState& qs, + std::string name); ~FirstOrderModelFmc() override; FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; } // initialize the model diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 2d6af9a63..51f88ad44 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -84,8 +84,8 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() return lem; } -BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) - : QuantifiersModule(qe) +BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe) { } @@ -493,8 +493,8 @@ void BoundedIntegers::checkOwnership(Node f) d_ranges.push_back( r ); d_rms[r].reset( new IntRangeDecisionHeuristic(r, - d_quantEngine->getSatContext(), - d_quantEngine->getUserContext(), + d_qstate.getSatContext(), + d_qstate.getUserContext(), d_quantEngine->getValuation(), isProxy)); d_quantEngine->getTheoryEngine() diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index bc509d78a..ff971bc12 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -159,8 +159,9 @@ private: } }; std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; -public: - BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); + + public: + BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs); virtual ~BoundedIntegers(); void presolve() override; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 173803a7f..effb5938c 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -280,9 +280,8 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } } - -FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) : -QModelBuilder( c, qe ){ +FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : QModelBuilder(qe) +{ d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index c49cd596b..89a472948 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -147,8 +147,9 @@ private: void mkCondVec( Node n, std::vector< Node > & cond ); Node evaluateInterpreted( Node n, std::vector< Node > & vals ); Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); -public: - FullModelChecker( context::Context* c, QuantifiersEngine* qe ); + + public: + FullModelChecker(QuantifiersEngine* qe); void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 796ee85fa..4f34c3baa 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -29,11 +29,13 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe) +QModelBuilder::QModelBuilder(QuantifiersEngine* qe) : TheoryEngineModelBuilder(qe->getTheoryEngine()), d_qe(qe), d_addedLemmas(0), - d_triedLemmas(0) {} + d_triedLemmas(0) +{ +} bool QModelBuilder::optUseModel() { return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound(); diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 052f6f802..16e6f2a0b 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -29,7 +29,7 @@ namespace quantifiers { class QModelBuilder : public TheoryEngineModelBuilder { -protected: + protected: //quantifiers engine QuantifiersEngine* d_qe; // must call preProcessBuildModelStd @@ -38,8 +38,9 @@ protected: /** number of lemmas generated while building model */ unsigned d_addedLemmas; unsigned d_triedLemmas; -public: - QModelBuilder( context::Context* c, QuantifiersEngine* qe ); + + public: + QModelBuilder(QuantifiersEngine* qe); //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 07840655a..8803fdb2c 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -35,12 +35,12 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; //Model Engine constructor -ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : -QuantifiersModule( qe ), -d_incomplete_check(true), -d_addedLemmas(0), -d_triedLemmas(0), -d_totalLemmas(0) +ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe), + d_incomplete_check(true), + d_addedLemmas(0), + d_triedLemmas(0), + d_totalLemmas(0) { } diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 6d9d3bfe3..5616eaf5e 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -43,8 +43,9 @@ private: int d_triedLemmas; int d_totalLemmas; public: - ModelEngine( context::Context* c, QuantifiersEngine* qe ); - virtual ~ModelEngine(); + ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs); + virtual ~ModelEngine(); + public: bool needsCheck(Theory::Effort e) override; QEffort needsModel(Theory::Effort e) override; diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 9d84ea575..c064819fc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -32,8 +32,10 @@ using namespace inst; namespace quantifiers { -InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd) - : QuantifiersModule(qe), d_rd(rd), d_fullSaturateLimit(-1) +InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, + QuantifiersState& qs, + RelevantDomain* rd) + : QuantifiersModule(qs, 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 a77eb8a90..a24aeedab 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -62,7 +62,9 @@ namespace quantifiers { class InstStrategyEnum : public QuantifiersModule { public: - InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd); + InstStrategyEnum(QuantifiersEngine* qe, + QuantifiersState& qs, + RelevantDomain* rd); ~InstStrategyEnum() {} /** Presolve */ void presolve() override; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 7592f22c7..b123c3e15 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -36,14 +36,15 @@ namespace theory { namespace quantifiers { Instantiate::Instantiate(QuantifiersEngine* qe, - context::UserContext* u, + QuantifiersState& qs, ProofNodeManager* pnm) : d_qe(qe), + d_qstate(qs), d_pnm(pnm), d_term_db(nullptr), d_term_util(nullptr), - d_total_inst_debug(u), - d_c_inst_match_trie_dom(u), + d_total_inst_debug(qs.getUserContext()), + d_c_inst_match_trie_dom(qs.getUserContext()), d_pfInst(pnm ? new CDProof(pnm) : nullptr) { } @@ -429,7 +430,7 @@ bool Instantiate::existsInstantiation(Node q, if (it != d_c_inst_match_trie.end()) { return it->second->existsInstMatch( - d_qe, q, terms, d_qe->getUserContext(), modEq); + d_qe, q, terms, d_qstate.getUserContext(), modEq); } } else @@ -524,11 +525,11 @@ bool Instantiate::recordInstantiationInternal(Node q, } else { - imt = new inst::CDInstMatchTrie(d_qe->getUserContext()); + imt = new inst::CDInstMatchTrie(d_qstate.getUserContext()); d_c_inst_match_trie[q] = imt; } d_c_inst_match_trie_dom.insert(q); - return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq); + return imt->addInstMatch(d_qe, q, terms, d_qstate.getUserContext(), modEq); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq); diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 4cc3c3d6d..3a51c8904 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -89,7 +89,7 @@ class Instantiate : public QuantifiersUtil public: Instantiate(QuantifiersEngine* qe, - context::UserContext* u, + QuantifiersState& qs, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -341,6 +341,8 @@ class Instantiate : public QuantifiersUtil /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; /** cache of term database for quantifiers engine */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index fa8982760..23942ba7e 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1837,9 +1837,10 @@ bool MatchGen::isHandled( TNode n ) { return true; } -QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c) - : QuantifiersModule(qe), - d_conflict(c, false), +QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, + QuantifiersState& qs) + : QuantifiersModule(qs, qe), + d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst<bool>(true)), d_false(NodeManager::currentNM()->mkConst<bool>(false)), d_effort(EFFORT_INVALID) diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 90385865b..f90f1db18 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -230,8 +230,9 @@ private: //for equivalence classes public: bool areMatchEqual( TNode n1, TNode n2 ); bool areMatchDisequal( TNode n1, TNode n2 ); -public: - QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); + + public: + QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs); /** register quantifier */ void registerQuantifier(Node q) override; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 615ff987a..588d4de76 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -25,10 +25,9 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; - -QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) : -QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){ - +QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe), d_added_split(qs.getUserContext()) +{ } void QuantDSplit::checkOwnership(Node q) diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 12cf5e5af..6f9e74fad 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -49,7 +49,7 @@ class QuantDSplit : public QuantifiersModule { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - QuantDSplit( QuantifiersEngine * qe, context::Context* c ); + QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs); /** 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 23815dc37..cbaa8bfe6 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -18,13 +18,17 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -using namespace std; using namespace CVC4::kind; -using namespace CVC4::context; namespace CVC4 { namespace theory { +QuantifiersModule::QuantifiersModule(quantifiers::QuantifiersState& qs, + QuantifiersEngine* qe) + : d_quantEngine(qe), d_qstate(qs) +{ +} + QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) { return QEFFORT_NONE; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 507c71698..240282d3d 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_state.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -57,7 +58,7 @@ class QuantifiersModule { }; public: - QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){} + QuantifiersModule(quantifiers::QuantifiersState& qs, QuantifiersEngine* qe); virtual ~QuantifiersModule(){} /** Presolve. * @@ -156,6 +157,8 @@ class QuantifiersModule { protected: /** pointer to the quantifiers engine that owns this module */ QuantifiersEngine* d_quantEngine; + /** The state of the quantifiers engine */ + quantifiers::QuantifiersState& d_qstate; };/* class QuantifiersModule */ /** Quantifiers utility diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 9dbca674e..d8b4062fc 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -39,71 +39,71 @@ QuantifiersModules::QuantifiersModules() } QuantifiersModules::~QuantifiersModules() {} void QuantifiersModules::initialize(QuantifiersEngine* qe, - context::Context* c, + QuantifiersState& qs, std::vector<QuantifiersModule*>& modules) { // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); + d_qcf.reset(new QuantConflictFind(qe, qs)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c)); + d_sg_gen.reset(new ConjectureGenerator(qe, qs)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new quantifiers::InstantiationEngine(qe)); + d_inst_engine.reset(new InstantiationEngine(qe, qs)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) { - d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); + d_i_cbqi.reset(new InstStrategyCegqi(qe, qs)); modules.push_back(d_i_cbqi.get()); qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { - d_synth_e.reset(new quantifiers::SynthEngine(qe, c)); + d_synth_e.reset(new SynthEngine(qe, qs)); modules.push_back(d_synth_e.get()); } // finite model finding if (options::fmfBound()) { - d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); + d_bint.reset(new BoundedIntegers(qe, qs)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) { - d_model_engine.reset(new quantifiers::ModelEngine(c, qe)); + d_model_engine.reset(new ModelEngine(qe, qs)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new quantifiers::QuantDSplit(qe, c)); + d_qsplit.reset(new QuantDSplit(qe, qs)); modules.push_back(d_qsplit.get()); } if (options::quantAntiSkolem()) { - d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe)); + d_anti_skolem.reset(new QuantAntiSkolem(qe, qs)); modules.push_back(d_anti_skolem.get()); } if (options::quantAlphaEquiv()) { - d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe)); + d_alpha_equiv.reset(new AlphaEquivalence(qe)); } // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { - d_rel_dom.reset(new quantifiers::RelevantDomain(qe)); - d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get())); + d_rel_dom.reset(new RelevantDomain(qe)); + d_fs.reset(new InstStrategyEnum(qe, qs, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new quantifiers::SygusInst(qe)); + d_sygus_inst.reset(new SygusInst(qe, qs)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index a4c5dfb6e..e83a13ea7 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -53,37 +53,38 @@ class QuantifiersModules * a pointer to each module it constructs to modules. */ void initialize(QuantifiersEngine* qe, - context::Context* c, + QuantifiersState& qs, std::vector<QuantifiersModule*>& modules); + private: //------------------------------ quantifier utilities /** relevant domain */ - std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; + std::unique_ptr<RelevantDomain> d_rel_dom; //------------------------------ quantifiers modules /** alpha equivalence */ - std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv; + std::unique_ptr<AlphaEquivalence> d_alpha_equiv; /** instantiation engine */ - std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine; + std::unique_ptr<InstantiationEngine> d_inst_engine; /** model engine */ - std::unique_ptr<quantifiers::ModelEngine> d_model_engine; + std::unique_ptr<ModelEngine> d_model_engine; /** bounded integers utility */ - std::unique_ptr<quantifiers::BoundedIntegers> d_bint; + std::unique_ptr<BoundedIntegers> d_bint; /** Conflict find mechanism for quantifiers */ - std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; + std::unique_ptr<QuantConflictFind> d_qcf; /** subgoal generator */ - std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; + std::unique_ptr<ConjectureGenerator> d_sg_gen; /** ceg instantiation */ - std::unique_ptr<quantifiers::SynthEngine> d_synth_e; + std::unique_ptr<SynthEngine> d_synth_e; /** full saturation */ - std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; + std::unique_ptr<InstStrategyEnum> d_fs; /** counterexample-based quantifier instantiation */ - std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi; + std::unique_ptr<InstStrategyCegqi> d_i_cbqi; /** quantifiers splitting */ - std::unique_ptr<quantifiers::QuantDSplit> d_qsplit; + std::unique_ptr<QuantDSplit> d_qsplit; /** quantifiers anti-skolemization */ - std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem; + std::unique_ptr<QuantAntiSkolem> d_anti_skolem; /** SyGuS instantiation engine */ - std::unique_ptr<quantifiers::SygusInst> d_sygus_inst; + std::unique_ptr<SygusInst> d_sygus_inst; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 61dd0c15e..901b7ad82 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -29,13 +29,14 @@ namespace theory { namespace quantifiers { Skolemize::Skolemize(QuantifiersEngine* qe, - context::UserContext* u, + QuantifiersState& qs, ProofNodeManager* pnm) : d_quantEngine(qe), - d_skolemized(u), + d_skolemized(qs.getUserContext()), d_pnm(pnm), d_epg(pnm == nullptr ? nullptr - : new EagerProofGenerator(pnm, u, "Skolemize::epg")) + : new EagerProofGenerator( + pnm, qs.getUserContext(), "Skolemize::epg")) { } diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index cb81a5c3a..8cf3e3176 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -64,9 +64,7 @@ class Skolemize typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; public: - Skolemize(QuantifiersEngine* qe, - context::UserContext* u, - ProofNodeManager* pnm); + Skolemize(QuantifiersEngine* qe, QuantifiersState& qs, ProofNodeManager* pnm); ~Skolemize() {} /** skolemize quantified formula q * If the return value ret of this function is non-null, then ret is a trust diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 4588e8952..42e7e2f13 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -29,8 +29,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p) - : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p) +CegisUnif::CegisUnif(QuantifiersEngine* qe, + QuantifiersState& qs, + SynthConjecture* p) + : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p) { } @@ -398,8 +400,8 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, } CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( - QuantifiersEngine* qe, SynthConjecture* parent) - : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()), + QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent) + : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()), d_qe(qe), d_parent(parent) { diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index aca85a691..ee9ae0132 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -47,7 +47,9 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent); + CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, + QuantifiersState& qs, + SynthConjecture* parent); /** Make the n^th literal of this strategy (G_uq_n). * * This call may add new lemmas of the form described above @@ -202,7 +204,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersEngine* qe, SynthConjecture* p); + CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p); ~CegisUnif() override; /** Retrieves enumerators for constructing solutions * diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index ad125a70f..b007f8716 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -43,8 +43,10 @@ namespace theory { namespace quantifiers { SynthConjecture::SynthConjecture(QuantifiersEngine* qe, + QuantifiersState& qs, SygusStatistics& s) : d_qe(qe), + d_qstate(qs), d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), @@ -56,7 +58,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_exampleInfer(new ExampleInfer(d_tds)), d_ceg_pbe(new SygusPbe(qe, this)), d_ceg_cegis(new Cegis(qe, this)), - d_ceg_cegisUnif(new CegisUnif(qe, this)), + d_ceg_cegisUnif(new CegisUnif(qe, qs, this)), d_sygus_ccore(new CegisCoreConnective(qe, this)), d_master(nullptr), d_set_ce_sk_vars(false), @@ -235,7 +237,7 @@ void SynthConjecture::assign(Node q) d_feasible_strategy.reset( new DecisionStrategySingleton("sygus_feasible", d_feasible_guard, - d_qe->getSatContext(), + d_qstate.getSatContext(), d_qe->getValuation())); d_qe->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 7786f57ad..1d43e30ff 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -82,7 +82,9 @@ class EnumValGenerator class SynthConjecture { public: - SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s); + SynthConjecture(QuantifiersEngine* qe, + QuantifiersState& qs, + SygusStatistics& s); ~SynthConjecture(); /** presolve */ void presolve(); @@ -199,6 +201,8 @@ class SynthConjecture private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; /** reference to the statistics of parent */ SygusStatistics& d_stats; /** term database sygus of d_qe */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f49cc962f..09a6add1c 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -30,14 +30,14 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) - : QuantifiersModule(qe), +SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe), d_tds(qe->getTermDatabaseSygus()), d_conj(nullptr), d_sqp(qe) { d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(d_quantEngine, d_statistics))); + new SynthConjecture(d_quantEngine, qs, d_statistics))); d_conj = d_conjs.back().get(); } @@ -159,7 +159,7 @@ void SynthEngine::assignConjecture(Node q) if (d_conjs.back()->isAssigned()) { d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(d_quantEngine, d_statistics))); + new SynthConjecture(d_quantEngine, d_qstate, d_statistics))); } d_conjs.back()->assign(q); } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 25981748e..e3cf2e47b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -33,7 +33,7 @@ class SynthEngine : public QuantifiersModule typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; public: - SynthEngine(QuantifiersEngine* qe, context::Context* c); + SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs); ~SynthEngine(); /** presolve * diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index ccc23f109..210ebb921 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -46,8 +46,9 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) +TermDbSygus::TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs) : d_quantEngine(qe), + d_qstate(qs), 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 e082cf15b..1bf6b6ca7 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -54,7 +54,7 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r); // TODO :issue #1235 split and document this class class TermDbSygus { public: - TermDbSygus(context::Context* c, QuantifiersEngine* qe); + TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs); ~TermDbSygus() {} /** Reset this utility */ bool reset(Theory::Effort e); @@ -316,6 +316,8 @@ class TermDbSygus { private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; //------------------------------utilities /** sygus explanation */ diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 50c983ee7..12ce544d3 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -180,11 +180,11 @@ void addSpecialValues( } // namespace -SygusInst::SygusInst(QuantifiersEngine* qe) - : QuantifiersModule(qe), - d_ce_lemma_added(qe->getUserContext()), - d_global_terms(qe->getUserContext()), - d_notified_assertions(qe->getUserContext()) +SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs) + : QuantifiersModule(qs, qe), + d_ce_lemma_added(qs.getUserContext()), + d_global_terms(qs.getUserContext()), + d_notified_assertions(qs.getUserContext()) { } @@ -518,7 +518,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types) DecisionStrategy* ds = new DecisionStrategySingleton("CeLiteral", lit, - d_quantEngine->getSatContext(), + d_qstate.getSatContext(), d_quantEngine->getValuation()); d_dstrat[q].reset(ds); diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 0358b4984..10363f5a2 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -62,7 +62,7 @@ namespace quantifiers { class SygusInst : public QuantifiersModule { public: - SygusInst(QuantifiersEngine* qe); + SygusInst(QuantifiersEngine* qe, QuantifiersState& qs); ~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 0ed488891..047a3cd41 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -33,10 +33,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TermDb::TermDb(context::Context* c, context::UserContext* u, - QuantifiersEngine* qe) - : d_quantEngine(qe), - d_inactive_map(c) { +TermDb::TermDb(QuantifiersState& qs, QuantifiersEngine* qe) + : d_quantEngine(qe), d_inactive_map(qs.getSatContext()) +{ d_consistent_ee = true; d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index dff595757..afb8d0c0c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -76,7 +76,7 @@ class TermDb : public QuantifiersUtil { typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; public: - TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); + TermDb(QuantifiersState& qs, QuantifiersEngine* qe); ~TermDb(); /** presolve (called once per user check-sat) */ void presolve(); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 387a3e9d8..aaf8f347c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -43,7 +43,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, const LogicInfo& logicInfo, ProofNodeManager* pnm) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), - d_qstate(c, u, valuation) + d_qstate(c, u, valuation), + d_qengine(d_qstate, pnm) { out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute("qid", this); @@ -59,6 +60,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, } // indicate we are using the quantifiers theory state object d_theoryState = &d_qstate; + + // Set the pointer to the quantifiers engine, which this theory owns. This + // pointer will be retreived by TheoryEngine and set to all theories + // post-construction. + d_quantEngine = &d_qengine; } TheoryQuantifiers::~TheoryQuantifiers() { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index b46390284..82a588009 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -23,6 +23,7 @@ #include "theory/quantifiers/proof_checker.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers_engine.h" #include "theory/theory.h" #include "theory/valuation.h" @@ -80,6 +81,8 @@ class TheoryQuantifiers : public Theory { QuantifiersProofRuleChecker d_qChecker; /** The quantifiers state */ QuantifiersState d_qstate; + /** The quantifiers engine, which lives here */ + QuantifiersEngine d_qengine; };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8b3ea8622..f60bb724f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,37 +30,34 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, - DecisionManager& dm, +QuantifiersEngine::QuantifiersEngine(quantifiers::QuantifiersState& qstate, ProofNodeManager* pnm) - : d_te(te), - d_context(te->getSatContext()), - d_userContext(te->getUserContext()), - d_decManager(dm), + : d_qstate(qstate), + d_te(nullptr), + d_decManager(nullptr), d_masterEqualityEngine(nullptr), - d_eq_query( - new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)), + d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), d_term_util(new quantifiers::TermUtil(this)), d_term_canon(new expr::TermCanonize), - d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)), + d_term_db(new quantifiers::TermDb(qstate, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), - d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)), - d_skolemize(new quantifiers::Skolemize(this, d_userContext, pnm)), + d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)), + d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), d_term_enum(new quantifiers::TermEnumeration), - d_conflict_c(d_context, false), - d_quants_prereg(d_userContext), - d_quants_red(d_userContext), - d_lemmas_produced_c(d_userContext), - d_ierCounter_c(d_context), - d_presolve(d_userContext, true), - d_presolve_in(d_userContext), - d_presolve_cache(d_userContext), - d_presolve_cache_wq(d_userContext), - d_presolve_cache_wic(d_userContext) + d_conflict_c(qstate.getSatContext(), false), + d_quants_prereg(qstate.getUserContext()), + d_quants_red(qstate.getUserContext()), + d_lemmas_produced_c(qstate.getUserContext()), + d_ierCounter_c(qstate.getSatContext()), + d_presolve(qstate.getUserContext(), true), + d_presolve_in(qstate.getUserContext()), + d_presolve_cache(qstate.getUserContext()), + d_presolve_cache_wq(qstate.getUserContext()), + d_presolve_cache_wic(qstate.getUserContext()) { //---- utilities d_util.push_back(d_eq_query.get()); @@ -71,7 +68,7 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, if (options::sygus() || options::sygusInst()) { // must be constructed here since it is required for datatypes finistInit - d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this)); + d_sygus_tdb.reset(new quantifiers::TermDbSygus(this, qstate)); } d_util.push_back(d_instantiate.get()); @@ -106,53 +103,43 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - this, d_context, "FirstOrderModelFmc")); - d_builder.reset( - new quantifiers::fmcheck::FullModelChecker(d_context, this)); + this, qstate, "FirstOrderModelFmc")); + d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_model.reset( - new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel")); - d_builder.reset(new quantifiers::QModelBuilder(d_context, this)); + new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel")); + d_builder.reset(new quantifiers::QModelBuilder(this)); } }else{ d_model.reset( - new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel")); + new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel")); } } QuantifiersEngine::~QuantifiersEngine() {} -void QuantifiersEngine::finishInit() +void QuantifiersEngine::finishInit(TheoryEngine* te, + DecisionManager* dm, + eq::EqualityEngine* mee) { - // Initialize the modules and the utilities here. We delay their - // initialization to here, since this is after TheoryQuantifiers finishInit, - // which has initialized the state and inference manager of this engine. + d_te = te; + d_decManager = dm; + d_masterEqualityEngine = mee; + // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(this, d_context, d_modules); + d_qmodules->initialize(this, d_qstate, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); } } -void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee) -{ - d_masterEqualityEngine = mee; -} - TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; } DecisionManager* QuantifiersEngine::getDecisionManager() { - return &d_decManager; -} - -context::Context* QuantifiersEngine::getSatContext() { return d_context; } - -context::UserContext* QuantifiersEngine::getUserContext() -{ - return d_userContext; + return d_decManager; } OutputChannel& QuantifiersEngine::getOutputChannel() diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 0c3bb181e..7ed183342 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_state.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" @@ -59,20 +60,14 @@ class QuantifiersEngine { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, + QuantifiersEngine(quantifiers::QuantifiersState& qstate, ProofNodeManager* pnm); ~QuantifiersEngine(); - /** finish initialize */ - void finishInit(); //---------------------- external interface /** get theory engine */ TheoryEngine* getTheoryEngine() const; /** Get the decision manager */ DecisionManager* getDecisionManager(); - /** get default sat context for quantifiers engine */ - context::Context* getSatContext(); - /** get default sat context for quantifiers engine */ - context::UserContext* getUserContext(); /** get default output channel for the quantifiers engine */ OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ @@ -110,8 +105,19 @@ class QuantifiersEngine { //---------------------- end utilities private: //---------------------- private initialization - /** Set the master equality engine */ - void setMasterEqualityEngine(eq::EqualityEngine* mee); + /** + * Finish initialize, which passes pointers to the objects that quantifiers + * engine needs but were not available when it was created. This is + * called after theories have been created but before they have finished + * initialization. + * + * @param te The theory engine + * @param dm The decision manager of the theory engine + * @param mee The master equality engine of the theory engine + */ + void finishInit(TheoryEngine* te, + DecisionManager* dm, + eq::EqualityEngine* mee); //---------------------- end private initialization /** * Maps quantified formulas to the module that owns them, if any module has @@ -329,14 +335,12 @@ public: Statistics d_statistics; private: + /** The quantifiers state object */ + quantifiers::QuantifiersState& d_qstate; /** Pointer to theory engine object */ TheoryEngine* d_te; - /** The SAT context */ - context::Context* d_context; - /** The user context */ - context::UserContext* d_userContext; /** Reference to the decision manager of the theory engine */ - DecisionManager& d_decManager; + DecisionManager* d_decManager; /** Pointer to the master equality engine */ eq::EqualityEngine* d_masterEqualityEngine; /** vector of utilities for quantifiers */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 5bea454e8..fef3fdc67 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -68,8 +68,7 @@ Theory::Theory(TheoryId id, d_facts(satContext), d_factsHead(satContext, 0), d_sharedTermsIndex(satContext, 0), - d_careGraph(NULL), - d_quantEngine(NULL), + d_careGraph(nullptr), d_decManager(nullptr), d_instanceName(name), d_checkTime(getStatsPrefix(id) + name + "::checkTime"), @@ -82,6 +81,7 @@ Theory::Theory(TheoryId id, d_allocEqualityEngine(nullptr), d_theoryState(nullptr), d_inferManager(nullptr), + d_quantEngine(nullptr), d_pnm(pnm) { smtStatisticsRegistry()->registerStat(&d_checkTime); @@ -115,7 +115,6 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee) void Theory::setQuantifiersEngine(QuantifiersEngine* qe) { - Assert(d_quantEngine == nullptr); // quantifiers engine may be null if not in quantified logic d_quantEngine = qe; } diff --git a/src/theory/theory.h b/src/theory/theory.h index 0eb3d9a33..fa26ab65e 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -140,12 +140,6 @@ class Theory { /** The care graph the theory will use during combination. */ CareGraph* d_careGraph; - /** - * Pointer to the quantifiers engine (or NULL, if quantifiers are not - * supported or not enabled). Not owned by the theory. - */ - QuantifiersEngine* d_quantEngine; - /** Pointer to the decision manager. */ DecisionManager* d_decManager; @@ -234,6 +228,12 @@ class Theory { */ TheoryInferenceManager* d_inferManager; + /** + * Pointer to the quantifiers engine (or NULL, if quantifiers are not + * supported or not enabled). Not owned by the theory. + */ + QuantifiersEngine* d_quantEngine; + /** Pointer to proof node manager */ ProofNodeManager* d_pnm; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 27ae0018e..16d68ea5c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -169,8 +169,10 @@ void TheoryEngine::finishInit() // initialize the quantifiers engine if (d_logicInfo.isQuantified()) { - // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm); + // get the quantifiers engine, which is initialized by the quantifiers + // theory + d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine(); + Assert(d_quantEngine != nullptr); } // initialize the theory combination manager, which decides and allocates the // equality engines to use for all theories. @@ -178,10 +180,11 @@ void TheoryEngine::finishInit() // get pointer to the shared solver d_sharedSolver = d_tc->getSharedSolver(); - // set the core equality engine on quantifiers engine + // finish initializing the quantifiers engine if (d_logicInfo.isQuantified()) { - d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine()); + d_quantEngine->finishInit( + this, d_decManager.get(), d_tc->getCoreEqualityEngine()); } // finish initializing the theories by linking them with the appropriate @@ -205,12 +208,6 @@ void TheoryEngine::finishInit() // finish initializing the theory t->finishInit(); } - - // finish initializing the quantifiers engine - if (d_logicInfo.isQuantified()) - { - d_quantEngine->finishInit(); - } } ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; } @@ -283,8 +280,6 @@ TheoryEngine::~TheoryEngine() { } } - delete d_quantEngine; - smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index df57d9903..0be511e47 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -156,9 +156,7 @@ class TheoryEngine { std::unique_ptr<theory::CombinationEngine> d_tc; /** The shared solver of the above combination engine. */ theory::SharedSolver* d_sharedSolver; - /** - * The quantifiers engine - */ + /** The quantifiers engine, which is owned by the quantifiers theory */ theory::QuantifiersEngine* d_quantEngine; /** * The decision manager |