From dc6a56da3c03fc6ba110f5a3292fd3cdcc0f36b1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Feb 2021 19:51:21 -0600 Subject: [PATCH] Add state and inference manager to inst match generator (#5968) In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities. --- .../ematching/inst_match_generator.cpp | 100 +++++++++++------- .../ematching/inst_match_generator.h | 66 ++++++++---- .../ematching/inst_match_generator_multi.cpp | 13 ++- .../ematching/inst_match_generator_multi.h | 2 + .../inst_match_generator_multi_linear.cpp | 8 +- .../inst_match_generator_multi_linear.h | 3 +- .../ematching/inst_match_generator_simple.cpp | 11 +- .../ematching/inst_match_generator_simple.h | 6 +- src/theory/quantifiers/ematching/trigger.cpp | 10 +- .../ematching/var_match_generator.cpp | 11 +- .../ematching/var_match_generator.h | 5 +- 11 files changed, 158 insertions(+), 77 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 4cdb207f3..ce535d5e8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -35,27 +35,33 @@ namespace CVC4 { namespace theory { namespace inst { +IMGenerator::IMGenerator(quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim) + : d_qstate(qs), d_qim(qim) +{ +} + bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m) { return tparent->sendInstantiation(m); } -InstMatchGenerator::InstMatchGenerator( Node pat ){ +InstMatchGenerator::InstMatchGenerator( + Node pat, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim) + : IMGenerator(qs, qim) +{ d_cg = nullptr; d_needsReset = true; d_active_add = true; - Assert(quantifiers::TermUtil::hasInstConstAttr(pat)); + Assert(pat.isNull() || quantifiers::TermUtil::hasInstConstAttr(pat)); d_pattern = pat; d_match_pattern = pat; - d_match_pattern_type = pat.getType(); - d_next = nullptr; - d_independent_gen = false; -} - -InstMatchGenerator::InstMatchGenerator() { - d_cg = nullptr; - d_needsReset = true; - d_active_add = true; + if (!pat.isNull()) + { + d_match_pattern_type = pat.getType(); + } d_next = nullptr; d_independent_gen = false; } @@ -186,7 +192,8 @@ void InstMatchGenerator::initialize(Node q, } else { - InstMatchGenerator* cimg = getInstMatchGenerator(q, pat); + InstMatchGenerator* cimg = + getInstMatchGenerator(q, pat, d_qstate, d_qim); if (cimg) { d_children.push_back(cimg); @@ -286,7 +293,6 @@ int InstMatchGenerator::getMatch( Trace("matching-fail") << "Internal error for match generator." << std::endl; return -2; } - quantifiers::QuantifiersState& qs = qe->getState(); bool success = true; std::vector prev; // if t is null @@ -304,7 +310,7 @@ int InstMatchGenerator::getMatch( Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..." << std::endl; bool addToPrev = m.get(ct).isNull(); - if (!m.set(qs, ct, t[i])) + if (!m.set(d_qstate, ct, t[i])) { // match is in conflict Trace("matching-fail") @@ -320,7 +326,7 @@ int InstMatchGenerator::getMatch( } else if (ct == -1) { - if (!qs.areEqual(d_match_pattern[i], t[i])) + if (!d_qstate.areEqual(d_match_pattern[i], t[i])) { Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; @@ -336,7 +342,7 @@ int InstMatchGenerator::getMatch( if (d_match_pattern.getKind() == INST_CONSTANT) { bool addToPrev = m.get(d_children_types[0]).isNull(); - if (!m.set(qs, d_children_types[0], t)) + if (!m.set(d_qstate, d_children_types[0], t)) { success = false; } @@ -372,7 +378,7 @@ int InstMatchGenerator::getMatch( { if (t.getType().isBoolean()) { - t_match = nm->mkConst(!qs.areEqual(nm->mkConst(true), t)); + t_match = nm->mkConst(!d_qstate.areEqual(nm->mkConst(true), t)); } else { @@ -392,7 +398,7 @@ int InstMatchGenerator::getMatch( if (!t_match.isNull()) { bool addToPrev = m.get(v).isNull(); - if (!m.set(qs, v, t_match)) + if (!m.set(d_qstate, v, t_match)) { success = false; } @@ -468,7 +474,7 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ // we did not properly initialize the candidate generator, thus we fail return false; } - eqc = qe->getState().getRepresentative(eqc); + eqc = d_qstate.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; @@ -510,7 +516,7 @@ int InstMatchGenerator::getNextMatch(Node f, Node t = d_curr_first_candidate; do{ Trace("matching-debug2") << "Matching candidate : " << t << std::endl; - Assert(!qe->getState().isInConflict()); + Assert(!d_qstate.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() ){ @@ -524,8 +530,7 @@ int InstMatchGenerator::getNextMatch(Node f, } //get the next candidate term t if( success<0 ){ - t = qe->getState().isInConflict() ? Node::null() - : d_cg->getNextCandidate(); + t = d_qstate.isInConflict() ? Node::null() : d_cg->getNextCandidate(); }else{ d_curr_first_candidate = d_cg->getNextCandidate(); } @@ -556,14 +561,14 @@ uint64_t InstMatchGenerator::addInstantiations(Node f, if (sendInstantiation(tparent, m)) { addedLemmas++; - if (qe->getState().isInConflict()) + if (d_qstate.isInConflict()) { break; } } }else{ addedLemmas++; - if (qe->getState().isInConflict()) + if (d_qstate.isInConflict()) { break; } @@ -574,17 +579,29 @@ uint64_t InstMatchGenerator::addInstantiations(Node f, return addedLemmas; } - -InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) { +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( + Node q, + Node pat, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe) +{ std::vector< Node > pats; pats.push_back( pat ); std::map< Node, InstMatchGenerator * > pat_map_init; - return mkInstMatchGenerator( q, pats, qe, pat_map_init ); + return mkInstMatchGenerator(q, pats, qs, qim, qe, pat_map_init); } -InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) { +InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( + Node q, + std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe) +{ Assert(pats.size() > 1); - InstMatchGeneratorMultiLinear * imgm = new InstMatchGeneratorMultiLinear( q, pats, qe ); + InstMatchGeneratorMultiLinear* imgm = + new InstMatchGeneratorMultiLinear(q, pats, qs, qim); std::vector< InstMatchGenerator* > gens; imgm->initialize(q, qe, gens); Assert(gens.size() == pats.size()); @@ -597,12 +614,18 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std:: pat_map_init[pn] = g; } //return mkInstMatchGenerator( q, patsn, qe, pat_map_init ); - imgm->d_next = mkInstMatchGenerator( q, patsn, qe, pat_map_init ); + imgm->d_next = mkInstMatchGenerator(q, patsn, qs, qim, qe, pat_map_init); return imgm; } -InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe, - std::map< Node, InstMatchGenerator * >& pat_map_init ) { +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( + Node q, + std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe, + std::map& pat_map_init) +{ size_t pCounter = 0; InstMatchGenerator* prev = NULL; InstMatchGenerator* oinit = NULL; @@ -612,7 +635,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vecto 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]); + init = new InstMatchGenerator(pats[pCounter], qs, qim); }else{ init = iti->second; } @@ -635,7 +658,11 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vecto return oinit; } -InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) +InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator( + Node q, + Node n, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim) { if (n.getKind() != INST_CONSTANT) { @@ -657,13 +684,14 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) if (!x.isNull()) { Node s = PatternTermSelector::getInversion(n, x); - VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s); + VarMatchGeneratorTermSubs* vmg = + new VarMatchGeneratorTermSubs(x, s, qs, qim); Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl; return vmg; } } - return new InstMatchGenerator(n); + return new InstMatchGenerator(n, qs, qim); } }/* 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 b5c81b766..135a1e8dd 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -26,6 +26,11 @@ namespace theory { class QuantifiersEngine; +namespace quantifiers { +class QuantifiersState; +class QuantifiersInferenceManager; +} // namespace quantifiers + namespace inst { class Trigger; @@ -49,21 +54,23 @@ class Trigger; */ class IMGenerator { public: - virtual ~IMGenerator() {} - /** Reset instantiation round. + IMGenerator(quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim); + virtual ~IMGenerator() {} + /** Reset instantiation round. * * Called once at beginning of an instantiation round. */ - virtual void resetInstantiationRound(QuantifiersEngine* qe) {} - /** Reset. + virtual void resetInstantiationRound(QuantifiersEngine* qe) {} + /** Reset. * * eqc is the equivalence class to search in (any if eqc=null). * Returns true if this generator can produce instantiations, and false * 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; } - /** Get the next match. + virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; } + /** Get the next match. * * Must call reset( eqc ) before this function. This constructs an * instantiation, which it populates in data structure m, @@ -74,12 +81,12 @@ public: * * Returns a value >0 if an instantiation was successfully generated */ - virtual int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) - { - return 0; + virtual int getNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent) + { + return 0; } /** add instantiations * @@ -112,6 +119,10 @@ public: * lemma cache. */ bool sendInstantiation(Trigger* tparent, InstMatch& m); + /** The state of the quantifiers engine */ + quantifiers::QuantifiersState& d_qstate; + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& d_qim; };/* class IMGenerator */ class CandidateGenerator; @@ -239,9 +250,12 @@ 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, - QuantifiersEngine* qe); + static InstMatchGenerator* mkInstMatchGenerator( + Node q, + Node pat, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe); /** mkInstMatchGenerator for the multi trigger case * * This linked list of InstMatchGenerator classes with one @@ -249,9 +263,12 @@ class InstMatchGenerator : public IMGenerator { * InstMatchGenerators corresponding to each unique subterm of pats with * free variables. */ - static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q, - std::vector& pats, - QuantifiersEngine* qe); + static InstMatchGenerator* mkInstMatchGeneratorMulti( + Node q, + std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe); /** mkInstMatchGenerator * * This generates a linked list of InstMatchGenerators for each unique @@ -268,6 +285,8 @@ class InstMatchGenerator : public IMGenerator { static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, QuantifiersEngine* qe, std::map& pat_map_init); //-------------------------------end construction of inst match generators @@ -278,8 +297,9 @@ class InstMatchGenerator : public IMGenerator { * These are intentionally private, and are called during linked list * construction in mkInstMatchGenerator. */ - InstMatchGenerator(Node pat); - InstMatchGenerator(); + InstMatchGenerator(Node pat, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim); /** The pattern we are producing matches for. * * This term and d_match_pattern can be different since this @@ -413,7 +433,11 @@ class InstMatchGenerator : public IMGenerator { * appropriate matching algorithm for n within q * within a linked list of InstMatchGenerators. */ - static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); + static InstMatchGenerator* getInstMatchGenerator( + Node q, + Node n, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim); };/* 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 e4fb3fc41..5c5dcfef1 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -23,10 +23,13 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q, - std::vector& pats, - QuantifiersEngine* qe) - : d_quant(q) +InstMatchGeneratorMulti::InstMatchGeneratorMulti( + Node q, + std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe) + : IMGenerator(qs, qim), d_quant(q) { Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl; @@ -55,7 +58,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q, Node n = pats[i]; // make the match generator InstMatchGenerator* img = - InstMatchGenerator::mkInstMatchGenerator(q, n, qe); + InstMatchGenerator::mkInstMatchGenerator(q, n, qs, qim, qe); img->setActiveAdd(false); d_children.push_back(img); // compute unique/shared variables diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index 2007e652d..846996668 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -40,6 +40,8 @@ class InstMatchGeneratorMulti : public IMGenerator /** constructors */ InstMatchGeneratorMulti(Node q, std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, QuantifiersEngine* qe); /** destructor */ ~InstMatchGeneratorMulti() override; 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 1eb9ccdad..66433ba78 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -22,7 +22,11 @@ namespace theory { namespace inst { InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( - Node q, std::vector& pats, QuantifiersEngine* qe) + Node q, + std::vector& pats, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim) + : InstMatchGenerator(Node::null(), qs, qim) { // order patterns to maximize eager matching failures std::map > var_contains; @@ -98,7 +102,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( { Node po = pats_ordered[i]; Trace("multi-trigger-linear") << "...make for " << po << std::endl; - InstMatchGenerator* cimg = getInstMatchGenerator(q, po); + InstMatchGenerator* cimg = getInstMatchGenerator(q, po, qs, qim); Assert(cimg != nullptr); d_children.push_back(cimg); // this could be improved 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 245b3d794..81a37b0f8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -81,7 +81,8 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator /** constructor */ InstMatchGeneratorMultiLinear(Node q, std::vector& pats, - QuantifiersEngine* qe); + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim); }; } // 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 a46eb12ce..39dd8ed22 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -22,10 +22,13 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q, - Node pat, - QuantifiersEngine* qe) - : d_quant(q), d_match_pattern(pat) +InstMatchGeneratorSimple::InstMatchGeneratorSimple( + Node q, + Node pat, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe) + : IMGenerator(qs, qim), d_quant(q), d_match_pattern(pat) { if (d_match_pattern.getKind() == NOT) { diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 243050772..9a01498ef 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -49,7 +49,11 @@ class InstMatchGeneratorSimple : public IMGenerator { public: /** constructors */ - InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe); + InstMatchGeneratorSimple(Node q, + Node pat, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + QuantifiersEngine* qe); /** Reset instantiation round. */ void resetInstantiationRound(QuantifiersEngine* qe) override; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index d57c3356e..79bd5c1dd 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -64,17 +64,19 @@ Trigger::Trigger(QuantifiersEngine* qe, if( d_nodes.size()==1 ){ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) { - d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe); + d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qs, qim, qe); ++(qe->d_statistics.d_triggers); }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe); + d_mg = + InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qs, qim, qe); ++(qe->d_statistics.d_simple_triggers); } }else{ if( options::multiTriggerCache() ){ - d_mg = new InstMatchGeneratorMulti(q, d_nodes, qe); + d_mg = new InstMatchGeneratorMulti(q, d_nodes, qs, qim, qe); }else{ - d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe); + d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( + q, d_nodes, qs, qim, qe); } if (Trace.isOn("multi-trigger")) { diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 4edacb827..8448fe810 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -21,8 +21,15 @@ namespace CVC4 { namespace theory { namespace inst { -VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Node var, Node subs) - : InstMatchGenerator(), d_var(var), d_subs(subs), d_rm_prev(false) +VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( + Node var, + Node subs, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim) + : InstMatchGenerator(Node::null(), qs, qim), + d_var(var), + d_subs(subs), + d_rm_prev(false) { d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); d_var_type = d_var.getType(); diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index c1030e11d..7e64fed36 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -32,7 +32,10 @@ namespace inst { class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: - VarMatchGeneratorTermSubs(Node var, Node subs); + VarMatchGeneratorTermSubs(Node var, + Node subs, + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim); /** Reset */ bool reset(Node eqc, QuantifiersEngine* qe) override; -- 2.30.2