From 248f841f37b8b2d514d7308faa8f4573115f82e9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 24 Aug 2018 19:40:36 -0500 Subject: [PATCH] Clean up quantifiers engine initialization. (#2371) --- src/theory/quantifiers_engine.cpp | 290 ++++++++++++++++----------- src/theory/quantifiers_engine.h | 319 ++++++++++++++---------------- 2 files changed, 326 insertions(+), 283 deletions(-) diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a5cd95d29..510953035 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -70,10 +70,36 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te) : d_te(te), + d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), + d_eq_inference(nullptr), + d_inst_prop(nullptr), + d_tr_trie(new inst::TriggerTrie), + d_model(nullptr), + d_quant_rel(nullptr), + d_rel_dom(nullptr), + d_bv_invert(nullptr), + d_builder(nullptr), + d_qepr(nullptr), + d_term_util(new quantifiers::TermUtil(this)), + d_term_db(new quantifiers::TermDb(c, u, this)), + d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), d_instantiate(new quantifiers::Instantiate(this, u)), d_skolemize(new quantifiers::Skolemize(this, u)), d_term_enum(new quantifiers::TermEnumeration), + d_alpha_equiv(nullptr), + d_inst_engine(nullptr), + d_model_engine(nullptr), + d_bint(nullptr), + d_qcf(nullptr), + d_rr_engine(nullptr), + d_sg_gen(nullptr), + d_ceg_inst(nullptr), + d_lte_part_inst(nullptr), + d_fs(nullptr), + d_i_cbqi(nullptr), + d_qsplit(nullptr), + d_anti_skolem(nullptr), d_conflict_c(c, false), // d_quants(u), d_quants_prereg(u), @@ -89,41 +115,29 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_presolve_cache_wq(u), d_presolve_cache_wic(u) { - //utilities - d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this ); - d_util.push_back( d_eq_query ); + //---- 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()); - // term util must come first - d_term_util = new quantifiers::TermUtil(this); - d_util.push_back(d_term_util); - - d_term_db = new quantifiers::TermDb( c, u, this ); - d_util.push_back( d_term_db ); - if (options::ceGuidedInst()) { - d_sygus_tdb = new quantifiers::TermDbSygus(c, this); - }else{ - d_sygus_tdb = NULL; + d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); } if( options::instPropagate() ){ // notice that this option is incompatible with options::qcfAllConflict() - d_inst_prop = new quantifiers::InstPropagator( this ); - d_util.push_back( d_inst_prop ); + d_inst_prop.reset(new quantifiers::InstPropagator(this)); + d_util.push_back(d_inst_prop.get()); d_instantiate->addNotify(d_inst_prop->getInstantiationNotify()); - }else{ - d_inst_prop = NULL; } if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference(c, false); - }else{ - d_eq_inference = NULL; + d_eq_inference.reset(new quantifiers::EqualityInference(c, false)); } d_util.push_back(d_instantiate.get()); - d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; @@ -135,37 +149,15 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::relevantTriggers() ){ - d_quant_rel = new quantifiers::QuantRelevance; - d_util.push_back(d_quant_rel); - }else{ - d_quant_rel = NULL; + d_quant_rel.reset(new quantifiers::QuantRelevance); + d_util.push_back(d_quant_rel.get()); } if( options::quantEpr() ){ Assert( !options::incrementalSolving() ); - d_qepr = new quantifiers::QuantEPR; - }else{ - d_qepr = NULL; + d_qepr.reset(new quantifiers::QuantEPR); } - - - d_qcf = NULL; - d_sg_gen = NULL; - d_inst_engine = NULL; - d_i_cbqi = NULL; - d_qsplit = NULL; - d_anti_skolem = NULL; - d_model = NULL; - d_model_engine = NULL; - d_bint = NULL; - d_rr_engine = NULL; - d_ceg_inst = NULL; - d_lte_part_inst = NULL; - d_alpha_equiv = NULL; - d_fs = NULL; - d_rel_dom = NULL; - d_bv_invert = NULL; - d_builder = NULL; + //---- end utilities //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -178,70 +170,70 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, bool needsRelDom = false; //add quantifiers modules if( options::quantConflictFind() || options::quantRewriteRules() ){ - d_qcf = new quantifiers::QuantConflictFind( this, c); - d_modules.push_back( d_qcf ); + d_qcf.reset(new quantifiers::QuantConflictFind(this, c)); + d_modules.push_back(d_qcf.get()); } if( options::conjectureGen() ){ - d_sg_gen = new quantifiers::ConjectureGenerator( this, c ); - d_modules.push_back( d_sg_gen ); + d_sg_gen.reset(new quantifiers::ConjectureGenerator(this, c)); + d_modules.push_back(d_sg_gen.get()); } if( !options::finiteModelFind() || options::fmfInstEngine() ){ - d_inst_engine = new quantifiers::InstantiationEngine( this ); - d_modules.push_back( d_inst_engine ); + d_inst_engine.reset(new quantifiers::InstantiationEngine(this)); + d_modules.push_back(d_inst_engine.get()); } if( options::cbqi() ){ - d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); - d_modules.push_back( d_i_cbqi ); + d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(this)); + d_modules.push_back(d_i_cbqi.get()); if( options::cbqiBv() ){ // if doing instantiation for BV, need the inverter class - d_bv_invert = new quantifiers::BvInverter; + d_bv_invert.reset(new quantifiers::BvInverter); } } if( options::ceGuidedInst() ){ - d_ceg_inst = new quantifiers::CegInstantiation( this, c ); - d_modules.push_back( d_ceg_inst ); + d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c)); + d_modules.push_back(d_ceg_inst.get()); //needsBuilder = true; } //finite model finding if( options::finiteModelFind() ){ if( options::fmfBound() ){ - d_bint = new quantifiers::BoundedIntegers( c, this ); - d_modules.push_back( d_bint ); + d_bint.reset(new quantifiers::BoundedIntegers(c, this)); + d_modules.push_back(d_bint.get()); } - d_model_engine = new quantifiers::ModelEngine( c, this ); - d_modules.push_back( d_model_engine ); + d_model_engine.reset(new quantifiers::ModelEngine(c, this)); + d_modules.push_back(d_model_engine.get()); //finite model finder has special ways of building the model needsBuilder = true; } if( options::quantRewriteRules() ){ - d_rr_engine = new quantifiers::RewriteEngine( c, this ); - d_modules.push_back(d_rr_engine); + d_rr_engine.reset(new quantifiers::RewriteEngine(c, this)); + d_modules.push_back(d_rr_engine.get()); } if( options::ltePartialInst() ){ - d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); - d_modules.push_back( d_lte_part_inst ); + d_lte_part_inst.reset(new quantifiers::LtePartialInst(this, c)); + d_modules.push_back(d_lte_part_inst.get()); } if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){ - d_qsplit = new quantifiers::QuantDSplit( this, c ); - d_modules.push_back( d_qsplit ); + d_qsplit.reset(new quantifiers::QuantDSplit(this, c)); + d_modules.push_back(d_qsplit.get()); } if( options::quantAntiSkolem() ){ - d_anti_skolem = new quantifiers::QuantAntiSkolem( this ); - d_modules.push_back( d_anti_skolem ); + d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this)); + d_modules.push_back(d_anti_skolem.get()); } if( options::quantAlphaEquiv() ){ - d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); + d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this)); } //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ - d_fs = new quantifiers::InstStrategyEnum(this); - d_modules.push_back( d_fs ); + d_fs.reset(new quantifiers::InstStrategyEnum(this)); + d_modules.push_back(d_fs.get()); needsRelDom = true; } if( needsRelDom ){ - d_rel_dom = new quantifiers::RelevantDomain( this ); - d_util.push_back( d_rel_dom ); + d_rel_dom.reset(new quantifiers::RelevantDomain(this)); + d_util.push_back(d_rel_dom.get()); } // if we require specialized ways of building the model @@ -252,53 +244,27 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, || options::fmfBound()) { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; - d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); - d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); + d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( + this, c, "FirstOrderModelFmc")); + d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this)); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; - d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" ); - d_builder = new quantifiers::AbsMbqiBuilder( c, this ); + d_model.reset( + new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs")); + d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; - d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); - d_builder = new quantifiers::QModelBuilderDefault( c, this ); + d_model.reset( + new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); + d_builder.reset(new quantifiers::QModelBuilderDefault(c, this)); } }else{ - d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); + d_model.reset( + new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); } } -QuantifiersEngine::~QuantifiersEngine() -{ - delete d_alpha_equiv; - delete d_builder; - delete d_qepr; - delete d_rr_engine; - delete d_bint; - delete d_model_engine; - delete d_inst_engine; - delete d_qcf; - delete d_quant_rel; - delete d_rel_dom; - delete d_bv_invert; - delete d_model; - delete d_tr_trie; - delete d_term_db; - delete d_sygus_tdb; - delete d_term_util; - delete d_eq_inference; - delete d_eq_query; - delete d_sg_gen; - delete d_ceg_inst; - delete d_lte_part_inst; - delete d_fs; - delete d_i_cbqi; - delete d_qsplit; - delete d_anti_skolem; - delete d_inst_prop; -} - -EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } +QuantifiersEngine::~QuantifiersEngine() {} context::Context* QuantifiersEngine::getSatContext() { @@ -325,6 +291,96 @@ const LogicInfo& QuantifiersEngine::getLogicInfo() const return d_te->getLogicInfo(); } +EqualityQuery* QuantifiersEngine::getEqualityQuery() const +{ + return d_eq_query.get(); +} +quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const +{ + return d_eq_inference.get(); +} +quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const +{ + return d_rel_dom.get(); +} +quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const +{ + return d_bv_invert.get(); +} +quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const +{ + return d_quant_rel.get(); +} +quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const +{ + return d_builder.get(); +} +quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const +{ + return d_qepr.get(); +} +quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const +{ + return d_model.get(); +} +quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const +{ + return d_term_db.get(); +} +quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const +{ + return d_sygus_tdb.get(); +} +quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const +{ + return d_term_util.get(); +} +quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const +{ + return d_quant_attr.get(); +} +quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const +{ + return d_instantiate.get(); +} +quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const +{ + return d_skolemize.get(); +} +quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const +{ + return d_term_enum.get(); +} +inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const +{ + return d_tr_trie.get(); +} + +quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const +{ + return d_bint.get(); +} +quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const +{ + return d_qcf.get(); +} +quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const +{ + return d_rr_engine.get(); +} +quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const +{ + return d_ceg_inst.get(); +} +quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const +{ + return d_fs.get(); +} +quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const +{ + return d_i_cbqi.get(); +} + QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); if( it==d_owner.end() ){ @@ -419,7 +475,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ // if we want to use the model's equality engine, build the model now if( d_useModelEe && !d_model->isBuilt() ){ Trace("quant-engine-debug") << "Build the model." << std::endl; - if( !d_te->getModelBuilder()->buildModel( d_model ) ){ + if (!d_te->getModelBuilder()->buildModel(d_model.get())) + { //we are done if model building was unsuccessful flushLemmas(); if( d_hasAddedLemma ){ @@ -582,9 +639,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ { // theory engine's model builder is quantifier engine's builder if it // has one - Assert(!d_builder || d_builder == d_te->getModelBuilder()); + Assert(!getModelBuilder() + || getModelBuilder() == d_te->getModelBuilder()); Trace("quant-engine-debug") << "Build model..." << std::endl; - if (!d_te->getModelBuilder()->buildModel(d_model)) + if (!d_te->getModelBuilder()->buildModel(d_model.get())) { flushLemmas(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 674954023..aabca1640 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -84,134 +84,17 @@ namespace inst { class QuantifiersEngine { - // TODO: remove these github issue #1163 - friend class quantifiers::InstantiationEngine; - friend class quantifiers::InstStrategyCbqi; - friend class quantifiers::InstStrategyCegqi; - friend class quantifiers::ModelEngine; - friend class quantifiers::RewriteEngine; - friend class quantifiers::QuantConflictFind; - friend class inst::InstMatch; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDList NodeList; typedef context::CDList BoolList; typedef context::CDHashSet NodeSet; -private: - /** reference to theory engine object */ - TheoryEngine* d_te; - /** vector of utilities for quantifiers */ - std::vector< QuantifiersUtil* > d_util; - /** vector of modules for quantifiers */ - std::vector< QuantifiersModule* > d_modules; - /** equality query class */ - quantifiers::EqualityQueryQuantifiersEngine* d_eq_query; - /** equality inference class */ - quantifiers::EqualityInference* d_eq_inference; - /** for computing relevance of quantifiers */ - quantifiers::QuantRelevance* d_quant_rel; - /** relevant domain */ - quantifiers::RelevantDomain* d_rel_dom; - /** inversion utility for BV instantiation */ - quantifiers::BvInverter * d_bv_invert; - /** alpha equivalence */ - quantifiers::AlphaEquivalence * d_alpha_equiv; - /** model builder */ - quantifiers::QModelBuilder* d_builder; - /** utility for effectively propositional logic */ - quantifiers::QuantEPR* d_qepr; - /** term database */ - quantifiers::TermDb* d_term_db; - /** sygus term database */ - quantifiers::TermDbSygus* d_sygus_tdb; - /** term utilities */ - quantifiers::TermUtil* d_term_util; - /** quantifiers attributes */ - std::unique_ptr d_quant_attr; - /** instantiate utility */ - std::unique_ptr d_instantiate; - /** skolemize utility */ - std::unique_ptr d_skolemize; - /** term enumeration utility */ - std::unique_ptr d_term_enum; - /** instantiation engine */ - quantifiers::InstantiationEngine* d_inst_engine; - /** model engine */ - quantifiers::ModelEngine* d_model_engine; - /** bounded integers utility */ - quantifiers::BoundedIntegers * d_bint; - /** Conflict find mechanism for quantifiers */ - quantifiers::QuantConflictFind* d_qcf; - /** rewrite rules utility */ - quantifiers::RewriteEngine * d_rr_engine; - /** subgoal generator */ - quantifiers::ConjectureGenerator * d_sg_gen; - /** ceg instantiation */ - quantifiers::CegInstantiation * d_ceg_inst; - /** lte partial instantiation */ - quantifiers::LtePartialInst * d_lte_part_inst; - /** full saturation */ - quantifiers::InstStrategyEnum* d_fs; - /** counterexample-based quantifier instantiation */ - quantifiers::InstStrategyCbqi * d_i_cbqi; - /** quantifiers splitting */ - quantifiers::QuantDSplit * d_qsplit; - /** quantifiers anti-skolemization */ - quantifiers::QuantAntiSkolem * d_anti_skolem; - /** quantifiers instantiation propagtor */ - quantifiers::InstPropagator * d_inst_prop; - - private: //this information is reset during check - /** current effort level */ - QuantifiersModule::QEffort d_curr_effort_level; - /** are we in conflict */ - bool d_conflict; - context::CDO d_conflict_c; - /** has added lemma this round */ - bool d_hasAddedLemma; - /** whether to use model equality engine */ - bool d_useModelEe; - private: - /** list of all quantifiers seen */ - std::map< Node, bool > d_quants; - /** quantifiers pre-registered */ - NodeSet d_quants_prereg; - /** quantifiers reduced */ - BoolMap d_quants_red; - std::map< Node, Node > d_quants_red_lem; - /** list of all lemmas produced */ - //std::map< Node, bool > d_lemmas_produced; - BoolMap d_lemmas_produced_c; - /** lemmas waiting */ - std::vector< Node > d_lemmas_waiting; - /** phase requirements waiting */ - std::map< Node, bool > d_phase_req_waiting; - /** all triggers will be stored in this trie */ - inst::TriggerTrie* d_tr_trie; - /** extended model object */ - quantifiers::FirstOrderModel* d_model; - /** inst round counters TODO: make context-dependent? */ - context::CDO< int > d_ierCounter_c; - int d_ierCounter; - int d_ierCounter_lc; - int d_ierCounterLastLc; - int d_inst_when_phase; - /** has presolve been called */ - context::CDO< bool > d_presolve; - /** presolve cache */ - NodeSet d_presolve_in; - NodeList d_presolve_cache; - BoolList d_presolve_cache_wq; - BoolList d_presolve_cache_wic; public: QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); + //---------------------- external interface /** get theory engine */ - TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query */ - EqualityQuery* getEqualityQuery(); - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; } + TheoryEngine* getTheoryEngine() const { return d_te; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); /** get default sat context for quantifiers engine */ @@ -222,42 +105,56 @@ public: Valuation& getValuation(); /** get the logic info for the quantifiers engine */ const LogicInfo& getLogicInfo() const; + //---------------------- end external interface + //---------------------- utilities + /** get equality query */ + EqualityQuery* getEqualityQuery() const; + /** get the equality inference */ + quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; } + quantifiers::RelevantDomain* getRelevantDomain() const; /** get the BV inverter utility */ - quantifiers::BvInverter * getBvInverter() { return d_bv_invert; } + quantifiers::BvInverter* getBvInverter() const; /** get quantifier relevance */ - quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; } + quantifiers::QuantRelevance* getQuantifierRelevance() const; /** get the model builder */ - quantifiers::QModelBuilder* getModelBuilder() { return d_builder; } + quantifiers::QModelBuilder* getModelBuilder() const; /** get utility for EPR */ - quantifiers::QuantEPR* getQuantEPR() { return d_qepr; } - public: // modules - /** get instantiation engine */ - quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } - /** get model engine */ - quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } + quantifiers::QuantEPR* getQuantEPR() const; + /** get model */ + quantifiers::FirstOrderModel* getModel() const; + /** get term database */ + quantifiers::TermDb* getTermDatabase() const; + /** get term database sygus */ + quantifiers::TermDbSygus* getTermDatabaseSygus() const; + /** get term utilities */ + quantifiers::TermUtil* getTermUtil() const; + /** get quantifiers attributes */ + quantifiers::QuantAttributes* getQuantAttributes() const; + /** get instantiate utility */ + quantifiers::Instantiate* getInstantiate() const; + /** get skolemize utility */ + quantifiers::Skolemize* getSkolemize() const; + /** get term enumeration utility */ + quantifiers::TermEnumeration* getTermEnumeration() const; + /** get trigger database */ + inst::TriggerTrie* getTriggerDatabase() const; + //---------------------- end utilities + //---------------------- modules /** get bounded integers utility */ - quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } + quantifiers::BoundedIntegers* getBoundedIntegers() const; /** Conflict find mechanism for quantifiers */ - quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; } + quantifiers::QuantConflictFind* getConflictFind() const; /** rewrite rules utility */ - quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; } - /** subgoal generator */ - quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; } + quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ - quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } - /** local theory ext partial inst */ - quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } + quantifiers::CegInstantiation* getCegInstantiation() const; /** get full saturation */ - quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; } + quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ - quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; } - /** get quantifiers splitting */ - quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; } - /** get quantifiers anti-skolemization */ - quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; } -private: + quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const; + //---------------------- end modules + private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; std::map< Node, int > d_owner_priority; @@ -331,29 +228,6 @@ public: /** get user pat mode */ quantifiers::UserPatMode getInstUserPatMode(); public: - /** get model */ - quantifiers::FirstOrderModel* getModel() { return d_model; } - /** get term database */ - quantifiers::TermDb* getTermDatabase() { return d_term_db; } - /** get term database sygus */ - quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; } - /** get term utilities */ - quantifiers::TermUtil* getTermUtil() { return d_term_util; } - /** get quantifiers attributes */ - quantifiers::QuantAttributes* getQuantAttributes() { - return d_quant_attr.get(); - } - /** get instantiate utility */ - quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); } - /** get skolemize utility */ - quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } - /** get term enumeration utility */ - quantifiers::TermEnumeration* getTermEnumeration() - { - return d_term_enum.get(); - } - /** get trigger database */ - inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ @@ -439,6 +313,117 @@ public: ~Statistics(); };/* class QuantifiersEngine::Statistics */ Statistics d_statistics; + + private: + /** reference to theory engine object */ + TheoryEngine* d_te; + /** vector of utilities for quantifiers */ + std::vector d_util; + /** vector of modules for quantifiers */ + std::vector d_modules; + //------------- quantifiers utilities + /** equality query class */ + std::unique_ptr d_eq_query; + /** equality inference class */ + std::unique_ptr d_eq_inference; + /** quantifiers instantiation propagtor */ + std::unique_ptr d_inst_prop; + /** all triggers will be stored in this trie */ + std::unique_ptr d_tr_trie; + /** extended model object */ + std::unique_ptr d_model; + /** for computing relevance of quantifiers */ + std::unique_ptr d_quant_rel; + /** relevant domain */ + std::unique_ptr d_rel_dom; + /** inversion utility for BV instantiation */ + std::unique_ptr d_bv_invert; + /** model builder */ + std::unique_ptr d_builder; + /** utility for effectively propositional logic */ + std::unique_ptr d_qepr; + /** term utilities */ + std::unique_ptr d_term_util; + /** term database */ + std::unique_ptr d_term_db; + /** sygus term database */ + std::unique_ptr d_sygus_tdb; + /** quantifiers attributes */ + std::unique_ptr d_quant_attr; + /** instantiate utility */ + std::unique_ptr d_instantiate; + /** skolemize utility */ + std::unique_ptr d_skolemize; + /** term enumeration utility */ + std::unique_ptr d_term_enum; + //------------- end quantifiers utilities + //------------- quantifiers modules + /** alpha equivalence */ + std::unique_ptr d_alpha_equiv; + /** instantiation engine */ + std::unique_ptr d_inst_engine; + /** model engine */ + std::unique_ptr d_model_engine; + /** bounded integers utility */ + std::unique_ptr d_bint; + /** Conflict find mechanism for quantifiers */ + std::unique_ptr d_qcf; + /** rewrite rules utility */ + std::unique_ptr d_rr_engine; + /** subgoal generator */ + std::unique_ptr d_sg_gen; + /** ceg instantiation */ + std::unique_ptr d_ceg_inst; + /** lte partial instantiation */ + std::unique_ptr d_lte_part_inst; + /** full saturation */ + std::unique_ptr d_fs; + /** counterexample-based quantifier instantiation */ + std::unique_ptr d_i_cbqi; + /** quantifiers splitting */ + std::unique_ptr d_qsplit; + /** quantifiers anti-skolemization */ + std::unique_ptr d_anti_skolem; + //------------- end quantifiers modules + //------------- temporary information during check + /** current effort level */ + QuantifiersModule::QEffort d_curr_effort_level; + /** are we in conflict */ + bool d_conflict; + context::CDO d_conflict_c; + /** has added lemma this round */ + bool d_hasAddedLemma; + /** whether to use model equality engine */ + bool d_useModelEe; + //------------- end temporary information during check + private: + /** list of all quantifiers seen */ + std::map d_quants; + /** quantifiers pre-registered */ + NodeSet d_quants_prereg; + /** quantifiers reduced */ + BoolMap d_quants_red; + std::map d_quants_red_lem; + /** list of all lemmas produced */ + // std::map< Node, bool > d_lemmas_produced; + BoolMap d_lemmas_produced_c; + /** lemmas waiting */ + std::vector d_lemmas_waiting; + /** phase requirements waiting */ + std::map d_phase_req_waiting; + /** inst round counters TODO: make context-dependent? */ + context::CDO d_ierCounter_c; + int d_ierCounter; + int d_ierCounter_lc; + int d_ierCounterLastLc; + int d_inst_when_phase; + /** has presolve been called */ + context::CDO d_presolve; + /** presolve cache */ + NodeSet d_presolve_in; + NodeList d_presolve_cache; + BoolList d_presolve_cache_wq; + BoolList d_presolve_cache_wic; };/* class QuantifiersEngine */ }/* CVC4::theory namespace */ -- 2.30.2