From 91d701dd898acfddd55edffa9bf11cb175b09147 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Mar 2021 19:50:00 -0600 Subject: [PATCH] Simplify instantiation match generator interface (#6121) --- .../ematching/inst_match_generator.cpp | 131 ++++++++---------- .../ematching/inst_match_generator.h | 117 ++++++---------- .../ematching/inst_match_generator_multi.cpp | 73 ++++------ .../ematching/inst_match_generator_multi.h | 22 +-- .../inst_match_generator_multi_linear.cpp | 28 ++-- .../inst_match_generator_multi_linear.h | 16 +-- .../ematching/inst_match_generator_simple.cpp | 64 ++++----- .../ematching/inst_match_generator_simple.h | 18 +-- src/theory/quantifiers/ematching/trigger.cpp | 24 ++-- src/theory/quantifiers/ematching/trigger.h | 2 +- .../ematching/var_match_generator.cpp | 21 ++- .../ematching/var_match_generator.h | 12 +- 12 files changed, 202 insertions(+), 326 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 719451d1e..584b3ebbf 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -36,24 +36,23 @@ namespace CVC4 { namespace theory { namespace inst { -IMGenerator::IMGenerator(quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim) - : d_qstate(qs), d_qim(qim) +IMGenerator::IMGenerator(Trigger* tparent) + : d_tparent(tparent), d_qstate(tparent->d_qstate) { } -bool IMGenerator::sendInstantiation(Trigger* tparent, - InstMatch& m, - InferenceId id) +bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id) { - return tparent->sendInstantiation(m, id); + return d_tparent->sendInstantiation(m, id); } -InstMatchGenerator::InstMatchGenerator( - Node pat, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim) - : IMGenerator(qs, qim) +QuantifiersEngine* IMGenerator::getQuantifiersEngine() +{ + return d_tparent->d_quantEngine; +} + +InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat) + : IMGenerator(tparent) { d_cg = nullptr; d_needsReset = true; @@ -85,19 +84,21 @@ void InstMatchGenerator::setActiveAdd(bool val){ } } -int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) { +int InstMatchGenerator::getActiveScore() +{ if( d_match_pattern.isNull() ){ return -1; } - else if (TriggerTermInfo::isAtomicTrigger(d_match_pattern)) + quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + if (TriggerTermInfo::isAtomicTrigger(d_match_pattern)) { - Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); - unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f ); + Node f = tdb->getMatchOperator(d_match_pattern); + unsigned ngt = tdb->getNumGroundTerms(f); Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl; return ngt; }else if( d_match_pattern.getKind()==INST_CONSTANT ){ TypeNode tn = d_match_pattern.getType(); - unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn ); + unsigned ngtt = tdb->getNumTypeGroundTerms(tn); Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl; return ngtt; } @@ -105,7 +106,6 @@ int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) { } void InstMatchGenerator::initialize(Node q, - QuantifiersEngine* qe, std::vector& gens) { if (d_pattern.isNull()) @@ -172,7 +172,8 @@ void InstMatchGenerator::initialize(Node q, d_match_pattern_type = d_match_pattern.getType(); Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - d_match_pattern_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern); + quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + d_match_pattern_op = tdb->getMatchOperator(d_match_pattern); // now, collect children of d_match_pattern Kind mpk = d_match_pattern.getKind(); @@ -195,8 +196,7 @@ void InstMatchGenerator::initialize(Node q, } else { - InstMatchGenerator* cimg = - getInstMatchGenerator(q, pat, d_qstate, d_qim); + InstMatchGenerator* cimg = getInstMatchGenerator(d_tparent, q, pat); if (cimg) { d_children.push_back(cimg); @@ -216,6 +216,7 @@ void InstMatchGenerator::initialize(Node q, } } + QuantifiersEngine* qe = getQuantifiersEngine(); // create candidate generator if (mpk == APPLY_SELECTOR) { @@ -254,7 +255,7 @@ void InstMatchGenerator::initialize(Node q, { if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL) { - Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern); + Node selectorExpr = tdb->getMatchOperator(d_pattern); size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr); const DType& dt = datatypes::utils::datatypeOf(selectorExpr); const DTypeConstructor& c = dt[selectorIndex]; @@ -285,8 +286,7 @@ void InstMatchGenerator::initialize(Node q, } /** get match (not modulo equality) */ -int InstMatchGenerator::getMatch( - Node f, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent) +int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m) { Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; @@ -419,7 +419,7 @@ int InstMatchGenerator::getMatch( // we will be requesting candidates for matching terms for each child for (size_t i = 0, size = d_children.size(); i < size; i++) { - if (!d_children[i]->reset(t[d_children_index[i]], qe)) + if (!d_children[i]->reset(t[d_children_index[i]])) { success = false; break; @@ -428,8 +428,8 @@ int InstMatchGenerator::getMatch( if (success) { Trace("matching-debug2") << "Continue next " << d_next << std::endl; - ret_val = continueNextMatch( - f, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING); + ret_val = + continueNextMatch(f, m, InferenceId::QUANTIFIERS_INST_E_MATCHING); } } if (ret_val < 0) @@ -444,22 +444,21 @@ int InstMatchGenerator::getMatch( int InstMatchGenerator::continueNextMatch(Node q, InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent, InferenceId id) { if( d_next!=NULL ){ - return d_next->getNextMatch(q, m, qe, tparent); + return d_next->getNextMatch(q, m); } if (d_active_add) { - return sendInstantiation(tparent, m, id) ? 1 : -1; + return sendInstantiation(m, id) ? 1 : -1; } return 1; } /** reset instantiation round */ -void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ +void InstMatchGenerator::resetInstantiationRound() +{ if( !d_match_pattern.isNull() ){ Trace("matching-debug2") << this << " reset instantiation round." << std::endl; d_needsReset = true; @@ -468,12 +467,13 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ } } if( d_next ){ - d_next->resetInstantiationRound( qe ); + d_next->resetInstantiationRound(); } d_curr_exclude_match.clear(); } -bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ +bool InstMatchGenerator::reset(Node eqc) +{ if (d_cg == nullptr) { // we did not properly initialize the candidate generator, thus we fail @@ -506,14 +506,11 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ return !d_curr_first_candidate.isNull(); } -int InstMatchGenerator::getNextMatch(Node f, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) +int InstMatchGenerator::getNextMatch(Node f, InstMatch& m) { if( d_needsReset ){ Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; - reset( d_eq_class, qe ); + reset(d_eq_class); } d_curr_matched = Node::null(); Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl; @@ -527,7 +524,7 @@ int InstMatchGenerator::getNextMatch(Node f, if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){ Assert(t.getType().isComparableTo(d_match_pattern_type)); Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl; - success = getMatch(f, t, m, qe, tparent); + success = getMatch(f, t, m); if( d_independent_gen && success<0 ){ Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull()); d_curr_exclude_match[t] = true; @@ -546,24 +543,22 @@ int InstMatchGenerator::getNextMatch(Node f, Trace("matching-summary") << "..." << d_match_pattern << " failed, reset." << std::endl; Trace("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset - reset( d_eq_class, qe ); + reset(d_eq_class); }else{ Trace("matching-summary") << "..." << d_match_pattern << " success." << std::endl; } return success; } -uint64_t InstMatchGenerator::addInstantiations(Node f, - QuantifiersEngine* qe, - Trigger* tparent) +uint64_t InstMatchGenerator::addInstantiations(Node f) { //try to add instantiation for each match produced uint64_t addedLemmas = 0; InstMatch m( f ); - while (getNextMatch(f, m, qe, tparent) > 0) + while (getNextMatch(f, m) > 0) { if( !d_active_add ){ - if (sendInstantiation(tparent, m, InferenceId::UNKNOWN)) + if (sendInstantiation(m, InferenceId::UNKNOWN)) { addedLemmas++; if (d_qstate.isInConflict()) @@ -584,31 +579,24 @@ uint64_t InstMatchGenerator::addInstantiations(Node f, return addedLemmas; } -InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( - Node q, - Node pat, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe) +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Trigger* tparent, + Node q, + Node pat) { std::vector< Node > pats; pats.push_back( pat ); std::map< Node, InstMatchGenerator * > pat_map_init; - return mkInstMatchGenerator(q, pats, qs, qim, qe, pat_map_init); + return mkInstMatchGenerator(tparent, q, pats, pat_map_init); } InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( - Node q, - std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe) + Trigger* tparent, Node q, std::vector& pats) { Assert(pats.size() > 1); InstMatchGeneratorMultiLinear* imgm = - new InstMatchGeneratorMultiLinear(q, pats, qs, qim); + new InstMatchGeneratorMultiLinear(tparent, q, pats); std::vector< InstMatchGenerator* > gens; - imgm->initialize(q, qe, gens); + imgm->initialize(q, gens); Assert(gens.size() == pats.size()); std::vector< Node > patsn; std::map< Node, InstMatchGenerator * > pat_map_init; @@ -618,17 +606,14 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( patsn.push_back( pn ); pat_map_init[pn] = g; } - //return mkInstMatchGenerator( q, patsn, qe, pat_map_init ); - imgm->d_next = mkInstMatchGenerator(q, patsn, qs, qim, qe, pat_map_init); + imgm->d_next = mkInstMatchGenerator(tparent, q, patsn, pat_map_init); return imgm; } InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( + Trigger* tparent, Node q, std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe, std::map& pat_map_init) { size_t pCounter = 0; @@ -640,7 +625,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( InstMatchGenerator* init; std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] ); if( iti==pat_map_init.end() ){ - init = new InstMatchGenerator(pats[pCounter], qs, qim); + init = new InstMatchGenerator(tparent, pats[pCounter]); }else{ init = iti->second; } @@ -654,7 +639,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( if( prev ){ prev->d_next = curr; } - curr->initialize(q, qe, gens); + curr->initialize(q, gens); prev = curr; counter++; } @@ -663,11 +648,9 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( return oinit; } -InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator( - Node q, - Node n, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim) +InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, + Node q, + Node n) { if (n.getKind() != INST_CONSTANT) { @@ -690,13 +673,13 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator( { Node s = PatternTermSelector::getInversion(n, x); VarMatchGeneratorTermSubs* vmg = - new VarMatchGeneratorTermSubs(x, s, qs, qim); + new VarMatchGeneratorTermSubs(tparent, x, s); Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl; return vmg; } } - return new InstMatchGenerator(n, qs, qim); + return new InstMatchGenerator(tparent, n); } }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 7a22a5ded..99414c90d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -29,7 +29,6 @@ class QuantifiersEngine; namespace quantifiers { class QuantifiersState; -class QuantifiersInferenceManager; } // namespace quantifiers namespace inst { @@ -55,14 +54,13 @@ class Trigger; */ class IMGenerator { public: - IMGenerator(quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim); + IMGenerator(Trigger* tparent); virtual ~IMGenerator() {} /** Reset instantiation round. * * Called once at beginning of an instantiation round. */ - virtual void resetInstantiationRound(QuantifiersEngine* qe) {} + virtual void resetInstantiationRound() {} /** Reset. * * eqc is the equivalence class to search in (any if eqc=null). @@ -70,7 +68,7 @@ public: * otherwise. An example of when it returns false is if it can be determined * that no appropriate matchable terms occur based on eqc. */ - virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; } + virtual bool reset(Node eqc) { return true; } /** Get the next match. * * Must call reset( eqc ) before this function. This constructs an @@ -82,14 +80,8 @@ public: * * Returns a value >0 if an instantiation was successfully generated */ - virtual int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) - { - return 0; - } - /** add instantiations + virtual int getNextMatch(Node q, InstMatch& m) { return 0; } + /** add instantiations * * This add all available instantiations for q based on the current context * using the implemented matching algorithm. It typically is implemented as a @@ -98,32 +90,30 @@ public: * It returns the number of instantiations added using calls to calls to * Instantiate::addInstantiation(...). */ - virtual uint64_t addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) - { - return 0; - } - /** get active score + virtual uint64_t addInstantiations(Node q) { return 0; } + /** get active score * * A heuristic value indicating how active this generator is. */ - virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; } - protected: - /** send instantiation - * - * This method sends instantiation, specified by m, to the parent trigger - * object, which will in turn make a call to - * Instantiate::addInstantiation(...). This method returns true if a - * call to Instantiate::addInstantiation(...) was successfully made, - * indicating that an instantiation was enqueued in the quantifier engine's - * lemma cache. - */ - bool sendInstantiation(Trigger* tparent, InstMatch& m, InferenceId id); - /** The state of the quantifiers engine */ - quantifiers::QuantifiersState& d_qstate; - /** The quantifiers inference manager */ - quantifiers::QuantifiersInferenceManager& d_qim; + virtual int getActiveScore() { return 0; } + +protected: + /** send instantiation + * + * This method sends instantiation, specified by m, to the parent trigger + * object, which will in turn make a call to + * Instantiate::addInstantiation(...). This method returns true if a + * call to Instantiate::addInstantiation(...) was successfully made, + * indicating that an instantiation was enqueued in the quantifier engine's + * lemma cache. + */ + bool sendInstantiation(InstMatch& m, InferenceId id); + /** The parent trigger that owns this */ + Trigger* d_tparent; + /** The state of the quantifiers engine */ + quantifiers::QuantifiersState& d_qstate; + // !!!!!!!!! temporarily available (project #15) + QuantifiersEngine* getQuantifiersEngine(); };/* class IMGenerator */ class CandidateGenerator; @@ -206,18 +196,13 @@ class InstMatchGenerator : public IMGenerator { ~InstMatchGenerator() override; /** Reset instantiation round. */ - void resetInstantiationRound(QuantifiersEngine* qe) override; + void resetInstantiationRound() override; /** Reset. */ - bool reset(Node eqc, QuantifiersEngine* qe) override; + bool reset(Node eqc) override; /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; + int getNextMatch(Node q, InstMatch& m) override; /** Add instantiations. */ - uint64_t addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) override; + uint64_t addInstantiations(Node q) override; /** set active add flag (true by default) * @@ -232,7 +217,7 @@ class InstMatchGenerator : public IMGenerator { * * See Trigger::getActiveScore for details. */ - int getActiveScore(QuantifiersEngine* qe) override; + int getActiveScore() override; /** exclude match * * Exclude matching d_match_pattern with Node n on subsequent calls to @@ -251,12 +236,9 @@ class InstMatchGenerator : public IMGenerator { void setIndependent() { d_independent_gen = true; } //-------------------------------construction of inst match generators /** mkInstMatchGenerator for single triggers, calls the method below */ - static InstMatchGenerator* mkInstMatchGenerator( - Node q, - Node pat, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe); + static InstMatchGenerator* mkInstMatchGenerator(Trigger* tparent, + Node q, + Node pat); /** mkInstMatchGenerator for the multi trigger case * * This linked list of InstMatchGenerator classes with one @@ -264,12 +246,9 @@ class InstMatchGenerator : public IMGenerator { * InstMatchGenerators corresponding to each unique subterm of pats with * free variables. */ - static InstMatchGenerator* mkInstMatchGeneratorMulti( - Node q, - std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe); + static InstMatchGenerator* mkInstMatchGeneratorMulti(Trigger* tparent, + Node q, + std::vector& pats); /** mkInstMatchGenerator * * This generates a linked list of InstMatchGenerators for each unique @@ -284,11 +263,9 @@ class InstMatchGenerator : public IMGenerator { * It calls initialize(...) for all InstMatchGenerators generated by this call. */ static InstMatchGenerator* mkInstMatchGenerator( + Trigger* tparent, Node q, std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe, std::map& pat_map_init); //-------------------------------end construction of inst match generators @@ -298,9 +275,7 @@ class InstMatchGenerator : public IMGenerator { * These are intentionally private, and are called during linked list * construction in mkInstMatchGenerator. */ - InstMatchGenerator(Node pat, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim); + InstMatchGenerator(Trigger* tparent, Node pat); /** The pattern we are producing matches for. * * This term and d_match_pattern can be different since this @@ -399,8 +374,7 @@ class InstMatchGenerator : public IMGenerator { * their match operator (see TermDatabase::getMatchOperator) is the same. * only valid for use where !d_match_pattern.isNull(). */ - int getMatch( - Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent); + int getMatch(Node q, Node t, InstMatch& m); /** Initialize this generator. * * q is the quantified formula associated with this generator. @@ -413,7 +387,6 @@ class InstMatchGenerator : public IMGenerator { * constructed in this way, it adds them to gens. */ void initialize(Node q, - QuantifiersEngine* qe, std::vector& gens); /** Continue next match * @@ -426,8 +399,6 @@ class InstMatchGenerator : public IMGenerator { */ int continueNextMatch(Node q, InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent, InferenceId id); /** Get inst match generator * @@ -435,11 +406,9 @@ class InstMatchGenerator : public IMGenerator { * appropriate matching algorithm for n within q * within a linked list of InstMatchGenerators. */ - static InstMatchGenerator* getInstMatchGenerator( - Node q, - Node n, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim); + static InstMatchGenerator* getInstMatchGenerator(Trigger* tparent, + Node q, + Node n); };/* class InstMatchGenerator */ } diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index a1674e89f..2920be1a2 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -25,13 +25,10 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatchGeneratorMulti::InstMatchGeneratorMulti( - Node q, - std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe) - : IMGenerator(qs, qim), d_quant(q) +InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent, + Node q, + std::vector& pats) + : IMGenerator(tparent), d_quant(q) { Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl; @@ -60,7 +57,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node n = pats[i]; // make the match generator InstMatchGenerator* img = - InstMatchGenerator::mkInstMatchGenerator(q, n, qs, qim, qe); + InstMatchGenerator::mkInstMatchGenerator(tparent, q, n); img->setActiveAdd(false); d_children.push_back(img); // compute unique/shared variables @@ -134,20 +131,20 @@ InstMatchGeneratorMulti::~InstMatchGeneratorMulti() /** reset instantiation round (call this whenever equivalence classes have * changed) */ -void InstMatchGeneratorMulti::resetInstantiationRound(QuantifiersEngine* qe) +void InstMatchGeneratorMulti::resetInstantiationRound() { for (InstMatchGenerator* c : d_children) { - c->resetInstantiationRound(qe); + c->resetInstantiationRound(); } } /** reset, eqc is the equivalence class to search in (any if eqc=null) */ -bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe) +bool InstMatchGeneratorMulti::reset(Node eqc) { for (InstMatchGenerator* c : d_children) { - if (!c->reset(eqc, qe)) + if (!c->reset(eqc)) { // do not return false here } @@ -155,9 +152,7 @@ bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe) return true; } -uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) +uint64_t InstMatchGeneratorMulti::addInstantiations(Node q) { uint64_t addedLemmas = 0; Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl; @@ -166,7 +161,7 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl; std::vector newMatches; InstMatch m(q); - while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0) + while (d_children[i]->getNextMatch(q, m) > 0) { // m.makeRepresentative( qe ); newMatches.push_back(InstMatch(&m)); @@ -179,8 +174,8 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl; - processNewMatch(qe, tparent, newMatches[j], i, addedLemmas); - if (qe->getState().isInConflict()) + processNewMatch(newMatches[j], i, addedLemmas); + if (d_qstate.isInConflict()) { return addedLemmas; } @@ -189,15 +184,12 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q, return addedLemmas; } -void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, +void InstMatchGeneratorMulti::processNewMatch(InstMatch& m, size_t fromChildIndex, uint64_t& addedLemmas) { // see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch( - qe->getState(), d_quant, m.d_vals); + d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.d_vals); // possibly only do the following if we know that new matches will be // produced? the issue is that instantiations are filtered in quantifiers // engine, and so there is no guarentee that @@ -207,9 +199,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, << "Child " << fromChildIndex << " produced match " << m << std::endl; // process new instantiations size_t childIndex = (fromChildIndex + 1) % d_children.size(); - processNewInstantiations(qe, - tparent, - m, + processNewInstantiations(m, addedLemmas, d_children_trie[childIndex].getTrie(), 0, @@ -218,9 +208,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, true); } -void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, +void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m, uint64_t& addedLemmas, InstMatchTrie* tr, size_t trieIndex, @@ -228,12 +216,11 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, size_t endChildIndex, bool modEq) { - Assert(!qe->getState().isInConflict()); + Assert(!d_qstate.isInConflict()); if (childIndex == endChildIndex) { // m is an instantiation - if (sendInstantiation( - tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT)) + if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT)) { addedLemmas++; Trace("multi-trigger-cache-debug") @@ -253,16 +240,14 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, { InstMatch mn(&m); mn.setValue(curr_index, d.first); - processNewInstantiations(qe, - tparent, - mn, + processNewInstantiations(mn, addedLemmas, &(d.second), trieIndex + 1, childIndex, endChildIndex, modEq); - if (qe->getState().isInConflict()) + if (d_qstate.isInConflict()) { break; } @@ -272,9 +257,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, std::map::iterator it = tr->d_data.find(n); if (it != tr->d_data.end()) { - processNewInstantiations(qe, - tparent, - m, + processNewInstantiations(m, addedLemmas, &(it->second), trieIndex + 1, @@ -286,7 +269,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, { return; } - quantifiers::QuantifiersState& qs = qe->getState(); + quantifiers::QuantifiersState& qs = d_qstate; // check modulo equality for other possible instantiations if (!qs.hasTerm(n)) { @@ -301,16 +284,14 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, std::map::iterator itc = tr->d_data.find(en); if (itc != tr->d_data.end()) { - processNewInstantiations(qe, - tparent, - m, + processNewInstantiations(m, addedLemmas, &(itc->second), trieIndex + 1, childIndex, endChildIndex, modEq); - if (qe->getState().isInConflict()) + if (d_qstate.isInConflict()) { break; } @@ -322,9 +303,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, else { size_t newChildIndex = (childIndex + 1) % d_children.size(); - processNewInstantiations(qe, - tparent, - m, + processNewInstantiations(m, addedLemmas, d_children_trie[newChildIndex].getTrie(), 0, diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index 53db94c67..85cbff7f0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -38,22 +38,16 @@ class InstMatchGeneratorMulti : public IMGenerator { public: /** constructors */ - InstMatchGeneratorMulti(Node q, - std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe); + InstMatchGeneratorMulti(Trigger* tparent, Node q, std::vector& pats); /** destructor */ ~InstMatchGeneratorMulti() override; /** Reset instantiation round. */ - void resetInstantiationRound(QuantifiersEngine* qe) override; + void resetInstantiationRound() override; /** Reset. */ - bool reset(Node eqc, QuantifiersEngine* qe) override; + bool reset(Node eqc) override; /** Add instantiations. */ - uint64_t addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) override; + uint64_t addInstantiations(Node q) override; private: /** process new match @@ -63,9 +57,7 @@ class InstMatchGeneratorMulti : public IMGenerator * addedLemmas is how many instantiations we succesfully send * via IMGenerator::sendInstantiation(...) calls. */ - void processNewMatch(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, + void processNewMatch(InstMatch& m, size_t fromChildIndex, uint64_t& addedLemmas); /** helper for process new match @@ -78,9 +70,7 @@ class InstMatchGeneratorMulti : public IMGenerator * computed by this function returns to. * modEq is whether we are matching modulo equality. */ - void processNewInstantiations(QuantifiersEngine* qe, - Trigger* tparent, - InstMatch& m, + void processNewInstantiations(InstMatch& m, uint64_t& addedLemmas, InstMatchTrie* tr, size_t trieIndex, diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index d70011bfb..ac7bb5f3c 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -25,11 +25,8 @@ namespace theory { namespace inst { InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( - Node q, - std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim) - : InstMatchGenerator(Node::null(), qs, qim) + Trigger* tparent, Node q, std::vector& pats) + : InstMatchGenerator(tparent, Node::null()) { // order patterns to maximize eager matching failures std::map > var_contains; @@ -105,7 +102,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( { Node po = pats_ordered[i]; Trace("multi-trigger-linear") << "...make for " << po << std::endl; - InstMatchGenerator* cimg = getInstMatchGenerator(q, po, qs, qim); + InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po); Assert(cimg != nullptr); d_children.push_back(cimg); // this could be improved @@ -116,11 +113,11 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( } } -int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe) +int InstMatchGeneratorMultiLinear::resetChildren() { for (InstMatchGenerator* c : d_children) { - if (!c->reset(Node::null(), qe)) + if (!c->reset(Node::null())) { return -2; } @@ -128,27 +125,24 @@ int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe) return 1; } -bool InstMatchGeneratorMultiLinear::reset(Node eqc, QuantifiersEngine* qe) +bool InstMatchGeneratorMultiLinear::reset(Node eqc) { Assert(eqc.isNull()); if (options::multiTriggerLinear()) { return true; } - return resetChildren(qe) > 0; + return resetChildren() > 0; } -int InstMatchGeneratorMultiLinear::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) +int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) { Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl; if (options::multiTriggerLinear()) { // reset everyone - int rc_ret = resetChildren(qe); + int rc_ret = resetChildren(); if (rc_ret < 0) { return rc_ret; @@ -158,8 +152,8 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl; Assert(d_next != nullptr); - int ret_val = continueNextMatch( - q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL); + int ret_val = + continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL); if (ret_val > 0) { Trace("multi-trigger-linear") diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index d83883df9..ce1e79229 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -68,21 +68,17 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator public: /** Reset. */ - bool reset(Node eqc, QuantifiersEngine* qe) override; + bool reset(Node eqc) override; /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; + int getNextMatch(Node q, InstMatch& m) override; protected: /** reset the children of this generator */ - int resetChildren(QuantifiersEngine* qe); + int resetChildren(); /** constructor */ - InstMatchGeneratorMultiLinear(Node q, - std::vector& pats, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim); + InstMatchGeneratorMultiLinear(Trigger* tparent, + Node q, + std::vector& pats); }; } // namespace inst diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 879bd50b9..eaf917545 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -28,13 +28,10 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatchGeneratorSimple::InstMatchGeneratorSimple( - Node q, - Node pat, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe) - : IMGenerator(qs, qim), d_quant(q), d_match_pattern(pat) +InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, + Node q, + Node pat) + : IMGenerator(tparent), d_quant(q), d_match_pattern(pat) { if (d_match_pattern.getKind() == NOT) { @@ -68,41 +65,40 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( } d_match_pattern_arg_types.push_back(d_match_pattern[i].getType()); } - d_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern); + quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + d_op = tdb->getMatchOperator(d_match_pattern); } -void InstMatchGeneratorSimple::resetInstantiationRound(QuantifiersEngine* qe) {} -uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) +void InstMatchGeneratorSimple::resetInstantiationRound() {} +uint64_t InstMatchGeneratorSimple::addInstantiations(Node q) { - quantifiers::QuantifiersState& qs = qe->getState(); uint64_t addedLemmas = 0; TNodeTrie* tat; + quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); if (d_eqc.isNull()) { - tat = qe->getTermDatabase()->getTermArgTrie(d_op); + tat = tdb->getTermArgTrie(d_op); } else { if (d_pol) { - tat = qe->getTermDatabase()->getTermArgTrie(d_eqc, d_op); + tat = tdb->getTermArgTrie(d_eqc, d_op); } else { // iterate over all classes except r - tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op); - if (tat && !qs.isInConflict()) + tat = tdb->getTermArgTrie(Node::null(), d_op); + if (tat && !d_qstate.isInConflict()) { - Node r = qs.getRepresentative(d_eqc); + Node r = d_qstate.getRepresentative(d_eqc); for (std::pair& t : tat->d_data) { if (t.first != r) { InstMatch m(q); - addInstantiations(m, qe, addedLemmas, 0, &(t.second), tparent); - if (qs.isInConflict()) + addInstantiations(m, addedLemmas, 0, &(t.second)); + if (d_qstate.isInConflict()) { break; } @@ -115,20 +111,18 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; - if (tat && !qs.isInConflict()) + if (tat && !d_qstate.isInConflict()) { InstMatch m(q); - addInstantiations(m, qe, addedLemmas, 0, tat, tparent); + addInstantiations(m, addedLemmas, 0, tat); } return addedLemmas; } void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, - QuantifiersEngine* qe, uint64_t& addedLemmas, size_t argIndex, - TNodeTrie* tat, - Trigger* tparent) + TNodeTrie* tat) { Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; @@ -150,15 +144,13 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } // we do not need the trigger parent for simple triggers (no post-processing // required) - if (sendInstantiation( - tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE)) + if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE)) { addedLemmas++; Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; } return; } - quantifiers::QuantifiersState& qs = qe->getState(); if (d_match_pattern[argIndex].getKind() == INST_CONSTANT) { int v = d_var_num[argIndex]; @@ -173,10 +165,9 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, if (prev.isNull() || prev == t) { m.setValue(v, t); - addInstantiations( - m, qe, addedLemmas, argIndex + 1, &(tt.second), tparent); + addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second)); m.setValue(v, prev); - if (qs.isInConflict()) + if (d_qstate.isInConflict()) { break; } @@ -186,18 +177,19 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } // inst constant from another quantified formula, treat as ground term? } - Node r = qs.getRepresentative(d_match_pattern[argIndex]); + Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]); std::map::iterator it = tat->d_data.find(r); if (it != tat->d_data.end()) { - addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second), tparent); + addInstantiations(m, addedLemmas, argIndex + 1, &(it->second)); } } -int InstMatchGeneratorSimple::getActiveScore(QuantifiersEngine* qe) +int InstMatchGeneratorSimple::getActiveScore() { - Node f = qe->getTermDatabase()->getMatchOperator(d_match_pattern); - size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f); + quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase(); + Node f = tdb->getMatchOperator(d_match_pattern); + size_t ngt = tdb->getNumGroundTerms(f); Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl; return static_cast(ngt); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index dd8746f71..bfb4b6840 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -49,20 +49,14 @@ class InstMatchGeneratorSimple : public IMGenerator { public: /** constructors */ - InstMatchGeneratorSimple(Node q, - Node pat, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim, - QuantifiersEngine* qe); + InstMatchGeneratorSimple(Trigger* tparent, Node q, Node pat); /** Reset instantiation round. */ - void resetInstantiationRound(QuantifiersEngine* qe) override; + void resetInstantiationRound() override; /** Add instantiations. */ - uint64_t addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) override; + uint64_t addInstantiations(Node q) override; /** Get active score. */ - int getActiveScore(QuantifiersEngine* qe) override; + int getActiveScore() override; private: /** quantified formula for the trigger term */ @@ -101,11 +95,9 @@ class InstMatchGeneratorSimple : public IMGenerator * tat is the term index we are currently traversing. */ void addInstantiations(InstMatch& m, - QuantifiersEngine* qe, uint64_t& addedLemmas, size_t argIndex, - TNodeTrie* tat, - Trigger* tparent); + TNodeTrie* tat); }; } // namespace inst diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 7d397403d..62a63a2d5 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -69,19 +69,17 @@ Trigger::Trigger(QuantifiersEngine* qe, if( d_nodes.size()==1 ){ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) { - d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qs, qim, qe); + d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); ++(qe->d_statistics.d_triggers); }else{ - d_mg = - InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qs, qim, qe); + d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); ++(qe->d_statistics.d_simple_triggers); } }else{ if( options::multiTriggerCache() ){ - d_mg = new InstMatchGeneratorMulti(q, d_nodes, qs, qim, qe); + d_mg = new InstMatchGeneratorMulti(this, q, d_nodes); }else{ - d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( - q, d_nodes, qs, qim, qe); + d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes); } if (Trace.isOn("multi-trigger")) { @@ -101,13 +99,9 @@ Trigger::~Trigger() { delete d_mg; } -void Trigger::resetInstantiationRound(){ - d_mg->resetInstantiationRound( d_quantEngine ); -} +void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); } -void Trigger::reset( Node eqc ){ - d_mg->reset( eqc, d_quantEngine ); -} +void Trigger::reset(Node eqc) { d_mg->reset(eqc); } bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } @@ -138,7 +132,7 @@ uint64_t Trigger::addInstantiations() } } } - uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this); + uint64_t addedLemmas = d_mg->addInstantiations(d_quant); if (Debug.isOn("inst-trigger")) { if (addedLemmas > 0) @@ -316,9 +310,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars); } -int Trigger::getActiveScore() { - return d_mg->getActiveScore( d_quantEngine ); -} +int Trigger::getActiveScore() { return d_mg->getActiveScore(); } Node Trigger::ensureGroundTermPreprocessed(Valuation& val, Node n, diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 31661e611..b5a271fae 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -247,7 +247,7 @@ class Trigger { * This example would fail to match when f(a) is not registered. */ std::vector d_groundTerms; - /** The quantifiers engine associated with this trigger. */ + // !!!!!!!!!!!!!!!!!! temporarily available (project #15) QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers state */ quantifiers::QuantifiersState& d_qstate; diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 20e157808..c8d907bcf 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -23,12 +23,10 @@ namespace CVC4 { namespace theory { namespace inst { -VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( - Node var, - Node subs, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim) - : InstMatchGenerator(Node::null(), qs, qim), +VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent, + Node var, + Node subs) + : InstMatchGenerator(tparent, Node::null()), d_var(var), d_subs(subs), d_rm_prev(false) @@ -37,16 +35,13 @@ VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( d_var_type = d_var.getType(); } -bool VarMatchGeneratorTermSubs::reset(Node eqc, QuantifiersEngine* qe) +bool VarMatchGeneratorTermSubs::reset(Node eqc) { d_eq_class = eqc; return true; } -int VarMatchGeneratorTermSubs::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) +int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m) { int ret_val = -1; if (!d_eq_class.isNull()) @@ -61,14 +56,14 @@ 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->getState(), d_children_types[0], s)) + if (!m.set(d_qstate, d_children_types[0], s)) { return -1; } else { ret_val = continueNextMatch( - q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN); + q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN); if (ret_val > 0) { return ret_val; diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index 910dbc79b..591c47958 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -31,18 +31,12 @@ namespace inst { class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: - VarMatchGeneratorTermSubs(Node var, - Node subs, - quantifiers::QuantifiersState& qs, - quantifiers::QuantifiersInferenceManager& qim); + VarMatchGeneratorTermSubs(Trigger* tparent, Node var, Node subs); /** Reset */ - bool reset(Node eqc, QuantifiersEngine* qe) override; + bool reset(Node eqc) override; /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; + int getNextMatch(Node q, InstMatch& m) override; private: /** variable we are matching (x in the example x+1). */ -- 2.30.2