From 7e5fe049ad88405a90fd5a43caa872d646d4b8e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Mar 2021 19:52:48 -0500 Subject: [PATCH] Miscellaneous elimination of dependencies on quantifiers engine (#6238) This should be the last PR before quantifiers engine will not be passed to quantifiers modules. --- .../quantifiers/cegqi/ceg_instantiator.cpp | 6 +++--- src/theory/quantifiers/cegqi/ceg_instantiator.h | 17 ++++++++--------- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 6 +----- src/theory/quantifiers/ematching/im_generator.h | 4 +--- src/theory/quantifiers/quantifiers_modules.cpp | 2 +- src/theory/quantifiers/relevant_domain.cpp | 16 +++++++++------- src/theory/quantifiers/relevant_domain.h | 14 ++++++++++---- .../quantifiers/sygus/sygus_process_conj.h | 3 --- .../quantifiers/sygus/sygus_qe_preproc.cpp | 2 +- src/theory/quantifiers/sygus/sygus_qe_preproc.h | 9 +-------- src/theory/quantifiers/sygus/synth_engine.cpp | 4 +--- src/theory/quantifiers/term_database.h | 4 ---- 12 files changed, 36 insertions(+), 51 deletions(-) diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index fd6a087ca..38b9c739e 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -29,7 +29,6 @@ #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -185,11 +184,12 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop) CegInstantiator::CegInstantiator(Node q, QuantifiersState& qs, + TermRegistry& tr, InstStrategyCegqi* parent) : d_quant(q), d_qstate(qs), + d_treg(tr), d_parent(parent), - d_qe(parent->getQuantifiersEngine()), d_is_nested_quant(false), d_effort(CEG_INST_EFFORT_NONE) { @@ -1437,7 +1437,7 @@ void CegInstantiator::processAssertions() { } Node CegInstantiator::getModelValue( Node n ) { - return d_qe->getModel()->getValue( n ); + return d_treg.getModel()->getValue(n); } Node CegInstantiator::getBoundVariable(TypeNode tn) diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 217584de8..bca62f2ef 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -24,15 +24,13 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class Instantiator; class InstantiatorPreprocess; class InstStrategyCegqi; class QuantifiersState; +class TermRegistry; /** * Descriptions of the types of constraints that a term was solved for in. @@ -209,7 +207,10 @@ class CegInstantiator { * The instantiator will be constructing instantiations for quantified formula * q, parent is the owner of this object. */ - CegInstantiator(Node q, QuantifiersState& qs, InstStrategyCegqi* parent); + CegInstantiator(Node q, + QuantifiersState& qs, + TermRegistry& tr, + InstStrategyCegqi* parent); virtual ~CegInstantiator(); /** check * This adds instantiations based on the state of d_vars in current context @@ -233,8 +234,6 @@ class CegInstantiator { std::vector& ce_vars, std::vector& auxLems); //------------------------------interface for instantiators - /** get quantifiers engine */ - QuantifiersEngine* getQuantifiersEngine() { return d_qe; } /** push stack variable * This adds a new variable to solve for in the stack * of variables we are processing. This stack is only @@ -251,7 +250,7 @@ class CegInstantiator { * instantiation, specified by sf. * * This function returns true if a call to - * QuantifiersEngine::addInstantiation(...) + * Instantiate::addInstantiation(...) * was successfully made in a recursive call. * * The solved form sf is reverted to its original state if @@ -349,10 +348,10 @@ class CegInstantiator { Node d_quant; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; + /** Reference to the term registry */ + TermRegistry& d_treg; /** The parent of this instantiator */ InstStrategyCegqi* d_parent; - /** quantified formula associated with this instantiator */ - QuantifiersEngine* d_qe; //-------------------------------globally cached /** cache from nodes to the set of variables it contains diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 8318c5f4c..3690cbcac 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -16,9 +16,6 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -26,7 +23,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace std; @@ -511,7 +507,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map>::iterator it = d_cinst.find(q); if( it==d_cinst.end() ){ - d_cinst[q].reset(new CegInstantiator(q, d_qstate, this)); + d_cinst[q].reset(new CegInstantiator(q, d_qstate, d_treg, this)); return d_cinst[q].get(); } return it->second.get(); diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 6968a0dee..b277ec180 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -24,10 +24,8 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { + class QuantifiersState; class TermRegistry; diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 0c8c9399b..a45029074 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -111,7 +111,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { - d_rel_dom.reset(new RelevantDomain(qe, qr)); + d_rel_dom.reset(new RelevantDomain(qs, qr, tr)); d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 456a7a8fc..8210c5e8a 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -19,8 +19,8 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -72,8 +72,10 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs) } } -RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr) - : d_qe(qe), d_qreg(qr) +RelevantDomain::RelevantDomain(QuantifiersState& qs, + QuantifiersRegistry& qr, + TermRegistry& tr) + : d_qs(qs), d_qreg(qr), d_treg(tr) { d_is_computed = false; } @@ -111,7 +113,7 @@ void RelevantDomain::compute(){ it2->second->reset(); } } - FirstOrderModel* fm = d_qe->getModel(); + FirstOrderModel* fm = d_treg.getModel(); for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = fm->getAssertedQuantifier( i ); Node icf = d_qreg.getInstConstantBody(q); @@ -120,7 +122,7 @@ void RelevantDomain::compute(){ } Trace("rel-dom-debug") << "account for ground terms" << std::endl; - TermDb * db = d_qe->getTermDatabase(); + TermDb* db = d_treg.getTermDatabase(); for (unsigned k = 0; k < db->getNumOperators(); k++) { Node op = db->getOperator(k); @@ -145,7 +147,7 @@ void RelevantDomain::compute(){ RDomain * r = it2->second; RDomain * rp = r->getParent(); if( r==rp ){ - r->removeRedundantTerms(d_qe->getState()); + r->removeRedundantTerms(d_qs); for( unsigned i=0; id_terms.size(); i++ ){ Trace("rel-dom") << r->d_terms[i] << " "; } @@ -160,7 +162,7 @@ void RelevantDomain::compute(){ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) { Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl; - Node op = d_qe->getTermDatabase()->getMatchOperator( n ); + Node op = d_treg.getTermDatabase()->getMatchOperator(n); for( unsigned i=0; i d_ri_map; - /** Quantifiers engine associated with this utility. */ - QuantifiersEngine* d_qe; - /** The quantifiers registry */ + /** Reference to the quantifiers state object */ + QuantifiersState& d_qs; + /** Reference to the quantifiers registry */ QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; /** have we computed the relevant domain on this full effort check? */ bool d_is_computed; /** relevant domain literal diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 5185e549f..de136d546 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -28,9 +28,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { /** This file contains techniques that compute diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 800ba6261..c8582cce5 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -25,7 +25,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusQePreproc::SygusQePreproc(QuantifiersEngine* qe) {} +SygusQePreproc::SygusQePreproc() {} Node SygusQePreproc::preprocess(Node q) { diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 3629164ee..4cfa8a624 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -19,9 +19,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { /** @@ -37,17 +34,13 @@ namespace quantifiers { class SygusQePreproc { public: - SygusQePreproc(QuantifiersEngine* qe); + SygusQePreproc(); ~SygusQePreproc() {} /** * Preprocess. Returns a lemma of the form q = nq where nq is obtained * by the quantifier elimination technique outlined above. */ Node preprocess(Node q); - - private: - /** Pointer to quantifiers engine */ - QuantifiersEngine* d_quantEngine; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f4d50118e..1d71af6b4 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -32,9 +32,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), - d_conj(nullptr), - d_sqp(qe) + : QuantifiersModule(qs, qim, qr, tr, qe), d_conj(nullptr), d_sqp() { d_conjs.push_back(std::unique_ptr( new SynthConjecture(qs, qim, qr, tr, d_statistics))); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 6506a6123..bafaa8bdd 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -30,9 +30,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class QuantifiersState; @@ -67,7 +64,6 @@ class DbList * lazily for performance reasons. */ class TermDb : public QuantifiersUtil { - friend class ::CVC4::theory::QuantifiersEngine; using NodeBoolMap = context::CDHashMap; using NodeList = context::CDList; using NodeSet = context::CDHashSet; -- 2.30.2