Eliminating dependencies from inst utils (#5882)

Towards eliminating dependence on QuantifierEngine from inst_match_trie.

diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 371bc337880ca85505b739a555e63c5c8034242b..a0114ba80316e95b2e6031aea03a5cc3f4a6acd7 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -191,7 +191,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
                                               uint64_t& addedLemmas)
 {
   // see if these produce new matches
-  d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
+  d_children_trie[fromChildIndex].addInstMatch(qe->getState(), d_quant, m);
   // 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/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 0bd5000f1835abbcfb4fc4ad8b9cf13dadde91f8..0eef03d9de3d155c01664f2c567b266cf6275adf 100644 (file)
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 
@@ -25,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
+bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
                                  Node f,
                                  std::vector<Node>& m,
                                  bool modEq,
@@ -44,7 +45,7 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   if (it != d_data.end())
   {
     bool ret =
-        it->second.addInstMatch(qe, f, m, modEq, imtio, onlyExist, index + 1);
+        it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1);
     if (!onlyExist || !ret)
     {
       return ret;
@@ -52,7 +53,6 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   }
   if (modEq)
   {
-    quantifiers::QuantifiersState& qs = qe->getState();
     // check modulo equality if any other instantiation match exists
     if (!n.isNull() && qs.hasTerm(n))
     {
@@ -66,7 +66,7 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
           if (itc != d_data.end())
           {
             if (itc->second.addInstMatch(
-                    qe, f, m, modEq, imtio, true, index + 1))
+                    qs, f, m, modEq, imtio, true, index + 1))
             {
               return false;
             }
@@ -78,7 +78,7 @@ bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   }
   if (!onlyExist)
   {
-    d_data[n].addInstMatch(qe, f, m, modEq, imtio, false, index + 1);
+    d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1);
   }
   return true;
 }
@@ -291,10 +291,9 @@ CDInstMatchTrie::~CDInstMatchTrie()
   d_data.clear();
 }
 
-bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
+bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
                                    Node f,
                                    std::vector<Node>& m,
-                                   context::Context* c,
                                    bool modEq,
                                    unsigned index,
                                    bool onlyExist)
@@ -320,8 +319,7 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
   if (it != d_data.end())
   {
-    bool ret =
-        it->second->addInstMatch(qe, f, m, c, modEq, index + 1, onlyExist);
+    bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist);
     if (!onlyExist || !ret)
     {
       return reset || ret;
@@ -330,7 +328,6 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
   if (modEq)
   {
     // check modulo equality if any other instantiation match exists
-    quantifiers::QuantifiersState& qs = qe->getState();
     if (!n.isNull() && qs.hasTerm(n))
     {
       eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
@@ -342,7 +339,7 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
           std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
           if (itc != d_data.end())
           {
-            if (itc->second->addInstMatch(qe, f, m, c, modEq, index + 1, true))
+            if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true))
             {
               return false;
             }
@@ -355,11 +352,10 @@ bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe,
 
   if (!onlyExist)
   {
-    // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
-    CDInstMatchTrie* imt = new CDInstMatchTrie(c);
+    CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
     Assert(d_data.find(n) == d_data.end());
     d_data[n] = imt;
-    imt->addInstMatch(qe, f, m, c, modEq, index + 1, false);
+    imt->addInstMatch(qs, f, m, modEq, index + 1, false);
   }
   return true;
 }

diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index c978a6952ebddfc202b9d93d64cd768c6df33dd8..51b19f2efab3524aa3837993e5ca9b756f988333 100644 (file)
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -29,6 +29,10 @@ namespace theory {
 
 class QuantifiersEngine;
 
+namespace {
+class QuantifiersState;
+}
+
 namespace inst {
 
 /** trie for InstMatch objects
@@ -57,26 +61,26 @@ class InstMatchTrie
    * The domain of m is the bound variables of quantified formula q.
    * It returns true if (the suffix) of m exists in this trie.
    * If modEq is true, we check for duplication modulo equality the current
-   * equalities in the active equality engine of qe.
+   * equalities in the equality engine of qs.
    */
-  bool existsInstMatch(QuantifiersEngine* qe,
+  bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
                        InstMatch& m,
                        bool modEq = false,
                        ImtIndexOrder* imtio = NULL,
                        unsigned index = 0)
   {
-    return !addInstMatch(qe, q, m, modEq, imtio, true, index);
+    return !addInstMatch(qs, q, m, modEq, imtio, true, index);
   }
   /** exists inst match, vector version */
-  bool existsInstMatch(QuantifiersEngine* qe,
+  bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
                        std::vector<Node>& m,
                        bool modEq = false,
                        ImtIndexOrder* imtio = NULL,
                        unsigned index = 0)
   {
-    return !addInstMatch(qe, q, m, modEq, imtio, true, index);
+    return !addInstMatch(qs, q, m, modEq, imtio, true, index);
   }
   /** add inst match
    *
@@ -84,9 +88,9 @@ class InstMatchTrie
    * trie, and returns true if and only if m did not already occur in this trie.
    * The domain of m is the bound variables of quantified formula q.
    * If modEq is true, we check for duplication modulo equality the current
-   * equalities in the active equality engine of qe.
+   * equalities in the equality engine of qs.
    */
-  bool addInstMatch(QuantifiersEngine* qe,
+  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
                     InstMatch& m,
                     bool modEq = false,
@@ -94,10 +98,10 @@ class InstMatchTrie
                     bool onlyExist = false,
                     unsigned index = 0)
   {
-    return addInstMatch(qe, q, m.d_vals, modEq, imtio, onlyExist, index);
+    return addInstMatch(qs, q, m.d_vals, modEq, imtio, onlyExist, index);
   }
   /** add inst match, vector version */
-  bool addInstMatch(QuantifiersEngine* qe,
+  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node f,
                     std::vector<Node>& m,
                     bool modEq = false,
@@ -235,27 +239,25 @@ class CDInstMatchTrie
    * The domain of m is the bound variables of quantified formula q.
    * It returns true if (the suffix) of m exists in this trie.
    * If modEq is true, we check for duplication modulo equality the current
-   * equalities in the active equality engine of qe.
+   * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool existsInstMatch(QuantifiersEngine* qe,
+  bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
                        InstMatch& m,
-                       context::Context* c,
                        bool modEq = false,
                        unsigned index = 0)
   {
-    return !addInstMatch(qe, q, m, c, modEq, index, true);
+    return !addInstMatch(qs, q, m, modEq, index, true);
   }
   /** exists inst match, vector version */
-  bool existsInstMatch(QuantifiersEngine* qe,
+  bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
                        std::vector<Node>& m,
-                       context::Context* c,
                        bool modEq = false,
                        unsigned index = 0)
   {
-    return !addInstMatch(qe, q, m, c, modEq, index, true);
+    return !addInstMatch(qs, q, m, modEq, index, true);
   }
   /** add inst match
    *
@@ -263,24 +265,22 @@ class CDInstMatchTrie
    * trie, and returns true if and only if m did not already occur in this trie.
    * The domain of m is the bound variables of quantified formula q.
    * If modEq is true, we check for duplication modulo equality the current
-   * equalities in the active equality engine of qe.
+   * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool addInstMatch(QuantifiersEngine* qe,
+  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
                     InstMatch& m,
-                    context::Context* c,
                     bool modEq = false,
                     unsigned index = 0,
                     bool onlyExist = false)
   {
-    return addInstMatch(qe, q, m.d_vals, c, modEq, index, onlyExist);
+    return addInstMatch(qs, q, m.d_vals, modEq, index, onlyExist);
   }
   /** add inst match, vector version */
-  bool addInstMatch(QuantifiersEngine* qe,
+  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
                     std::vector<Node>& m,
-                    context::Context* c,
                     bool modEq = false,
                     unsigned index = 0,
                     bool onlyExist = false);
@@ -413,27 +413,27 @@ class InstMatchTrieOrdered
    *
    * This method returns true if the match m was not previously added to this
    * class. If modEq is true, we consider duplicates modulo the current
-   * equalities stored in the active equality engine of quantifiers engine.
+   * equalities stored in the equality engine of qs.
    */
-  bool addInstMatch(QuantifiersEngine* qe,
+  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
                     InstMatch& m,
                     bool modEq = false)
   {
-    return d_imt.addInstMatch(qe, q, m, modEq, d_imtio);
+    return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
   }
   /** returns true if this trie contains m
    *
    * This method returns true if the match m exists in this
    * class. If modEq is true, we consider duplicates modulo the current
-   * equalities stored in the active equality engine of quantifiers engine.
+   * equalities stored in the equality engine of qs.
    */
-  bool existsInstMatch(QuantifiersEngine* qe,
+  bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
                        InstMatch& m,
                        bool modEq = false)
   {
-    return d_imt.existsInstMatch(qe, q, m, modEq, d_imtio);
+    return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
   }
 
  private:

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 4db53c4b7025742d5ce3ad2e37d0f722c81e1307..36179673529ec9eb66a613870aa14b39d11fdd72 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -419,8 +419,7 @@ bool Instantiate::existsInstantiation(Node q,
         d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
-      return it->second->existsInstMatch(
-          d_qe, q, terms, d_qstate.getUserContext(), modEq);
+      return it->second->existsInstMatch(d_qstate, q, terms, modEq);
     }
   }
   else
@@ -429,7 +428,7 @@ bool Instantiate::existsInstantiation(Node q,
         d_inst_match_trie.find(q);
     if (it != d_inst_match_trie.end())
     {
-      return it->second.existsInstMatch(d_qe, q, terms, modEq);
+      return it->second.existsInstMatch(d_qstate, q, terms, modEq);
     }
   }
   return false;
@@ -519,10 +518,10 @@ bool Instantiate::recordInstantiationInternal(Node q,
       d_c_inst_match_trie[q] = imt;
     }
     d_c_inst_match_trie_dom.insert(q);
-    return imt->addInstMatch(d_qe, q, terms, d_qstate.getUserContext(), modEq);
+    return imt->addInstMatch(d_qstate, q, terms, modEq);
   }
   Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-  return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq);
+  return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms, modEq);
 }
 
 bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)