From 0bcaeb9cd75ec2268b6fe237bc037865d5122b5a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 4 Feb 2021 16:55:00 -0600 Subject: [PATCH] Introduce quantifiers registry utility (#5829) This is a simple module for determining which quantifiers module has ownership of quantified formulas. This is work towards eliminating dependencies of quantifiers modules. Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR. --- src/CMakeLists.txt | 2 + .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 10 +-- .../quantifiers/cegqi/inst_strategy_cegqi.h | 3 +- .../quantifiers/conjecture_generator.cpp | 5 +- src/theory/quantifiers/conjecture_generator.h | 3 +- .../ematching/instantiation_engine.cpp | 9 +-- .../ematching/instantiation_engine.h | 3 +- .../quantifiers/fmf/bounded_integers.cpp | 5 +- src/theory/quantifiers/fmf/bounded_integers.h | 3 +- src/theory/quantifiers/fmf/model_engine.cpp | 14 ++-- src/theory/quantifiers/fmf/model_engine.h | 3 +- .../quantifiers/inst_strategy_enumerative.cpp | 5 +- .../quantifiers/inst_strategy_enumerative.h | 1 + .../quantifiers/quant_conflict_find.cpp | 10 +-- src/theory/quantifiers/quant_conflict_find.h | 3 +- src/theory/quantifiers/quant_split.cpp | 7 +- src/theory/quantifiers/quant_split.h | 3 +- src/theory/quantifiers/quant_util.cpp | 3 +- src/theory/quantifiers/quant_util.h | 4 ++ .../quantifiers/quantifiers_attributes.cpp | 8 +-- .../quantifiers/quantifiers_attributes.h | 8 +-- .../quantifiers/quantifiers_modules.cpp | 21 +++--- src/theory/quantifiers/quantifiers_modules.h | 1 + .../quantifiers/quantifiers_registry.cpp | 65 +++++++++++++++++ src/theory/quantifiers/quantifiers_registry.h | 69 +++++++++++++++++++ src/theory/quantifiers/sygus/synth_engine.cpp | 18 ++++- src/theory/quantifiers/sygus/synth_engine.h | 5 +- src/theory/quantifiers/sygus_inst.cpp | 5 +- src/theory/quantifiers/sygus_inst.h | 3 +- src/theory/quantifiers_engine.cpp | 52 ++------------ src/theory/quantifiers_engine.h | 25 +------ 31 files changed, 242 insertions(+), 134 deletions(-) create mode 100644 src/theory/quantifiers/quantifiers_registry.cpp create mode 100644 src/theory/quantifiers/quantifiers_registry.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c5673a396..7a7a90981 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -731,6 +731,8 @@ libcvc4_add_sources( theory/quantifiers/quantifiers_inference_manager.h theory/quantifiers/quantifiers_modules.cpp theory/quantifiers/quantifiers_modules.h + theory/quantifiers/quantifiers_registry.cpp + theory/quantifiers/quantifiers_registry.h theory/quantifiers/quantifiers_rewriter.cpp theory/quantifiers/quantifiers_rewriter.h theory/quantifiers/quantifiers_state.cpp diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index c539bfdb0..037cb74d7 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -49,8 +49,9 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), @@ -309,11 +310,12 @@ bool InstStrategyCegqi::checkCompleteFor(Node q) void InstStrategyCegqi::checkOwnership(Node q) { - if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ + if (d_qreg.getOwner(q) == nullptr && doCbqi(q)) + { if (d_do_cbqi[q] == CEG_HANDLED) { //take full ownership of the quantified formula - d_quantEngine->setOwner( q, this ); + d_qreg.setOwner(q, this); } } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index d4b78d306..a6a3c36cd 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -71,7 +71,8 @@ class InstStrategyCegqi : public QuantifiersModule public: InstStrategyCegqi(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~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 db8bc90d1..83a102633 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, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, 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 c73abd19b..644461da2 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -438,7 +438,8 @@ private: //information about ground equivalence classes public: ConjectureGenerator(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~ConjectureGenerator(); /* needs check */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 69c33d329..96b3bd0b0 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -35,8 +35,9 @@ namespace quantifiers { InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_instStrategies(), d_isup(), d_i_ag(), @@ -210,7 +211,7 @@ void InstantiationEngine::checkOwnership(Node q) } } if( hasPat ){ - d_quantEngine->setOwner( q, this, 1 ); + d_qreg.setOwner(q, this, 1); } } } @@ -260,7 +261,7 @@ void InstantiationEngine::addUserNoPattern(Node q, Node pat) { bool InstantiationEngine::shouldProcess(Node q) { - if (!d_quantEngine->hasOwnership(q, this)) + if (!d_qreg.hasOwnership(q, this)) { return false; } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index f5b999cea..016784152 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -50,7 +50,8 @@ class InstantiationEngine : public QuantifiersModule { public: InstantiationEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~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 9144bca2a..a6862f513 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -86,8 +86,9 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe) + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe) { } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 685c07d82..74ff8a19b 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -163,7 +163,8 @@ private: public: BoundedIntegers(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); virtual ~BoundedIntegers(); void presolve() override; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 715002f7b..618a72047 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -35,8 +35,9 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), @@ -187,7 +188,8 @@ int ModelEngine::checkModel(){ if( Trace.isOn("model-engine") ){ for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){ + if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this)) + { int totalInst = 1; for( unsigned j=0; jgetAssertedQuantifier( i, true ); Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier - if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ + if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this)) + { exhaustiveInstantiate( q, e ); if (d_qstate.isInConflict()) { @@ -318,7 +321,8 @@ void ModelEngine::debugPrint( const char* c ){ Trace( c ) << "Quantifiers: " << std::endl; for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_quantEngine->hasOwnership( q, this ) ){ + if (d_qreg.hasOwnership(q, this)) + { Trace( c ) << " "; if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ Trace( c ) << "*Inactive* "; diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 3e212b319..1cb780dd0 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -45,7 +45,8 @@ private: public: ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); virtual ~ModelEngine(); public: diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index c0f294528..f22e67815 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -35,8 +35,9 @@ namespace quantifiers { InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, RelevantDomain* rd) - : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1) { } void InstStrategyEnum::presolve() @@ -130,7 +131,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) for (unsigned i = 0; i < nquant; i++) { Node q = fm->getAssertedQuantifier(i, true); - bool doProcess = d_quantEngine->hasOwnership(q, this) + bool doProcess = d_qreg.hasOwnership(q, this) && fm->isQuantifierActive(q) && alreadyProc.find(q) == alreadyProc.end(); if (doProcess) diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 5687624db..35c43d740 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -65,6 +65,7 @@ class InstStrategyEnum : public QuantifiersModule InstStrategyEnum(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, RelevantDomain* rd); ~InstStrategyEnum() {} /** Presolve */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c025dc29e..433de2f85 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1840,8 +1840,9 @@ bool MatchGen::isHandled( TNode n ) { QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), @@ -1852,7 +1853,8 @@ QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, //-------------------------------------------------- registration void QuantConflictFind::registerQuantifier( Node q ) { - if( d_quantEngine->hasOwnership( q, this ) ){ + if (d_qreg.hasOwnership(q, this)) + { d_quants.push_back( q ); d_quant_id[q] = d_quants.size(); if( Trace.isOn("qcf-qregister") ){ @@ -2022,7 +2024,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) for (unsigned i = 0; i < nquant; i++) { Node q = fm->getAssertedQuantifier(i, true); - if (d_quantEngine->hasOwnership(q, this) + if (d_qreg.hasOwnership(q, this) && d_irr_quant.find(q) == d_irr_quant.end() && fm->isQuantifierActive(q)) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 15b3d119a..5ffe4426a 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -234,7 +234,8 @@ private: //for equivalence classes public: QuantConflictFind(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); /** register quantifier */ void registerQuantifier(Node q) override; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index ad65c06cd..a1dc5acf3 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -27,8 +27,9 @@ using namespace CVC4::theory::quantifiers; QuantDSplit::QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), d_added_split(qs.getUserContext()) + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_added_split(qs.getUserContext()) { } @@ -100,7 +101,7 @@ void QuantDSplit::checkOwnership(Node q) if (takeOwnership) { Trace("quant-dsplit-debug") << "Will take ownership." << std::endl; - d_quantEngine->setOwner( q, this ); + d_qreg.setOwner(q, this); } // Notice we may not take ownership in some cases, meaning that both the // original quantified formula and the split one are generated. This may diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 76ac1a974..8fb9b4eb6 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -51,7 +51,8 @@ class QuantDSplit : public QuantifiersModule { public: QuantDSplit(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); /** 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 6ce46ad99..db643d96b 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -26,8 +26,9 @@ namespace theory { QuantifiersModule::QuantifiersModule( quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, QuantifiersEngine* qe) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) { } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 417e6820d..9037e94fa 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -22,6 +22,7 @@ #include #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -61,6 +62,7 @@ class QuantifiersModule { public: QuantifiersModule(quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, QuantifiersEngine* qe); virtual ~QuantifiersModule(){} /** Presolve. @@ -168,6 +170,8 @@ class QuantifiersModule { quantifiers::QuantifiersState& d_qstate; /** The quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry& d_qreg; };/* class QuantifiersModule */ /** Quantifiers utility diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 15715152b..ad5d5dba7 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -18,7 +18,6 @@ #include "theory/arith/arith_msum.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; @@ -34,11 +33,8 @@ bool QAttributes::isStandard() const && !d_isInternal; } -QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : -d_quantEngine(qe) { +QuantAttributes::QuantAttributes() {} -} - void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){ Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; if (attr == "fun-def") @@ -182,8 +178,6 @@ void QuantAttributes::computeAttributes( Node q ) { } d_fun_defs[f] = true; } - // set ownership of quantified formula q based on the computed attributes - d_quantEngine->setOwner(q, qa); } void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 91a0d504f..740588b84 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -25,8 +25,6 @@ namespace CVC4 { namespace theory { -class QuantifiersEngine; - /** Attribute true for function definition quantifiers */ struct FunDefAttributeId {}; typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute; @@ -176,8 +174,8 @@ struct QAttributes */ class QuantAttributes { -public: - QuantAttributes( QuantifiersEngine * qe ); + public: + QuantAttributes(); ~QuantAttributes(){} /** set user attribute * This function applies an attribute @@ -238,8 +236,6 @@ public: static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level); private: - /** pointer to quantifiers engine */ - QuantifiersEngine * d_quantEngine; /** cache of attributes */ std::map< Node, QAttributes > d_qattr; /** function definitions */ diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 573824b80..f1a05f401 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -40,49 +40,50 @@ QuantifiersModules::~QuantifiersModules() {} void QuantifiersModules::initialize(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, std::vector& modules) { // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qe, qs, qim)); + d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim)); + d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new InstantiationEngine(qe, qs, qim)); + d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim)); + d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr)); 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, qim)); + d_synth_e.reset(new SynthEngine(qe, qs, qim, qr)); modules.push_back(d_synth_e.get()); } // finite model finding if (options::fmfBound()) { - d_bint.reset(new BoundedIntegers(qe, qs, qim)); + d_bint.reset(new BoundedIntegers(qe, qs, qim, qr)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) { - d_model_engine.reset(new ModelEngine(qe, qs, qim)); + d_model_engine.reset(new ModelEngine(qe, qs, qim, qr)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qe, qs, qim)); + d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) @@ -93,12 +94,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, qim, d_rel_dom.get())); + d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qe, qs, qim)); + d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index ba48cc68b..08266c8fe 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -54,6 +54,7 @@ class QuantifiersModules void initialize(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, std::vector& modules); private: diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp new file mode 100644 index 000000000..1633382c8 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file quantifiers_registry.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 The quantifiers registry + **/ + +#include "theory/quantifiers/quantifiers_registry.h" + +#include "theory/quantifiers/quant_util.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const +{ + std::map::const_iterator it = d_owner.find(q); + if (it == d_owner.end()) + { + return nullptr; + } + return it->second; +} + +void QuantifiersRegistry::setOwner(Node q, + QuantifiersModule* m, + int32_t priority) +{ + QuantifiersModule* mo = getOwner(q); + if (mo == m) + { + return; + } + if (mo != nullptr) + { + if (priority <= d_owner_priority[q]) + { + Trace("quant-warn") << "WARNING: setting owner of " << q << " to " + << (m ? m->identify() : "null") + << ", but already has owner " << mo->identify() + << " with higher priority!" << std::endl; + return; + } + } + d_owner[q] = m; + d_owner_priority[q] = priority; +} + +bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const +{ + QuantifiersModule* mo = getOwner(q); + return mo == m || mo == nullptr; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h new file mode 100644 index 000000000..59db1dfe2 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \file quantifiers_registry.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 The quantifiers registry + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersModule; + +namespace quantifiers { + +/** + * The quantifiers registry, which manages basic information about which + * quantifiers modules have ownership of quantified formulas. + */ +class QuantifiersRegistry +{ + public: + QuantifiersRegistry() {} + ~QuantifiersRegistry() {} + /** get the owner of quantified formula q */ + QuantifiersModule* getOwner(Node q) const; + /** + * Set owner of quantified formula q to module m with given priority. If + * the quantified formula has previously been assigned an owner with + * lower priority, that owner is overwritten. + */ + void setOwner(Node q, QuantifiersModule* m, int32_t priority = 0); + /** + * Return true if module q has no owner registered or if its registered owner is m. + */ + bool hasOwnership(Node q, QuantifiersModule* m) const; + + private: + /** + * Maps quantified formulas to the module that owns them, if any module has + * specifically taken ownership of it. + */ + std::map d_owner; + /** + * The priority value associated with the ownership of quantified formulas + * in the domain of the above map, where higher values take higher + * precendence. + */ + std::map d_owner_priority; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 4b35bc545..869d22737 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -31,8 +31,9 @@ namespace quantifiers { SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_tds(qe->getTermDatabaseSygus()), d_conj(nullptr), d_sqp(qe) @@ -164,11 +165,22 @@ void SynthEngine::assignConjecture(Node q) d_conjs.back()->assign(q); } +void SynthEngine::checkOwnership(Node q) +{ + // take ownership of quantified formulas with sygus attribute, and function + // definitions when options::sygusRecFun is true. + QuantAttributes* qa = d_quantEngine->getQuantAttributes(); + if (qa->isSygus(q) || (options::sygusRecFun() && qa->isFunDef(q))) + { + d_qreg.setOwner(q, this, 2); + } +} + void SynthEngine::registerQuantifier(Node q) { Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q << std::endl; - if (d_quantEngine->getOwner(q) != this) + if (d_qreg.getOwner(q) != this) { return; } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 63175cf0c..4cb73d450 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -35,7 +35,8 @@ class SynthEngine : public QuantifiersModule public: SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~SynthEngine(); /** presolve * @@ -49,6 +50,8 @@ class SynthEngine : public QuantifiersModule QEffort needsModel(Theory::Effort e) override; /* Call during quantifier engine's check */ void check(Theory::Effort e, QEffort quant_e) override; + /** check ownership */ + void checkOwnership(Node q) override; /* Called for new quantifiers */ void registerQuantifier(Node q) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 66c9cbf79..69836feba 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -181,8 +181,9 @@ void addSpecialValues( SygusInst::SygusInst(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, 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 4820398be..123ec1f5e 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -64,7 +64,8 @@ class SygusInst : public QuantifiersModule public: SygusInst(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim); + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr); ~SygusInst() = default; bool needsCheck(Theory::Effort e) override; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 921c5100f..c7ef88339 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -40,6 +40,7 @@ QuantifiersEngine::QuantifiersEngine( d_qim(qim), d_te(nullptr), d_decManager(nullptr), + d_qreg(), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), @@ -47,7 +48,7 @@ QuantifiersEngine::QuantifiersEngine( d_term_db(new quantifiers::TermDb(qstate, qim, this)), d_eq_query(nullptr), d_sygus_tdb(nullptr), - d_quant_attr(new quantifiers::QuantAttributes(this)), + d_quant_attr(new quantifiers::QuantAttributes), d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)), d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), d_term_enum(new quantifiers::TermEnumeration), @@ -128,7 +129,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) d_decManager = dm; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(this, d_qstate, d_qim, d_modules); + d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); @@ -198,49 +199,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const return d_tr_trie.get(); } -QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { - std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); - if( it==d_owner.end() ){ - return NULL; - }else{ - return it->second; - } -} - -void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) { - QuantifiersModule * mo = getOwner( q ); - if( mo!=m ){ - if( mo!=NULL ){ - if( priority<=d_owner_priority[q] ){ - Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl; - return; - } - } - d_owner[q] = m; - d_owner_priority[q] = priority; - } -} - -void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) -{ - if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) - { - if (d_qmodules->d_synth_e.get() == nullptr) - { - Trace("quant-warn") << "WARNING : synth engine is null, and we have : " - << q << std::endl; - } - // set synth engine as owner since this is either a conjecture or a function - // definition to be used by sygus - setOwner(q, d_qmodules->d_synth_e.get(), 2); - } -} - -bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { - QuantifiersModule * mo = getOwner( q ); - return mo==m || mo==NULL; -} - bool QuantifiersEngine::isFiniteBound(Node q, Node v) const { quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); @@ -592,7 +550,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ bool hasCompleteM = false; Node q = d_model->getAssertedQuantifier( i ); - QuantifiersModule * qmd = getOwner( q ); + QuantifiersModule* qmd = d_qreg.getOwner(q); if( qmd!=NULL ){ hasCompleteM = qmd->checkCompleteFor( q ); }else{ @@ -719,7 +677,7 @@ void QuantifiersEngine::registerQuantifierInternal(Node f) << "..." << std::endl; mdl->checkOwnership(f); } - QuantifiersModule* qm = getOwner(f); + QuantifiersModule* qm = d_qreg.getOwner(f); Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify()) << std::endl; // register with each module diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f38a43757..b7a1df8a6 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -113,30 +113,7 @@ class QuantifiersEngine { */ void finishInit(TheoryEngine* te, DecisionManager* dm); //---------------------- end private initialization - /** - * Maps quantified formulas to the module that owns them, if any module has - * specifically taken ownership of it. - */ - std::map< Node, QuantifiersModule * > d_owner; - /** - * The priority value associated with the ownership of quantified formulas - * in the domain of the above map, where higher values take higher - * precendence. - */ - std::map< Node, int > d_owner_priority; public: - /** get owner */ - QuantifiersModule * getOwner( Node q ); - /** - * Set owner of quantified formula q to module m with given priority. If - * the quantified formula has previously been assigned an owner with - * lower priority, that owner is overwritten. - */ - void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); - /** set owner of quantified formula q based on its attributes qa. */ - void setOwner(Node q, quantifiers::QAttributes& qa); - /** considers */ - bool hasOwnership( Node q, QuantifiersModule * m = NULL ); /** does variable v of quantified formula q have a finite bound? */ bool isFiniteBound(Node q, Node v) const; /** get bound var type @@ -343,6 +320,8 @@ public: /** vector of modules for quantifiers */ std::vector d_modules; //------------- quantifiers utilities + /** The quantifiers registry */ + quantifiers::QuantifiersRegistry d_qreg; /** all triggers will be stored in this trie */ std::unique_ptr d_tr_trie; /** extended model object */ -- 2.30.2