From 496aed3f37c37519b6a26b3346b7f06e43bb5351 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 16 Dec 2020 10:52:26 -0600
Subject: [PATCH] (proof-new) Use bound variable manager (#5679)

This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.

This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.
---
 src/expr/CMakeLists.txt                       |   2 +
 src/expr/bound_var_manager.cpp                |   3 +-
 src/expr/node_manager.cpp                     |   6 +-
 src/expr/node_manager.h                       |   7 +-
 src/expr/skolem_manager.cpp                   |  38 +++--
 src/expr/skolem_manager.h                     |  11 --
 src/theory/arrays/skolem_cache.cpp            |  14 +-
 .../quantifiers/quantifiers_rewriter.cpp      | 158 ++++++++++--------
 src/theory/quantifiers/quantifiers_rewriter.h |  19 ++-
 src/theory/strings/skolem_cache.cpp           |  13 +-
 10 files changed, 138 insertions(+), 133 deletions(-)

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index ea35284fb..65cf36c34 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -17,6 +17,8 @@ libcvc4_add_sources(
   attribute.cpp
   attribute_internals.h
   attribute_unique_id.h
+  bound_var_manager.cpp
+  bound_var_manager.h
   buffered_proof_generator.cpp
   buffered_proof_generator.h
   emptyset.cpp
diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index 1532e43de..9aa3834e6 100644
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -18,8 +18,7 @@
 
 namespace CVC4 {
 
-// TODO: only enable when proofs are enabled
-BoundVarManager::BoundVarManager() : d_keepCacheVals(true) {}
+BoundVarManager::BoundVarManager() : d_keepCacheVals(false) {}
 
 BoundVarManager::~BoundVarManager() {}
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 49f460f45..540e02979 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -24,6 +24,7 @@
 #include "base/check.h"
 #include "base/listener.h"
 #include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
@@ -94,6 +95,7 @@ typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAtt
 NodeManager::NodeManager(ExprManager* exprManager)
     : d_statisticsRegistry(new StatisticsRegistry()),
       d_skManager(new SkolemManager),
+      d_bvManager(new BoundVarManager),
       next_id(0),
       d_attrManager(new expr::attr::AttributeManager()),
       d_exprManager(exprManager),
@@ -192,8 +194,10 @@ NodeManager::~NodeManager() {
 
   NodeManagerScope nms(this);
 
-  // Destroy skolem manager before cleaning up attributes and zombies
+  // Destroy skolem and bound var manager before cleaning up attributes and
+  // zombies
   d_skManager = nullptr;
+  d_bvManager = nullptr;
 
   {
     ScopedBool dontGC(d_inReclaimZombies);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1dd495ba2..1e70dd766 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -43,6 +43,7 @@ namespace CVC4 {
 class StatisticsRegistry;
 class ResourceManager;
 class SkolemManager;
+class BoundVarManager;
 
 class DType;
 
@@ -108,7 +109,9 @@ class NodeManager {
   StatisticsRegistry* d_statisticsRegistry;
 
   /** The skolem manager */
-  std::shared_ptr<SkolemManager> d_skManager;
+  std::unique_ptr<SkolemManager> d_skManager;
+  /** The bound variable manager */
+  std::unique_ptr<BoundVarManager> d_bvManager;
 
   NodeValuePool d_nodeValuePool;
 
@@ -386,6 +389,8 @@ class NodeManager {
   static NodeManager* currentNM() { return s_current; }
   /** Get this node manager's skolem manager */
   SkolemManager* getSkolemManager() { return d_skManager.get(); }
+  /** Get this node manager's bound variable manager */
+  BoundVarManager* getBoundVarManager() { return d_bvManager.get(); }
 
   /** Get this node manager's statistics registry */
   StatisticsRegistry* getStatisticsRegistry() const
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index a3647e84f..53cbf76de 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -15,12 +15,24 @@
 #include "expr/skolem_manager.h"
 
 #include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
 #include "expr/node_algorithm.h"
 
 using namespace CVC4::kind;
 
 namespace CVC4 {
 
+/**
+ * Attribute for associating terms to a unique bound variable.  This
+ * is used to construct canonical bound variables e.g. for constructing
+ * bound variables for witness terms in the skolemize method below.
+ */
+struct WitnessBoundVarAttributeId
+{
+};
+typedef expr::Attribute<WitnessBoundVarAttributeId, Node>
+    WitnessBoundVarAttribute;
+
 // Attributes are global maps from Nodes to data. Thus, note that these could
 // be implemented as internal maps in SkolemManager.
 struct WitnessFormAttributeId
@@ -81,7 +93,7 @@ Node SkolemManager::mkSkolemize(Node q,
                                 int flags,
                                 ProofGenerator* pg)
 {
-  Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
+  Trace("sk-manager-debug") << "mkSkolemize " << q << std::endl;
   Assert(q.getKind() == EXISTS);
   Node currQ = q;
   for (const Node& av : q[0])
@@ -99,6 +111,7 @@ Node SkolemManager::mkSkolemize(Node q,
     // Same as above, this may overwrite an existing proof generator
     d_gens[q] = pg;
   }
+  Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ << std::endl;
   return currQ;
 }
 
@@ -114,6 +127,7 @@ Node SkolemManager::skolemize(Node q,
   std::vector<Node> ovarsW;
   Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  BoundVarManager* bvm = nm->getBoundVarManager();
   for (const Node& av : q[0])
   {
     if (v.isNull())
@@ -126,7 +140,7 @@ Node SkolemManager::skolemize(Node q,
     // method deterministic ensures that the proof checker (e.g. for
     // quantifiers) is capable of proving the expected value for conclusions
     // of proof rules, instead of an alpha-equivalent variant of a conclusion.
-    Node avp = getOrMakeBoundVariable(av);
+    Node avp = bvm->mkBoundVar<WitnessBoundVarAttribute>(av, av.getType());
     ovarsW.push_back(avp);
     ovars.push_back(av);
   }
@@ -136,11 +150,12 @@ Node SkolemManager::skolemize(Node q,
   Trace("sk-manager-debug") << "make exists predicate" << std::endl;
   if (!ovars.empty())
   {
-    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW);
-    pred = nm->mkNode(EXISTS, bvl, pred);
     // skolem form keeps the old variables
-    bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
     qskolem = nm->mkNode(EXISTS, bvl, pred);
+    // update the predicate
+    bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW);
+    pred = nm->mkNode(EXISTS, bvl, pred);
   }
   Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
   // don't use a proof generator, since this may be an intermediate, partially
@@ -344,17 +359,4 @@ Node SkolemManager::getOrMakeSkolem(Node w,
   return k;
 }
 
-Node SkolemManager::getOrMakeBoundVariable(Node t)
-{
-  std::map<Node, Node>::iterator it = d_witnessBoundVar.find(t);
-  if (it != d_witnessBoundVar.end())
-  {
-    return it->second;
-  }
-  TypeNode tt = t.getType();
-  Node v = NodeManager::currentNM()->mkBoundVar(tt);
-  d_witnessBoundVar[t] = v;
-  return v;
-}
-
 }  // namespace CVC4
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 537c0b1e9..59e48528d 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -187,11 +187,6 @@ class SkolemManager
    * Mapping from witness terms to proof generators.
    */
   std::map<Node, ProofGenerator*> d_gens;
-  /**
-   * Map to canonical bound variables. This is used for example by the method
-   * mkExistential.
-   */
-  std::map<Node, Node> d_witnessBoundVar;
   /** Convert to witness or skolem form */
   static Node convertInternal(Node n, bool toWitness);
   /** Get or make skolem attribute for witness term w */
@@ -217,12 +212,6 @@ class SkolemManager
                  const std::string& prefix,
                  const std::string& comment = "",
                  int flags = NodeManager::SKOLEM_DEFAULT);
-  /**
-   * Get or make bound variable unique to t whose type is the same as t. This
-   * is used to construct canonical bound variables e.g. for constructing
-   * bound variables for witness terms in the skolemize method above.
-   */
-  Node getOrMakeBoundVariable(Node t);
 };
 
 }  // namespace CVC4
diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
index 4028a53a8..b32e89bca 100644
--- a/src/theory/arrays/skolem_cache.cpp
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -15,6 +15,7 @@
 #include "theory/arrays/skolem_cache.h"
 
 #include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_node.h"
 
@@ -66,20 +67,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq)
 
 Node SkolemCache::getExtIndexVar(Node deq)
 {
-  ExtIndexVarAttribute eiva;
-  if (deq.hasAttribute(eiva))
-  {
-    return deq.getAttribute(eiva);
-  }
   Node a = deq[0][0];
-  Node b = deq[0][1];
   TypeNode atn = a.getType();
   Assert(atn.isArray());
-  Assert(atn == b.getType());
+  Assert(atn == deq[0][1].getType());
   TypeNode atnIndex = atn.getArrayIndexType();
-  Node v = NodeManager::currentNM()->mkBoundVar(atnIndex);
-  deq.setAttribute(eiva, v);
-  return v;
+  BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager();
+  return bvm->mkBoundVar<ExtIndexVarAttribute>(deq, atnIndex);
 }
 
 }  // namespace arrays
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1f45fd85f..6ca2e5b22 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
+#include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
@@ -36,6 +37,30 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+/**
+ * Attributes used for constructing bound variables in a canonical way. These
+ * are attributes that map to bound variable, introduced for the following
+ * purposes:
+ * - QRewPrenexAttribute: cached on (v, body) where we are prenexing bound
+ * variable v in a nested quantified formula within the given body.
+ * - QRewMiniscopeAttribute: cached on (v, q, i) where q is being miniscoped
+ * for F_i in its body (and F_1 ... F_n), and v is one of the bound variables
+ * that q binds.
+ * - QRewDtExpandAttribute: cached on
+ */
+struct QRewPrenexAttributeId
+{
+};
+typedef expr::Attribute<QRewPrenexAttributeId, Node> QRewPrenexAttribute;
+struct QRewMiniscopeAttributeId
+{
+};
+typedef expr::Attribute<QRewMiniscopeAttributeId, Node> QRewMiniscopeAttribute;
+struct QRewDtExpandAttributeId
+{
+};
+typedef expr::Attribute<QRewDtExpandAttributeId, Node> QRewDtExpandAttribute;
+
 std::ostream& operator<<(std::ostream& out, RewriteStep s)
 {
   switch (s)
@@ -777,7 +802,9 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
 {
   if (lit.getKind() == NOT)
   {
-    return getVarElimLit(lit[0], !pol, args, vars, subs);
+    lit = lit[0];
+    pol = !pol;
+    Assert(lit.getKind() != NOT);
   }
   NodeManager* nm = NodeManager::currentNM();
   Trace("var-elim-quant-debug")
@@ -857,23 +884,6 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
       }
     }
   }
-  else if (lit.getKind() == APPLY_TESTER && pol
-           && lit[0].getKind() == BOUND_VARIABLE && options::dtVarExpandQuant())
-  {
-    Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
-                         << std::endl;
-    Node tester = lit.getOperator();
-    unsigned index = datatypes::utils::indexOf(tester);
-    Node s = datatypeExpand(index, lit[0], args);
-    if (!s.isNull())
-    {
-      vars.push_back(lit[0]);
-      subs.push_back(s);
-      Trace("var-elim-dt") << "...apply substitution " << s << "/" << lit[0]
-                           << std::endl;
-      return true;
-    }
-  }
   if (lit.getKind() == BOUND_VARIABLE)
   {
     std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
@@ -947,37 +957,6 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
   return false;
 }
 
-Node QuantifiersRewriter::datatypeExpand(unsigned index,
-                                         Node v,
-                                         std::vector<Node>& args)
-{
-  if (!v.getType().isDatatype())
-  {
-    return Node::null();
-  }
-  std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
-  if (ita == args.end())
-  {
-    return Node::null();
-  }
-  const DType& dt = v.getType().getDType();
-  Assert(index < dt.getNumConstructors());
-  const DTypeConstructor& c = dt[index];
-  std::vector<Node> newChildren;
-  newChildren.push_back(c.getConstructor());
-  std::vector<Node> newVars;
-  for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
-  {
-    TypeNode tn = c.getArgType(j);
-    Node vn = NodeManager::currentNM()->mkBoundVar(tn);
-    newChildren.push_back(vn);
-    newVars.push_back(vn);
-  }
-  args.erase(ita);
-  args.insert(args.end(), newVars.begin(), newVars.end());
-  return NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, newChildren);
-}
-
 bool QuantifiersRewriter::getVarElim(Node n,
                                      bool pol,
                                      std::vector<Node>& args,
@@ -987,9 +966,12 @@ bool QuantifiersRewriter::getVarElim(Node n,
   Kind nk = n.getKind();
   if (nk == NOT)
   {
-    return getVarElim(n[0], !pol, args, vars, subs);
+    n = n[0];
+    pol = !pol;
+    nk = n.getKind();
+    Assert(nk != NOT);
   }
-  else if ((nk == AND && pol) || (nk == OR && !pol))
+  if ((nk == AND && pol) || (nk == OR && !pol))
   {
     for (const Node& cn : n)
     {
@@ -1255,7 +1237,13 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){
+Node QuantifiersRewriter::computePrenex(Node q,
+                                        Node body,
+                                        std::vector<Node>& args,
+                                        std::vector<Node>& nargs,
+                                        bool pol,
+                                        bool prenexAgg)
+{
   NodeManager* nm = NodeManager::currentNM();
   Kind k = body.getKind();
   if (k == FORALL)
@@ -1263,12 +1251,25 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
     if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){
       std::vector< Node > terms;
       std::vector< Node > subs;
+      BoundVarManager* bvm = nm->getBoundVarManager();
       //for doing prenexing of same-signed quantifiers
       //must rename each variable that already exists
       for (const Node& v : body[0])
       {
         terms.push_back(v);
-        subs.push_back(nm->mkBoundVar(v.getType()));
+        TypeNode vt = v.getType();
+        Node vv;
+        if (!q.isNull())
+        {
+          Node cacheVal = BoundVarManager::getCacheValue(q, v);
+          vv = bvm->mkBoundVar<QRewPrenexAttribute>(cacheVal, vt);
+        }
+        else
+        {
+          // not specific to a quantified formula, use normal
+          vv = nm->mkBoundVar(vt);
+        }
+        subs.push_back(vv);
       }
       if( pol ){
         args.insert( args.end(), subs.begin(), subs.end() );
@@ -1286,14 +1287,14 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
     Node nn = nm->mkNode(AND,
                          nm->mkNode(OR, body[0].notNode(), body[1]),
                          nm->mkNode(OR, body[0], body[2]));
-    return computePrenex( nn, args, nargs, pol, prenexAgg );
+    return computePrenex(q, nn, args, nargs, pol, prenexAgg);
   }
   else if (prenexAgg && k == EQUAL && body[0].getType().isBoolean())
   {
     Node nn = nm->mkNode(AND,
                          nm->mkNode(OR, body[0].notNode(), body[1]),
                          nm->mkNode(OR, body[0], body[1].notNode()));
-    return computePrenex( nn, args, nargs, pol, prenexAgg );
+    return computePrenex(q, nn, args, nargs, pol, prenexAgg);
   }else if( body.getType().isBoolean() ){
     Assert(k != EXISTS);
     bool childrenChanged = false;
@@ -1308,7 +1309,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
         newChildren.push_back( body[i] );
         continue;
       }
-      Node n = computePrenex(body[i], args, nargs, newPol, prenexAgg);
+      Node n = computePrenex(q, body[i], args, nargs, newPol, prenexAgg);
       newChildren.push_back(n);
       childrenChanged = n != body[i] || childrenChanged;
     }
@@ -1369,7 +1370,8 @@ Node QuantifiersRewriter::computePrenexAgg(Node n,
   {
     std::vector<Node> args;
     std::vector<Node> nargs;
-    Node nn = computePrenex(n, args, nargs, true, true);
+    Node q;
+    Node nn = computePrenex(q, n, args, nargs, true, true);
     if (n != nn)
     {
       Node nnn = computePrenexAgg(nn, visited);
@@ -1554,12 +1556,15 @@ Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, std::v
 }
 
 //computes miniscoping, also eliminates variables that do not occur free in body
-Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
+Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa)
+{
   NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> args(q[0].begin(), q[0].end());
+  Node body = q[1];
   if( body.getKind()==FORALL ){
     //combine prenex
     std::vector< Node > newArgs;
-    newArgs.insert( newArgs.end(), args.begin(), args.end() );
+    newArgs.insert(newArgs.end(), q[0].begin(), q[0].end());
     for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
       newArgs.push_back( body[0][i] );
     }
@@ -1569,19 +1574,23 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
     // be applied first
     if (options::miniscopeQuant() || options::aggressiveMiniscopeQuant())
     {
+      BoundVarManager* bvm = nm->getBoundVarManager();
       // Break apart the quantifed formula
       // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
       NodeBuilder<> t(kind::AND);
       std::vector<Node> argsc;
-      for (unsigned i = 0, nchild = body.getNumChildren(); i < nchild; i++)
+      for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
       {
         if (argsc.empty())
         {
           // If not done so, we must create fresh copy of args. This is to
           // ensure that quantified formulas do not reuse variables.
-          for (const Node& v : args)
+          for (const Node& v : q[0])
           {
-            argsc.push_back(nm->mkBoundVar(v.getType()));
+            TypeNode vt = v.getType();
+            Node cacheVal = BoundVarManager::getCacheValue(q, v, i);
+            Node vv = bvm->mkBoundVar<QRewMiniscopeAttribute>(cacheVal, vt);
+            argsc.push_back(vv);
           }
         }
         Node b = body[i];
@@ -1595,7 +1604,10 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
         }
         else
         {
-          t << computeMiniscoping(argsc, bodyc, qa);
+          // make the miniscoped quantified formula
+          Node cbvl = nm->mkNode(BOUND_VAR_LIST, argsc);
+          Node qq = nm->mkNode(FORALL, cbvl, bodyc);
+          t << qq;
           // We used argsc, clear so we will construct a fresh copy above.
           argsc.clear();
         }
@@ -1807,14 +1819,8 @@ Node QuantifiersRewriter::computeOperation(Node f,
                                            QAttributes& qa)
 {
   Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
-  std::vector< Node > args;
-  for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-    args.push_back( f[0][i] );
-  }
-  Node n = f[1];
-  if( computeOption==COMPUTE_ELIM_SYMBOLS ){
-    n = computeElimSymbols( n );
-  }else if( computeOption==COMPUTE_MINISCOPING ){
+  if (computeOption == COMPUTE_MINISCOPING)
+  {
     if (options::prenexQuant() == options::PrenexQuantMode::NORMAL)
     {
       if( !qa.d_qid_num.isNull() ){
@@ -1823,7 +1829,13 @@ Node QuantifiersRewriter::computeOperation(Node f,
       }
     }
     //return directly
-    return computeMiniscoping( args, n, qa );
+    return computeMiniscoping(f, qa);
+  }
+  std::vector<Node> args(f[0].begin(), f[0].end());
+  Node n = f[1];
+  if (computeOption == COMPUTE_ELIM_SYMBOLS)
+  {
+    n = computeElimSymbols(n);
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return computeAggressiveMiniscoping( args, n );
   }
@@ -1854,7 +1866,7 @@ Node QuantifiersRewriter::computeOperation(Node f,
     else
     {
       std::vector< Node > nargs;
-      n = computePrenex( n, args, nargs, true, false );
+      n = computePrenex(f, n, args, nargs, true, false);
       Assert(nargs.empty());
     }
   }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 78586fc87..1ceab7fc0 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -161,13 +161,6 @@ class QuantifiersRewriter : public TheoryRewriter
       std::map<Node, Node>& pcons,
       std::map<Node, std::map<int, Node> >& ncons,
       std::vector<Node>& conj);
-  /** datatype expand
-   *
-   * If v occurs in args and has a datatype type whose index^th constructor is
-   * C, this method returns a node of the form C( x1, ..., xn ), removes v from
-   * args and adds x1...xn to args.
-   */
-  static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args);
 
   //-------------------------------------variable elimination
   /** compute variable elimination
@@ -232,7 +225,10 @@ class QuantifiersRewriter : public TheoryRewriter
   //------------------------------------- end extended rewrite
  public:
   static Node computeElimSymbols( Node body );
-  static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
+  /**
+   * Compute miniscoping in quantified formula q with attributes in qa.
+   */
+  static Node computeMiniscoping(Node q, QAttributes& qa);
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   /**
    * This function removes top-level quantifiers from subformulas of body
@@ -250,7 +246,12 @@ class QuantifiersRewriter : public TheoryRewriter
    *   (or (P x z) (not (Q y z)))
    * and add {x} to args, and {y} to nargs.
    */
-  static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
+  static Node computePrenex(Node q,
+                            Node body,
+                            std::vector<Node>& args,
+                            std::vector<Node>& nargs,
+                            bool pol,
+                            bool prenexAgg);
   /**
    * Apply prenexing aggressively. Returns the prenex normal form of n.
    */
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index f5f2dfd35..b68eb4a04 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -15,6 +15,8 @@
 #include "theory/strings/skolem_cache.h"
 
 #include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/theory_strings_utils.h"
@@ -273,15 +275,10 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 
 Node SkolemCache::mkIndexVar(Node t)
 {
-  IndexVarAttribute iva;
-  if (t.hasAttribute(iva))
-  {
-    return t.getAttribute(iva);
-  }
   NodeManager* nm = NodeManager::currentNM();
-  Node v = nm->mkBoundVar(nm->integerType());
-  t.setAttribute(iva, v);
-  return v;
+  TypeNode intType = nm->integerType();
+  BoundVarManager* bvm = nm->getBoundVarManager();
+  return bvm->mkBoundVar<IndexVarAttribute>(t, intType);
 }
 
 }  // namespace strings
-- 
2.30.2