Simplify interface to instantiate (#5926)

Does not support InstMatch interfaces anymore, which are spurious.

6 files changed, 8 insertions, 6 deletions

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 4c606a273..875c74aa4 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -368,7 +368,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
   }
 }
 
@@ -381,7 +381,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
   }
   else
   {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index f03d1cf20..b5c81b766 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -19,7 +19,7 @@
 
 #include <map>
 #include "expr/node_trie.h"
-#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/inst_match.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 4f393bc4f..e4fb3fc41 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -191,7 +191,8 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
                                               uint64_t& addedLemmas)
 {
   // see if these produce new matches
-  d_children_trie[fromChildIndex].addInstMatch(qe->getState(), d_quant, m);
+  d_children_trie[fromChildIndex].addInstMatch(
+      qe->getState(), 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
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index b68d362cc..2007e652d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -21,6 +21,7 @@
 #include <vector>
 #include "expr/node_trie.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
+#include "theory/quantifiers/inst_match_trie.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index b5ef7792d..a46eb12ce 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -140,7 +140,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // we do not need the trigger parent for simple triggers (no post-processing
     // required)
-    if (qe->getInstantiate()->addInstantiation(d_quant, m))
+    if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals))
     {
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index ac43d3bc9..8d9cfd3a3 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -143,7 +143,7 @@ uint64_t Trigger::addInstantiations()
 
 bool Trigger::sendInstantiation(InstMatch& m)
 {
-  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
 }
 
 bool Trigger::mkTriggerTerms(Node q,