Add state and inference manager to inst match generator (#5968)

In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 4cdb207f3262e8304bcc3277ba3e9b49ae09bf35..ce535d5e89d81dbb803d512dab42c535888510fb 100644 (file)
--- 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<int> 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<Node>& 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<Node>& pats,
+    quantifiers::QuantifiersState& qs,
+    quantifiers::QuantifiersInferenceManager& qim,
+    QuantifiersEngine* qe,
+    std::map<Node, InstMatchGenerator*>& 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 b5c81b76680114c415ad917eb04f4280506133a6..135a1e8dd6f6145892fe60a1eabc0310a83df1eb 100644 (file)
--- 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<Node>& pats,
-                                                       QuantifiersEngine* qe);
+  static InstMatchGenerator* mkInstMatchGeneratorMulti(
+      Node q,
+      std::vector<Node>& 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<Node>& pats,
+      quantifiers::QuantifiersState& qs,
+      quantifiers::QuantifiersInferenceManager& qim,
       QuantifiersEngine* qe,
       std::map<Node, InstMatchGenerator*>& 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 e4fb3fc41cbbbb96aec6506c1f8c037786edd8b6..5c5dcfef195af54b676e1519f4c14a3ff9e39599 100644 (file)
--- 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<Node>& pats,
-                                                 QuantifiersEngine* qe)
-    : d_quant(q)
+InstMatchGeneratorMulti::InstMatchGeneratorMulti(
+    Node q,
+    std::vector<Node>& 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 2007e652ddc0de18b9783cbf7e2a5fc071b9b587..84699666826277ffb776d752a21545bb1a298519 100644 (file)
--- 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<Node>& 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 1eb9ccdad061ac51c53cb683cf4bd698beb2bf95..66433ba7835b96c03fe14986c1a6e38465ca7822 100644 (file)
--- 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<Node>& pats, QuantifiersEngine* qe)
+    Node q,
+    std::vector<Node>& pats,
+    quantifiers::QuantifiersState& qs,
+    quantifiers::QuantifiersInferenceManager& qim)
+    : InstMatchGenerator(Node::null(), qs, qim)
 {
   // order patterns to maximize eager matching failures
   std::map<Node, std::vector<Node> > 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 245b3d7942030c1a018c93f9c6d813fb2c04c282..81a37b0f8c0fff5a666fb852d99dbb0c6efe1f94 100644 (file)
--- 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<Node>& 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 a46eb12ce7669e858e59b9f76ad3493a90189622..39dd8ed22ee8cfce0281d829733228c5c2347dac 100644 (file)
--- 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 2430507721ad5db99473fd06606bcb9fa848c2de..9a01498ef44420a6746afc31bd34d8fb9d9d5e15 100644 (file)
--- 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 d57c3356e67b7aa046d60fc8d9ff7befd7413aef..79bd5c1ddc1bdec51b471085232292fd442833b2 100644 (file)
--- 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 4edacb827a21c36de062056dc6d112ffb11cfc7b..8448fe8102391c85cd8dbef303cf6d8ee939ec57 100644 (file)
--- 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 c1030e11d57403b5a53e00614d80102ebced3853..7e64fed363e81d55f01ea5ff594969eea98ed90c 100644 (file)
--- 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;