Fix for bug 544.

1 files changed, 31 insertions, 23 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 30aa79aca..c1596dddc 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -43,8 +43,10 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
   d_tt(),
   d_ffDt(),
   d_ttDt(),
+  d_varCache(),
   d_termCache(),
-  d_typeCache() {
+  d_typeCache(),
+  d_datatypeCache() {
 
   // set up our "false" and "true" conversions based on command-line option
   if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
@@ -250,10 +252,10 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
           Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
           Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
           Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
-          d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
-          d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+          d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+          d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
-            d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+            d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
           }
         }
         out = &newD;
@@ -400,12 +402,18 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
     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()) {
+      BooleanTermVarCache::iterator i = d_varCache.find(top);
+      if(i != d_varCache.end()) {
         result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
         worklist.pop();
         goto next_worklist;
       }
+      BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
+      if(j != d_termCache.end()) {
+        result.top() << ((*j).second.isNull() ? Node(top) : (*j).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
@@ -511,7 +519,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
               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;
+              d_varCache[top] = n;
               result.top() << n;
               worklist.pop();
               goto next_worklist;
@@ -536,7 +544,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
                                    nm->mkConst(false), n_ff);
             Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
             d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
-            d_termCache[make_pair(top, parentTheory)] = n;
+            d_varCache[top] = n;
             result.top() << n;
             worklist.pop();
             goto next_worklist;
@@ -548,7 +556,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             top.setAttribute(BooleanTermAttr(), n);
             Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
             d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-            d_termCache[make_pair(top, parentTheory)] = n;
+            d_varCache[top] = n;
             result.top() << n;
             worklist.pop();
             goto next_worklist;
@@ -568,12 +576,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
                                    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;
+            d_varCache[top] = n;
             result.top() << n;
             worklist.pop();
             goto next_worklist;
           }
-          d_termCache[make_pair(top, parentTheory)] = Node::null();
+          d_varCache[top] = Node::null();
           result.top() << top;
           worklist.pop();
           goto next_worklist;
@@ -588,12 +596,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             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;
+            d_varCache[top] = n;
             result.top() << n;
             worklist.pop();
             goto next_worklist;
           }
-          d_termCache[make_pair(top, parentTheory)] = Node::null();
+          d_varCache[top] = Node::null();
           result.top() << top;
           worklist.pop();
           goto next_worklist;
@@ -601,7 +609,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           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(),
+            Assert(d_varCache.find(top) == d_varCache.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",
@@ -610,12 +618,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             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;
+            d_varCache[top] = n;
             result.top() << n;
             worklist.pop();
             goto next_worklist;
           } else {
-            d_termCache[make_pair(top, parentTheory)] = Node::null();
+            d_varCache[top] = Node::null();
             result.top() << top;
             worklist.pop();
             goto next_worklist;
@@ -630,13 +638,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           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(),
+            Assert(d_varCache.find(top) != d_varCache.end(),
                    "constructor `%s' not in cache", top.toString().c_str());
-            result.top() << d_termCache[make_pair(top, parentTheory)];
+            result.top() << d_varCache[top];
             worklist.pop();
             goto next_worklist;
           }
-          d_termCache[make_pair(top, parentTheory)] = Node::null();
+          d_varCache[top] = Node::null();
           result.top() << top;
           worklist.pop();
           goto next_worklist;
@@ -648,13 +656,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           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(),
+            Assert(d_varCache.find(top) != d_varCache.end(),
                    "tester or selector `%s' not in cache", top.toString().c_str());
-            result.top() << d_termCache[make_pair(top, parentTheory)];
+            result.top() << d_varCache[top];
             worklist.pop();
             goto next_worklist;
           } else {
-            d_termCache[make_pair(top, parentTheory)] = Node::null();
+            d_varCache[top] = Node::null();
             result.top() << top;
             worklist.pop();
             goto next_worklist;
@@ -670,7 +678,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
                                     NodeManager::SKOLEM_EXACT_NAME);
               Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
               top.setAttribute(BooleanTermAttr(), n);
-              d_termCache[make_pair(top, parentTheory)] = n;
+              d_varCache[top] = n;
               result.top() << n;
               worklist.pop();
               goto next_worklist;