Make extended rewriter methods const (#6948)

2 files changed, 61 insertions, 47 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index aa7e183bb..58a78b4aa 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -48,7 +48,7 @@ ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr)
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-void ExtendedRewriter::setCache(Node n, Node ret)
+void ExtendedRewriter::setCache(Node n, Node ret) const
 {
   if (d_aggr)
   {
@@ -62,7 +62,7 @@ void ExtendedRewriter::setCache(Node n, Node ret)
   }
 }
 
-Node ExtendedRewriter::getCache(Node n)
+Node ExtendedRewriter::getCache(Node n) const
 {
   if (d_aggr)
   {
@@ -83,7 +83,7 @@ Node ExtendedRewriter::getCache(Node n)
 
 bool ExtendedRewriter::addToChildren(Node nc,
                                      std::vector<Node>& children,
-                                     bool dropDup)
+                                     bool dropDup) const
 {
   // If the operator is non-additive, do not consider duplicates
   if (dropDup
@@ -95,7 +95,7 @@ bool ExtendedRewriter::addToChildren(Node nc,
   return true;
 }
 
-Node ExtendedRewriter::extendedRewrite(Node n)
+Node ExtendedRewriter::extendedRewrite(Node n) const
 {
   n = Rewriter::rewrite(n);
 
@@ -280,7 +280,7 @@ Node ExtendedRewriter::extendedRewrite(Node n)
   return ret;
 }
 
-Node ExtendedRewriter::extendedRewriteAggr(Node n)
+Node ExtendedRewriter::extendedRewriteAggr(Node n) const
 {
   Node new_ret;
   Trace("q-ext-rewrite-debug2")
@@ -341,7 +341,7 @@ Node ExtendedRewriter::extendedRewriteAggr(Node n)
   return new_ret;
 }
 
-Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
+Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const
 {
   Assert(n.getKind() == itek);
   Assert(n[1] != n[2]);
@@ -561,7 +561,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
   return new_ret;
 }
 
-Node ExtendedRewriter::extendedRewriteAndOr(Node n)
+Node ExtendedRewriter::extendedRewriteAndOr(Node n) const
 {
   // all the below rewrites are aggressive
   if (!d_aggr)
@@ -592,7 +592,7 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n)
   return new_ret;
 }
 
-Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n)
+Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const
 {
   Assert(n.getKind() != ITE);
   if (n.isClosure())
@@ -715,7 +715,7 @@ Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n)
   return Node::null();
 }
 
-Node ExtendedRewriter::extendedRewriteNnf(Node ret)
+Node ExtendedRewriter::extendedRewriteNnf(Node ret) const
 {
   Assert(ret.getKind() == NOT);
 
@@ -761,8 +761,11 @@ Node ExtendedRewriter::extendedRewriteNnf(Node ret)
   return NodeManager::currentNM()->mkNode(nk, new_children);
 }
 
-Node ExtendedRewriter::extendedRewriteBcp(
-    Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node ret)
+Node ExtendedRewriter::extendedRewriteBcp(Kind andk,
+                                          Kind ork,
+                                          Kind notk,
+                                          std::map<Kind, bool>& bcp_kinds,
+                                          Node ret) const
 {
   Kind k = ret.getKind();
   Assert(k == andk || k == ork);
@@ -926,7 +929,7 @@ Node ExtendedRewriter::extendedRewriteBcp(
 Node ExtendedRewriter::extendedRewriteFactoring(Kind andk,
                                                 Kind ork,
                                                 Kind notk,
-                                                Node n)
+                                                Node n) const
 {
   Trace("ext-rew-factoring") << "Factoring: *** INPUT: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
@@ -1019,7 +1022,7 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
                                             Kind notk,
                                             std::map<Kind, bool>& bcp_kinds,
                                             Node n,
-                                            bool isXor)
+                                            bool isXor) const
 {
   Assert(n.getKind() == andk || n.getKind() == ork);
   Trace("ext-rew-eqres") << "Eq res: **** INPUT: " << n << std::endl;
@@ -1166,7 +1169,7 @@ class SimpSubsumeTrie
 };
 
 Node ExtendedRewriter::extendedRewriteEqChain(
-    Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor)
+    Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) const
 {
   Assert(ret.getKind() == eqk);
 
@@ -1527,9 +1530,10 @@ Node ExtendedRewriter::extendedRewriteEqChain(
   return Node::null();
 }
 
-Node ExtendedRewriter::partialSubstitute(Node n,
-                                         const std::map<Node, Node>& assign,
-                                         const std::map<Kind, bool>& rkinds)
+Node ExtendedRewriter::partialSubstitute(
+    Node n,
+    const std::map<Node, Node>& assign,
+    const std::map<Kind, bool>& rkinds) const
 {
   std::unordered_map<TNode, Node> visited;
   std::unordered_map<TNode, Node>::iterator it;
@@ -1601,10 +1605,11 @@ Node ExtendedRewriter::partialSubstitute(Node n,
   return visited[n];
 }
 
-Node ExtendedRewriter::partialSubstitute(Node n,
-                                         const std::vector<Node>& vars,
-                                         const std::vector<Node>& subs,
-                                         const std::map<Kind, bool>& rkinds)
+Node ExtendedRewriter::partialSubstitute(
+    Node n,
+    const std::vector<Node>& vars,
+    const std::vector<Node>& subs,
+    const std::map<Kind, bool>& rkinds) const
 {
   Assert(vars.size() == subs.size());
   std::map<Node, Node> assign;
@@ -1615,7 +1620,7 @@ Node ExtendedRewriter::partialSubstitute(Node n,
   return partialSubstitute(n, assign, rkinds);
 }
 
-Node ExtendedRewriter::solveEquality(Node n)
+Node ExtendedRewriter::solveEquality(Node n) const
 {
   // TODO (#1706) : implement
   Assert(n.getKind() == EQUAL);
@@ -1626,7 +1631,7 @@ Node ExtendedRewriter::solveEquality(Node n)
 bool ExtendedRewriter::inferSubstitution(Node n,
                                          std::vector<Node>& vars,
                                          std::vector<Node>& subs,
-                                         bool usePred)
+                                         bool usePred) const
 {
   if (n.getKind() == AND)
   {
@@ -1696,7 +1701,7 @@ bool ExtendedRewriter::inferSubstitution(Node n,
   return false;
 }
 
-Node ExtendedRewriter::extendedRewriteStrings(Node ret)
+Node ExtendedRewriter::extendedRewriteStrings(Node ret) const
 {
   Node new_ret;
   Trace("q-ext-rewrite-debug")
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 047318e86..8996fc441 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -51,7 +51,7 @@ class ExtendedRewriter
   ExtendedRewriter(bool aggr = true);
   ~ExtendedRewriter() {}
   /** return the extended rewritten form of n */
-  Node extendedRewrite(Node n);
+  Node extendedRewrite(Node n) const;
 
  private:
   /**
@@ -69,16 +69,16 @@ class ExtendedRewriter
   Node d_true;
   Node d_false;
   /** cache that the extended rewritten form of n is ret */
-  void setCache(Node n, Node ret);
+  void setCache(Node n, Node ret) const;
   /** get the cache for n */
-  Node getCache(Node n);
+  Node getCache(Node n) const;
   /** add to children
    *
    * Adds nc to the vector of children, if dropDup is true, we do not add
    * nc if it already occurs in children. This method returns false in this
    * case, otherwise it returns true.
    */
-  bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup);
+  bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup) const;
 
   //--------------------------------------generic utilities
   /** Rewrite ITE, for example:
@@ -92,13 +92,13 @@ class ExtendedRewriter
    * take. If full is false, then we do only perform rewrites that
    * strictly decrease the term size of n.
    */
-  Node extendedRewriteIte(Kind itek, Node n, bool full = true);
+  Node extendedRewriteIte(Kind itek, Node n, bool full = true) const;
   /** Rewrite AND/OR
    *
    * This implements BCP, factoring, and equality resolution for the Boolean
    * term n whose top symbolic is AND/OR.
    */
-  Node extendedRewriteAndOr(Node n);
+  Node extendedRewriteAndOr(Node n) const;
   /** Pull ITE, for example:
    *
    *   D=C2 ---> false
@@ -111,7 +111,7 @@ class ExtendedRewriter
    *
    * If this function returns a non-null node ret, then n ---> ret.
    */
-  Node extendedRewritePullIte(Kind itek, Node n);
+  Node extendedRewritePullIte(Kind itek, Node n) const;
   /** Negation Normal Form (NNF), for example:
    *
    *   ~( A & B ) ---> ( ~ A | ~B )
@@ -119,7 +119,7 @@ class ExtendedRewriter
    *
    * If this function returns a non-null node ret, then n ---> ret.
    */
-  Node extendedRewriteNnf(Node n);
+  Node extendedRewriteNnf(Node n) const;
   /** (type-independent) Boolean constraint propagation, for example:
    *
    *   ~A & ( B V A ) ---> ~A & B
@@ -137,8 +137,11 @@ class ExtendedRewriter
    *
    * If this function returns a non-null node ret, then n ---> ret.
    */
-  Node extendedRewriteBcp(
-      Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n);
+  Node extendedRewriteBcp(Kind andk,
+                          Kind ork,
+                          Kind notk,
+                          std::map<Kind, bool>& bcp_kinds,
+                          Node n) const;
   /** (type-independent) factoring, for example:
    *
    *   ( A V B ) ^ ( A V C ) ----> A V ( B ^ C )
@@ -147,7 +150,7 @@ class ExtendedRewriter
    * This function takes as arguments the kinds that specify AND, OR, NOT.
    * We assume that the children of n do not contain duplicates.
    */
-  Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n);
+  Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n) const;
   /** (type-independent) equality resolution, for example:
    *
    *   ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
@@ -167,7 +170,7 @@ class ExtendedRewriter
                             Kind notk,
                             std::map<Kind, bool>& bcp_kinds,
                             Node n,
-                            bool isXor = false);
+                            bool isXor = false) const;
   /** (type-independent) Equality chain rewriting, for example:
    *
    *   A = ( A = B ) ---> B
@@ -178,26 +181,32 @@ class ExtendedRewriter
    * This function takes as arguments the kinds that specify EQUAL, AND, OR,
    * and NOT. If the flag isXor is true, the eqk is treated as XOR.
    */
-  Node extendedRewriteEqChain(
-      Kind eqk, Kind andk, Kind ork, Kind notk, Node n, bool isXor = false);
+  Node extendedRewriteEqChain(Kind eqk,
+                              Kind andk,
+                              Kind ork,
+                              Kind notk,
+                              Node n,
+                              bool isXor = false) const;
   /** extended rewrite aggressive
    *
    * All aggressive rewriting techniques (those that should be prioritized
    * at a lower level) go in this function.
    */
-  Node extendedRewriteAggr(Node n);
+  Node extendedRewriteAggr(Node n) const;
   /** Decompose right associative chain
    *
    * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and
    * appends t1...tn to children.
    */
-  Node decomposeRightAssocChain(Kind k, Node n, std::vector<Node>& children);
+  Node decomposeRightAssocChain(Kind k,
+                                Node n,
+                                std::vector<Node>& children) const;
   /** Make right associative chain
    *
    * Sorts children to obtain list { tn...t1 }, and returns the term
    * f( ... f( f( base, tn ), t{n-1} ) ... t1 ).
    */
-  Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children);
+  Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children) const;
   /** Partial substitute
    *
    * Applies the substitution specified by assign to n, recursing only beneath
@@ -206,18 +215,18 @@ class ExtendedRewriter
    */
   Node partialSubstitute(Node n,
                          const std::map<Node, Node>& assign,
-                         const std::map<Kind, bool>& rkinds);
+                         const std::map<Kind, bool>& rkinds) const;
   /** same as above, with vectors */
   Node partialSubstitute(Node n,
                          const std::vector<Node>& vars,
                          const std::vector<Node>& subs,
-                         const std::map<Kind, bool>& rkinds);
+                         const std::map<Kind, bool>& rkinds) const;
   /** solve equality
    *
    * If this function returns a non-null node n', then n' is equivalent to n
    * and is of the form that can be used by inferSubstitution below.
    */
-  Node solveEquality(Node n);
+  Node solveEquality(Node n) const;
   /** infer substitution
    *
    * If n is an equality of the form x = t, where t is either:
@@ -231,12 +240,12 @@ class ExtendedRewriter
   bool inferSubstitution(Node n,
                          std::vector<Node>& vars,
                          std::vector<Node>& subs,
-                         bool usePred = false);
+                         bool usePred = false) const;
   /** extended rewrite
    *
    * Prints debug information, indicating the rewrite n ---> ret was found.
    */
-  inline void debugExtendedRewrite(Node n, Node ret, const char* c) const;
+  void debugExtendedRewrite(Node n, Node ret, const char* c) const;
   //--------------------------------------end generic utilities
 
   //--------------------------------------theory-specific top-level calls
@@ -245,7 +254,7 @@ class ExtendedRewriter
    * If this method returns a non-null node ret', then ret is equivalent to
    * ret'.
    */
-  Node extendedRewriteStrings(Node ret);
+  Node extendedRewriteStrings(Node ret) const;
   //--------------------------------------end theory-specific top-level calls
 };