diff options
38 files changed, 315 insertions, 473 deletions
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 5e242659f..71eac49a0 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -77,21 +77,11 @@ const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const return d_eemanager->getEeTheoryInfo(tid); } -eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine() -{ - return d_eemanager->getCoreEqualityEngine(); -} - void CombinationEngine::resetModel() { d_mmanager->resetModel(); } void CombinationEngine::postProcessModel(bool incomplete) { - // should have a consistent core equality engine - eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine(); - if (mee != nullptr) - { - AlwaysAssert(mee->consistent()); - } + d_eemanager->notifyModel(incomplete); // postprocess with the model d_mmanager->postProcessModel(incomplete); } diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 4413da603..765a49d68 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -49,15 +49,8 @@ class CombinationEngine /** Finish initialization */ void finishInit(); - //-------------------------- equality engine /** Get equality engine theory information for theory with identifier tid. */ const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const; - /** - * Get the "core" equality engine. This is the equality engine that - * quantifiers should use. - */ - eq::EqualityEngine* getCoreEqualityEngine(); - //-------------------------- end equality engine //-------------------------- model /** * Reset the model maintained by this class. This resets all local information diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h index 6e40ceb7b..5b8dc3b93 100644 --- a/src/theory/ee_manager.h +++ b/src/theory/ee_manager.h @@ -73,17 +73,17 @@ class EqEngineManager * Get the equality engine theory information for theory with the given id. */ const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const; - /** - * Get the core equality engine, which is the equality engine that the - * quantifiers engine should use. This corresponds to the master equality - * engine if eeMode is distributed, or the central equality engine if eeMode - * is central. - */ - virtual eq::EqualityEngine* getCoreEqualityEngine() = 0; /** Allocate equality engine that is context-dependent on c with info esi */ eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi, context::Context* c); + /** + * Notify this class that we are about to terminate with a model. This method + * is for debugging only. + * + * @param incomplete Whether we are answering "unknown" instead of "sat". + */ + virtual void notifyModel(bool incomplete) {} protected: /** Reference to the theory engine */ diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 3fb5fc0ce..496b04a52 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -47,6 +47,19 @@ void EqEngineManagerDistributed::initializeTheories() Unhandled() << "Expected shared solver to use equality engine"; } + const LogicInfo& logicInfo = d_te.getLogicInfo(); + if (logicInfo.isQuantified()) + { + // construct the master equality engine + Assert(d_masterEqualityEngine == nullptr); + QuantifiersEngine* qe = d_te.getQuantifiersEngine(); + Assert(qe != nullptr); + d_masterEENotify.reset(new MasterNotifyClass(qe)); + d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(), + d_te.getSatContext(), + "theory::master", + false)); + } // allocate equality engines per theory for (TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; @@ -63,48 +76,34 @@ void EqEngineManagerDistributed::initializeTheories() EeSetupInfo esi; if (!t->needsEqualityEngine(esi)) { - // theory said it doesn't need an equality engine, skip + // the theory said it doesn't need an equality engine, skip + continue; + } + if (esi.d_useMaster) + { + // the theory said it wants to use the master equality engine + eet.d_usedEe = d_masterEqualityEngine.get(); continue; } // allocate the equality engine eet.d_allocEe.reset(allocateEqualityEngine(esi, c)); // the theory uses the equality engine eet.d_usedEe = eet.d_allocEe.get(); + // if there is a master equality engine + if (d_masterEqualityEngine != nullptr) + { + // set the master equality engine of the theory's equality engine + eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine.get()); + } } +} - const LogicInfo& logicInfo = d_te.getLogicInfo(); - if (logicInfo.isQuantified()) +void EqEngineManagerDistributed::notifyModel(bool incomplete) +{ + // should have a consistent master equality engine + if (d_masterEqualityEngine.get() != nullptr) { - // construct the master equality engine - Assert(d_masterEqualityEngine == nullptr); - QuantifiersEngine* qe = d_te.getQuantifiersEngine(); - Assert(qe != nullptr); - d_masterEENotify.reset(new MasterNotifyClass(qe)); - d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(), - d_te.getSatContext(), - "theory::master", - false)); - - for (TheoryId theoryId = theory::THEORY_FIRST; - theoryId != theory::THEORY_LAST; - ++theoryId) - { - Theory* t = d_te.theoryOf(theoryId); - if (t == nullptr) - { - // theory not active, skip - continue; - } - EeTheoryInfo& eet = d_einfo[theoryId]; - // Get the allocated equality engine, and connect it to the master - // equality engine. - eq::EqualityEngine* eeAlloc = eet.d_allocEe.get(); - if (eeAlloc != nullptr) - { - // set the master equality engine of the theory's equality engine - eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get()); - } - } + AlwaysAssert(d_masterEqualityEngine->consistent()); } } @@ -114,10 +113,5 @@ void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t) d_quantEngine->eqNotifyNewClass(t); } -eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine() -{ - return d_masterEqualityEngine.get(); -} - } // namespace theory } // namespace CVC4 diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index c7c1e7f4c..9578706d9 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -52,8 +52,9 @@ class EqEngineManagerDistributed : public EqEngineManager * per theories and connects them to a master equality engine. */ void initializeTheories() override; - /** get the core equality engine */ - eq::EqualityEngine* getCoreEqualityEngine() override; + /** Notify model */ + void notifyModel(bool incomplete) override; + private: /** notify class for master equality engine */ class MasterNotifyClass : public theory::eq::EqualityEngineNotify diff --git a/src/theory/ee_setup_info.h b/src/theory/ee_setup_info.h index 78f2f211e..7770cfc49 100644 --- a/src/theory/ee_setup_info.h +++ b/src/theory/ee_setup_info.h @@ -37,13 +37,21 @@ class EqualityEngineNotify; */ struct EeSetupInfo { - EeSetupInfo() : d_notify(nullptr), d_constantsAreTriggers(true) {} + EeSetupInfo() + : d_notify(nullptr), d_constantsAreTriggers(true), d_useMaster(false) + { + } /** The notification class of the theory */ eq::EqualityEngineNotify* d_notify; /** The name of the equality engine */ std::string d_name; /** Constants are triggers */ bool d_constantsAreTriggers; + /** + * Whether we want our state to use the master equality engine. This should + * be true exclusively for the theory of quantifiers. + */ + bool d_useMaster; }; } // namespace theory diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index a8632c02f..411ab36b9 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -663,9 +663,10 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); Node pvr = pv; - if (d_qe->getMasterEqualityEngine()->hasTerm(pv)) + eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); + if (ee->hasTerm(pv)) { - pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv); + pvr = ee->getRepresentative(pv); } Trace("cegqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " @@ -1306,7 +1307,7 @@ void CegInstantiator::processAssertions() { d_curr_type_eqc.clear(); // must use master equality engine to avoid value instantiations - eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); //for each variable for( unsigned i=0; i<d_vars.size(); i++ ){ diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 0fd5249e8..cdee268d6 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -59,7 +59,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) if( isExcludedEqc( eqc ) ){ d_mode = cand_term_none; }else{ - eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); + eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); if( ee->hasTerm( eqc ) ){ TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op); if( tat ){ @@ -93,6 +93,7 @@ Node CandidateGeneratorQE::getNextCandidate(){ Node CandidateGeneratorQE::getNextCandidateInternal() { if( d_mode==cand_term_db ){ + eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; //get next candidate term in the uf term database while( d_term_iter<d_term_iter_limit ){ @@ -103,7 +104,7 @@ Node CandidateGeneratorQE::getNextCandidateInternal() if( d_exclude_eqc.empty() ){ return n; }else{ - Node r = d_qe->getEqualityQuery()->getRepresentative( n ); + Node r = ee->getRepresentative(n); if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ Debug("cand-gen-qe") << "...returning " << n << std::endl; return n; @@ -143,8 +144,9 @@ CandidateGenerator( qe ), d_match_pattern( mpat ){ } void CandidateGeneratorQELitDeq::reset( Node eqc ){ - Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) ); - d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); + eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); + Node falset = NodeManager::currentNM()->mkConst(false); + d_eqc_false = eq::EqClassIterator(falset, ee); } Node CandidateGeneratorQELitDeq::getNextCandidate(){ @@ -177,7 +179,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp } void CandidateGeneratorQEAll::reset( Node eqc ) { - d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine()); d_firstTime = true; } diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index cdfb9c85c..6d13ef2ee 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -231,7 +231,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); - EqualityQuery* eq = d_quantEngine->getEqualityQuery(); + quantifiers::QuantifiersState& qs = d_quantEngine->getState(); for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -283,10 +283,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) } else if (!itf->second.isNull()) { - if (!eq->areEqual(itf->second, args[k])) + if (!qs.areEqual(itf->second, args[k])) { if (!d_quantEngine->getTermDatabase()->isEntailed( - itf->second.eqNode(args[k]), true, eq)) + itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); } @@ -318,7 +318,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) { if (!itf->second.isNull()) { - Node r = eq->getRepresentative(itf->second); + Node r = qs.getRepresentative(itf->second); std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r); if (itfr != arg_to_rep.end()) { diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 63731c444..4cdb207f3 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -285,7 +286,7 @@ int InstMatchGenerator::getMatch( Trace("matching-fail") << "Internal error for match generator." << std::endl; return -2; } - EqualityQuery* q = qe->getEqualityQuery(); + quantifiers::QuantifiersState& qs = qe->getState(); bool success = true; std::vector<int> prev; // if t is null @@ -303,7 +304,7 @@ int InstMatchGenerator::getMatch( Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..." << std::endl; bool addToPrev = m.get(ct).isNull(); - if (!m.set(q, ct, t[i])) + if (!m.set(qs, ct, t[i])) { // match is in conflict Trace("matching-fail") @@ -319,7 +320,7 @@ int InstMatchGenerator::getMatch( } else if (ct == -1) { - if (!q->areEqual(d_match_pattern[i], t[i])) + if (!qs.areEqual(d_match_pattern[i], t[i])) { Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; @@ -335,7 +336,7 @@ int InstMatchGenerator::getMatch( if (d_match_pattern.getKind() == INST_CONSTANT) { bool addToPrev = m.get(d_children_types[0]).isNull(); - if (!m.set(q, d_children_types[0], t)) + if (!m.set(qs, d_children_types[0], t)) { success = false; } @@ -371,7 +372,7 @@ int InstMatchGenerator::getMatch( { if (t.getType().isBoolean()) { - t_match = nm->mkConst(!q->areEqual(nm->mkConst(true), t)); + t_match = nm->mkConst(!qs.areEqual(nm->mkConst(true), t)); } else { @@ -391,7 +392,7 @@ int InstMatchGenerator::getMatch( if (!t_match.isNull()) { bool addToPrev = m.get(v).isNull(); - if (!m.set(q, v, t_match)) + if (!m.set(qs, v, t_match)) { success = false; } @@ -467,7 +468,7 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ // we did not properly initialize the candidate generator, thus we fail return false; } - eqc = qe->getEqualityQuery()->getRepresentative( eqc ); + eqc = qe->getState().getRepresentative(eqc); Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl; if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){ d_eq_class = d_eq_class_rel; @@ -509,7 +510,7 @@ int InstMatchGenerator::getNextMatch(Node f, Node t = d_curr_first_candidate; do{ Trace("matching-debug2") << "Matching candidate : " << t << std::endl; - Assert(!qe->inConflict()); + Assert(!qe->getState().isInConflict()); //if t not null, try to fit it into match m if( !t.isNull() ){ if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){ @@ -523,7 +524,8 @@ int InstMatchGenerator::getNextMatch(Node f, } //get the next candidate term t if( success<0 ){ - t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate(); + t = qe->getState().isInConflict() ? Node::null() + : d_cg->getNextCandidate(); }else{ d_curr_first_candidate = d_cg->getNextCandidate(); } @@ -554,13 +556,15 @@ uint64_t InstMatchGenerator::addInstantiations(Node f, if (sendInstantiation(tparent, m)) { addedLemmas++; - if( qe->inConflict() ){ + if (qe->getState().isInConflict()) + { break; } } }else{ addedLemmas++; - if( qe->inConflict() ){ + if (qe->getState().isInConflict()) + { break; } } diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index b4a7457a3..371bc3378 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -174,7 +175,7 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl; processNewMatch(qe, tparent, newMatches[j], i, addedLemmas); - if (qe->inConflict()) + if (qe->getState().isInConflict()) { return addedLemmas; } @@ -221,7 +222,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, size_t endChildIndex, bool modEq) { - Assert(!qe->inConflict()); + Assert(!qe->getState().isInConflict()); if (childIndex == endChildIndex) { // m is an instantiation @@ -256,7 +257,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, childIndex, endChildIndex, modEq); - if (qe->inConflict()) + if (qe->getState().isInConflict()) { break; } @@ -280,13 +281,13 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, { return; } - eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine(); + quantifiers::QuantifiersState& qs = qe->getState(); // check modulo equality for other possible instantiations - if (!ee->hasTerm(n)) + if (!qs.hasTerm(n)) { return; } - eq::EqClassIterator eqc(ee->getRepresentative(n), ee); + eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); while (!eqc.isFinished()) { Node en = (*eqc); @@ -304,7 +305,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, childIndex, endChildIndex, modEq); - if (qe->inConflict()) + if (qe->getState().isInConflict()) { break; } diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 8c3de21a9..b5ef7792d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -67,6 +67,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, QuantifiersEngine* qe, Trigger* tparent) { + quantifiers::QuantifiersState& qs = qe->getState(); uint64_t addedLemmas = 0; TNodeTrie* tat; if (d_eqc.isNull()) @@ -83,16 +84,16 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, { // iterate over all classes except r tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op); - if (tat && !qe->inConflict()) + if (tat && !qs.isInConflict()) { - Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); + Node r = qs.getRepresentative(d_eqc); for (std::pair<const TNode, TNodeTrie>& t : tat->d_data) { if (t.first != r) { InstMatch m(q); addInstantiations(m, qe, addedLemmas, 0, &(t.second)); - if (qe->inConflict()) + if (qs.isInConflict()) { break; } @@ -105,7 +106,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; - if (tat && !qe->inConflict()) + if (tat && !qs.isInConflict()) { InstMatch m(q); addInstantiations(m, qe, addedLemmas, 0, tat); @@ -146,6 +147,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } return; } + quantifiers::QuantifiersState& qs = qe->getState(); if (d_match_pattern[argIndex].getKind() == INST_CONSTANT) { int v = d_var_num[argIndex]; @@ -162,7 +164,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, m.setValue(v, t); addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); m.setValue(v, prev); - if (qe->inConflict()) + if (qs.isInConflict()) { break; } @@ -172,7 +174,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } // inst constant from another quantified formula, treat as ground term? } - Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]); + Node r = qs.getRepresentative(d_match_pattern[argIndex]); std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r); if (it != tat->d_data.end()) { diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index cd0ab7976..48c02f288 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -98,8 +98,9 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Trace("inst-engine-debug") << " -> unfinished= " << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED) - << ", conflict=" << d_quantEngine->inConflict() << std::endl; - if( d_quantEngine->inConflict() ){ + << ", conflict=" << d_qstate.isInConflict() << std::endl; + if (d_qstate.isInConflict()) + { return; } else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED) @@ -165,7 +166,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) { unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); doInstantiationRound(e); - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting); Trace("inst-engine") << "Conflict, added lemmas = " diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 470120be2..b1caa739e 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -109,7 +109,7 @@ uint64_t Trigger::addInstantiations() { // for each ground term t that does not exist in the equality engine, we // add a purification lemma of the form (k = t). - eq::EqualityEngine* ee = d_quantEngine->getEqualityQuery()->getEngine(); + eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine(); for (const Node& gt : d_groundTerms) { if (!ee->hasTerm(gt)) diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 0553c1745..4edacb827 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -52,7 +52,7 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, d_eq_class = Node::null(); // if( s.getType().isSubtypeOf( d_var_type ) ){ d_rm_prev = m.get(d_children_types[0]).isNull(); - if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) + if (!m.set(qe->getState(), d_children_types[0], s)) { return -1; } diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index b8515df91..08741ef0f 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -33,7 +33,10 @@ namespace quantifiers { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( QuantifiersState& qs, QuantifiersEngine* qe) - : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0) + : d_qe(qe), + d_qstate(qs), + d_eqi_counter(qs.getSatContext()), + d_reset_count(0) { } @@ -46,51 +49,12 @@ bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ return true; } -bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ - return getEngine()->hasTerm( a ); -} - -Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - return ee->getRepresentative( a ); - }else{ - return a; - } -} - -bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areEqual( a, b ); - }else{ - return false; - } - } -} - -bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areDisequal( a, b, false ); - }else{ - return a.isConst() && b.isConst(); - } - } -} - Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, Node q, int index) { Assert(q.isNull() || q.getKind() == FORALL); - Node r = getRepresentative( a ); + Node r = d_qstate.getRepresentative(a); if( options::finiteModelFind() ){ if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any @@ -99,7 +63,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if (!tr.isNull()) { r = tr; - r = getRepresentative( r ); + r = d_qstate.getRepresentative(r); }else{ if( r.getType().isSort() ){ Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; @@ -129,7 +93,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, // find best selection for representative Node r_best; std::vector<Node> eqc; - getEquivalenceClass(r, eqc); + d_qstate.getEquivalenceClass(r, eqc); Trace("internal-rep-select") << "Choose representative for equivalence class : " << eqc << ", type = " << v_tn << std::endl; @@ -180,30 +144,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, return r_best; } -eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getMasterEqualityEngine(); -} - -void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - Node rep = ee->getRepresentative( a ); - eq::EqClassIterator eqc_iter( rep, ee ); - while( !eqc_iter.isFinished() ){ - eqc.push_back( *eqc_iter ); - eqc_iter++; - } - }else{ - eqc.push_back( a ); - } - //a should be in its equivalence class - Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end()); -} - -TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { - return d_qe->getTermDatabase()->getCongruentTerm( f, args ); -} - //helper functions Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){ diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index b82b9ae64..a3f895f54 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -29,11 +29,7 @@ namespace quantifiers { /** EqualityQueryQuantifiersEngine class * - * This is a wrapper class around an equality engine that is used for - * queries required by algorithms in the quantifiers theory. It uses an equality - * engine, as determined by the quantifiers engine it points to. - * - * The main extension of this class wrt EqualityQuery is the function + * The main method of this class is the function * getInternalRepresentative, which is used by instantiation-based methods * that are agnostic with respect to choosing terms within an equivalence class. * Examples of such methods are finite model finding and enumerative @@ -41,7 +37,7 @@ namespace quantifiers { * representative based on the internal heuristic, which is currently based on * choosing the term that was previously chosen as a representative earliest. */ -class EqualityQueryQuantifiersEngine : public EqualityQuery +class EqualityQueryQuantifiersEngine : public QuantifiersUtil { public: EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe); @@ -52,32 +48,6 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery void registerQuantifier(Node q) override {} /** identify */ std::string identify() const override { return "EqualityQueryQE"; } - /** does the equality engine have term a */ - bool hasTerm(Node a) override; - /** get the representative of a */ - Node getRepresentative(Node a) override; - /** are a and b equal? */ - bool areEqual(Node a, Node b) override; - /** are a and b disequal? */ - bool areDisequal(Node a, Node b) override; - /** get equality engine - * This may either be the master equality engine or the model's equality - * engine. - */ - eq::EqualityEngine* getEngine() override; - /** get list of members in the equivalence class of a */ - void getEquivalenceClass(Node a, std::vector<Node>& eqc) override; - /** get congruent term - * If possible, returns a term n such that: - * (1) n is a term in the equality engine from getEngine(). - * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class - * of args[i] for i=1...k - * Otherwise, returns the null node. - * - * Notice that f should be a "match operator", returned by - * TermDb::getMatchOperator. - */ - TNode getCongruentTerm(Node f, std::vector<TNode>& args) override; /** gets the current best representative in the equivalence * class of a, based on some heuristic. Currently, the default heuristic * chooses terms that were previously chosen as representatives @@ -97,6 +67,8 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery private: /** pointer to theory engine */ QuantifiersEngine* d_qe; + /** the quantifiers state */ + QuantifiersState& d_qstate; /** quantifiers equality inference */ context::CDO< unsigned > d_eqi_counter; /** internal representatives */ diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index b2c7bf704..053174d07 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -358,7 +358,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Node r = fm->getRepresentative( it->second[a] ); if( Trace.isOn("fmc-model-debug") ){ std::vector< Node > eqc; - d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc ); + d_qstate.getEquivalenceClass(r, eqc); Trace("fmc-model-debug") << " " << (it->second[a]==r); Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 4d74c1697..427d82e7c 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -279,14 +279,13 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; - EqualityQuery* qy = d_quantEngine->getEqualityQuery(); Instantiate* inst = d_quantEngine->getInstantiate(); while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); for (unsigned i = 0; i < riter.getNumTerms(); i++) { - m.set(qy, i, riter.getCurrentTerm(i)); + m.set(d_qstate, i, riter.getCurrentTerm(i)); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index b2b58220a..5d6779406 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -45,24 +45,6 @@ void InstMatch::add(InstMatch& m) } } -bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){ - Assert(d_vals.size() == m.d_vals.size()); - for (unsigned i = 0, size = d_vals.size(); i < size; i++) - { - if( !m.d_vals[i].isNull() ){ - if( d_vals[i].isNull() ){ - d_vals[i] = m.d_vals[i]; - }else{ - if( !q->areEqual( d_vals[i], m.d_vals[i]) ){ - clear(); - return false; - } - } - } - } - return true; -} - void InstMatch::debugPrint( const char* c ){ for (unsigned i = 0, size = d_vals.size(); i < size; i++) { @@ -111,20 +93,14 @@ void InstMatch::setValue(size_t i, TNode n) Assert(i < d_vals.size()); d_vals[i] = n; } -bool InstMatch::set(EqualityQuery* q, size_t i, TNode n) +bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n) { Assert(i < d_vals.size()); if( !d_vals[i].isNull() ){ - if (q->areEqual(d_vals[i], n)) - { - return true; - }else{ - return false; - } - }else{ - d_vals[i] = n; - return true; + return qs.areEqual(d_vals[i], n); } + d_vals[i] = n; + return true; } }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index a51c0ecdc..e3d7909b7 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -24,7 +24,9 @@ namespace CVC4 { namespace theory { -class EqualityQuery; +namespace quantifiers { +class QuantifiersState; +} namespace inst { @@ -50,13 +52,6 @@ public: * not already initialized in this match. */ void add(InstMatch& m); - /** merge with match m - * - * This method returns true if the merge was successful, that is, all jointly - * initialized fields of this class and m are equivalent modulo the equalities - * given by q. - */ - bool merge( EqualityQuery* q, InstMatch& m ); /** is this complete, i.e. are all fields non-null? */ bool isComplete(); /** is this empty, i.e. are all fields the null node? */ @@ -87,7 +82,7 @@ public: * This method returns true if the i^th field was previously uninitialized, * or is equivalent to n modulo the equalities given by q. */ - bool set(EqualityQuery* q, size_t i, TNode n); + bool set(quantifiers::QuantifiersState& qs, size_t i, TNode n); }; inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index aaf7cb4bc..0bd5000f1 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -52,12 +52,11 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, } if (modEq) { + quantifiers::QuantifiersState& qs = qe->getState(); // check modulo equality if any other instantiation match exists - if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n)) + if (!n.isNull() && qs.hasTerm(n)) { - eq::EqClassIterator eqc( - qe->getEqualityQuery()->getEngine()->getRepresentative(n), - qe->getEqualityQuery()->getEngine()); + eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); while (!eqc.isFinished()) { Node en = (*eqc); @@ -331,11 +330,10 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, if (modEq) { // check modulo equality if any other instantiation match exists - if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n)) + quantifiers::QuantifiersState& qs = qe->getState(); + if (!n.isNull() && qs.hasTerm(n)) { - eq::EqClassIterator eqc( - qe->getEqualityQuery()->getEngine()->getRepresentative(n), - qe->getEqualityQuery()->getEngine()); + eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); while (!eqc.isFinished()) { Node en = (*eqc); diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index a63954838..c978a6952 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -28,7 +28,6 @@ namespace CVC4 { namespace theory { class QuantifiersEngine; -class EqualityQuery; namespace inst { diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index d1c09a9e8..c0f294528 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -188,7 +188,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) std::map<TypeNode, std::vector<Node> > term_db_list; std::vector<TypeNode> ftypes; TermDb* tdb = d_quantEngine->getTermDatabase(); - EqualityQuery* qy = d_quantEngine->getEqualityQuery(); + QuantifiersState& qs = d_quantEngine->getState(); // iterate over substitutions for variables for (unsigned i = 0; i < f[0].getNumChildren(); i++) { @@ -212,7 +212,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) Node gt = tdb->getTypeGroundTerm(ftypes[i], j); if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) { - Node rep = qy->getRepresentative(gt); + Node rep = qs.getRepresentative(gt); if (reps_found.find(rep) == reps_found.end()) { reps_found[rep] = gt; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index bd7a1b122..4359b8b19 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -589,7 +589,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms); inst = Rewriter::rewrite(inst); Node inst_eval = p->getTermDatabase()->evaluateTerm( - inst, nullptr, options::qcfTConstraint(), true); + inst, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; for( unsigned i=0; i<terms.size(); i++ ){ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b561b589b..6ce46ad99 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -38,22 +38,22 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const { - return d_quantEngine->getMasterEqualityEngine(); + return d_qstate.getEqualityEngine(); } bool QuantifiersModule::areEqual(TNode n1, TNode n2) const { - return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ); + return d_qstate.areEqual(n1, n2); } bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const { - return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ); + return d_qstate.areDisequal(n1, n2); } TNode QuantifiersModule::getRepresentative(TNode n) const { - return d_quantEngine->getEqualityQuery()->getRepresentative( n ); + return d_qstate.getRepresentative(n); } QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 16791b130..417e6820d 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -221,32 +221,6 @@ public: static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); }; -/** EqualityQuery -* This is a wrapper class around equality engine. -*/ -class EqualityQuery : public QuantifiersUtil { -public: - EqualityQuery(){} - virtual ~EqualityQuery(){}; - /** extends engine */ - virtual bool extendsEngine() { return false; } - /** contains term */ - virtual bool hasTerm( Node a ) = 0; - /** get the representative of the equivalence class of a */ - virtual Node getRepresentative( Node a ) = 0; - /** returns true if a and b are equal in the current context */ - virtual bool areEqual( Node a, Node b ) = 0; - /** returns true is a and b are disequal in the current context */ - virtual bool areDisequal( Node a, Node b ) = 0; - /** get the equality engine associated with this query */ - virtual eq::EqualityEngine* getEngine() = 0; - /** get the equivalence class of a */ - virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; - /** get the term that exists in EE that is congruent to f with args (f is - * returned by TermDb::getMatchOperator(...)) */ - virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; -};/* class EqualityQuery */ - /** Types of bounds that can be inferred for quantified formulas */ enum BoundVarType { diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 2893fd686..1743cafe5 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -51,12 +51,13 @@ RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() { } } -void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) { +void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs) +{ std::map< Node, Node > rterms; for( unsigned i=0; i<d_terms.size(); i++ ){ Node r = d_terms[i]; if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){ - r = qe->getEqualityQuery()->getRepresentative( d_terms[i] ); + r = qs.getRepresentative(d_terms[i]); } if( rterms.find( r )==rterms.end() ){ rterms[r] = d_terms[i]; @@ -141,7 +142,7 @@ void RelevantDomain::compute(){ RDomain * r = it2->second; RDomain * rp = r->getParent(); if( r==rp ){ - r->removeRedundantTerms( d_qe ); + r->removeRedundantTerms(d_qe->getState()); for( unsigned i=0; i<r->d_terms.size(); i++ ){ Trace("rel-dom") << r->d_terms[i] << " "; } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 6da4ce75a..36364191c 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -84,7 +84,7 @@ class RelevantDomain : public QuantifiersUtil /** remove redundant terms for d_terms, removes * duplicates modulo equality. */ - void removeRedundantTerms( QuantifiersEngine * qe ); + void removeRedundantTerms(QuantifiersState& qs); /** is n in this relevant domain? */ bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3f33b07b8..c39654aa5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -258,7 +258,7 @@ void TermDb::addTerm(Node n, void TermDb::computeArgReps( TNode n ) { if (d_arg_reps.find(n) == d_arg_reps.end()) { - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); for (const TNode& nc : n) { TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc; @@ -281,7 +281,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { { ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); } - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); for (TNode ff : ops) { for (const Node& n : d_op_map[ff]) @@ -316,7 +316,6 @@ void TermDb::computeUfTerms( TNode f ) { unsigned nonCongruentCount = 0; unsigned alreadyCongruentCount = 0; unsigned relevantCount = 0; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); NodeManager* nm = NodeManager::currentNM(); for (TNode ff : ops) { @@ -330,7 +329,7 @@ void TermDb::computeUfTerms( TNode f ) { for (const Node& n : it->second) { // to be added to term index, term must be relevant, and exist in EE - if (!hasTermCurrent(n) || !ee->hasTerm(n)) + if (!hasTermCurrent(n) || !d_qstate.hasTerm(n)) { Trace("term-db-debug") << n << " is not relevant." << std::endl; continue; @@ -358,20 +357,20 @@ void TermDb::computeUfTerms( TNode f ) { } } Trace("term-db-debug") << std::endl; - Assert(ee->hasTerm(n)); - Trace("term-db-debug") << " and value : " << ee->getRepresentative(n) - << std::endl; + Assert(d_qstate.hasTerm(n)); + Trace("term-db-debug") + << " and value : " << d_qstate.getRepresentative(n) << std::endl; Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]); - Assert(ee->hasTerm(at)); + Assert(d_qstate.hasTerm(at)); Trace("term-db-debug2") << "...add term returned " << at << std::endl; - if (at != n && ee->areEqual(at, n)) + if (at != n && d_qstate.areEqual(at, n)) { setTermInactive(n); Trace("term-db-debug") << n << " is redundant." << std::endl; congruentCount++; continue; } - if (ee->areDisequal(at, n, false)) + if (d_qstate.areDisequal(at, n)) { std::vector<Node> lits; lits.push_back(nm->mkNode(EQUAL, at, n)); @@ -512,9 +511,8 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { f = getOperatorRepresentative( f ); } computeUfTerms( f ); - Assert(!d_quantEngine->getMasterEqualityEngine()->hasTerm(r) - || d_quantEngine->getMasterEqualityEngine()->getRepresentative(r) - == r); + Assert(!d_qstate.getEqualityEngine()->hasTerm(r) + || d_qstate.getEqualityEngine()->getRepresentative(r) == r); std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); if( it != d_func_map_rel_dom.end() ){ std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); @@ -531,7 +529,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { Node TermDb::evaluateTerm2(TNode n, std::map<TNode, Node>& visited, std::vector<Node>& exp, - EqualityQuery* qy, bool useEntailmentTests, bool computeExp, bool reqHasTerm) @@ -546,10 +543,10 @@ Node TermDb::evaluateTerm2(TNode n, if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ //do nothing } - else if (qy->hasTerm(n)) + else if (d_qstate.hasTerm(n)) { Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; - ret = qy->getRepresentative(n); + ret = d_qstate.getRepresentative(n); if (computeExp) { if (n != ret) @@ -570,7 +567,6 @@ Node TermDb::evaluateTerm2(TNode n, TNode c = evaluateTerm2(n[i], visited, tempExp, - qy, useEntailmentTests, computeExp, reqHasTerm); @@ -595,7 +591,6 @@ Node TermDb::evaluateTerm2(TNode n, ret = evaluateTerm2(n[c == d_true ? 1 : 2], visited, tempExp, - qy, useEntailmentTests, computeExp, reqHasTerm); @@ -628,7 +623,7 @@ Node TermDb::evaluateTerm2(TNode n, if (!f.isNull()) { // if f is congruent to a term indexed by this class - TNode nn = qy->getCongruentTerm(f, args); + TNode nn = getCongruentTerm(f, args); Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl; if (!nn.isNull()) @@ -644,7 +639,7 @@ Node TermDb::evaluateTerm2(TNode n, } } } - ret = qy->getRepresentative(nn); + ret = d_qstate.getRepresentative(nn); Trace("term-db-eval") << "return rep" << std::endl; ret_set = true; reqHasTerm = false; @@ -669,7 +664,7 @@ Node TermDb::evaluateTerm2(TNode n, ret = Rewriter::rewrite(ret); if (ret.getKind() == EQUAL) { - if (qy->areDisequal(ret[0], ret[1])) + if (d_qstate.areDisequal(ret[0], ret[1])) { ret = d_false; } @@ -706,7 +701,7 @@ Node TermDb::evaluateTerm2(TNode n, if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT && k != FORALL) { - if (!qy->hasTerm(ret)) + if (!d_qstate.hasTerm(ret)) { ret = Node::null(); } @@ -723,11 +718,14 @@ Node TermDb::evaluateTerm2(TNode n, return ret; } - -TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) { - Assert(!qy->extendsEngine()); +TNode TermDb::getEntailedTerm2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool hasSubs) +{ Trace("term-db-entail") << "get entailed term : " << n << std::endl; - if( qy->getEngine()->hasTerm( n ) ){ + if (d_qstate.hasTerm(n)) + { Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; return n; }else if( n.getKind()==BOUND_VARIABLE ){ @@ -736,18 +734,18 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su if( it!=subs.end() ){ Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; if( subsRep ){ - Assert(qy->getEngine()->hasTerm(it->second)); - Assert(qy->getEngine()->getRepresentative(it->second) == it->second); + Assert(d_qstate.hasTerm(it->second)); + Assert(d_qstate.getRepresentative(it->second) == it->second); return it->second; - }else{ - return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy ); } + return getEntailedTerm2(it->second, subs, subsRep, hasSubs); } } }else if( n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ - if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ - return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy ); + if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + { + return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); } } }else{ @@ -756,15 +754,15 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su if( !f.isNull() ){ std::vector< TNode > args; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy ); + TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs); if( c.isNull() ){ return TNode::null(); } - c = qy->getEngine()->getRepresentative( c ); + c = d_qstate.getRepresentative(c); Trace("term-db-entail") << " child " << i << " : " << c << std::endl; args.push_back( c ); } - TNode nn = qy->getCongruentTerm( f, args ); + TNode nn = getCongruentTerm(f, args); Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl; return nn; } @@ -774,77 +772,66 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su } Node TermDb::evaluateTerm(TNode n, - EqualityQuery* qy, bool useEntailmentTests, bool reqHasTerm) { - if( qy==NULL ){ - qy = d_quantEngine->getEqualityQuery(); - } std::map< TNode, Node > visited; std::vector<Node> exp; - return evaluateTerm2( - n, visited, exp, qy, useEntailmentTests, false, reqHasTerm); + return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); } Node TermDb::evaluateTerm(TNode n, std::vector<Node>& exp, - EqualityQuery* qy, bool useEntailmentTests, bool reqHasTerm) { - if (qy == NULL) - { - qy = d_quantEngine->getEqualityQuery(); - } std::map<TNode, Node> visited; - return evaluateTerm2( - n, visited, exp, qy, useEntailmentTests, true, reqHasTerm); + return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); } -TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) { - if( qy==NULL ){ - qy = d_quantEngine->getEqualityQuery(); - } - return getEntailedTerm2( n, subs, subsRep, true, qy ); +TNode TermDb::getEntailedTerm(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep) +{ + return getEntailedTerm2(n, subs, subsRep, true); } -TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) { - if( qy==NULL ){ - qy = d_quantEngine->getEqualityQuery(); - } +TNode TermDb::getEntailedTerm(TNode n) +{ std::map< TNode, TNode > subs; - return getEntailedTerm2( n, subs, false, false, qy ); + return getEntailedTerm2(n, subs, false, false); } -bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) { - Assert(!qy->extendsEngine()); +bool TermDb::isEntailed2( + TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol) +{ Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert(n.getType().isBoolean()); if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ - TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy ); + TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); if( !n1.isNull() ){ - TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy ); + TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); if( !n2.isNull() ){ if( n1==n2 ){ return pol; }else{ - Assert(qy->getEngine()->hasTerm(n1)); - Assert(qy->getEngine()->hasTerm(n2)); + Assert(d_qstate.hasTerm(n1)); + Assert(d_qstate.hasTerm(n2)); if( pol ){ - return qy->getEngine()->areEqual( n1, n2 ); + return d_qstate.areEqual(n1, n2); }else{ - return qy->getEngine()->areDisequal( n1, n2, false ); + return d_qstate.areDisequal(n1, n2); } } } } }else if( n.getKind()==NOT ){ - return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy ); + return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); }else if( n.getKind()==OR || n.getKind()==AND ){ bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){ + if (isEntailed2(n[i], subs, subsRep, hasSubs, pol)) + { if( simPol ){ return true; } @@ -858,45 +845,45 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, //Boolean equality here }else if( n.getKind()==EQUAL || n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ - if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ + if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + { unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2; bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; - return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy ); + return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol); } } }else if( n.getKind()==APPLY_UF ){ - TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy ); + TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs); if( !n1.isNull() ){ - Assert(qy->hasTerm(n1)); + Assert(d_qstate.hasTerm(n1)); if( n1==d_true ){ return pol; }else if( n1==d_false ){ return !pol; }else{ - return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false ); + return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false); } } }else if( n.getKind()==FORALL && !pol ){ - return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy ); + return isEntailed2(n[1], subs, subsRep, hasSubs, pol); } return false; } -bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) { - if( qy==NULL ){ - Assert(d_consistent_ee); - qy = d_quantEngine->getEqualityQuery(); - } +bool TermDb::isEntailed(TNode n, bool pol) +{ + Assert(d_consistent_ee); std::map< TNode, TNode > subs; - return isEntailed2( n, subs, false, false, pol, qy ); + return isEntailed2(n, subs, false, false, pol); } -bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) { - if( qy==NULL ){ - Assert(d_consistent_ee); - qy = d_quantEngine->getEqualityQuery(); - } - return isEntailed2( n, subs, subsRep, true, pol, qy ); +bool TermDb::isEntailed(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool pol) +{ + Assert(d_consistent_ee); + return isEntailed2(n, subs, subsRep, true, pol); } bool TermDb::isTermActive( Node n ) { @@ -971,8 +958,8 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r ); if( it==d_term_elig_eqc.end() ){ Node h; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); while (!eqc_i.isFinished()) { TNode n = (*eqc_i); @@ -1025,7 +1012,7 @@ bool TermDb::reset( Theory::Effort effort ){ d_func_map_rel_dom.clear(); d_consistent_ee = true; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); Assert(ee->consistent()); // if higher-order, add equalities for the purification terms now @@ -1083,7 +1070,7 @@ bool TermDb::reset( Theory::Effort effort ){ bool addedFirst = false; Node first; //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); if( first.isNull() ){ @@ -1125,8 +1112,9 @@ bool TermDb::reset( Theory::Effort effort ){ //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed for (const Node& n : d_iclosure_processed) { - if( !ee->hasTerm( n ) ){ - ee->addTerm( n ); + if (!ee->hasTerm(n)) + { + ee->addTerm(n); } } @@ -1141,7 +1129,7 @@ bool TermDb::reset( Theory::Effort effort ){ if( r.getType().isFunction() ){ Trace("quant-ho") << " process function eqc " << r << std::endl; Node first; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); Node n_use; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index c246ea6fc..244762d24 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -31,22 +31,9 @@ namespace theory { class QuantifiersEngine; -namespace inst{ - class Trigger; - class HigherOrderTrigger; -} - namespace quantifiers { -namespace fmcheck { - class FullModelChecker; -} - -class TermDbSygus; -class QuantConflictFind; -class RelevantDomain; class ConjectureGenerator; -class TermGenerator; class TermGenEnv; /** Term Database @@ -182,9 +169,9 @@ class TermDb : public QuantifiersUtil { /** evaluate term * * Returns a term n' such that n = n' is entailed based on the equality - * information qy. This function may generate new terms. In particular, + * information ee. This function may generate new terms. In particular, * we typically rewrite subterms of n of maximal size to terms that exist in - * the equality engine specified by qy. + * the equality engine specified by ee. * * useEntailmentTests is whether to call the theory engine's entailmentTest * on literals n for which this call fails to find a term n' that is @@ -204,59 +191,53 @@ class TermDb : public QuantifiersUtil { */ Node evaluateTerm(TNode n, std::vector<Node>& exp, - EqualityQuery* qy = NULL, bool useEntailmentTests = false, bool reqHasTerm = false); /** same as above, without exp */ Node evaluateTerm(TNode n, - EqualityQuery* qy = NULL, bool useEntailmentTests = false, bool reqHasTerm = false); /** get entailed term * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by qy), - * (2) n = n' is entailed in the current context. - * It returns null if no such term can be found. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL); + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n = n' is entailed in the current context. + * It returns null if no such term can be found. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n); /** get entailed term * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by qy), - * (2) n * subs = n' is entailed in the current context, where * is denotes - * substitution application. - * It returns null if no such term can be found. - * subsRep is whether the substitution maps to terms that are representatives - * according to qy. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep, - EqualityQuery* qy = NULL); + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n * subs = n' is entailed in the current context, where * denotes + * substitution application. + * It returns null if no such term can be found. + * subsRep is whether the substitution maps to terms that are representatives + * according to the quantifiers state. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep); /** is entailed - * Checks whether the current context entails n with polarity pol, based on the - * equality information qy. - * Returns true if the entailment can be successfully shown. - */ - bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL); + * Checks whether the current context entails n with polarity pol, based on + * the equality information in the quantifiers state. Returns true if the + * entailment can be successfully shown. + */ + bool isEntailed(TNode n, bool pol); /** is entailed * - * Checks whether the current context entails ( n * subs ) with polarity pol, - * based on the equality information qy, - * where * denotes substitution application. - * subsRep is whether the substitution maps to terms that are representatives - * according to qy. - */ + * Checks whether the current context entails ( n * subs ) with polarity pol, + * based on the equality information in the quantifiers state, + * where * denotes substitution application. + * subsRep is whether the substitution maps to terms that are representatives + * according to in the quantifiers state. + */ bool isEntailed(TNode n, std::map<TNode, TNode>& subs, bool subsRep, - bool pol, - EqualityQuery* qy = NULL); + bool pol); /** is the term n active in the current context? * * By default, all terms are active. A term is inactive if: @@ -354,14 +335,20 @@ class TermDb : public QuantifiersUtil { Node evaluateTerm2(TNode n, std::map<TNode, Node>& visited, std::vector<Node>& exp, - EqualityQuery* qy, bool useEntailmentTests, bool computeExp, bool reqHasTerm); /** helper for get entailed term */ - TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); + TNode getEntailedTerm2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool hasSubs); /** helper for is entailed */ - bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); + bool isEntailed2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool hasSubs, + bool pol); /** compute uf eqc terms : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 4dd59d12f..1cbb2ce40 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -83,6 +83,13 @@ void TheoryQuantifiers::finishInit() d_valuation.setUnevaluatedKind(WITNESS); } +bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi) +{ + // use the master equality engine + esi.d_useMaster = true; + return true; +} + void TheoryQuantifiers::preRegisterTerm(TNode n) { if (n.getKind() != FORALL) @@ -164,7 +171,7 @@ bool TheoryQuantifiers::preNotifyFact( getQuantifiersEngine()->addTermToDatabase(atom[0], false, true); if (!options::lteRestrictInstClosure()) { - getQuantifiersEngine()->getMasterEqualityEngine()->addTerm(atom[0]); + d_qstate.getEqualityEngine()->addTerm(atom[0]); } } else diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 8d2366065..2283d5ea8 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -47,6 +47,8 @@ class TheoryQuantifiers : public Theory { TheoryRewriter* getTheoryRewriter() override; /** finish initialization */ void finishInit() override; + /** needs equality engine */ + bool needsEqualityEngine(EeSetupInfo& esi) override; //--------------------------------- end initialization void preRegisterTerm(TNode n) override; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7cec8721c..2cc904ed1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -39,7 +39,6 @@ QuantifiersEngine::QuantifiersEngine( d_qim(qim), d_te(nullptr), d_decManager(nullptr), - d_masterEqualityEngine(nullptr), d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)), d_tr_trie(new inst::TriggerTrie), d_model(nullptr), @@ -120,13 +119,10 @@ QuantifiersEngine::QuantifiersEngine( QuantifiersEngine::~QuantifiersEngine() {} -void QuantifiersEngine::finishInit(TheoryEngine* te, - DecisionManager* dm, - eq::EqualityEngine* mee) +void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) { d_te = te; d_decManager = dm; - d_masterEqualityEngine = mee; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); d_qmodules->initialize(this, d_qstate, d_qim, d_modules); @@ -147,12 +143,16 @@ OutputChannel& QuantifiersEngine::getOutputChannel() { return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel(); } -/** get default valuation for the quantifiers engine */ Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); } -EqualityQuery* QuantifiersEngine::getEqualityQuery() const +quantifiers::QuantifiersState& QuantifiersEngine::getState() { - return d_eq_query.get(); + return d_qstate; +} +quantifiers::QuantifiersInferenceManager& +QuantifiersEngine::getInferenceManager() +{ + return d_qim; } quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { @@ -352,8 +352,8 @@ void QuantifiersEngine::ppNotifyAssertions( void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_statistics.d_time); - - if (!getMasterEqualityEngine()->consistent()) + Assert(d_qstate.getEqualityEngine() != nullptr); + if (!d_qstate.getEqualityEngine()->consistent()) { Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; @@ -885,8 +885,6 @@ bool QuantifiersEngine::hasAddedLemma() const return !d_lemmas_waiting.empty() || d_hasAddedLemma; } -bool QuantifiersEngine::inConflict() const { return d_qstate.isInConflict(); } - bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode @@ -1067,11 +1065,6 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr); } -eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const -{ - return d_masterEqualityEngine; -} - Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return d_eq_query->getInternalRepresentative(a, q, index); } @@ -1100,7 +1093,7 @@ bool QuantifiersEngine::getSynthSolutions( } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { - eq::EqualityEngine* ee = getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 126fca01f..74f432585 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -73,12 +73,12 @@ class QuantifiersEngine { OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ Valuation& getValuation(); + /** The quantifiers state object */ + quantifiers::QuantifiersState& getState(); + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& getInferenceManager(); //---------------------- end external interface //---------------------- utilities - /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine() const; - /** get equality query */ - EqualityQuery* getEqualityQuery() const; /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; /** get model */ @@ -110,11 +110,8 @@ class QuantifiersEngine { * * @param te The theory engine * @param dm The decision manager of the theory engine - * @param mee The master equality engine of the theory engine */ - void finishInit(TheoryEngine* te, - DecisionManager* dm, - eq::EqualityEngine* mee); + void finishInit(TheoryEngine* te, DecisionManager* dm); //---------------------- end private initialization /** * Maps quantified formulas to the module that owns them, if any module has @@ -227,8 +224,6 @@ public: void markRelevant(Node q); /** has added lemma */ bool hasAddedLemma() const; - /** is in conflict */ - bool inConflict() const; /** get current q effort */ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } /** get number of waiting lemmas */ @@ -343,8 +338,6 @@ public: TheoryEngine* d_te; /** Reference to the decision manager of the theory engine */ DecisionManager* d_decManager; - /** Pointer to the master equality engine */ - eq::EqualityEngine* d_masterEqualityEngine; /** vector of utilities for quantifiers */ std::vector<QuantifiersUtil*> d_util; /** vector of modules for quantifiers */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ba65fe69d..18d9bb572 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -183,8 +183,7 @@ void TheoryEngine::finishInit() // finish initializing the quantifiers engine if (d_logicInfo.isQuantified()) { - d_quantEngine->finishInit( - this, d_decManager.get(), d_tc->getCoreEqualityEngine()); + d_quantEngine->finishInit(this, d_decManager.get()); } // finish initializing the theories by linking them with the appropriate diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index 47528e1a6..e145baa6a 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -119,6 +119,26 @@ bool TheoryState::areDisequal(TNode a, TNode b) const return d_ee->areDisequal(a, b, false); } +void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const +{ + if (d_ee->hasTerm(a)) + { + Node rep = d_ee->getRepresentative(a); + eq::EqClassIterator eqc_iter(rep, d_ee); + while (!eqc_iter.isFinished()) + { + eqc.push_back(*eqc_iter); + eqc_iter++; + } + } + else + { + eqc.push_back(a); + } + // a should be in its equivalence class + Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end()); +} + eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; } void TheoryState::notifyInConflict() { d_conflict = true; } diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 7c2a044bf..891016f0a 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -60,6 +60,8 @@ class TheoryState * returns true if the representative of a and b are distinct constants. */ virtual bool areDisequal(TNode a, TNode b) const; + /** get list of members in the equivalence class of a */ + virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const; /** get equality engine */ eq::EqualityEngine* getEqualityEngine() const; //-------------------------------------- end equality information |