Simplify interface to instantiate (#5926)

Does not support InstMatch interfaces anymore, which are spurious.

1 files changed, 25 insertions, 138 deletions

diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index c8d0214b6..c45badc38 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief inst match class
+ ** \brief inst match trie class
  **/
 
 #include "cvc4_private.h"
@@ -22,14 +22,13 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "expr/node.h"
-#include "theory/quantifiers/inst_match.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
 
-namespace {
+namespace quantifiers {
 class QuantifiersState;
 }
 
@@ -65,23 +64,10 @@ class InstMatchTrie
    */
   bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
-                       InstMatch& m,
+                       const std::vector<Node>& m,
                        bool modEq = false,
-                       ImtIndexOrder* imtio = NULL,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, imtio, true, index);
-  }
-  /** exists inst match, vector version */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
-                       Node q,
-                       std::vector<Node>& m,
-                       bool modEq = false,
-                       ImtIndexOrder* imtio = NULL,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, imtio, true, index);
-  }
+                       ImtIndexOrder* imtio = nullptr,
+                       unsigned index = 0);
   /** add inst match
    *
    * This method adds (the suffix of) m starting at the given index to this
@@ -91,21 +77,10 @@ class InstMatchTrie
    * equalities in the equality engine of qs.
    */
   bool addInstMatch(quantifiers::QuantifiersState& qs,
-                    Node q,
-                    InstMatch& m,
-                    bool modEq = false,
-                    ImtIndexOrder* imtio = NULL,
-                    bool onlyExist = false,
-                    unsigned index = 0)
-  {
-    return addInstMatch(qs, q, m.d_vals, modEq, imtio, onlyExist, index);
-  }
-  /** add inst match, vector version */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node f,
-                    std::vector<Node>& m,
+                    const std::vector<Node>& m,
                     bool modEq = false,
-                    ImtIndexOrder* imtio = NULL,
+                    ImtIndexOrder* imtio = nullptr,
                     bool onlyExist = false,
                     unsigned index = 0);
   /** remove inst match
@@ -115,8 +90,8 @@ class InstMatchTrie
    * The domain of m is the bound variables of quantified formula q.
    */
   bool removeInstMatch(Node f,
-                       std::vector<Node>& m,
-                       ImtIndexOrder* imtio = NULL,
+                       const std::vector<Node>& m,
+                       ImtIndexOrder* imtio = nullptr,
                        unsigned index = 0);
   /**
    * Adds the instantiations for q into insts.
@@ -124,16 +99,9 @@ class InstMatchTrie
   void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
 
   /** clear the data of this class */
-  void clear() { d_data.clear(); }
+  void clear();
   /** print this class */
-  void print(std::ostream& out,
-             Node q,
-             bool useActive,
-             std::vector<Node>& active) const
-  {
-    std::vector<TNode> terms;
-    print(out, q, terms, useActive, active);
-  }
+  void print(std::ostream& out, Node q) const;
   /** the data */
   std::map<Node, InstMatchTrie> d_data;
 
@@ -145,21 +113,7 @@ class InstMatchTrie
   /** helper for print
    * terms accumulates the path we are on in the trie.
    */
-  void print(std::ostream& out,
-             Node q,
-             std::vector<TNode>& terms,
-             bool useActive,
-             std::vector<Node>& active) const;
-  /** set instantiation lemma at this node in the trie */
-  void setInstLemma(Node n)
-  {
-    d_data.clear();
-    d_data[n].clear();
-  }
-  /** does this node of the trie store an instantiation lemma? */
-  bool hasInstLemma() const { return !d_data.empty(); }
-  /** get the instantiation lemma stored in this node of the trie */
-  Node getInstLemma() const { return d_data.begin()->first; }
+  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
 };
 
 /** trie for InstMatch objects
@@ -183,21 +137,9 @@ class CDInstMatchTrie
    */
   bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
-                       InstMatch& m,
+                       const std::vector<Node>& m,
                        bool modEq = false,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, index, true);
-  }
-  /** exists inst match, vector version */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
-                       Node q,
-                       std::vector<Node>& m,
-                       bool modEq = false,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, index, true);
-  }
+                       unsigned index = 0);
   /** add inst match
    *
    * This method adds (the suffix of) m starting at the given index to this
@@ -209,17 +151,7 @@ class CDInstMatchTrie
    */
   bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
-                    InstMatch& m,
-                    bool modEq = false,
-                    unsigned index = 0,
-                    bool onlyExist = false)
-  {
-    return addInstMatch(qs, q, m.d_vals, modEq, index, onlyExist);
-  }
-  /** add inst match, vector version */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
-                    Node q,
-                    std::vector<Node>& m,
+                    const std::vector<Node>& m,
                     bool modEq = false,
                     unsigned index = 0,
                     bool onlyExist = false);
@@ -229,67 +161,28 @@ class CDInstMatchTrie
    * It returns true if and only if this entry existed in this trie.
    * The domain of m is the bound variables of quantified formula q.
    */
-  bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0);
+  bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
   /**
    * Adds the instantiations for q into insts.
    */
   void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
 
   /** print this class */
-  void print(std::ostream& out,
-             Node q,
-             bool useActive,
-             std::vector<Node>& active) const
-  {
-    std::vector<TNode> terms;
-    print(out, q, terms, useActive, active);
-  }
+  void print(std::ostream& out, Node q) const;
 
  private:
   /** Helper for getInstantiations.*/
   void getInstantiations(Node q,
                          std::vector<std::vector<Node>>& insts,
                          std::vector<Node>& terms) const;
+  /** helper for print
+   * terms accumulates the path we are on in the trie.
+   */
+  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
   /** the data */
   std::map<Node, CDInstMatchTrie*> d_data;
   /** is valid */
   context::CDO<bool> d_valid;
-  /** helper for print
-   * terms accumulates the path we are on in the trie.
-   */
-  void print(std::ostream& out,
-             Node q,
-             std::vector<TNode>& terms,
-             bool useActive,
-             std::vector<Node>& active) const;
-  /** helper for get instantiations
-   * terms accumulates the path we are on in the trie.
-   */
-  void getInstantiations(std::vector<Node>& insts,
-                         Node q,
-                         std::vector<Node>& terms,
-                         QuantifiersEngine* qe,
-                         bool useActive,
-                         std::vector<Node>& active) const;
-  /** helper for get explanation for inst lemma
-   * terms accumulates the path we are on in the trie.
-   */
-  void getExplanationForInstLemmas(
-      Node q,
-      std::vector<Node>& terms,
-      const std::vector<Node>& lems,
-      std::map<Node, Node>& quant,
-      std::map<Node, std::vector<Node> >& tvec) const;
-  /** set instantiation lemma at this node in the trie */
-  void setInstLemma(Node n)
-  {
-    d_data.clear();
-    d_data[n] = NULL;
-  }
-  /** does this node of the trie store an instantiation lemma? */
-  bool hasInstLemma() const { return !d_data.empty(); }
-  /** get the instantiation lemma stored in this node of the trie */
-  Node getInstLemma() const { return d_data.begin()->first; }
 };
 
 /** inst match trie ordered
@@ -314,11 +207,8 @@ class InstMatchTrieOrdered
    */
   bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
-                    InstMatch& m,
-                    bool modEq = false)
-  {
-    return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
-  }
+                    const std::vector<Node>& m,
+                    bool modEq = false);
   /** returns true if this trie contains m
    *
    * This method returns true if the match m exists in this
@@ -327,11 +217,8 @@ class InstMatchTrieOrdered
    */
   bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
-                       InstMatch& m,
-                       bool modEq = false)
-  {
-    return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
-  }
+                       const std::vector<Node>& m,
+                       bool modEq = false);
 
  private:
   /** the ordering */