Address comments from PR #1164. (#1174)

Make eliminateSkolemFunctions(...) iterative and some more minor fixes.

2 files changed, 75 insertions, 67 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index a0b78d6d4..5152b2917 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/bv_inverter.h"
 
 #include <algorithm>
+#include <stack>
 
 #include "theory/quantifiers/term_database.h"
 
@@ -87,9 +88,9 @@ Node BvInverter::getInversionSkolemFor(Node cond, TypeNode tn) {
 }
 
 Node BvInverter::getInversionSkolemFunctionFor(TypeNode tn) {
+  NodeManager* nm = NodeManager::currentNM();
   // function maps conditions to skolems
-  TypeNode ftn = NodeManager::currentNM()->mkFunctionType(
-      NodeManager::currentNM()->booleanType(), tn);
+  TypeNode ftn = nm->mkFunctionType(nm->booleanType(), tn);
   return getSolveVariable(ftn);
 }
 
@@ -144,71 +145,83 @@ Node BvInverter::getPathToPv(
   return Node::null();
 }
 
-Node BvInverter::eliminateSkolemFunctions(
-    TNode n, std::vector<Node>& side_conditions,
-    std::unordered_map<TNode, Node, TNodeHashFunction>& visited) {
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it =
-      visited.find(n);
-  if (it == visited.end()) {
-    Trace("bv-invert-debug")
-        << "eliminateSkolemFunctions from " << n << "..." << std::endl;
-    Node ret = n;
-    bool childChanged = false;
-    std::vector<Node> children;
-    if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      children.push_back(n.getOperator());
-    }
-    for (unsigned i = 0; i < n.getNumChildren(); i++) {
-      Node nc = eliminateSkolemFunctions(n[i], side_conditions, visited);
-      childChanged = childChanged || n[i] != nc;
-      children.push_back(nc);
-    }
-    if (childChanged) {
-      ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
-    }
-    // now, check if it is a skolem function
-    if (ret.getKind() == APPLY_UF) {
-      Node op = ret.getOperator();
-      TypeNode tnp = op.getType();
-      // is this a skolem function?
-      std::map<TypeNode, Node>::iterator its = d_solve_var.find(tnp);
-      if (its != d_solve_var.end() && its->second == op) {
-        Assert(ret.getNumChildren() == 1);
-        Assert(ret[0].getType().isBoolean());
+Node BvInverter::eliminateSkolemFunctions(TNode n,
+                                          std::vector<Node>& side_conditions) {
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::stack<TNode> visit;
+  TNode cur;
+
+  visit.push(n);
+  do {
+    cur = visit.top();
+    visit.pop();
+    it = visited.find(cur);
 
-        Node cond = ret[0];
-        // must rewrite now to ensure we lookup the correct skolem
-        cond = Rewriter::rewrite(cond);
+    if (it == visited.end()) {
+      visited[cur] = Node::null();
+      visit.push(cur);
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        visit.push(cur[i]);
+      }
+    } else if (it->second.isNull()) {
+      Trace("bv-invert-debug")
+          << "eliminateSkolemFunctions from " << cur << "..." << std::endl;
 
-        // if so, we replace by the (finalized) skolem variable
-        // Notice that since we are post-rewriting, skolem functions are already
-        // eliminated from cond
-        ret = getInversionSkolemFor(cond, ret.getType());
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        children.push_back(cur.getOperator());
+      }
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        it = visited.find(cur[i]);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cur[i] != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged) {
+        ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
+      }
+      // now, check if it is a skolem function
+      if (ret.getKind() == APPLY_UF) {
+        Node op = ret.getOperator();
+        TypeNode tnp = op.getType();
+        // is this a skolem function?
+        std::map<TypeNode, Node>::iterator its = d_solve_var.find(tnp);
+        if (its != d_solve_var.end() && its->second == op) {
+          Assert(ret.getNumChildren() == 1);
+          Assert(ret[0].getType().isBoolean());
 
-        // also must add (substituted) side condition to vector
-        // substitute ( solve variable -> inversion skolem )
-        TNode solve_var = getSolveVariable(ret.getType());
-        TNode tret = ret;
-        cond = cond.substitute(solve_var, tret);
-        if (std::find(side_conditions.begin(), side_conditions.end(), cond) ==
-            side_conditions.end()) {
-          side_conditions.push_back(cond);
+          Node cond = ret[0];
+          // must rewrite now to ensure we lookup the correct skolem
+          cond = Rewriter::rewrite(cond);
+
+          // if so, we replace by the (finalized) skolem variable
+          // Notice that since we are post-rewriting, skolem functions are
+          // already eliminated from cond
+          ret = getInversionSkolemFor(cond, ret.getType());
+
+          // also must add (substituted) side condition to vector
+          // substitute ( solve variable -> inversion skolem )
+          TNode solve_var = getSolveVariable(ret.getType());
+          TNode tret = ret;
+          cond = cond.substitute(solve_var, tret);
+          if (std::find(side_conditions.begin(), side_conditions.end(), cond) ==
+              side_conditions.end()) {
+            side_conditions.push_back(cond);
+          }
         }
       }
+      Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << cur
+                               << " returned " << ret << std::endl;
+      visited[cur] = ret;
     }
-    Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << n
-                             << " returned " << ret << std::endl;
-    visited[n] = ret;
-    return ret;
-  } else {
-    return it->second;
-  }
-}
-
-Node BvInverter::eliminateSkolemFunctions(TNode n,
-                                          std::vector<Node>& side_conditions) {
-  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
-  return eliminateSkolemFunctions(n, side_conditions, visited);
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
 }
 
 Node BvInverter::getPathToPv(Node lit, Node pv, Node sv, Node pvs,
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index ca6c97f83..724b3b7a7 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -42,7 +42,7 @@ class BvInverterStatus {
   BvInverterStatus() : d_status(0) {}
   ~BvInverterStatus() {}
   int d_status;
-  // TODO : may not need this (conditions are now appear explicitly in solved
+  // TODO : may not need this (conditions now appear explicitly in solved
   // forms) side conditions
   std::vector<Node> d_conds;
 };
@@ -111,11 +111,6 @@ class BvInverter {
   Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
 
-  /** helper function for eliminateSkolemFunctions */
-  Node eliminateSkolemFunctions(
-      TNode n, std::vector<Node>& side_conditions,
-      std::unordered_map<TNode, Node, TNodeHashFunction>& visited);
-
   // is operator k invertible?
   bool isInvertible(Kind k);