Fix for bug 544.

3 files changed, 90 insertions, 58 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;
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index 904d47b5f..89611f5ea 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -35,6 +35,9 @@ namespace attr {
 typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
 
 class BooleanTermConverter {
+  /** The type of the Boolean term conversion variable cache */
+  typedef std::hash_map<Node, Node, NodeHashFunction> BooleanTermVarCache;
+
   /** The type of the Boolean term conversion cache */
   typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
                          PairHashFunction< Node, bool,
@@ -58,6 +61,8 @@ class BooleanTermConverter {
   /** The conversion for "true" when in datatypes contexts. */
   Node d_ttDt;
 
+  /** The cache used during Boolean term variable conversion */
+  BooleanTermVarCache d_varCache;
   /** The cache used during Boolean term conversion */
   BooleanTermCache d_termCache;
   /** The cache used during Boolean term type conversion */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 88cefbdc2..0fadca424 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -313,7 +313,6 @@ class SmtEnginePrivate : public NodeManagerListener {
   hash_map<unsigned, Node> d_BVDivByZero;
   hash_map<unsigned, Node> d_BVRemByZero;
 
-
   /**
    * Function symbol used to implement uninterpreted
    * int-division-by-zero semantics.  Needed to deal with partial
@@ -560,6 +559,11 @@ public:
     throw(TypeCheckingException, LogicException);
 
   /**
+   * Rewrite Boolean terms in a Node.
+   */
+  Node rewriteBooleanTerms(TNode n);
+
+  /**
    * Simplify node "in" by expanding definitions and applying any
    * substitutions learned from preprocessing.
    */
@@ -2899,6 +2903,39 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
   return false;
 }
 
+Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
+  TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+  if(d_booleanTermConverter == NULL) {
+    // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
+    // to ExprManager notifications, etc.  Otherwise we might miss the "BooleanTerm" datatype
+    // definition, and not dump it properly.
+    d_booleanTermConverter = new BooleanTermConverter(d_smt);
+  }
+  Node retval = d_booleanTermConverter->rewriteBooleanTerms(n);
+  if(retval != n) {
+    switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
+    case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+    case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_BV);
+        d_smt.d_logic.lock();
+      }
+      break;
+    case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_DATATYPES);
+        d_smt.d_logic.lock();
+      }
+      break;
+    default:
+      Unhandled(mode);
+    }
+  }
+  return retval;
+}
+
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
 
@@ -2956,37 +2993,8 @@ void SmtEnginePrivate::processAssertions() {
   dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
   {
     Chat() << "rewriting Boolean terms..." << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
-    if(d_booleanTermConverter == NULL) {
-      // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
-      // to ExprManager notifications, etc.  Otherwise we might miss the "BooleanTerm" datatype
-      // definition, and not dump it properly.
-      d_booleanTermConverter = new BooleanTermConverter(d_smt);
-    }
     for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
-      Node n = d_booleanTermConverter->rewriteBooleanTerms(d_assertionsToPreprocess[i]);
-      if(n != d_assertionsToPreprocess[i]) {
-        switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
-        case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
-        case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
-          if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
-            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(THEORY_BV);
-            d_smt.d_logic.lock();
-          }
-          break;
-        case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
-          if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
-            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-            d_smt.d_logic.enableTheory(THEORY_DATATYPES);
-            d_smt.d_logic.lock();
-          }
-          break;
-        default:
-          Unhandled(mode);
-        }
-      }
-      d_assertionsToPreprocess[i] = n;
+      d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]);
     }
   }
   dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
@@ -3529,9 +3537,14 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   // do not need to apply preprocessing substitutions (should be recorded
   // in model already)
 
+  Node n = Node::fromExpr(e);
+  Trace("smt") << "--- getting value of " << n << endl;
+  TypeNode expectedType = n.getType();
+
   // Expand, then normalize
   hash_map<Node, Node, NodeHashFunction> cache;
-  Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+  n = d_private->expandDefinitions(n, cache);
+  n = d_private->rewriteBooleanTerms(n);
   n = Rewriter::rewrite(n);
 
   Trace("smt") << "--- getting value of " << n << endl;
@@ -3541,13 +3554,13 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
     resultNode = m->getValue(n);
   }
   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
-  resultNode = postprocess(resultNode, n.getType());
+  resultNode = postprocess(resultNode, expectedType);
   Trace("smt") << "--- model-post returned " << resultNode << endl;
   Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
-  Trace("smt") << "--- model-post expected " << n.getType() << endl;
+  Trace("smt") << "--- model-post expected " << expectedType << endl;
 
   // type-check the result we got
-  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
+  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType));
 
   // ensure it's a constant
   Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
@@ -3625,9 +3638,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
       ++i) {
     Assert((*i).getType() == boolType);
 
+    Trace("smt") << "--- getting value of " << *i << endl;
+
     // Expand, then normalize
     hash_map<Node, Node, NodeHashFunction> cache;
     Node n = d_private->expandDefinitions(*i, cache);
+    n = d_private->rewriteBooleanTerms(n);
     n = Rewriter::rewrite(n);
 
     Trace("smt") << "--- getting value of " << n << endl;
@@ -3639,6 +3655,9 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
     // type-check the result we got
     Assert(resultNode.isNull() || resultNode.getType() == boolType);
 
+    // ensure it's a constant
+    Assert(resultNode.isConst());
+
     vector<SExpr> v;
     if((*i).getKind() == kind::APPLY) {
       Assert((*i).getNumChildren() == 0);