diff options
Diffstat (limited to 'src/theory/quantifiers/fmf')
| -rw-r--r-- | src/theory/quantifiers/fmf/first_order_model_fmc.cpp | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/first_order_model_fmc.h | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 74 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.h | 14 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/model_builder.cpp | 36 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/model_builder.h | 21 |
6 files changed, 93 insertions, 60 deletions
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 |