diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-26 17:52:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-26 17:52:37 -0700 |
commit | 3aafd4a2ced87f0fd82ebe5279b73c84552502d5 (patch) | |
tree | 2e96b3cf82d4a1d2c74bb5a6b3227d5afb3716d1 /src/theory/quantifiers_engine.cpp | |
parent | 9ba1854be7d798a899a2b46c2707d376938c5d18 (diff) | |
parent | 923abd7000a2ab6e3c0776c59d159bdc3a4d9a52 (diff) |
Merge branch 'master' into splitEqRew
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 510 |
1 files changed, 277 insertions, 233 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f86d82874..e399af71d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -17,90 +17,190 @@ #include "options/quantifiers_options.h" #include "options/uf_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/datatypes/theory_datatypes.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_propagator.h" #include "theory/quantifiers/inst_strategy_enumerative.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/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_canonize.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_util.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/theory_uf_strong_solver.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_rel_dom(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<quantifiers::InstPropagator> d_inst_prop; + /** relevant domain */ + std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; + //------------------------------ end private quantifier utilities + //------------------------------ quantifiers modules + /** alpha equivalence */ + std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv; + /** instantiation engine */ + std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine; + /** model engine */ + std::unique_ptr<quantifiers::ModelEngine> d_model_engine; + /** bounded integers utility */ + std::unique_ptr<quantifiers::BoundedIntegers> d_bint; + /** Conflict find mechanism for quantifiers */ + std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; + /** rewrite rules utility */ + std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; + /** subgoal generator */ + std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; + /** ceg instantiation */ + std::unique_ptr<quantifiers::SynthEngine> d_synth_e; + /** lte partial instantiation */ + std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst; + /** full saturation */ + std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; + /** counterexample-based quantifier instantiation */ + std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi; + /** quantifiers splitting */ + std::unique_ptr<quantifiers::QuantDSplit> d_qsplit; + /** quantifiers anti-skolemization */ + std::unique_ptr<quantifiers::QuantAntiSkolem> 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. + */ + void initialize(QuantifiersEngine* qe, + context::Context* c, + std::vector<QuantifiersModule*>& modules, + bool& needsBuilder) + { + // 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()); + qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); + } + if (options::ceGuidedInst()) + { + d_synth_e.reset(new quantifiers::SynthEngine(qe, c)); + modules.push_back(d_synth_e.get()); + } + // finite model finding + if (options::fmfBound()) + { + d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); + modules.push_back(d_bint.get()); + } + if (options::finiteModelFind() || options::fmfBound()) + { + 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, d_qcf.get())); + 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_rel_dom.reset(new quantifiers::RelevantDomain(qe)); + d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get())); + modules.push_back(d_fs.get()); + } + } +}; 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_canon(new quantifiers::TermCanonize), + d_term_canon(new expr::TermCanonize), 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_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), @@ -116,6 +216,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 @@ -128,14 +231,11 @@ 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() ){ - d_eq_inference.reset(new quantifiers::EqualityInference(c, false)); - } d_util.push_back(d_instantiate.get()); @@ -149,11 +249,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; - if( options::relevantTriggers() ){ - d_quant_rel.reset(new quantifiers::QuantRelevance); - d_util.push_back(d_quant_rel.get()); - } - if( options::quantEpr() ){ Assert( !options::incrementalSolving() ); d_qepr.reset(new quantifiers::QuantEPR); @@ -168,75 +263,13 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); 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; - } - - if( needsRelDom ){ - d_rel_dom.reset(new quantifiers::RelevantDomain(this)); - d_util.push_back(d_rel_dom.get()); + d_private->initialize(this, c, d_modules, needsBuilder); + + if (d_private->d_rel_dom.get()) + { + d_util.push_back(d_private->d_rel_dom.get()); } - + // if we require specialized ways of building the model if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; @@ -290,22 +323,6 @@ 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(); @@ -330,7 +347,7 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const { return d_term_util.get(); } -quantifiers::TermCanonize* QuantifiersEngine::getTermCanonize() const +expr::TermCanonize* QuantifiersEngine::getTermCanonize() const { return d_term_canon.get(); } @@ -355,31 +372,6 @@ 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::SynthEngine* QuantifiersEngine::getSynthEngine() const -{ - return d_synth_e.get(); -} -quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const -{ - return d_fs.get(); -} -quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() 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() ){ @@ -403,24 +395,95 @@ 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; } -bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { - if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){ +bool QuantifiersEngine::isFiniteBound(Node q, Node v) const +{ + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi && bi->isBound(q, v)) + { return true; - }else{ - TypeNode tn = v.getType(); - if( tn.isSort() && options::finiteModelFind() ){ - return true; - } - else if (d_term_enum->mayComplete(tn)) + } + TypeNode tn = v.getType(); + if (tn.isSort() && options::finiteModelFind()) + { + return true; + } + else if (d_term_enum->mayComplete(tn)) + { + return true; + } + return false; +} + +BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const +{ + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi) + { + return bi->getBoundVarType(q, v); + } + return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE; +} + +void QuantifiersEngine::getBoundVarIndices(Node q, + std::vector<unsigned>& indices) const +{ + Assert(indices.empty()); + // we take the bounded variables first + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi) + { + bi->getBoundVarIndices(q, indices); + } + // then get the remaining ones + for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) + { + if (std::find(indices.begin(), indices.end(), i) == indices.end()) { - return true; + indices.push_back(i); } } +} + +bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, + bool initial, + Node q, + Node v, + std::vector<Node>& elements) const +{ + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi) + { + return bi->getBoundElements(rsi, initial, q, v, elements); + } return false; } @@ -446,24 +509,32 @@ void QuantifiersEngine::ppNotifyAssertions( Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr != NULL) << std::endl; - if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) || - d_qepr != NULL) { - for (unsigned i = 0; i < assertions.size(); i++) { - if (options::instLevelInputOnly() && options::instMaxLevel() != -1) { - quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i], - 0); - } - if (d_qepr != NULL) { - d_qepr->registerAssertion(assertions[i]); - } + if (options::instLevelInputOnly() && options::instMaxLevel() != -1) + { + for (const Node& a : assertions) + { + quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0); } - if (d_qepr != NULL) { - // must handle sources of other new constants e.g. separation logic - // FIXME: cleanup - sep::TheorySep* theory_sep = - static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP)); - theory_sep->initializeBounds(); - d_qepr->finishInit(); + } + if (d_qepr != NULL) + { + for (const Node& a : assertions) + { + d_qepr->registerAssertion(a); + } + // must handle sources of other new constants e.g. separation logic + // FIXME (as part of project 3) : cleanup + sep::TheorySep* theory_sep = + static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP)); + theory_sep->initializeBounds(); + d_qepr->finishInit(); + } + if (options::ceGuidedInst()) + { + quantifiers::SynthEngine* sye = d_private->d_synth_e.get(); + for (const Node& a : assertions) + { + sye->preregisterAssertion(a); } } } @@ -796,10 +867,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); @@ -955,25 +1027,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within void QuantifiersEngine::eqNotifyNewClass(TNode t) { addTermToDatabase( t ); - if( d_eq_inference ){ - d_eq_inference->eqNotifyNewClass( t ); - } -} - -void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) { - if( d_eq_inference ){ - d_eq_inference->eqNotifyMerge( t1, t2 ); - } -} - -void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) { - -} - -void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - //if( d_qcf ){ - // d_qcf->assertDisequal( t1, t2 ); - //} } bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ @@ -1014,18 +1067,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 ); @@ -1141,9 +1182,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; } @@ -1232,16 +1273,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 ){ @@ -1254,7 +1296,7 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map) { - d_synth_e->getSynthSolutions(sol_map); + d_private->d_synth_e->getSynthSolutions(sol_map); } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { @@ -1293,3 +1335,5 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { } } +} // namespace theory +} // namespace CVC4 |