From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 29 Mar 2013 20:50:13 +0000 (-0400)
Subject: make Boolean term conversion partially non-recursive (resolves bug 501)
X-Git-Tag: cvc5-1.0.0~7360
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=32f19d4e68e90cbae021321d4444be3f868783e5;p=cvc5.git

make Boolean term conversion partially non-recursive (resolves bug 501)
---

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 2eabdbea3..d3a600bf5 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -26,10 +26,12 @@
 #include "expr/kind.h"
 #include "util/hash.h"
 #include "util/bool.h"
+#include "util/ntuple.h"
 #include <string>
 #include <algorithm>
 #include <set>
 #include <map>
+#include <stack>
 
 using namespace std;
 using namespace CVC4::theory;
@@ -292,330 +294,407 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN
 }
 
 Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() {
-  Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
-
-  // we only distinguish between datatypes, booleans, and "other", and we
-  // don't even distinguish datatypes except when in "native" conversion
-  // mode
-  if(parentTheory != theory::THEORY_BOOL) {
-    if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE ||
-       parentTheory != theory::THEORY_DATATYPES) {
-      parentTheory = theory::THEORY_BUILTIN;
-    }
-  }
 
-  BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
-  if(i != d_termCache.end()) {
-    return (*i).second.isNull() ? Node(top) : (*i).second;
-  }
-
-  Kind k = top.getKind();
-  kind::MetaKind mk = top.getMetaKind();
+  stack< triple<TNode, theory::TheoryId, bool> > worklist;
+  worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
+  stack< NodeBuilder<> > result;
+  result.push(NodeBuilder<>(kind::TUPLE));
 
   NodeManager* nm = NodeManager::currentNM();
 
-  if(quantBoolVars.find(top) != quantBoolVars.end()) {
-    // this Bool variable is quantified over and we're changing it to a BitVector var
-    if(parentTheory == theory::THEORY_BOOL) {
-      return quantBoolVars[top].eqNode(d_tt);
-    } else {
-      return quantBoolVars[top];
-    }
-  }
+  while(!worklist.empty()) {
+    top = worklist.top().first;
+    parentTheory = worklist.top().second;
+    bool& childrenPushed = worklist.top().third;
 
-  if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
-    // still need to rewrite e.g. function applications over boolean
-    Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
-    Node n;
-    if(parentTheory == theory::THEORY_DATATYPES) {
-      n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt);
-    } else {
-      n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff);
+    Kind k = top.getKind();
+    kind::MetaKind mk = top.getMetaKind();
+
+    // we only distinguish between datatypes, booleans, and "other", and we
+    // don't even distinguish datatypes except when in "native" conversion
+    // mode
+    if(parentTheory != theory::THEORY_BOOL) {
+      if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE ||
+         parentTheory != theory::THEORY_DATATYPES) {
+        parentTheory = theory::THEORY_BUILTIN;
+      }
     }
-    Debug("boolean-terms") << "constructed ITE: " << n << endl;
-    return n;
-  }
 
-  if(mk == kind::metakind::CONSTANT) {
-    if(k == kind::STORE_ALL) {
-      const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>();
-      ArrayType arrType = asa.getType();
-      TypeNode indexType = TypeNode::fromType(arrType.getIndexType());
-      Type constituentType = arrType.getConstituentType();
-      if(constituentType.isBoolean()) {
-        // we have store_all(true) or store_all(false)
-        // just turn it into store_all(1) or store_all(0)
-        if(indexType.isBoolean()) {
-          // change index type to BV(1) also
-          indexType = d_tt.getType();
+    if(!childrenPushed) {
+      Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
+
+      BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
+      if(i != d_termCache.end()) {
+        result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
+        worklist.pop();
+        goto next_worklist;
+      }
+
+      if(quantBoolVars.find(top) != quantBoolVars.end()) {
+        // this Bool variable is quantified over and we're changing it to a BitVector var
+        if(parentTheory == theory::THEORY_BOOL) {
+          result.top() << quantBoolVars[top].eqNode(d_tt);
+        } else {
+          result.top() << quantBoolVars[top];
         }
-        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(),
-                              (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr());
-        Node n = nm->mkConst(asaRepl);
-        Debug("boolean-terms") << " returning new store_all: " << n << endl;
-        return n;
+        worklist.pop();
+        goto next_worklist;
       }
-      if(indexType.isBoolean()) {
-        // must change index type to BV(1)
-        indexType = d_tt.getType();
-        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
-        Node n = nm->mkConst(asaRepl);
-        Debug("boolean-terms") << " returning new store_all: " << n << endl;
-        return n;
+
+      if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
+        // still need to rewrite e.g. function applications over boolean
+        Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
+        Node n;
+        if(parentTheory == theory::THEORY_DATATYPES) {
+          n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt);
+        } else {
+          n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff);
+        }
+        Debug("boolean-terms") << "constructed ITE: " << n << endl;
+        result.top() << n;
+        worklist.pop();
+        goto next_worklist;
       }
-    }
-    return top;
-  } else if(mk == kind::metakind::VARIABLE) {
-    TypeNode t = top.getType();
-    if(t.isFunction()) {
-      for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
-        TypeNode newType = convertType(t[i], false);
-        if(newType != t[i]) {
-          vector<TypeNode> argTypes = t.getArgTypes();
-          replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType());
-          TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
-          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
-                                newType, "a function introduced by Boolean-term conversion",
-                                NodeManager::SKOLEM_EXACT_NAME);
-          Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
-          top.setAttribute(BooleanTermAttr(), n);
-          NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST);
-          NodeBuilder<> bodyBuilder(kind::APPLY_UF);
-          bodyBuilder << n;
-          for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
-            Node var = nm->mkBoundVar(t[j]);
-            boundVarsBuilder << var;
-            if(t[j].isBoolean()) {
-              bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff);
-            } else {
-              bodyBuilder << var;
+
+      if(mk == kind::metakind::CONSTANT) {
+        if(k == kind::STORE_ALL) {
+          const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>();
+          ArrayType arrType = asa.getType();
+          TypeNode indexType = TypeNode::fromType(arrType.getIndexType());
+          Type constituentType = arrType.getConstituentType();
+          if(constituentType.isBoolean()) {
+            // we have store_all(true) or store_all(false)
+            // just turn it into store_all(1) or store_all(0)
+            if(indexType.isBoolean()) {
+              // change index type to BV(1) also
+              indexType = d_tt.getType();
             }
+            ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(),
+                                  (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr());
+            Node n = nm->mkConst(asaRepl);
+            Debug("boolean-terms") << " returning new store_all: " << n << endl;
+            result.top() << n;
+            worklist.pop();
+            goto next_worklist;
+          }
+          if(indexType.isBoolean()) {
+            // must change index type to BV(1)
+            indexType = d_tt.getType();
+            ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
+            Node n = nm->mkConst(asaRepl);
+            Debug("boolean-terms") << " returning new store_all: " << n << endl;
+            result.top() << n;
+            worklist.pop();
+            goto next_worklist;
           }
-          Node boundVars = boundVarsBuilder;
-          Node body = bodyBuilder;
-          Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
-          Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
-          d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
-          d_termCache[make_pair(top, parentTheory)] = n;
-          return n;
         }
-      }
-    } else if(t.isArray()) {
-      TypeNode indexType = convertType(t.getArrayIndexType(), false);
-      TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
-      if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) {
-        TypeNode newType = nm->mkArrayType(indexType, constituentType);
-        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
-                              newType, "an array variable introduced by Boolean-term conversion",
-                              NodeManager::SKOLEM_EXACT_NAME);
-        top.setAttribute(BooleanTermAttr(), n);
-        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-        Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
-        Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
-        Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
-        Node repl = nm->mkNode(kind::STORE,
-                    nm->mkNode(kind::STORE, base, nm->mkConst(false),
-                               nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true),
-                               nm->mkNode(kind::EQUAL, n_tt, d_tt));
-        Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
-        d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
-        d_termCache[make_pair(top, parentTheory)] = n;
-        return n;
-      }
-      d_termCache[make_pair(top, parentTheory)] = Node::null();
-      return top;
-    } else if(t.isTuple() || t.isRecord()) {
-      TypeNode newType = convertType(t, true);
-      if(t != newType) {
-        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
-                              newType, "a tuple/record variable introduced by Boolean-term conversion",
-                              NodeManager::SKOLEM_EXACT_NAME);
-        top.setAttribute(BooleanTermAttr(), n);
-        n.setAttribute(BooleanTermAttr(), top);
-        Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
-        d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-        d_termCache[make_pair(top, parentTheory)] = n;
-        return n;
-      }
-      d_termCache[make_pair(top, parentTheory)] = Node::null();
-      return top;
-    } else if(t.isDatatype() || t.isParametricDatatype()) {
-      Debug("boolean-terms") << "found a var of datatype type" << endl;
-      TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
-      if(t != newT) {
-        Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(),
-               "Node `%s' already in cache ?!", top.toString().c_str());
-        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
-                              newT, "a datatype variable introduced by Boolean-term conversion",
-                              NodeManager::SKOLEM_EXACT_NAME);
-        Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
-        top.setAttribute(BooleanTermAttr(), n);
-        d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-        Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
-        d_termCache[make_pair(top, parentTheory)] = n;
-        return n;
-      } else {
-        d_termCache[make_pair(top, parentTheory)] = Node::null();
-        return top;
-      }
-    } else if(t.isConstructor()) {
-      Assert(parentTheory != theory::THEORY_BOOL);
-      Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
-             t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
-      const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
-                           t[t.getNumChildren() - 1].getConst<Datatype>() :
-                           t[t.getNumChildren() - 1][0].getConst<Datatype>();
-      TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-      const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
-      if(dt != dt2) {
-        Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
-               "constructor `%s' not in cache", top.toString().c_str());
-        return d_termCache[make_pair(top, parentTheory)];
-      }
-      d_termCache[make_pair(top, parentTheory)] = Node::null();
-      return top;
-    } else if(t.isTester() || t.isSelector()) {
-      Assert(parentTheory != theory::THEORY_BOOL);
-      const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
-                           t[0].getConst<Datatype>() :
-                           t[0][0].getConst<Datatype>();
-      TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-      const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
-      if(dt != dt2) {
-        Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
-               "tester or selector `%s' not in cache", top.toString().c_str());
-        return d_termCache[make_pair(top, parentTheory)];
-      } else {
-        d_termCache[make_pair(top, parentTheory)] = Node::null();
-        return top;
-      }
-    } else if(t.getNumChildren() > 0) {
-      for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
-        if((*i).isBoolean()) {
-          vector<TypeNode> argTypes(t.begin(), t.end());
-          replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
-          TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
-          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
-                                newType, "a variable introduced by Boolean-term conversion",
-                                NodeManager::SKOLEM_EXACT_NAME);
-          Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-          top.setAttribute(BooleanTermAttr(), n);
-          d_termCache[make_pair(top, parentTheory)] = n;
-          return n;
+        result.top() << top;
+        worklist.pop();
+        goto next_worklist;
+      } else if(mk == kind::metakind::VARIABLE) {
+        TypeNode t = top.getType();
+        if(t.isFunction()) {
+          for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
+            TypeNode newType = convertType(t[i], false);
+            if(newType != t[i]) {
+              vector<TypeNode> argTypes = t.getArgTypes();
+              replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType());
+              TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
+              Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
+                                    newType, "a function introduced by Boolean-term conversion",
+                                    NodeManager::SKOLEM_EXACT_NAME);
+              Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
+              top.setAttribute(BooleanTermAttr(), n);
+              NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST);
+              NodeBuilder<> bodyBuilder(kind::APPLY_UF);
+              bodyBuilder << n;
+              for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
+                Node var = nm->mkBoundVar(t[j]);
+                boundVarsBuilder << var;
+                if(t[j].isBoolean()) {
+                  bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff);
+                } else {
+                  bodyBuilder << var;
+                }
+              }
+              Node boundVars = boundVarsBuilder;
+              Node body = bodyBuilder;
+              Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
+              Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
+              d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
+              d_termCache[make_pair(top, parentTheory)] = n;
+              result.top() << n;
+              worklist.pop();
+              goto next_worklist;
+            }
+          }
+        } else if(t.isArray()) {
+          TypeNode indexType = convertType(t.getArrayIndexType(), false);
+          TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
+          if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) {
+            TypeNode newType = nm->mkArrayType(indexType, constituentType);
+            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+                                  newType, "an array variable introduced by Boolean-term conversion",
+                                  NodeManager::SKOLEM_EXACT_NAME);
+            top.setAttribute(BooleanTermAttr(), n);
+            Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+            Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
+            Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
+            Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
+            Node repl = nm->mkNode(kind::STORE,
+                                   nm->mkNode(kind::STORE, base, nm->mkConst(false),
+                                              nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true),
+                                   nm->mkNode(kind::EQUAL, n_tt, d_tt));
+            Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
+            d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
+            d_termCache[make_pair(top, parentTheory)] = n;
+            result.top() << n;
+            worklist.pop();
+            goto next_worklist;
+          }
+          d_termCache[make_pair(top, parentTheory)] = Node::null();
+          result.top() << top;
+          worklist.pop();
+          goto next_worklist;
+        } else if(t.isTuple() || t.isRecord()) {
+          TypeNode newType = convertType(t, true);
+          if(t != newType) {
+            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+                                  newType, "a tuple/record variable introduced by Boolean-term conversion",
+                                  NodeManager::SKOLEM_EXACT_NAME);
+            top.setAttribute(BooleanTermAttr(), n);
+            n.setAttribute(BooleanTermAttr(), top);
+            Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
+            d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
+            Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+            d_termCache[make_pair(top, parentTheory)] = n;
+            result.top() << n;
+            worklist.pop();
+            goto next_worklist;
+          }
+          d_termCache[make_pair(top, parentTheory)] = Node::null();
+          result.top() << top;
+          worklist.pop();
+          goto next_worklist;
+        } else if(t.isDatatype() || t.isParametricDatatype()) {
+          Debug("boolean-terms") << "found a var of datatype type" << endl;
+          TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
+          if(t != newT) {
+            Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(),
+                   "Node `%s' already in cache ?!", top.toString().c_str());
+            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+                                  newT, "a datatype variable introduced by Boolean-term conversion",
+                                  NodeManager::SKOLEM_EXACT_NAME);
+            Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
+            top.setAttribute(BooleanTermAttr(), n);
+            d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
+            Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
+            d_termCache[make_pair(top, parentTheory)] = n;
+            result.top() << n;
+            worklist.pop();
+            goto next_worklist;
+          } else {
+            d_termCache[make_pair(top, parentTheory)] = Node::null();
+            result.top() << top;
+            worklist.pop();
+            goto next_worklist;
+          }
+        } else if(t.isConstructor()) {
+          Assert(parentTheory != theory::THEORY_BOOL);
+          Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
+                 t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
+          const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
+            t[t.getNumChildren() - 1].getConst<Datatype>() :
+            t[t.getNumChildren() - 1][0].getConst<Datatype>();
+          TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
+          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
+          if(dt != dt2) {
+            Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
+                   "constructor `%s' not in cache", top.toString().c_str());
+            result.top() << d_termCache[make_pair(top, parentTheory)];
+            worklist.pop();
+            goto next_worklist;
+          }
+          d_termCache[make_pair(top, parentTheory)] = Node::null();
+          result.top() << top;
+          worklist.pop();
+          goto next_worklist;
+        } else if(t.isTester() || t.isSelector()) {
+          Assert(parentTheory != theory::THEORY_BOOL);
+          const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
+            t[0].getConst<Datatype>() :
+            t[0][0].getConst<Datatype>();
+          TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
+          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
+          if(dt != dt2) {
+            Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
+                   "tester or selector `%s' not in cache", top.toString().c_str());
+            result.top() << d_termCache[make_pair(top, parentTheory)];
+            worklist.pop();
+            goto next_worklist;
+          } else {
+            d_termCache[make_pair(top, parentTheory)] = Node::null();
+            result.top() << top;
+            worklist.pop();
+            goto next_worklist;
+          }
+        } else if(t.getNumChildren() > 0) {
+          for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
+            if((*i).isBoolean()) {
+              vector<TypeNode> argTypes(t.begin(), t.end());
+              replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
+              TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
+              Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+                                    newType, "a variable introduced by Boolean-term conversion",
+                                    NodeManager::SKOLEM_EXACT_NAME);
+              Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+              top.setAttribute(BooleanTermAttr(), n);
+              d_termCache[make_pair(top, parentTheory)] = n;
+              result.top() << n;
+              worklist.pop();
+              goto next_worklist;
+            }
+          }
         }
+        result.top() << top;
+        worklist.pop();
+        goto next_worklist;
       }
-    }
-    return top;
-  }
-  switch(k) {
-  case kind::LAMBDA:
-    Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str());
+      switch(k) {
+      case kind::LAMBDA:
+        Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str());
 
-  case kind::BOUND_VAR_LIST:
-    return top;
+      case kind::BOUND_VAR_LIST:
+        result.top() << top;
+        worklist.pop();
+        goto next_worklist;
 
-  case kind::REWRITE_RULE:
-  case kind::RR_REWRITE:
-  case kind::RR_DEDUCTION:
-  case kind::RR_REDUCTION:
-    // not yet supported
-    return top;
+      case kind::REWRITE_RULE:
+      case kind::RR_REWRITE:
+      case kind::RR_DEDUCTION:
+      case kind::RR_REDUCTION:
+        // not yet supported
+        result.top() << top;
+        worklist.pop();
+        goto next_worklist;
 
-  case kind::FORALL:
-  case kind::EXISTS: {
-    Debug("bt") << "looking at quantifier -> " << top << endl;
-    set<TNode> ourVars;
-    for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
-      if((*i).getType().isBoolean()) {
-        ourVars.insert(*i);
-      }
-    }
-    if(ourVars.empty()) {
-      // Simple case, quantifier doesn't quantify over Boolean vars,
-      // no special handling needed for quantifier.  Fall through.
-      Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl;
-    } else {
-      set<TNode> output;
-      hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen;
-      collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen);
-      if(output.empty()) {
-        // Simple case, quantifier quantifies over Boolean vars, but they
-        // don't occur in term context.  Fall through.
-        Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl;
-      } else {
-        Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl;
-        // We have Boolean vars appearing in term context.  Convert their
-        // types in the quantifier.
-        for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) {
-          Node newVar = nm->mkBoundVar((*i).toString(), nm->mkBitVectorType(1));
-          Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
-          quantBoolVars[*i] = newVar;
-        }
-        vector<TNode> boundVars;
+      case kind::FORALL:
+      case kind::EXISTS: {
+        Debug("bt") << "looking at quantifier -> " << top << endl;
+        set<TNode> ourVars;
         for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
-          map<TNode, Node>::const_iterator j = quantBoolVars.find(*i);
-          if(j == quantBoolVars.end()) {
-            boundVars.push_back(*i);
+          if((*i).getType().isBoolean()) {
+            ourVars.insert(*i);
+          }
+        }
+        if(ourVars.empty()) {
+          // Simple case, quantifier doesn't quantify over Boolean vars,
+          // no special handling needed for quantifier.  Fall through.
+          Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl;
+        } else {
+          set<TNode> output;
+          hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen;
+          collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen);
+          if(output.empty()) {
+            // Simple case, quantifier quantifies over Boolean vars, but they
+            // don't occur in term context.  Fall through.
+            Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl;
           } else {
-            boundVars.push_back((*j).second);
+            Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl;
+            // We have Boolean vars appearing in term context.  Convert their
+            // types in the quantifier.
+            for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) {
+              Node newVar = nm->mkBoundVar((*i).toString(), nm->mkBitVectorType(1));
+              Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
+              quantBoolVars[*i] = newVar;
+            }
+            vector<TNode> boundVars;
+            for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
+              map<TNode, Node>::const_iterator j = quantBoolVars.find(*i);
+              if(j == quantBoolVars.end()) {
+                boundVars.push_back(*i);
+              } else {
+                boundVars.push_back((*j).second);
+              }
+            }
+            Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
+            Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
+            Node quant = nm->mkNode(top.getKind(), boundVarList, body);
+            Debug("bt") << "rewrote quantifier to -> " << quant << endl;
+            d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
+            d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
+            d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff);
+            result.top() << quant;
+            worklist.pop();
+            goto next_worklist;
           }
         }
-        Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
-        Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
-        Node quant = nm->mkNode(top.getKind(), boundVarList, body);
-        Debug("bt") << "rewrote quantifier to -> " << quant << endl;
-        d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
-        d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
-        d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff);
-        return quant;
+        /* intentional fall-through for some cases above */
       }
-    }
-    /* intentional fall-through for some cases above */
-  }
 
-  default:
-    NodeBuilder<> b(k);
-    Debug("bt") << "looking at: " << top << endl;
-    if(mk == kind::metakind::PARAMETERIZED) {
-      if(k == kind::RECORD) {
-        b << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
-      } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
-        Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
-        b << asc;
-        Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
-        asc.setAttribute(BooleanTermAttr(), top.getOperator());
-      } else if(kindToTheoryId(k) != THEORY_BV &&
-                k != kind::TUPLE_SELECT &&
-                k != kind::TUPLE_UPDATE &&
-                k != kind::RECORD_SELECT &&
-                k != kind::RECORD_UPDATE) {
-        Debug("bt") << "rewriting: " << top.getOperator() << endl;
-        b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
-        Debug("bt") << "got: " << b.getOperator() << endl;
-      } else {
-        b << top.getOperator();
+      default:
+        result.push(NodeBuilder<>(k));
+        Debug("bt") << "looking at: " << top << endl;
+        // rewrite the operator, as necessary
+        if(mk == kind::metakind::PARAMETERIZED) {
+          if(k == kind::RECORD) {
+            result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
+          } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+            Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
+            result.top() << asc;
+            Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
+            asc.setAttribute(BooleanTermAttr(), top.getOperator());
+          } else if(kindToTheoryId(k) != THEORY_BV &&
+                    k != kind::TUPLE_SELECT &&
+                    k != kind::TUPLE_UPDATE &&
+                    k != kind::RECORD_SELECT &&
+                    k != kind::RECORD_UPDATE) {
+            Debug("bt") << "rewriting: " << top.getOperator() << endl;
+            result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
+            Debug("bt") << "got: " << result.top().getOperator() << endl;
+          } else {
+            result.top() << top.getOperator();
+          }
+        }
+        // push children
+        for(int i = top.getNumChildren() - 1; i >= 0; --i) {
+          Debug("bt") << "rewriting: " << top[i] << endl;
+          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), false));
+          //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
+          //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
+        }
+        childrenPushed = true;
       }
-    }
-    for(unsigned i = 0; i < top.getNumChildren(); ++i) {
-      Debug("bt") << "rewriting: " << top[i] << endl;
-      b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
-      Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
-    }
-    Node n = b;
-    Debug("boolean-terms") << "constructed: " << n << endl;
-    if(parentTheory == theory::THEORY_BOOL) {
-      if(n.getType().isBitVector() &&
-         n.getType().getBitVectorSize() == 1) {
-        n = nm->mkNode(kind::EQUAL, n, d_tt);
-      } else if(n.getType().isDatatype() &&
-                n.getType().hasAttribute(BooleanTermAttr())) {
-        n = nm->mkNode(kind::EQUAL, n, d_ttDt);
+    } else {
+      Node n = result.top();
+      result.pop();
+      Debug("boolean-terms") << "constructed: " << n << endl;
+      if(parentTheory == theory::THEORY_BOOL) {
+        if(n.getType().isBitVector() &&
+           n.getType().getBitVectorSize() == 1) {
+          n = nm->mkNode(kind::EQUAL, n, d_tt);
+        } else if(n.getType().isDatatype() &&
+                  n.getType().hasAttribute(BooleanTermAttr())) {
+          n = nm->mkNode(kind::EQUAL, n, d_ttDt);
+        }
       }
+      d_termCache[make_pair(top, parentTheory)] = n;
+      result.top() << n;
+      worklist.pop();
+      goto next_worklist;
     }
-    d_termCache[make_pair(top, parentTheory)] = n;
-    return n;
+
+  next_worklist:
+    ;
   }
+
+  Assert(worklist.size() == 0);
+  Assert(result.size() == 1);
+  Node retval = result.top()[0];
+  result.top().clear();
+  result.pop();
+  return retval;
+
 }/* BooleanTermConverter::rewriteBooleanTermsRec() */
 
 }/* CVC4::smt namespace */