From: Andrew Reynolds Date: Thu, 4 Feb 2021 21:18:05 +0000 (-0600) Subject: Eliminate equality query dependence on quantifiers engine (#5831) X-Git-Tag: cvc5-1.0.0~2323 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c8d7db69e6b5274c21029f231a1d312518d658e7;p=cvc5.git Eliminate equality query dependence on quantifiers engine (#5831) This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on. --- diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 08741ef0f..c60c98d70 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -19,9 +19,6 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4::kind; @@ -32,9 +29,10 @@ namespace theory { namespace quantifiers { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( - QuantifiersState& qs, QuantifiersEngine* qe) - : d_qe(qe), - d_qstate(qs), + QuantifiersState& qs, TermDb* tdb, FirstOrderModel* m) + : d_qstate(qs), + d_tdb(tdb), + d_model(m), d_eqi_counter(qs.getSatContext()), d_reset_count(0) { @@ -58,8 +56,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if( options::finiteModelFind() ){ if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any - if( d_qe->getModel() ){ - Node tr = d_qe->getModel()->getRepSet()->getTermForRepresentative(r); + if (d_model != nullptr) + { + Node tr = d_model->getRepSet()->getTermForRepresentative(r); if (!tr.isNull()) { r = tr; @@ -173,7 +172,10 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, return -2; }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; - }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ + } + else if (options::lteRestrictInstClosure() + && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false))) + { return -1; }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index a3f895f54..9944bf703 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -27,6 +27,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class TermDb; +class FirstOrderModel; + /** EqualityQueryQuantifiersEngine class * * The main method of this class is the function @@ -40,7 +43,9 @@ namespace quantifiers { class EqualityQueryQuantifiersEngine : public QuantifiersUtil { public: - EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe); + EqualityQueryQuantifiersEngine(QuantifiersState& qs, + TermDb* tdb, + FirstOrderModel* m); virtual ~EqualityQueryQuantifiersEngine(); /** reset */ bool reset(Theory::Effort e) override; @@ -65,10 +70,12 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil Node getInternalRepresentative(Node a, Node q, int index); private: - /** pointer to theory engine */ - QuantifiersEngine* d_qe; /** the quantifiers state */ QuantifiersState& d_qstate; + /** Pointer to the term database */ + TermDb* d_tdb; + /** Pointer to the model */ + FirstOrderModel* d_model; /** quantifiers equality inference */ context::CDO< unsigned > d_eqi_counter; /** internal representatives */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 8f587c09d..db977c53d 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -118,7 +118,7 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) // terms in rep_set are now constants which mapped to terms through // TheoryModel. Thus, should introduce a constant and a term. // For now, we just add an arbitrary term. - Node var = d_qe->getModel()->getSomeDomainElement(tn); + Node var = getSomeDomainElement(tn); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set.add(tn, var); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 28397fd14..921c5100f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -40,12 +40,12 @@ QuantifiersEngine::QuantifiersEngine( d_qim(qim), d_te(nullptr), d_decManager(nullptr), - 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), 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_instantiate(new quantifiers::Instantiate(this, qstate, pnm)), @@ -62,7 +62,6 @@ QuantifiersEngine::QuantifiersEngine( d_presolve_cache_wic(qstate.getUserContext()) { //---- utilities - d_util.push_back(d_eq_query.get()); // term util must come before the other utilities d_util.push_back(d_term_util.get()); d_util.push_back(d_term_db.get()); @@ -116,6 +115,9 @@ QuantifiersEngine::QuantifiersEngine( d_model.reset( new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel")); } + d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine( + qstate, d_term_db.get(), d_model.get())); + d_util.insert(d_util.begin(), d_eq_query.get()); } QuantifiersEngine::~QuantifiersEngine() {} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 74f432585..f38a43757 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -343,8 +343,6 @@ public: /** vector of modules for quantifiers */ std::vector d_modules; //------------- quantifiers utilities - /** equality query class */ - std::unique_ptr d_eq_query; /** all triggers will be stored in this trie */ std::unique_ptr d_tr_trie; /** extended model object */ @@ -355,6 +353,8 @@ public: std::unique_ptr d_term_util; /** term database */ std::unique_ptr d_term_db; + /** equality query class */ + std::unique_ptr d_eq_query; /** sygus term database */ std::unique_ptr d_sygus_tdb; /** quantifiers attributes */