From 65128efc1d0a4c2007ebb7b47712888481c07843 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 10 Apr 2014 16:38:37 -0400
Subject: [PATCH] Boolean terms conversion fix for datatypes, fixes a problem
 Andy discovered on his branch.

---
 src/smt/boolean_terms.cpp | 23 ++++++++++++++++++++---
 src/smt/boolean_terms.h   |  2 ++
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 4555aac51..111324dfa 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -46,7 +46,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
   d_varCache(smt.d_userContext),
   d_termCache(smt.d_userContext),
   d_typeCache(),
-  d_datatypeCache() {
+  d_datatypeCache(),
+  d_datatypeReverseCache() {
 
   // set up our "false" and "true" conversions based on command-line option
   if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
@@ -116,6 +117,10 @@ static inline bool isBoolean(TNode top, unsigned i) {
 // to be for model-substitution, so the "in" is a Boolean-term-converted
 // node, and "as" is the original.  See how it's used in function
 // handling, below.
+//
+// Note this isn't the case any longer, and parts of what's below have
+// been repurposed for *forward* conversion, meaning this works in either
+// direction.
 Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
   if(in.getType() == as) {
     return in;
@@ -133,7 +138,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
     }
     Assert(as.isDatatype());
     const Datatype* dt2 = &as.getDatatype();
-    const Datatype* dt1 = d_datatypeCache[dt2];
+    const Datatype* dt1;
+    if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
+      dt1 = d_datatypeCache[dt2];
+    } else {
+      dt1 = d_datatypeReverseCache[dt2];
+    }
     Assert(dt1 != NULL, "expected datatype in cache");
     Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
     Node out;
@@ -165,7 +175,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
       toParams.push_back(as[i + 1]);
     }
-    const Datatype* dt1 = d_datatypeCache[dt2];
+    const Datatype* dt1;
+    if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
+      dt1 = d_datatypeCache[dt2];
+    } else {
+      dt1 = d_datatypeReverseCache[dt2];
+    }
     Assert(dt1 != NULL, "expected datatype in cache");
     Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
     Node out;
@@ -259,11 +274,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
           }
         }
         out = &newD;
+        d_datatypeReverseCache[&newD] = &dt;
         return newD;
       }
     }
   }
 
+  // this is identity; don't need the reverse cache
   out = &dt;
   return dt;
 
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index b289e3469..bdd9ff839 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -69,6 +69,8 @@ class BooleanTermConverter {
   BooleanTermTypeCache d_typeCache;
   /** The cache used during Boolean term datatype conversion */
   BooleanTermDatatypeCache d_datatypeCache;
+  /** A (reverse) cache for Boolean term datatype conversion */
+  BooleanTermDatatypeCache d_datatypeReverseCache;
 
   Node rewriteAs(TNode in, TypeNode as) throw();
 
-- 
2.30.2