From d1ef66608567252526f1a5e1f675f08d342cc343 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 8 Aug 2019 16:49:08 -0500 Subject: [PATCH] Reorganize includes for quantifiers engine (#3169) --- .../quantifiers/quantifiers_attributes.cpp | 22 +- src/theory/quantifiers_engine.cpp | 329 +++++++++++------- src/theory/quantifiers_engine.h | 110 ++---- 3 files changed, 256 insertions(+), 205 deletions(-) diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index d93de6a54..87d6ec0c3 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -213,28 +213,18 @@ bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) { void QuantAttributes::computeAttributes( Node q ) { computeQuantAttributes( q, d_qattr[q] ); - if( !d_qattr[q].d_rr.isNull() ){ - if( d_quantEngine->getRewriteEngine()==NULL ){ - Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; - } - //set rewrite engine as owner - d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 ); - } - if( d_qattr[q].isFunDef() ){ - Node f = d_qattr[q].d_fundef_f; + QAttributes& qa = d_qattr[q]; + if (qa.isFunDef()) + { + Node f = qa.d_fundef_f; if( d_fun_defs.find( f )!=d_fun_defs.end() ){ Message() << "Cannot define function " << f << " more than once." << std::endl; AlwaysAssert(false); } d_fun_defs[f] = true; } - if( d_qattr[q].d_sygus ){ - if (d_quantEngine->getSynthEngine() == nullptr) - { - Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; - } - d_quantEngine->setOwner(q, d_quantEngine->getSynthEngine(), 2); - } + // set ownership of quantified formula q based on the computed attributes + d_quantEngine->setOwner(q, qa); } void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0af120f5a..f0b0c31df 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -17,16 +17,169 @@ #include "options/quantifiers_options.h" #include "options/uf_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/alpha_equivalence.h" +#include "theory/quantifiers/anti_skolem.h" +#include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" +#include "theory/quantifiers/fmf/full_model_check.h" +#include "theory/quantifiers/fmf/model_engine.h" +#include "theory/quantifiers/inst_propagator.h" +#include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/local_theory_ext.h" +#include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers/quant_split.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::inst; + +namespace CVC4 { +namespace theory { + +class QuantifiersEnginePrivate +{ + public: + QuantifiersEnginePrivate() + : d_inst_prop(nullptr), + 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_synth_e(nullptr), + d_lte_part_inst(nullptr), + d_fs(nullptr), + d_i_cbqi(nullptr), + d_qsplit(nullptr), + d_anti_skolem(nullptr) + { + } + ~QuantifiersEnginePrivate() {} + //------------------------------ private quantifier utilities + /** quantifiers instantiation propagator */ + std::unique_ptr d_inst_prop; + //------------------------------ end private quantifier 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_synth_e; + /** 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 + /** initialize + * + * This constructs the above modules based on the current options. It adds + * a pointer to each module it constructs to modules. This method sets + * needsBuilder to true if we require a strategy-specific model builder + * utility, and needsRelDom to true if we require the relevant domain + * utility. + */ + void initialize(QuantifiersEngine* qe, + context::Context* c, + std::vector& modules, + bool& needsBuilder, + bool& needsRelDom) + { + // add quantifiers modules + if (options::quantConflictFind() || options::quantRewriteRules()) + { + d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); + modules.push_back(d_qcf.get()); + } + if (options::conjectureGen()) + { + d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c)); + modules.push_back(d_sg_gen.get()); + } + if (!options::finiteModelFind() || options::fmfInstEngine()) + { + d_inst_engine.reset(new quantifiers::InstantiationEngine(qe)); + modules.push_back(d_inst_engine.get()); + } + if (options::cbqi()) + { + d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); + modules.push_back(d_i_cbqi.get()); + } + if (options::ceGuidedInst()) + { + d_synth_e.reset(new quantifiers::SynthEngine(qe, c)); + modules.push_back(d_synth_e.get()); + } + // finite model finding + if (options::finiteModelFind()) + { + if (options::fmfBound()) + { + d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); + modules.push_back(d_bint.get()); + } + d_model_engine.reset(new quantifiers::ModelEngine(c, qe)); + 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.reset(new quantifiers::RewriteEngine(c, qe)); + modules.push_back(d_rr_engine.get()); + } + if (options::ltePartialInst()) + { + d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c)); + modules.push_back(d_lte_part_inst.get()); + } + if (options::quantDynamicSplit() != quantifiers::QUANT_DSPLIT_MODE_NONE) + { + d_qsplit.reset(new quantifiers::QuantDSplit(qe, c)); + modules.push_back(d_qsplit.get()); + } + if (options::quantAntiSkolem()) + { + d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe)); + modules.push_back(d_anti_skolem.get()); + } + if (options::quantAlphaEquiv()) + { + d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe)); + } + // full saturation : instantiate from relevant domain, then arbitrary terms + if (options::fullSaturateQuant() || options::fullSaturateInterleave()) + { + d_fs.reset(new quantifiers::InstStrategyEnum(qe)); + modules.push_back(d_fs.get()); + needsRelDom = true; + } + } +}; QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, @@ -34,7 +187,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, : 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), @@ -50,19 +202,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, 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_synth_e(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), @@ -78,6 +217,9 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_presolve_cache_wq(u), d_presolve_cache_wic(u) { + // initialize the private utility + d_private.reset(new QuantifiersEnginePrivate); + //---- utilities d_util.push_back(d_eq_query.get()); // term util must come before the other utilities @@ -90,9 +232,9 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, if( options::instPropagate() ){ // notice that this option is incompatible with options::qcfAllConflict() - d_inst_prop.reset(new quantifiers::InstPropagator(this)); - d_util.push_back(d_inst_prop.get()); - d_instantiate->addNotify(d_inst_prop->getInstantiationNotify()); + d_private->d_inst_prop.reset(new quantifiers::InstPropagator(this)); + d_util.push_back(d_private->d_inst_prop.get()); + d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify()); } if( options::inferArithTriggerEq() ){ @@ -120,6 +262,12 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Assert( !options::incrementalSolving() ); d_qepr.reset(new quantifiers::QuantEPR); } + + if (options::cbqi() && options::cbqiBv()) + { + // if doing instantiation for BV, need the inverter class + d_bv_invert.reset(new quantifiers::BvInverter); + } //---- end utilities //allow theory combination to go first, once initially @@ -131,69 +279,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, bool needsBuilder = false; bool needsRelDom = false; - //add quantifiers modules - if( options::quantConflictFind() || options::quantRewriteRules() ){ - d_qcf.reset(new quantifiers::QuantConflictFind(this, c)); - d_modules.push_back(d_qcf.get()); - } - if( options::conjectureGen() ){ - 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.reset(new quantifiers::InstantiationEngine(this)); - d_modules.push_back(d_inst_engine.get()); - } - if( options::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.reset(new quantifiers::BvInverter); - } - } - if( options::ceGuidedInst() ){ - d_synth_e.reset(new quantifiers::SynthEngine(this, c)); - d_modules.push_back(d_synth_e.get()); - //needsBuilder = true; - } - //finite model finding - if( options::finiteModelFind() ){ - if( options::fmfBound() ){ - d_bint.reset(new quantifiers::BoundedIntegers(c, this)); - d_modules.push_back(d_bint.get()); - } - 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.reset(new quantifiers::RewriteEngine(c, this)); - d_modules.push_back(d_rr_engine.get()); - } - if( options::ltePartialInst() ){ - 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.reset(new quantifiers::QuantDSplit(this, c)); - d_modules.push_back(d_qsplit.get()); - } - if( options::quantAntiSkolem() ){ - d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this)); - d_modules.push_back(d_anti_skolem.get()); - } - if( options::quantAlphaEquiv() ){ - d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this)); - } - //full saturation : instantiate from relevant domain, then arbitrary terms - if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ - d_fs.reset(new quantifiers::InstStrategyEnum(this)); - d_modules.push_back(d_fs.get()); - needsRelDom = true; - } - + d_private->initialize(this, c, d_modules, needsBuilder, needsRelDom); + if( needsRelDom ){ d_rel_dom.reset(new quantifiers::RelevantDomain(this)); d_util.push_back(d_rel_dom.get()); @@ -319,27 +406,19 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const { - return d_bint.get(); + return d_private->d_bint.get(); } quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const { - return d_qcf.get(); -} -quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const -{ - return d_rr_engine.get(); + return d_private->d_qcf.get(); } quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { - return d_synth_e.get(); -} -quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const -{ - return d_fs.get(); + return d_private->d_synth_e.get(); } quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() const { - return d_i_cbqi.get(); + return d_private->d_i_cbqi.get(); } QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { @@ -365,6 +444,30 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) } } +void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) +{ + if (!qa.d_rr.isNull()) + { + if (d_private->d_rr_engine.get() == nullptr) + { + Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " + << q << std::endl; + } + // set rewrite engine as owner + setOwner(q, d_private->d_rr_engine.get(), 2); + } + if (qa.d_sygus) + { + if (d_private->d_synth_e.get() == nullptr) + { + Trace("quant-warn") << "WARNING : synth engine is null, and we have : " + << q << std::endl; + } + // set synth engine as owner + setOwner(q, d_private->d_synth_e.get(), 2); + } +} + bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { QuantifiersModule * mo = getOwner( q ); return mo==m || mo==NULL; @@ -758,10 +861,11 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { Node lem; std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q ); if( itr==d_quants_red_lem.end() ){ - if( d_alpha_equiv ){ + if (d_private->d_alpha_equiv) + { Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; //add equivalence with another quantified formula - lem = d_alpha_equiv->reduceQuantifier( q ); + lem = d_private->d_alpha_equiv->reduceQuantifier(q); if( !lem.isNull() ){ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; ++(d_statistics.d_red_alpha_equiv); @@ -976,18 +1080,6 @@ bool QuantifiersEngine::removeLemma( Node lem ) { void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } - -bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) { - if( d_qepr ){ - Assert( !options::incrementalSolving() ); - if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){ - Node lem = d_qepr->mkEPRAxiom( tn ); - Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl; - getOutputChannel().lemma( lem ); - } - } - return false; -} void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); @@ -1103,9 +1195,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } void QuantifiersEngine::printSynthSolution( std::ostream& out ) { - if (d_synth_e) + if (d_private->d_synth_e) { - d_synth_e->printSynthSolution(out); + d_private->d_synth_e->printSynthSolution(out); }else{ out << "Internal error : module for synth solution not found." << std::endl; } @@ -1194,16 +1286,17 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr); } -eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ +eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const +{ return d_te->getMasterEqualityEngine(); } -eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() { +eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const +{ if( d_useModelEe ){ return d_model->getEqualityEngine(); - }else{ - return d_te->getMasterEqualityEngine(); } + return d_te->getMasterEqualityEngine(); } Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ @@ -1216,7 +1309,7 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ void QuantifiersEngine::getSynthSolutions(std::map& sol_map) { - d_synth_e->getSynthSolutions(sol_map); + d_private->d_synth_e->getSynthSolutions(sol_map); } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { @@ -1255,3 +1348,5 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { } } +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e0669c0d4..7e5fe9102 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -17,53 +17,33 @@ #ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H #define CVC4__THEORY__QUANTIFIERS_ENGINE_H -#include #include -#include #include #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/term_canonize.h" -#include "options/quantifiers_modes.h" -#include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" -#include "theory/quantifiers/conjecture_generator.h" -#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" -#include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/bounded_integers.h" -#include "theory/quantifiers/fmf/full_model_check.h" -#include "theory/quantifiers/fmf/model_engine.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/inst_propagator.h" -#include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_relevance.h" -#include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/relevant_domain.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/theory.h" -#include "util/hash.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -72,6 +52,8 @@ class TheoryEngine; namespace theory { +class QuantifiersEnginePrivate; + // TODO: organize this more/review this, github issue #1163 class QuantifiersEngine { typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; @@ -97,16 +79,12 @@ public: const LogicInfo& getLogicInfo() const; //---------------------- end external interface //---------------------- utilities + /** get the master equality engine */ + eq::EqualityEngine* getMasterEqualityEngine() const; + /** get the active equality engine */ + eq::EqualityEngine* getActiveEqualityEngine() const; /** get equality query */ EqualityQuery* getEqualityQuery() const; - /** get the equality inference */ - quantifiers::EqualityInference* getEqualityInference() const; - /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() const; - /** get the BV inverter utility */ - quantifiers::BvInverter* getBvInverter() const; - /** get quantifier relevance */ - quantifiers::QuantRelevance* getQuantifierRelevance() const; /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; /** get utility for EPR */ @@ -132,29 +110,49 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities - //---------------------- modules + //---------------------- utilities (TODO move these utilities #1163) + /** get the equality inference */ + quantifiers::EqualityInference* getEqualityInference() const; + /** get relevant domain */ + quantifiers::RelevantDomain* getRelevantDomain() const; + /** get the BV inverter utility */ + quantifiers::BvInverter* getBvInverter() const; + /** get quantifier relevance */ + quantifiers::QuantRelevance* getQuantifierRelevance() const; + //---------------------- end utilities + //---------------------- modules (TODO remove these #1163) /** get bounded integers utility */ quantifiers::BoundedIntegers* getBoundedIntegers() const; /** Conflict find mechanism for quantifiers */ quantifiers::QuantConflictFind* getConflictFind() const; - /** rewrite rules utility */ - quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ quantifiers::SynthEngine* getSynthEngine() const; - /** get full saturation */ - quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const; //---------------------- end modules private: - /** owner of quantified formulas */ + /** + * Maps quantified formulas to the module that owns them, if any module has + * specifically taken ownership of it. + */ std::map< Node, QuantifiersModule * > d_owner; + /** + * The priority value associated with the ownership of quantified formulas + * in the domain of the above map, where higher values take higher + * precendence. + */ std::map< Node, int > d_owner_priority; public: /** get owner */ QuantifiersModule * getOwner( Node q ); - /** set owner */ + /** + * Set owner of quantified formula q to module m with given priority. If + * the quantified formula has previously been assigned an owner with + * lower priority, that owner is overwritten. + */ void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); + /** set owner of quantified formula q based on its attributes qa. */ + void setOwner(Node q, quantifiers::QAttributes& qa); /** considers */ bool hasOwnership( Node q, QuantifiersModule * m = NULL ); /** is finite bound */ @@ -199,8 +197,6 @@ public: bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); - /** add EPR axiom */ - bool addEPRAxiom( TypeNode tn ); /** mark relevant quantified formula, this will indicate it should be checked before the others */ void markRelevant( Node q ); /** has added lemma */ @@ -225,10 +221,6 @@ public: void eqNotifyPreMerge(TNode t1, TNode t2); void eqNotifyPostMerge(TNode t1, TNode t2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine(); - /** get the active equality engine */ - eq::EqualityEngine* getActiveEqualityEngine(); /** use model equality engine */ bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ @@ -316,8 +308,6 @@ public: 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 */ @@ -349,34 +339,10 @@ public: /** 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_synth_e; - /** 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 + /** + * The private utility, which contains all of the quantifiers modules. + */ + std::unique_ptr d_private; //------------- temporary information during check /** current effort level */ QuantifiersModule::QEffort d_curr_effort_level; -- 2.30.2