Support for Boolean term conversion in datatypes.

1 files changed, 293 insertions, 106 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 35184e42e..09d8fcbd4 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -21,6 +21,8 @@
 #include "smt/smt_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/model.h"
+#include "theory/booleans/boolean_term_conversion_mode.h"
+#include "theory/booleans/options.h"
 #include "expr/kind.h"
 #include "util/hash.h"
 #include "util/bool.h"
@@ -31,10 +33,56 @@
 
 using namespace std;
 using namespace CVC4::theory;
+using namespace CVC4::theory::booleans;
 
 namespace CVC4 {
 namespace smt {
 
+BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
+  d_smt(smt),
+  d_ff(),
+  d_tt(),
+  d_ffDt(),
+  d_ttDt(),
+  d_termCache(),
+  d_typeCache() {
+
+  // set up our "false" and "true" conversions based on command-line option
+  if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
+     options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) {
+    d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u));
+    d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+  }
+  if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) {
+    d_ffDt = d_ff;
+    d_ttDt = d_tt;
+  } else {
+    Datatype spec("BooleanTerm");
+    // don't change the order; false is assumed to come first by the model postprocessor
+    spec.addConstructor(DatatypeConstructor("BT_False"));
+    spec.addConstructor(DatatypeConstructor("BT_True"));
+    const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype();
+    d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor()));
+    d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor()));
+    // mark this datatype type as being special for Boolean term conversion
+    TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null());
+    if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) {
+      Assert(d_ff.isNull() && d_tt.isNull());
+      d_ff = d_ffDt;
+      d_tt = d_ttDt;
+    }
+  }
+
+  // assert that we set it up correctly
+  Assert(!d_ff.isNull() && !d_tt.isNull());
+  Assert(!d_ffDt.isNull() && !d_ttDt.isNull());
+  Assert(d_ff != d_tt);
+  Assert(d_ff.getType() == d_tt.getType());
+  Assert(d_ffDt != d_ttDt);
+  Assert(d_ffDt.getType() == d_ttDt.getType());
+
+}/* BooleanTermConverter::BooleanTermConverter() */
+
 static inline bool isBoolean(TNode top, unsigned i) {
   switch(top.getKind()) {
   case kind::NOT:
@@ -63,27 +111,51 @@ static inline bool isBoolean(TNode top, unsigned i) {
   }
 }
 
-const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
-  return dt;
-  // boolean terms not supported in datatypes, yet
+const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
+  const Datatype*& out = d_datatypeCache[&dt];
+  if(out != NULL) {
+    return *out;
+  }
 
-  Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl;
+  Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl;
   for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
     TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
     for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
-      if((*a).isBoolean()) {
-        Datatype newDt(dt.getName() + "'");
+      TypeNode converted = convertType(*a, true);
+      Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl;
+      if(*a != converted) {
+        SortConstructorType mySelfType;
+        set<Type> unresolvedTypes;
+        if(dt.isParametric()) {
+          mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters());
+          unresolvedTypes.insert(mySelfType);
+        }
+        vector<Datatype> newDtVector;
+        if(dt.isParametric()) {
+          newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters()));
+        } else {
+          newDtVector.push_back(Datatype(dt.getName() + "'"));
+        }
+        Datatype& newDt = newDtVector.front();
         Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
         for(c = dt.begin(); c != dt.end(); ++c) {
           DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
           t = TypeNode::fromType((*c).getConstructor().getType());
           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
-            if((*a).getType().getRangeType().isBoolean()) {
-              ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType());
-            } else {
-              Type argType = (*a).getType().getRangeType();
-              if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+            Type argType = (*a).getType().getRangeType();
+            if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+              Debug("boolean-terms") << "argtype " << argType << " is self" << endl;
+              if(dt.isParametric()) {
+                Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl;
+                ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters()));
+              } else {
                 ctor.addArg((*a).getName() + "'", DatatypeSelfType());
+              }
+            } else {
+              Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl;
+              converted = convertType(TypeNode::fromType(argType), true);
+              if(TypeNode::fromType(argType) != converted) {
+                ctor.addArg((*a).getName() + "'", converted.toType());
               } else {
                 ctor.addArg((*a).getName() + "'", argType);
               }
@@ -91,22 +163,107 @@ const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype
           }
           newDt.addConstructor(ctor);
         }
-        DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt);
+        vector<DatatypeType> newDttVector =
+          NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
+        DatatypeType& newDtt = newDttVector.front();
         const Datatype& newD = newDtt.getDatatype();
         for(c = dt.begin(); c != dt.end(); ++c) {
           Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
-          d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
-          d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+          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());
           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
-            d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+            d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
           }
         }
+        out = &newD;
         return newD;
       }
     }
   }
+
+  out = &dt;
   return dt;
-}/* BooleanTermConverter::booleanTermsConvertDatatype() */
+
+}/* BooleanTermConverter::convertDatatype() */
+
+TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) {
+  Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl;
+  // This function recursively converts the type.
+  if(type.isBoolean()) {
+    return datatypesContext ? d_ttDt.getType() : d_tt.getType();
+  }
+  const pair<TypeNode, bool> cacheKey(type, datatypesContext);
+  if(d_typeCache.find(cacheKey) != d_typeCache.end()) {
+    TypeNode out = d_typeCache[cacheKey];
+    return out.isNull() ? type : out;
+  }
+  TypeNode& outNode = d_typeCache[cacheKey];
+  if(type.getKind() == kind::DATATYPE_TYPE ||
+     type.getKind() == kind::PARAMETRIC_DATATYPE) {
+    bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE);
+    const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>();
+    TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
+    Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
+    if(parametric) {
+      // re-parameterize the translation
+      vector<TypeNode> params = type.getParamTypes();
+      for(size_t i = 0; i < params.size(); ++i) {
+        Debug("boolean-terms") << "in loop, got "<< params[i] << endl;
+        params[i] = convertType(params[i], true);
+        Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl;
+      }
+      params.insert(params.begin(), out[0]);
+      out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
+      Debug("boolean-terms") << "got OUT: " << out << endl;
+    }
+    if(out != type) {
+      outNode = out;// cache it
+      Debug("boolean-terms") << "OUT is same as TYPE" << endl;
+    } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
+    return out;
+  }
+  if(type.isRecord()) {
+    const Record& rec = type.getConst<Record>();
+    vector< pair<string, Type> > flds;
+    for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
+      TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
+      if(TypeNode::fromType((*i).second) != converted) {
+        flds.push_back(make_pair((*i).first, converted.toType()));
+      } else {
+        flds.push_back(*i);
+      }
+    }
+    TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
+    Debug("tuprec") << "converted " << type << " to " << newRec << endl;
+    if(newRec != type) {
+      outNode = newRec;// cache it
+    }
+    return newRec;
+  }
+  if(type.getNumChildren() > 0) {
+    Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
+    // This should handle tuples and arrays ok.
+    // Might handle function types too, but they can't go
+    // in other types, so it doesn't matter.
+    NodeBuilder<> b(type.getKind());
+    if(type.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      b << type.getOperator();
+    }
+    for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) {
+      b << convertType(*i, false);
+    }
+    TypeNode out = b;
+    if(out != type) {
+      outNode = out;// cache it
+    }
+    Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl;
+    return out;
+  }
+  // leave the cache at Null
+  return type;
+}/* BooleanTermConverter::convertType() */
 
 // look for vars from "vars" that occur in a term-context in n; transfer them to output.
 static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) {
@@ -134,11 +291,21 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN
   }
 }
 
-Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw() {
-  Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl;
+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_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
-  if(i != d_booleanTermCache.end()) {
+  BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory));
+  if(i != d_termCache.end()) {
     return (*i).second.isNull() ? Node(top) : (*i).second;
   }
 
@@ -147,22 +314,24 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
 
   NodeManager* nm = NodeManager::currentNM();
 
-  Node one = nm->mkConst(BitVector(1u, 1u));
-  Node zero = nm->mkConst(BitVector(1u, 0u));
-
   if(quantBoolVars.find(top) != quantBoolVars.end()) {
     // this Bool variable is quantified over and we're changing it to a BitVector var
-    if(boolParent) {
-      return quantBoolVars[top].eqNode(one);
+    if(parentTheory == theory::THEORY_BOOL) {
+      return quantBoolVars[top].eqNode(d_tt);
     } else {
       return quantBoolVars[top];
     }
   }
 
-  if(!boolParent && top.getType().isBoolean()) {
+  if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
     // still need to rewrite e.g. function applications over boolean
-    Node topRewritten = rewriteBooleanTermsRec(top, true, quantBoolVars);
-    Node n = nm->mkNode(kind::ITE, topRewritten, one, zero);
+    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;
     return n;
   }
@@ -176,19 +345,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
       if(constituentType.isBoolean()) {
         // we have store_all(true) or store_all(false)
         // just turn it into store_all(1) or store_all(0)
-        Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u));
         if(indexType.isBoolean()) {
           // change index type to BV(1) also
-          indexType = nm->mkBitVectorType(1);
+          indexType = d_tt.getType();
         }
-        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr());
+        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;
       }
       if(indexType.isBoolean()) {
         // must change index type to BV(1)
-        indexType = nm->mkBitVectorType(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;
@@ -200,9 +369,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
     TypeNode t = top.getType();
     if(t.isFunction()) {
       for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
-        if(t[i].isBoolean()) {
+        TypeNode newType = convertType(t[i], false);
+        if(newType != t[i]) {
           vector<TypeNode> argTypes = t.getArgTypes();
-          replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
+          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",
@@ -216,7 +386,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
             Node var = nm->mkBoundVar(t[j]);
             boundVarsBuilder << var;
             if(t[j].isBoolean()) {
-              bodyBuilder << nm->mkNode(kind::ITE, var, one, zero);
+              bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff);
             } else {
               bodyBuilder << var;
             }
@@ -226,105 +396,112 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
           Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
           Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
           d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
-          d_booleanTermCache[make_pair(top, boolParent)] = n;
+          d_termCache[make_pair(top, parentTheory)] = n;
           return n;
         }
       }
     } else if(t.isArray()) {
-      TypeNode indexType = t.getArrayIndexType();
-      TypeNode constituentType = t.getArrayConstituentType();
-      bool rewrite = false;
-      if(indexType.isBoolean()) {
-        indexType = nm->mkBitVectorType(1);
-        rewrite = true;
-      }
-      if(constituentType.isBoolean()) {
-        constituentType = nm->mkBitVectorType(1);
-        rewrite = true;
-      }
-      if(rewrite) {
+      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()),
+        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_zero = nm->mkNode(kind::SELECT, n, zero);
-        Node n_one = nm->mkNode(kind::SELECT, n, one);
+        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_zero, one)), nm->mkConst(true),
-                               nm->mkNode(kind::EQUAL, n_one, one));
+                               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_booleanTermCache[make_pair(top, boolParent)] = n;
+        d_termCache[make_pair(top, parentTheory)] = n;
         return n;
       }
-      d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+      d_termCache[make_pair(top, parentTheory)] = Node::null();
       return top;
-    } else if(t.isTuple()) {
-      return top;
-    } else if(t.isRecord()) {
+    } 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()) {
-      return top;// no support for datatypes at present
-      const Datatype& dt = t.getConst<Datatype>();
-      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
-      if(dt != dt2) {
-        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(),
+    } 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());
-        Assert(top.isVar());
-        TypeNode newType = TypeNode::fromType(dt2.getDatatypeType());
-        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
-                              newType, "an array variable introduced by Boolean-term conversion",
+        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);
-        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-        d_booleanTermCache[make_pair(top, boolParent)] = 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_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        d_termCache[make_pair(top, parentTheory)] = Node::null();
         return top;
       }
     } else if(t.isConstructor()) {
-      return top;// no support for datatypes at present
-      Assert(!boolParent);
-      const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
-      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      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_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+        Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
                "constructor `%s' not in cache", top.toString().c_str());
-        return d_booleanTermCache[make_pair(top, boolParent)];
-      } else {
-        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
-        return top;
+        return d_termCache[make_pair(top, parentTheory)];
       }
+      d_termCache[make_pair(top, parentTheory)] = Node::null();
+      return top;
     } else if(t.isTester() || t.isSelector()) {
-      return top;// no support for datatypes at present
-      Assert(!boolParent);
-      const Datatype& dt = t[0].getConst<Datatype>();
-      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      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_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+        Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
                "tester or selector `%s' not in cache", top.toString().c_str());
-        return d_booleanTermCache[make_pair(top, boolParent)];
+        return d_termCache[make_pair(top, parentTheory)];
       } else {
-        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        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, nm->mkBitVectorType(1));
+          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_booleanTermCache[make_pair(top, boolParent)] = n;
+          d_termCache[make_pair(top, parentTheory)] = n;
           return n;
         }
       }
@@ -385,11 +562,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
           }
         }
         Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
-        Node body = rewriteBooleanTermsRec(top[1], true, quantBoolVars);
+        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_booleanTermCache[make_pair(top, true)] = quant;
-        d_booleanTermCache[make_pair(top, false)] = quant.iteNode(one, zero);
+        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;
       }
     }
@@ -400,15 +578,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
     NodeBuilder<> b(k);
     Debug("bt") << "looking at: " << top << endl;
     if(mk == kind::metakind::PARAMETERIZED) {
-      if(kindToTheoryId(k) != THEORY_BV &&
-         k != kind::APPLY_TYPE_ASCRIPTION &&
-         k != kind::TUPLE_SELECT &&
-         k != kind::TUPLE_UPDATE &&
-         k != kind::RECORD_SELECT &&
-         k != kind::RECORD_UPDATE &&
-         k != kind::RECORD) {
+      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(), false, quantBoolVars);
+        b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
         Debug("bt") << "got: " << b.getOperator() << endl;
       } else {
         b << top.getOperator();
@@ -416,17 +599,21 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
     }
     for(unsigned i = 0; i < top.getNumChildren(); ++i) {
       Debug("bt") << "rewriting: " << top[i] << endl;
-      b << rewriteBooleanTermsRec(top[i], isBoolean(top, i), quantBoolVars);
+      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(boolParent &&
-       n.getType().isBitVector() &&
-       n.getType().getBitVectorSize() == 1) {
-      n = nm->mkNode(kind::EQUAL, n, one);
+    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_booleanTermCache[make_pair(top, boolParent)] = n;
+    d_termCache[make_pair(top, parentTheory)] = n;
     return n;
   }
 }/* BooleanTermConverter::rewriteBooleanTermsRec() */