From 134985065820077d2628023b9b72f78471392968 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Mar 2021 13:42:46 -0500 Subject: [PATCH] Move equality query utility into quantifiers model (#6186) This simplifies the initialization of quantifiers engine. This PR also makes general improvements to EqualityQuery. --- .../ematching/candidate_generator.cpp | 3 +- src/theory/quantifiers/equality_query.cpp | 52 ++++++++----------- src/theory/quantifiers/equality_query.h | 24 ++++----- src/theory/quantifiers/first_order_model.cpp | 10 +++- src/theory/quantifiers/first_order_model.h | 24 ++++++--- .../quantifiers/fmf/first_order_model_fmc.cpp | 10 ++++ src/theory/quantifiers/fmf/model_engine.cpp | 2 +- src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/quantifiers_engine.cpp | 7 +-- src/theory/quantifiers_engine.h | 14 ----- 10 files changed, 74 insertions(+), 74 deletions(-) diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 4a1a21798..4cc912e45 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -18,6 +18,7 @@ #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" @@ -193,7 +194,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( !nh.isNull() ){ if (options::instMaxLevel() != -1) { - nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); + nh = d_qe->getModel()->getInternalRepresentative(nh, d_f, d_index); //don't consider this if already the instantiation is ineligible if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f)) { diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index b94076c9f..48e5682f2 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -17,6 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" using namespace std; @@ -27,8 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( - QuantifiersState& qs, FirstOrderModel* m) +EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m) : d_qstate(qs), d_model(m), d_eqi_counter(qs.getSatContext()), @@ -36,18 +36,16 @@ EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( { } -EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ -} +EqualityQuery::~EqualityQuery() {} -bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ +bool EqualityQuery::reset(Theory::Effort e) +{ d_int_rep.clear(); d_reset_count++; return true; } -Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, - Node q, - int index) +Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) { Assert(q.isNull() || q.getKind() == FORALL); Node r = d_qstate.getRepresentative(a); @@ -74,7 +72,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); if (options::quantRepMode() == options::QuantRepMode::EE) { - int score = getRepScore(r, q, index, v_tn); + int32_t score = getRepScore(r, q, index, v_tn); if (score >= 0) { return r; @@ -94,10 +92,10 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, Trace("internal-rep-select") << "Choose representative for equivalence class : " << eqc << ", type = " << v_tn << std::endl; - int r_best_score = -1; + int32_t r_best_score = -1; for (const Node& n : eqc) { - int score = getRepScore(n, q, index, v_tn); + int32_t score = getRepScore(n, q, index, v_tn); if (score != -2) { if (r_best.isNull() @@ -143,7 +141,11 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, //helper functions -Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ){ +Node EqualityQuery::getInstance( + Node n, + const std::vector& eqc, + std::unordered_map& cache) +{ if(cache.find(n) != cache.end()) { return cache[n]; } @@ -161,10 +163,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod } //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better -int EqualityQueryQuantifiersEngine::getRepScore(Node n, - Node q, - int index, - TypeNode v_tn) +int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) { if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject return -2; @@ -174,21 +173,16 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ return n.getAttribute(InstLevelAttribute()); - }else{ - return options::instLevelInputOnly() ? -1 : 0; - } - }else{ - if (options::quantRepMode() == options::QuantRepMode::FIRST) - { - //score prefers earliest use of this term as a representative - return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; - } - else - { - Assert(options::quantRepMode() == options::QuantRepMode::DEPTH); - return quantifiers::TermUtil::getTermDepth( n ); } + return options::instLevelInputOnly() ? -1 : 0; + } + else if (options::quantRepMode() == options::QuantRepMode::FIRST) + { + // score prefers earliest use of this term as a representative + return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n]; } + Assert(options::quantRepMode() == options::QuantRepMode::DEPTH); + return quantifiers::TermUtil::getTermDepth(n); } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 6dec66b5c..887c54f42 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -21,15 +21,15 @@ #include "context/context.h" #include "expr/node.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/quantifiers_state.h" namespace CVC4 { namespace theory { namespace quantifiers { class FirstOrderModel; +class QuantifiersState; -/** EqualityQueryQuantifiersEngine class +/** EqualityQuery class * * The main method of this class is the function * getInternalRepresentative, which is used by instantiation-based methods @@ -39,18 +39,18 @@ class FirstOrderModel; * representative based on the internal heuristic, which is currently based on * choosing the term that was previously chosen as a representative earliest. */ -class EqualityQueryQuantifiersEngine : public QuantifiersUtil +class EqualityQuery : public QuantifiersUtil { public: - EqualityQueryQuantifiersEngine(QuantifiersState& qs, - FirstOrderModel* m); - virtual ~EqualityQueryQuantifiersEngine(); + EqualityQuery(QuantifiersState& qs, FirstOrderModel* m); + virtual ~EqualityQuery(); + /** reset */ bool reset(Theory::Effort e) override; /* Called for new quantifiers */ void registerQuantifier(Node q) override {} /** identify */ - std::string identify() const override { return "EqualityQueryQE"; } + std::string identify() const override { return "EqualityQuery"; } /** gets the current best representative in the equivalence * class of a, based on some heuristic. Currently, the default heuristic * chooses terms that were previously chosen as representatives @@ -65,7 +65,7 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil * Node::null() if all terms in the equivalence class of a * are ineligible. */ - Node getInternalRepresentative(Node a, Node q, int index); + Node getInternalRepresentative(Node a, Node q, size_t index); private: /** the quantifiers state */ @@ -77,16 +77,16 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil /** internal representatives */ std::map< TypeNode, std::map< Node, Node > > d_int_rep; /** rep score */ - std::map< Node, int > d_rep_score; + std::map d_rep_score; /** the number of times reset( e ) has been called */ - int d_reset_count; + size_t d_reset_count; /** processInferences : will merge equivalence classes in master equality engine, if possible */ bool processInferences( Theory::Effort e ); /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ); /** get score */ - int getRepScore( Node n, Node f, int index, TypeNode v_tn ); -}; /* EqualityQueryQuantifiersEngine */ + int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn); +}; /* EqualityQuery */ }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 001c2f62a..fd84dc500 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -23,10 +23,8 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace std; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory::quantifiers::fmcheck; namespace CVC4 { namespace theory { @@ -51,6 +49,7 @@ FirstOrderModel::FirstOrderModel(QuantifiersState& qs, d_qe(nullptr), d_qreg(qr), d_treg(tr), + d_eq_query(qs, this), d_forall_asserts(qs.getSatContext()), d_forallRlvComputed(false) { @@ -59,6 +58,11 @@ FirstOrderModel::FirstOrderModel(QuantifiersState& qs, //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; } +Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index) +{ + return d_eq_query.getInternalRepresentative(a, q, index); +} + void FirstOrderModel::assertQuantifier( Node n ){ if( n.getKind()==FORALL ){ d_forall_asserts.push_back( n ); @@ -163,6 +167,8 @@ bool FirstOrderModel::isModelBasis(TNode n) return n.getAttribute(ModelBasisAttribute()); } +EqualityQuery* FirstOrderModel::getEqualityQuery() { return &d_eq_query; } + /** needs check */ bool FirstOrderModel::checkNeeded() { return d_forall_asserts.size()>0; diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index c2660d933..b86abd960 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -18,7 +18,7 @@ #define CVC4__FIRST_ORDER_MODEL_H #include "context/cdlist.h" -#include "expr/attribute.h" +#include "theory/quantifiers/equality_query.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" @@ -33,13 +33,6 @@ class QuantifiersState; class TermRegistry; class QuantifiersRegistry; -namespace fmcheck { - class FirstOrderModelFmc; -}/* CVC4::theory::quantifiers::fmcheck namespace */ - -struct IsStarAttributeId {}; -typedef expr::Attribute IsStarAttribute; - // TODO (#1301) : document and refactor this class class FirstOrderModel : public TheoryModel { @@ -52,6 +45,17 @@ class FirstOrderModel : public TheoryModel //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) /** finish initialize */ void finishInit(QuantifiersEngine* qe); + /** get internal representative + * + * Choose a term that is equivalent to a in the current context that is the + * best term for instantiating the index^th variable of quantified formula q. + * If no legal term can be found, we return null. This can occur if: + * - a's type is not a subtype of the type of the index^th variable of q, + * - a is in an equivalent class with all terms that are restricted not to + * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample + * guided instantiation. + */ + Node getInternalRepresentative(Node a, Node q, size_t index); /** assert quantifier */ void assertQuantifier( Node n ); @@ -127,6 +131,8 @@ class FirstOrderModel : public TheoryModel * Has the term been marked as a model basis term? */ static bool isModelBasis(TNode n); + /** Get the equality query */ + EqualityQuery* getEqualityQuery(); protected: //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available @@ -135,6 +141,8 @@ class FirstOrderModel : public TheoryModel QuantifiersRegistry& d_qreg; /** Reference to the term registry */ TermRegistry& d_treg; + /** equality query class */ + EqualityQuery d_eq_query; /** list of quantifiers asserted in the current context */ context::CDList d_forall_asserts; /** diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index 252261b9c..9577e296b 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/fmf/first_order_model_fmc.h" +#include "expr/attribute.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/rewriter.h" @@ -24,6 +25,15 @@ namespace theory { namespace quantifiers { namespace fmcheck { +/** + * Marks that a term represents the entire domain of quantified formula for + * the finite model finding fmc algorithm. + */ +struct IsStarAttributeId +{ +}; +using IsStarAttribute = expr::Attribute; + FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 257926737..789a7bd7c 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -166,7 +166,7 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << std::endl; Trace("model-engine-debug") << " Term reps : "; for( size_t i=0; isecond.size(); i++ ){ - Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0); if (r.isNull()) { // there was an invalid equivalence class diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 6c8d826cb..be6101b81 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -131,7 +131,7 @@ bool Instantiate::addInstantiation(Node q, { // pick the best possible representative for instantiation, based on past // use and simplicity of term - terms[i] = d_qe->getInternalRepresentative(terms[i], q, i); + terms[i] = d_qe->getModel()->getInternalRepresentative(terms[i], q, i); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if (terms[i].isNull()) diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7d5c4cf19..68962de72 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -62,7 +62,6 @@ QuantifiersEngine::QuantifiersEngine( d_treg(tr), d_tr_trie(new inst::TriggerTrie), d_model(qm), - d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, qm)), d_instantiate( new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)), d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)), @@ -70,7 +69,7 @@ QuantifiersEngine::QuantifiersEngine( d_quants_red(qstate.getUserContext()) { // initialize the utilities - d_util.push_back(d_eq_query.get()); + d_util.push_back(d_model->getEqualityQuery()); // quantifiers registry must come before the remaining utilities d_util.push_back(&d_qreg); d_util.push_back(tr.getTermDatabase()); @@ -711,10 +710,6 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); } -Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ - return d_eq_query->getInternalRepresentative(a, q, index); -} - Node QuantifiersEngine::getNameForQuant(Node q) const { return d_qreg.getNameForQuant(q); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 625bac40a..4d3029ca9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -40,7 +40,6 @@ namespace inst { class TriggerTrie; } namespace quantifiers { -class EqualityQueryQuantifiersEngine; class FirstOrderModel; class Instantiate; class QModelBuilder; @@ -148,17 +147,6 @@ public: /** mark relevant quantified formula, this will indicate it should be checked * before the others */ void markRelevant(Node q); - /** get internal representative - * - * Choose a term that is equivalent to a in the current context that is the - * best term for instantiating the index^th variable of quantified formula q. - * If no legal term can be found, we return null. This can occur if: - * - a's type is not a subtype of the type of the index^th variable of q, - * - a is in an equivalent class with all terms that are restricted not to - * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample - * guided instantiation. - */ - Node getInternalRepresentative(Node a, Node q, int index); /** * Get quantifiers name, which returns a variable corresponding to the name of * quantified formula q if q has a name, or otherwise returns q itself. @@ -249,8 +237,6 @@ public: std::unique_ptr d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** equality query class */ - std::unique_ptr d_eq_query; /** instantiate utility */ std::unique_ptr d_instantiate; /** skolemize utility */ -- 2.30.2