diff options
21 files changed, 254 insertions, 181 deletions
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 3a2460959..4b04188f1 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -42,12 +42,6 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext()) : nullptr) { -} - -CombinationEngine::~CombinationEngine() {} - -void CombinationEngine::finishInit() -{ // create the equality engine, model manager, and shared solver if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) { @@ -64,7 +58,12 @@ void CombinationEngine::finishInit() Unhandled() << "CombinationEngine::finishInit: equality engine mode " << options::eeMode() << " not supported"; } +} + +CombinationEngine::~CombinationEngine() {} +void CombinationEngine::finishInit() +{ Assert(d_eemanager != nullptr); // initialize equality engines in all theories, including quantifiers engine diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 5c2b3b25a..b7499447f 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -32,7 +32,9 @@ ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem) d_eem(eem), d_modelEqualityEngine(nullptr), d_modelEqualityEngineAlloc(nullptr), - d_model(nullptr), + d_model(new TheoryModel(te.getUserContext(), + "DefaultModel", + options::assignFunctionValues())), d_modelBuilder(nullptr), d_modelBuilt(false), d_modelBuiltSuccess(false) @@ -51,14 +53,6 @@ void ModelManager::finishInit(eq::EqualityEngineNotify* notify) QuantifiersEngine* qe = d_te.getQuantifiersEngine(); Assert(qe != nullptr); d_modelBuilder = qe->getModelBuilder(); - d_model = qe->getModel(); - } - else - { - context::Context* u = d_te.getUserContext(); - d_alocModel.reset( - new TheoryModel(u, "DefaultModel", options::assignFunctionValues())); - d_model = d_alocModel.get(); } // make the default builder, e.g. in the case that the quantifiers engine does @@ -142,13 +136,13 @@ void ModelManager::postProcessModel(bool incomplete) } Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId << std::endl; - t->postProcessModel(d_model); + t->postProcessModel(d_model.get()); } // also call the model builder's post-process model - d_modelBuilder->postProcessModel(incomplete, d_model); + d_modelBuilder->postProcessModel(incomplete, d_model.get()); } -theory::TheoryModel* ModelManager::getModel() { return d_model; } +theory::TheoryModel* ModelManager::getModel() { return d_model.get(); } bool ModelManager::collectModelBooleanVariables() { diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index 50cd6a3d2..41559e7b6 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -73,7 +73,7 @@ class ModelManager */ void postProcessModel(bool incomplete); /** Get a pointer to model object maintained by this class. */ - theory::TheoryModel* getModel(); + TheoryModel* getModel(); //------------------------ finer grained control over model building /** * Prepare model, which is the manager-specific method for setting up the @@ -138,14 +138,12 @@ class ModelManager eq::EqualityEngine* d_modelEqualityEngine; /** The equality engine of the model, if we allocated it */ std::unique_ptr<eq::EqualityEngine> d_modelEqualityEngineAlloc; - /** The model object we are using */ - theory::TheoryModel* d_model; /** The model object we have allocated (if one exists) */ - std::unique_ptr<theory::TheoryModel> d_alocModel; + std::unique_ptr<TheoryModel> d_model; /** The model builder object we are using */ - theory::TheoryEngineModelBuilder* d_modelBuilder; + TheoryEngineModelBuilder* d_modelBuilder; /** The model builder object we have allocated (if one exists) */ - std::unique_ptr<theory::TheoryEngineModelBuilder> d_alocModelBuilder; + std::unique_ptr<TheoryEngineModelBuilder> d_alocModelBuilder; /** whether we have tried to build this model in the current context */ bool d_modelBuilt; /** whether this model has been built successfully */ diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index 6c807c647..f3a501f94 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -85,7 +85,7 @@ bool ModelManagerDistributed::prepareModel() collectAssertedTerms(theoryId, termSet); // also get relevant terms t->computeRelevantTerms(termSet); - if (!t->collectModelInfo(d_model, termSet)) + if (!t->collectModelInfo(d_model.get(), termSet)) { Trace("model-builder") << "ModelManagerDistributed: fail collect model info" << std::endl; @@ -106,7 +106,7 @@ bool ModelManagerDistributed::prepareModel() bool ModelManagerDistributed::finishBuildModel() const { // do not use relevant terms - if (!d_modelBuilder->buildModel(d_model)) + if (!d_modelBuilder->buildModel(d_model.get())) { Trace("model-builder") << "ModelManager: fail build model" << std::endl; return false; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index de71d62a7..d4bc7dfcb 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -44,10 +44,8 @@ using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_ FirstOrderModel::FirstOrderModel(QuantifiersState& qs, QuantifiersRegistry& qr, - TermRegistry& tr, - std::string name) - : TheoryModel(qs.getSatContext(), name, true), - d_qe(nullptr), + TermRegistry& tr) + : d_model(nullptr), d_qreg(qr), d_treg(tr), d_eq_query(qs, this), @@ -56,8 +54,32 @@ FirstOrderModel::FirstOrderModel(QuantifiersState& qs, { } -//!!!!!!!!!!!!!!!!!!!!! temporary (project #15) -void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; } +void FirstOrderModel::finishInit(TheoryModel* m) { d_model = m; } + +Node FirstOrderModel::getValue(TNode n) const { return d_model->getValue(n); } +bool FirstOrderModel::hasTerm(TNode a) { return d_model->hasTerm(a); } +Node FirstOrderModel::getRepresentative(TNode a) +{ + return d_model->getRepresentative(a); +} +bool FirstOrderModel::areEqual(TNode a, TNode b) +{ + return d_model->areEqual(a, b); +} +bool FirstOrderModel::areDisequal(TNode a, TNode b) +{ + return d_model->areDisequal(a, b); +} +eq::EqualityEngine* FirstOrderModel::getEqualityEngine() +{ + return d_model->getEqualityEngine(); +} +const RepSet* FirstOrderModel::getRepSet() const +{ + return d_model->getRepSet(); +} +RepSet* FirstOrderModel::getRepSetPtr() { return d_model->getRepSetPtr(); } +TheoryModel* FirstOrderModel::getTheoryModel() { return d_model; } Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index) { @@ -118,23 +140,25 @@ void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& vi Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ //check if there is even any domain elements at all - if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0) + RepSet* rs = d_model->getRepSetPtr(); + if (!rs->hasType(tn) || rs->getNumRepresentatives(tn) == 0) { Trace("fm-debug") << "Must create domain element for " << tn << "..." << std::endl; Node mbt = getModelBasisTerm(tn); Trace("fm-debug") << "Add to representative set..." << std::endl; - d_rep_set.add(tn, mbt); + rs->add(tn, mbt); } - return d_rep_set.d_type_reps[tn][0]; + return rs->getRepresentative(tn, 0); } bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) { + RepSet* rs = d_model->getRepSetPtr(); if (tn.isSort()) { // must ensure uninterpreted type is non-empty. - if (!d_rep_set.hasType(tn)) + if (!rs->hasType(tn)) { // terms in rep_set are now constants which mapped to terms through // TheoryModel. Thus, should introduce a constant and a term. @@ -142,7 +166,7 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) Node var = getSomeDomainElement(tn); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; - d_rep_set.add(tn, var); + rs->add(tn, var); } return true; } @@ -153,9 +177,9 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) { Trace("fm-debug") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; - d_rep_set.complete(tn); + rs->complete(tn); // must have succeeded - Assert(d_rep_set.hasType(tn)); + Assert(rs->hasType(tn)); return true; } Trace("fm-debug") << " variable cannot be bounded." << std::endl; diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 04b1fdb63..1969fdde7 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -26,7 +26,8 @@ namespace cvc5 { namespace theory { -class QuantifiersEngine; +class TheoryModel; +class RepSet; namespace quantifiers { @@ -35,17 +36,36 @@ class TermRegistry; class QuantifiersRegistry; // TODO (#1301) : document and refactor this class -class FirstOrderModel : public TheoryModel +class FirstOrderModel { public: FirstOrderModel(QuantifiersState& qs, QuantifiersRegistry& qr, - TermRegistry& tr, - std::string name); + TermRegistry& tr); + virtual ~FirstOrderModel() {} - //!!!!!!!!!!!!!!!!!!!!! temporary (project #15) - /** finish initialize */ - void finishInit(QuantifiersEngine* qe); + /** finish init */ + void finishInit(TheoryModel* m); + //---------------------------------- access functions for underlying model + /** Get value in the underlying theory model */ + Node getValue(TNode n) const; + /** does the equality engine of this model have term a? */ + bool hasTerm(TNode a); + /** get the representative of a in the equality engine of this model */ + Node getRepresentative(TNode a); + /** are a and b equal in the equality engine of this model? */ + bool areEqual(TNode a, TNode b); + /** are a and b disequal in the equality engine of this model? */ + bool areDisequal(TNode a, TNode b); + /** get the equality engine for this model */ + eq::EqualityEngine* getEqualityEngine(); + /** get the representative set object */ + const RepSet* getRepSet() const; + /** get the representative set object */ + RepSet* getRepSetPtr(); + /** get the entire theory model */ + TheoryModel* getTheoryModel(); + //---------------------------------- end access functions for underlying model /** get internal representative * * Choose a term that is equivalent to a in the current context that is the @@ -136,8 +156,8 @@ class FirstOrderModel : public TheoryModel EqualityQuery* getEqualityQuery(); protected: - //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available - QuantifiersEngine* d_qe; + /** Pointer to the underyling theory model */ + TheoryModel* d_model; /** The quantifiers registry */ QuantifiersRegistry& d_qreg; /** Reference to the term registry */ diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index 852b60521..e17271613 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -38,9 +38,8 @@ using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>; FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs, QuantifiersRegistry& qr, - TermRegistry& tr, - std::string name) - : FirstOrderModel(qs, qr, tr, name) + TermRegistry& tr) + : FirstOrderModel(qs, qr, tr) { } diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index 3c35fdbe8..f148a9e19 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -41,8 +41,7 @@ class FirstOrderModelFmc : public FirstOrderModel public: FirstOrderModelFmc(QuantifiersState& qs, QuantifiersRegistry& qr, - TermRegistry& tr, - std::string name); + TermRegistry& tr); ~FirstOrderModelFmc() override; // initialize the model void processInitialize(bool ispre) override; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index da220be18..fd91a94ab 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -286,26 +286,28 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } FullModelChecker::FullModelChecker(QuantifiersState& qs, + QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - QuantifiersInferenceManager& qim) - : QModelBuilder(qs, qr, qim) + TermRegistry& tr) + : QModelBuilder(qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(qs, qr, tr)) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } +void FullModelChecker::finishInit() { d_model = d_fm.get(); } + bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { //standard pre-process if( !preProcessBuildModelStd( m ) ){ return false; } - FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m; Trace("fmc") << "---Full Model Check preprocess() " << std::endl; d_preinitialized_eqc.clear(); d_preinitialized_types.clear(); //traverse equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(m->getEqualityEngine()); while( !eqcs_i.isFinished() ){ Node r = *eqcs_i; TypeNode tr = r.getType(); @@ -315,23 +317,24 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { //must ensure model basis terms exists in model for each relevant type Trace("fmc") << "preInitialize types..." << std::endl; - fm->initialize(); - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; + d_fm->initialize(); + for (std::pair<const Node, Def*>& mp : d_fm->d_models) + { + Node op = mp.first; Trace("fmc") << "preInitialize types for " << op << std::endl; TypeNode tno = op.getType(); for( unsigned i=0; i<tno.getNumChildren(); i++) { Trace("fmc") << "preInitializeType " << tno[i] << std::endl; - preInitializeType( fm, tno[i] ); + preInitializeType(m, tno[i]); Trace("fmc") << "finished preInitializeType " << tno[i] << std::endl; } } Trace("fmc") << "Finish preInitialize types" << std::endl; //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts - for (unsigned i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant; + for (unsigned i = 0, nquant = d_fm->getNumAssertedQuantifiers(); i < nquant; i++) { - Node q = fm->getAssertedQuantifier(i); + Node q = d_fm->getAssertedQuantifier(i); registerQuantifiedFormula(q); if (!isHandled(q)) { @@ -340,7 +343,7 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { // make sure all types are set for (const Node& v : q[0]) { - preInitializeType(fm, v.getType()); + preInitializeType(m, v.getType()); } } return true; @@ -352,13 +355,13 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ // nothing to do if no functions return true; } - FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m; + FirstOrderModelFmc* fm = d_fm.get(); Trace("fmc") << "---Full Model Check reset() " << std::endl; d_quant_models.clear(); d_rep_ids.clear(); d_star_insts.clear(); //process representatives - RepSet* rs = fm->getRepSetPtr(); + RepSet* rs = m->getRepSetPtr(); for (std::map<TypeNode, std::vector<Node> >::iterator it = rs->d_type_reps.begin(); it != rs->d_type_reps.end(); @@ -367,7 +370,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ if( it->first.isSort() ){ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; for( size_t a=0; a<it->second.size(); a++ ){ - Node r = fm->getRepresentative( it->second[a] ); + Node r = m->getRepresentative(it->second[a]); if( Trace.isOn("fmc-model-debug") ){ std::vector< Node > eqc; d_qstate.getEquivalenceClass(r, eqc); @@ -387,25 +390,27 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ } //now, make models - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; + for (std::pair<const Node, Def*>& fmm : d_fm->d_models) + { + Node op = fmm.first; //reset the model - fm->d_models[op]->reset(); + d_fm->d_models[op]->reset(); std::vector< Node > add_conds; std::vector< Node > add_values; bool needsDefault = true; - std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op ); - if( itut!=fm->d_uf_terms.end() ){ - Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl; - for( size_t i=0; i<itut->second.size(); i++ ){ - Node n = itut->second[i]; + if (m->hasUfTerms(op)) + { + const std::vector<Node>& uft = m->getUfTerms(op); + Trace("fmc-model-debug") + << uft.size() << " model values for " << op << " ... " << std::endl; + for (const Node& n : uft) + { // only consider unique up to congruence (in model equality engine)? add_conds.push_back( n ); add_values.push_back( n ); - Node r = fm->getRepresentative(n); + Node r = m->getRepresentative(n); Trace("fmc-model-debug") << n << " -> " << r << std::endl; - //AlwaysAssert( fm->areEqual( itut->second[i], r ) ); } }else{ Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl; @@ -413,17 +418,18 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Trace("fmc-model-debug") << std::endl; //possibly get default if( needsDefault ){ - Node nmb = fm->getModelBasisOpTerm(op); + Node nmb = d_fm->getModelBasisOpTerm(op); //add default value if necessary - if( fm->hasTerm( nmb ) ){ + if (m->hasTerm(nmb)) + { Trace("fmc-model-debug") << "Add default " << nmb << std::endl; add_conds.push_back( nmb ); add_values.push_back( nmb ); }else{ - Node vmb = getSomeDomainElement(fm, nmb.getType()); + Node vmb = getSomeDomainElement(d_fm.get(), nmb.getType()); Trace("fmc-model-debug") << "Add default to default representative " << nmb << " "; Trace("fmc-model-debug") - << fm->getRepSet()->getNumRepresentatives(nmb.getType()) + << m->getRepSet()->getNumRepresentatives(nmb.getType()) << std::endl; add_conds.push_back( nmb ); add_values.push_back( vmb ); @@ -536,32 +542,33 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ return TheoryEngineModelBuilder::processBuildModel( m ); } -void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ +void FullModelChecker::preInitializeType(TheoryModel* m, TypeNode tn) +{ if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){ d_preinitialized_types[tn] = true; if (tn.isFirstClass()) { Trace("fmc") << "Get model basis term " << tn << "..." << std::endl; - Node mb = fm->getModelBasisTerm(tn); + Node mb = d_fm->getModelBasisTerm(tn); Trace("fmc") << "...return " << mb << std::endl; // if the model basis term does not exist in the model, // either add it directly to the model's equality engine if no other terms // of this type exist, or otherwise assert that it is equal to the first // equivalence class of its type. - if (!fm->hasTerm(mb) && !mb.isConst()) + if (!m->hasTerm(mb) && !mb.isConst()) { std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn); if (itpe == d_preinitialized_eqc.end()) { Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl; - fm->d_equalityEngine->addTerm(mb); + m->getEqualityEngine()->addTerm(mb); } else { Trace("fmc") << "...add model basis eqc equality to model " << mb << " == " << itpe->second << " " << tn << std::endl; - bool ret = fm->assertEquality(mb, itpe->second, true); + bool ret = m->assertEquality(mb, itpe->second, true); AlwaysAssert(ret); } } @@ -1348,7 +1355,6 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const bool FullModelChecker::useSimpleModels() { return options::fmfFmcSimple(); } - void FullModelChecker::registerQuantifiedFormula(Node q) { if (d_quant_cond.find(q) != d_quant_cond.end()) diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index fd50d632f..fdaf18e81 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -113,7 +113,7 @@ protected: * if a bound variable is of type T, or an uninterpreted function has an * argument or a return value of type T. */ - void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ); + void preInitializeType(TheoryModel* m, TypeNode tn); /** for each type, an equivalence class of that type from the model */ std::map<TypeNode, Node> d_preinitialized_eqc; /** map from types to whether we have called the method above */ @@ -156,9 +156,11 @@ protected: public: FullModelChecker(QuantifiersState& qs, + QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - QuantifiersInferenceManager& qim); - + TermRegistry& tr); + /** finish init, which sets the model object */ + void finishInit() override; void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); @@ -173,7 +175,6 @@ protected: bool processBuildModel(TheoryModel* m) override; bool useSimpleModels(); - private: /** * Register quantified formula. @@ -183,6 +184,11 @@ protected: void registerQuantifiedFormula(Node q); /** Is quantified formula q handled by model-based instantiation? */ bool isHandled(Node q) const; + /** + * The first order model. This is an extended form of the first order model + * class that is specialized for this class. + */ + std::unique_ptr<FirstOrderModelFmc> d_fm; };/* class FullModelChecker */ } // namespace fmcheck diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index d012bea8a..ab3dbea95 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -30,17 +30,27 @@ using namespace cvc5::theory; using namespace cvc5::theory::quantifiers; QModelBuilder::QModelBuilder(QuantifiersState& qs, + QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - QuantifiersInferenceManager& qim) + TermRegistry& tr) : TheoryEngineModelBuilder(), d_addedLemmas(0), d_triedLemmas(0), d_qstate(qs), + d_qim(qim), d_qreg(qr), - d_qim(qim) + d_treg(tr), + d_model(nullptr) { } +void QModelBuilder::finishInit() +{ + // allocate the default model + d_modelAloc.reset(new FirstOrderModel(d_qstate, d_qreg, d_treg)); + d_model = d_modelAloc.get(); +} + bool QModelBuilder::optUseModel() { return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound(); } @@ -54,20 +64,23 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { d_triedLemmas = 0; if (options::fmfFunWellDefinedRelevant()) { - FirstOrderModel * fm = (FirstOrderModel*)m; //traverse equality engine std::map< TypeNode, bool > eqc_usort; eq::EqClassesIterator eqcs_i = - eq::EqClassesIterator(fm->getEqualityEngine()); + eq::EqClassesIterator(m->getEqualityEngine()); while( !eqcs_i.isFinished() ){ TypeNode tr = (*eqcs_i).getType(); eqc_usort[tr] = true; ++eqcs_i; } //look at quantified formulas - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i, true ); - if( fm->isQuantifierActive( q ) ){ + for (size_t i = 0, nquant = d_model->getNumAssertedQuantifiers(); + i < nquant; + i++) + { + Node q = d_model->getAssertedQuantifier(i, true); + if (d_model->isQuantifierActive(q)) + { //check if any of these quantified formulas can be set inactive if (q[0].getNumChildren() == 1) { @@ -79,7 +92,7 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { { Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; - fm->setQuantifierActive( q, false ); + d_model->setQuantifierActive(q, false); } } } @@ -92,7 +105,7 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { void QModelBuilder::debugModel( TheoryModel* m ){ //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true if( Trace.isOn("quant-check-model") ){ - FirstOrderModel* fm = (FirstOrderModel*)m; + FirstOrderModel* fm = d_model; Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl; int tests = 0; int bad = 0; @@ -105,7 +118,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){ vars.push_back( f[0][j] ); } QRepBoundExt qrbe(qbi, fm); - RepSetIterator riter(fm->getRepSet(), &qrbe); + RepSetIterator riter(m->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ while( !riter.isFinished() ){ tests++; @@ -115,7 +128,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){ terms.push_back( riter.getCurrentTerm( k ) ); } Node n = inst->getInstantiation(f, vars, terms); - Node val = fm->getValue( n ); + Node val = m->getValue(n); if (!val.isConst() || !val.getConst<bool>()) { Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl; @@ -138,3 +151,4 @@ void QModelBuilder::debugModel( TheoryModel* m ){ } } } +FirstOrderModel* QModelBuilder::getModel() { return d_model; } diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index df866fbe1..cfccd4d93 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -30,6 +30,7 @@ class FirstOrderModel; class QuantifiersState; class QuantifiersRegistry; class QuantifiersInferenceManager; +class TermRegistry; class QModelBuilder : public TheoryEngineModelBuilder { @@ -43,9 +44,11 @@ class QModelBuilder : public TheoryEngineModelBuilder public: QModelBuilder(QuantifiersState& qs, + QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - QuantifiersInferenceManager& qim); - + TermRegistry& tr); + /** finish init, which sets the model object */ + virtual void finishInit(); //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work // >0 : success @@ -60,16 +63,22 @@ class QModelBuilder : public TheoryEngineModelBuilder //statistics unsigned getNumAddedLemmas() { return d_addedLemmas; } unsigned getNumTriedLemmas() { return d_triedLemmas; } + /** get the model we are using */ + FirstOrderModel* getModel(); protected: - /** Pointer to quantifiers engine */ - QuantifiersEngine* d_qe; /** The quantifiers state object */ QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** Reference to the quantifiers registry */ QuantifiersRegistry& d_qreg; - /** The quantifiers inference manager */ - quantifiers::QuantifiersInferenceManager& d_qim; + /** Term registry */ + TermRegistry& d_treg; + /** Pointer to the model object we are using */ + FirstOrderModel* d_model; + /** The model object we have allocated */ + std::unique_ptr<FirstOrderModel> d_modelAloc; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 704a65bfb..f6b8f30f4 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -28,7 +28,6 @@ QuantifiersModules::QuantifiersModules() d_alpha_equiv(nullptr), d_inst_engine(nullptr), d_model_engine(nullptr), - d_builder(nullptr), d_bint(nullptr), d_qcf(nullptr), d_sg_gen(nullptr), @@ -45,6 +44,7 @@ void QuantifiersModules::initialize(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, + QModelBuilder* builder, std::vector<QuantifiersModule*>& modules) { // add quantifiers modules @@ -80,23 +80,10 @@ void QuantifiersModules::initialize(QuantifiersState& qs, d_bint.reset(new BoundedIntegers(qs, qim, qr, tr)); modules.push_back(d_bint.get()); } + if (options::finiteModelFind() || options::fmfBound()) { - Trace("quant-init-debug") - << "Initialize model engine, mbqi : " << options::mbqiMode() << " " - << options::fmfBound() << std::endl; - if (tr.useFmcModel()) - { - Trace("quant-init-debug") << "...make fmc builder." << std::endl; - d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim)); - } - else - { - Trace("quant-init-debug") - << "...make default model builder." << std::endl; - d_builder.reset(new QModelBuilder(qs, qr, qim)); - } - d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, d_builder.get())); + d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 659be0381..f41e81f34 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -61,6 +61,7 @@ class QuantifiersModules QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, + QModelBuilder* builder, std::vector<QuantifiersModule*>& modules); private: @@ -74,8 +75,6 @@ class QuantifiersModules std::unique_ptr<InstantiationEngine> d_inst_engine; /** model engine */ std::unique_ptr<ModelEngine> d_model_engine; - /** model builder */ - std::unique_ptr<quantifiers::QModelBuilder> d_builder; /** bounded integers utility */ std::unique_ptr<BoundedIntegers> d_bint; /** Conflict find mechanism for quantifiers */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 4e1aacbac..5b7bd1552 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -29,12 +29,12 @@ namespace quantifiers { TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) : d_presolve(qs.getUserContext(), true), - d_useFmcModel(false), d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), d_termPools(new TermPools(qs)), d_termDb(new TermDb(qs, qr)), - d_sygusTdb(nullptr) + d_sygusTdb(nullptr), + d_qmodel(nullptr) { if (options::sygus() || options::sygusInst()) { @@ -44,27 +44,12 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; - // Finite model finding requires specialized ways of building the model. - // We require constructing the model here, since it is required for - // initializing the CombinationEngine and the rest of quantifiers engine. - if ((options::finiteModelFind() || options::fmfBound()) - && (options::mbqiMode() == options::MbqiMode::FMC - || options::mbqiMode() == options::MbqiMode::TRUST - || options::fmfBound())) - { - d_useFmcModel = true; - d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - qs, qr, *this, "FirstOrderModelFmc")); - } - else - { - d_qmodel.reset( - new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel")); - } } -void TermRegistry::finishInit(QuantifiersInferenceManager* qim) +void TermRegistry::finishInit(FirstOrderModel* fm, + QuantifiersInferenceManager* qim) { + d_qmodel = fm; d_termDb->finishInit(qim); if (d_sygusTdb.get()) { @@ -149,9 +134,7 @@ TermEnumeration* TermRegistry::getTermEnumeration() const TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); } -FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); } - -bool TermRegistry::useFmcModel() const { return d_useFmcModel; } +FirstOrderModel* TermRegistry::getModel() const { return d_qmodel; } } // namespace quantifiers } // namespace theory diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 5dfc3f78d..cf2ba7a47 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -45,7 +45,7 @@ class TermRegistry TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr); /** Finish init, which sets the inference manager on modules of this class */ - void finishInit(QuantifiersInferenceManager* qim); + void finishInit(FirstOrderModel* fm, QuantifiersInferenceManager* qim); /** Presolve */ void presolve(); @@ -79,9 +79,6 @@ class TermRegistry void processInstantiation(Node q, const std::vector<Node>& terms); void processSkolemization(Node q, const std::vector<Node>& skolems); - /** Whether we use the full model check builder and corresponding model */ - bool useFmcModel() const; - /** get term database */ TermDb* getTermDatabase() const; /** get term database sygus */ @@ -109,7 +106,7 @@ class TermRegistry /** sygus term database */ std::unique_ptr<TermDbSygus> d_sygusTdb; /** extended model object */ - std::unique_ptr<FirstOrderModel> d_qmodel; + FirstOrderModel* d_qmodel; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 27b16e411..6bfedb0a2 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -49,19 +49,9 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, out.handleUserAttribute( "quant-elim", this ); out.handleUserAttribute( "quant-elim-partial", this ); - // Finish initializing the term registry by hooking it up to the inference - // manager. This is required due to a cyclic dependency between the term - // database and the instantiate module. Term database needs inference manager - // since it sends out lemmas when term indexing is inconsistent, instantiate - // needs term database for entailment checks. - d_treg.finishInit(&d_qim); - // construct the quantifiers engine d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm)); - //!!!!!!!!!!!!!! temporary (project #15) - d_treg.getModel()->finishInit(d_qengine.get()); - // indicate we are using the quantifiers theory state object d_theoryState = &d_qstate; // use the inference manager as the official inference manager diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5916390a6..2d1eeab84 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -44,21 +44,54 @@ namespace cvc5 { namespace theory { QuantifiersEngine::QuantifiersEngine( - quantifiers::QuantifiersState& qstate, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, ProofNodeManager* pnm) - : d_qstate(qstate), + : d_qstate(qs), d_qim(qim), d_te(nullptr), d_pnm(pnm), d_qreg(qr), d_treg(tr), - d_model(d_treg.getModel()), - d_quants_prereg(qstate.getUserContext()), - d_quants_red(qstate.getUserContext()) + d_model(nullptr), + d_quants_prereg(qs.getUserContext()), + d_quants_red(qs.getUserContext()) { + Trace("quant-init-debug") + << "Initialize model engine, mbqi : " << options::mbqiMode() << " " + << options::fmfBound() << std::endl; + // Finite model finding requires specialized ways of building the model. + // We require constructing the model here, since it is required for + // initializing the CombinationEngine and the rest of quantifiers engine. + if (options::fmfBound() + || (options::finiteModelFind() + && (options::mbqiMode() == options::MbqiMode::FMC + || options::mbqiMode() == options::MbqiMode::TRUST))) + { + Trace("quant-init-debug") << "...make fmc builder." << std::endl; + d_builder.reset( + new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr)); + } + else + { + Trace("quant-init-debug") << "...make default model builder." << std::endl; + d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr)); + } + // set the model object + d_builder->finishInit(); + d_model = d_builder->getModel(); + + // Finish initializing the term registry by hooking it up to the model and the + // inference manager. The former is required since theories are not given + // access to the model in their constructors currently. + // The latter is required due to a cyclic dependency between the term + // database and the instantiate module. Term database needs inference manager + // since it sends out lemmas when term indexing is inconsistent, instantiate + // needs term database for entailment checks. + d_treg.finishInit(d_model, &d_qim); + // initialize the utilities d_util.push_back(d_model->getEqualityQuery()); // quantifiers registry must come before the remaining utilities @@ -72,10 +105,13 @@ QuantifiersEngine::~QuantifiersEngine() {} void QuantifiersEngine::finishInit(TheoryEngine* te) { + // connect the quantifiers model to the underlying theory model + d_model->finishInit(te->getModel()); d_te = te; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(d_qstate, d_qim, d_qreg, d_treg, d_modules); + d_qmodules->initialize( + d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); @@ -95,11 +131,7 @@ quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry() quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { - return d_qmodules->d_builder.get(); -} -quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const -{ - return d_model; + return d_builder.get(); } /// !!!!!!!!!!!!!! temporary (project #15) diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index fd4889154..631f7bec1 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -69,8 +69,6 @@ class QuantifiersEngine { //---------------------- utilities /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; - /** get model */ - quantifiers::FirstOrderModel* getModel() const; /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; //---------------------- end utilities @@ -194,6 +192,8 @@ public: quantifiers::QuantifiersRegistry& d_qreg; /** The term registry */ quantifiers::TermRegistry& d_treg; + /** model builder */ + std::unique_ptr<quantifiers::QModelBuilder> d_builder; /** extended model object */ quantifiers::FirstOrderModel* d_model; //------------- end quantifiers utilities diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 40a64cb35..1543739e0 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -681,6 +681,18 @@ bool TheoryModel::areDisequal(TNode a, TNode b) } } +bool TheoryModel::hasUfTerms(Node f) const +{ + return d_uf_terms.find(f) != d_uf_terms.end(); +} + +const std::vector<Node>& TheoryModel::getUfTerms(Node f) const +{ + const auto it = d_uf_terms.find(f); + Assert(it != d_uf_terms.end()); + return it->second; +} + bool TheoryModel::areFunctionValuesEnabled() const { return d_enableFuncModels; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 42392c522..b4a089767 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -328,10 +328,10 @@ public: Cardinality getCardinality(TypeNode t) const; //---------------------------- function values - /** a map from functions f to a list of all APPLY_UF terms with operator f */ - std::map< Node, std::vector< Node > > d_uf_terms; - /** a map from functions f to a list of all HO_APPLY terms with first argument f */ - std::map< Node, std::vector< Node > > d_ho_uf_terms; + /** Does this model have terms for the given uninterpreted function? */ + bool hasUfTerms(Node f) const; + /** Get the terms for uninterpreted function f */ + const std::vector<Node>& getUfTerms(Node f) const; /** are function values enabled? */ bool areFunctionValuesEnabled() const; /** assign function value f to definition f_def */ @@ -423,6 +423,11 @@ public: //---------------------------- end separation logic //---------------------------- function values + /** a map from functions f to a list of all APPLY_UF terms with operator f */ + std::map<Node, std::vector<Node> > d_uf_terms; + /** a map from functions f to a list of all HO_APPLY terms with first argument + * f */ + std::map<Node, std::vector<Node> > d_ho_uf_terms; /** whether function models are enabled */ bool d_enableFuncModels; /** map from function terms to the (lambda) definitions |