From 9eceb1b5495f226b59f0ee6de32deca9fa24e3ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 18 Mar 2021 14:51:38 -0500 Subject: [PATCH] Eliminate dependency on quantifiers engine in quantifiers model (#6165) --- src/theory/quantifiers/first_order_model.cpp | 34 +++++++++++++++---- src/theory/quantifiers/first_order_model.h | 31 ++++++++--------- .../quantifiers/fmf/first_order_model_fmc.cpp | 6 ++-- .../quantifiers/fmf/first_order_model_fmc.h | 7 ++-- .../quantifiers/fmf/full_model_check.cpp | 17 +++++----- src/theory/quantifiers/fmf/full_model_check.h | 4 +-- src/theory/quantifiers/fmf/model_builder.cpp | 6 ++-- src/theory/quantifiers/fmf/model_builder.h | 10 +++--- src/theory/quantifiers_engine.cpp | 21 +++++++----- src/theory/uf/theory_uf_model.cpp | 6 +++- 10 files changed, 80 insertions(+), 62 deletions(-) diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 44c42b305..001c2f62a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -20,8 +20,8 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; @@ -32,18 +32,33 @@ namespace CVC4 { namespace theory { namespace quantifiers { -FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe, - QuantifiersState& qs, +struct ModelBasisAttributeId +{ +}; +using ModelBasisAttribute = expr::Attribute; +// for APPLY_UF terms, 1 : term has direct child with model basis attribute, +// 0 : term has no direct child with model basis attribute. +struct ModelBasisArgAttributeId +{ +}; +using ModelBasisArgAttribute = expr::Attribute; + +FirstOrderModel::FirstOrderModel(QuantifiersState& qs, QuantifiersRegistry& qr, + TermRegistry& tr, std::string name) : TheoryModel(qs.getSatContext(), name, true), - d_qe(qe), + d_qe(nullptr), d_qreg(qr), + d_treg(tr), d_forall_asserts(qs.getSatContext()), d_forallRlvComputed(false) { } +//!!!!!!!!!!!!!!!!!!!!! temporary (project #15) +void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; } + void FirstOrderModel::assertQuantifier( Node n ){ if( n.getKind()==FORALL ){ d_forall_asserts.push_back( n ); @@ -143,6 +158,11 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) } } +bool FirstOrderModel::isModelBasis(TNode n) +{ + return n.getAttribute(ModelBasisAttribute()); +} + /** needs check */ bool FirstOrderModel::checkNeeded() { return d_forall_asserts.size()>0; @@ -237,13 +257,13 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn) Node mbt; if (tn.isClosedEnumerable()) { - mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); + mbt = d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0); } else { if (options::fmfFreshDistConst()) { - mbt = d_qe->getTermDatabase()->getOrMakeTypeFreshVariable(tn); + mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn); } else { @@ -251,7 +271,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn) // may produce an inconsistent model by choosing an arbitrary // equivalence class for it. Hence, we require that it be an existing or // fresh variable. - mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn, true); + mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true); } } ModelBasisAttribute mba; diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 484d7738a..c2660d933 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -27,22 +27,10 @@ namespace theory { class QuantifiersEngine; -struct ModelBasisAttributeId -{ -}; -typedef expr::Attribute ModelBasisAttribute; -// for APPLY_UF terms, 1 : term has direct child with model basis attribute, -// 0 : term has no direct child with model basis attribute. -struct ModelBasisArgAttributeId -{ -}; -typedef expr::Attribute - ModelBasisArgAttribute; - namespace quantifiers { -class TermDb; class QuantifiersState; +class TermRegistry; class QuantifiersRegistry; namespace fmcheck { @@ -56,12 +44,15 @@ typedef expr::Attribute IsStarAttribute; class FirstOrderModel : public TheoryModel { public: - FirstOrderModel(QuantifiersEngine* qe, - QuantifiersState& qs, + FirstOrderModel(QuantifiersState& qs, QuantifiersRegistry& qr, + TermRegistry& tr, std::string name); - virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } + //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) + /** finish initialize */ + void finishInit(QuantifiersEngine* qe); + /** assert quantifier */ void assertQuantifier( Node n ); /** get number of asserted quantifiers */ @@ -132,12 +123,18 @@ class FirstOrderModel : public TheoryModel * has all representatives of type tn. */ bool initializeRepresentativesForType(TypeNode tn); + /** + * Has the term been marked as a model basis term? + */ + static bool isModelBasis(TNode n); protected: - /** quant engine */ + //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available QuantifiersEngine* d_qe; /** The quantifiers registry */ QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; /** 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 5ce5eecfc..252261b9c 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -24,11 +24,11 @@ namespace theory { namespace quantifiers { namespace fmcheck { -FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe, - QuantifiersState& qs, +FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs, QuantifiersRegistry& qr, + TermRegistry& tr, std::string name) - : FirstOrderModel(qe, qs, qr, name) + : FirstOrderModel(qs, qr, tr, name) { } diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index 8f371a96b..d8ae054ad 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -38,17 +38,16 @@ class FirstOrderModelFmc : public FirstOrderModel void processInitializeModelForTerm(Node n) override; public: - FirstOrderModelFmc(QuantifiersEngine* qe, - QuantifiersState& qs, + FirstOrderModelFmc(QuantifiersState& qs, QuantifiersRegistry& qr, + TermRegistry& tr, std::string name); ~FirstOrderModelFmc() override; - FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; } // initialize the model void processInitialize(bool ispre) override; Node getFunctionValue(Node op, const char* argPrefix); - bool isStar(Node n); + static bool isStar(Node n); Node getStar(TypeNode tn); }; /* class FirstOrderModelFmc */ diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index abcd5a794..be83f3b10 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -284,10 +284,9 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } } -FullModelChecker::FullModelChecker(QuantifiersEngine* qe, - QuantifiersState& qs, +FullModelChecker::FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr) - : QModelBuilder(qe, qs, qr) + : QModelBuilder(qs, qr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -298,8 +297,8 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { if( !preProcessBuildModelStd( m ) ){ return false; } - - FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); + + FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m; Trace("fmc") << "---Full Model Check preprocess() " << std::endl; d_preinitialized_eqc.clear(); d_preinitialized_types.clear(); @@ -346,7 +345,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ // nothing to do if no functions return true; } - FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); + FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m; Trace("fmc") << "---Full Model Check reset() " << std::endl; d_quant_models.clear(); d_rep_ids.clear(); @@ -573,11 +572,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { } void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { - FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel(); if( n.isNull() ){ Trace(tr) << "null"; } - else if(fm->isStar(n) && dispStar) { + else if (FirstOrderModelFmc::isStar(n) && dispStar) + { Trace(tr) << "*"; } else @@ -607,7 +606,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i { return 0; } - FirstOrderModelFmc* fmfmc = fm->asFirstOrderModelFmc(); + FirstOrderModelFmc* fmfmc = static_cast(fm); if (effort == 0) { if (options::mbqiMode() == options::MbqiMode::NONE) diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index b3c55ee7a..904a1b9a0 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -154,9 +154,7 @@ protected: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: - FullModelChecker(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersRegistry& qr); + FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr); 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 89e4fa29d..9aa687fbd 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -30,13 +30,11 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -QModelBuilder::QModelBuilder(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersRegistry& qr) +QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr) : TheoryEngineModelBuilder(), - d_qe(qe), d_addedLemmas(0), d_triedLemmas(0), + d_qe(nullptr), d_qstate(qs), d_qreg(qr) { diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 534226a7c..7ba7a66e2 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -32,8 +32,6 @@ class QuantifiersRegistry; class QModelBuilder : public TheoryEngineModelBuilder { protected: - //quantifiers engine - QuantifiersEngine* d_qe; // must call preProcessBuildModelStd bool preProcessBuildModel(TheoryModel* m) override; bool preProcessBuildModelStd(TheoryModel* m); @@ -42,9 +40,9 @@ class QModelBuilder : public TheoryEngineModelBuilder unsigned d_triedLemmas; public: - QModelBuilder(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersRegistry& qr); + QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr); + //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) + void finishInit(QuantifiersEngine* qe) { d_qe = qe; } //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work @@ -62,6 +60,8 @@ class QModelBuilder : public TheoryEngineModelBuilder unsigned getNumTriedLemmas() { return d_triedLemmas; } protected: + /** Pointer to quantifiers engine */ + QuantifiersEngine* d_qe; /** The quantifiers state object */ QuantifiersState& d_qstate; /** Reference to the quantifiers registry */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1784b976e..d6aaeed3f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -72,7 +72,7 @@ QuantifiersEngine::QuantifiersEngine( //---- utilities // quantifiers registry must come before the other utilities d_util.push_back(&d_qreg); - d_util.push_back(d_treg.getTermDatabase()); + d_util.push_back(tr.getTermDatabase()); d_util.push_back(d_instantiate.get()); @@ -93,19 +93,22 @@ QuantifiersEngine::QuantifiersEngine( { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - this, qstate, qr, "FirstOrderModelFmc")); - d_builder.reset( - new quantifiers::fmcheck::FullModelChecker(this, qstate, qr)); + qstate, qr, tr, "FirstOrderModelFmc")); + d_builder.reset(new quantifiers::fmcheck::FullModelChecker(qstate, qr)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; - d_model.reset(new quantifiers::FirstOrderModel( - this, qstate, qr, "FirstOrderModel")); - d_builder.reset(new quantifiers::QModelBuilder(this, qstate, qr)); + d_model.reset( + new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel")); + d_builder.reset(new quantifiers::QModelBuilder(qstate, qr)); } + d_builder->finishInit(this); }else{ - d_model.reset(new quantifiers::FirstOrderModel( - this, qstate, d_qreg, "FirstOrderModel")); + d_model.reset( + new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel")); } + //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) + d_model->finishInit(this); + // initialize the equality query d_eq_query.reset( new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get())); d_util.insert(d_util.begin(), d_eq_query.get()); diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 393f1f705..abb0c2e6c 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -45,7 +45,11 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int if( argIndex<(int)indexOrder.size() ){ //take r = null when argument is the model basis Node r; - if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){ + if (ground + || (!n.isNull() + && !quantifiers::FirstOrderModel::isModelBasis( + n[indexOrder[argIndex]]))) + { r = m->getRepresentative( n[ indexOrder[argIndex] ] ); } d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 ); -- 2.30.2