From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 28 Jan 2013 22:31:57 +0000 (-0500)
Subject: Support for Boolean term conversion in datatypes.
X-Git-Tag: cvc5-1.0.0~7371
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f44a81d1b62058fa56af952aa92be965690481e5;p=cvc5.git

Support for Boolean term conversion in datatypes.
---

diff --git a/NEWS b/NEWS
index 3c38aab56..9d4b5452d 100644
--- a/NEWS
+++ b/NEWS
@@ -15,5 +15,6 @@ Changes since 1.0
   use -q.  Previously, this would silence all output (including "sat" or
   "unsat") as well.  Now, single -q silences messages and warnings, and
   double -qq silences all output (except on exception or signal).
+* Boolean term support in datatypes
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 20 Feb 2013 18:31:50 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 20 Mar 2013 20:03:50 -0400
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5159f6b5a..eab41ee38 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -936,7 +936,7 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
       ("export of types belonging to theory of DATATYPES kinds unsupported");
   }
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
-     n.getKind() != kind::SORT_TYPE) { 
+     n.getKind() != kind::SORT_TYPE) {
     throw ExportUnsupportedException
       ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
   }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 5f813dbe8..bd3827f47 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -713,6 +713,10 @@ public:
   operator Node();
   operator Node() const;
 
+  // similarly for TypeNode
+  operator TypeNode();
+  operator TypeNode() const;
+
   NodeBuilder<nchild_thresh>& operator&=(TNode);
   NodeBuilder<nchild_thresh>& operator|=(TNode);
   NodeBuilder<nchild_thresh>& operator+=(TNode);
@@ -901,6 +905,16 @@ NodeBuilder<nchild_thresh>::operator Node() const {
   return constructNode();
 }
 
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() {
+  return constructTypeNode();
+}
+
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() const {
+  return constructTypeNode();
+}
+
 template <unsigned nchild_thresh>
 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   Assert(!isUsed(), "NodeBuilder is one-shot only; "
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 236f48017..7522b8110 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -94,15 +94,32 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
       return true;
     }
-    if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
-       getNumChildren() != t.getNumChildren()) {
+    if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
       return false;
     }
-    // children must be subtypes of t's, in order
-    for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-      if(!(*i).isSubtypeOf(*j)) {
+    if(isTuple()) {
+      if(getNumChildren() != t.getNumChildren()) {
         return false;
       }
+      // children must be subtypes of t's, in order
+      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+        if(!(*i).isSubtypeOf(*j)) {
+          return false;
+        }
+      }
+    } else {
+      const Record& r1 = getConst<Record>();
+      const Record& r2 = t.getConst<Record>();
+      if(r1.getNumFields() != r2.getNumFields()) {
+        return false;
+      }
+      // r1's fields must be subtypes of r2's, in order
+      // names must match also
+      for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+        if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
+          return false;
+        }
+      }
     }
     return true;
   }
@@ -125,15 +142,32 @@ bool TypeNode::isComparableTo(TypeNode t) const {
          NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
         return true;
       }
-      if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
-         getNumChildren() != t.getNumChildren()) {
+      if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
         return false;
       }
-      // children must be comparable to t's, in order
-      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-        if(!(*i).isComparableTo(*j)) {
+      if(isTuple()) {
+        if(getNumChildren() != t.getNumChildren()) {
+          return false;
+        }
+        // children must be comparable to t's, in order
+        for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+          if(!(*i).isComparableTo(*j)) {
+            return false;
+          }
+        }
+      } else {
+        const Record& r1 = getConst<Record>();
+        const Record& r2 = t.getConst<Record>();
+        if(r1.getNumFields() != r2.getNumFields()) {
           return false;
         }
+        // r1's fields must be comparable to r2's, in order
+        // names must match also
+        for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+          if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
+            return false;
+          }
+        }
       }
       return true;
     } else {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2cfeaafc1..524344612 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -817,7 +817,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( options::modelUninterpDtEnum() && tn.isSort() &&
         tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-      out << "DATATYPE " << std::endl;
+      out << "DATATYPE" << std::endl;
       out << "  " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
         if (i>0) {
@@ -1068,7 +1068,18 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
       out << ',' << endl;
     }
     const Datatype& dt = (*i).getDatatype();
-    out << "  " << dt.getName() << " = ";
+    out << "  " << dt.getName();
+    if(dt.isParametric()) {
+      out << '[';
+      for(size_t j = 0; j < dt.getNumParameters(); ++j) {
+        if(j > 0) {
+          out << ',';
+        }
+        out << dt.getParameter(j);
+      }
+      out << ']';
+    }
+    out << " = ";
     bool firstConstructor = true;
     for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
       if(! firstConstructor) {
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() */
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index c53eadfa0..06f25f9ef 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -38,35 +38,64 @@ typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
 
 class BooleanTermConverter {
   /** The type of the Boolean term conversion cache */
-  typedef std::hash_map< std::pair<Node, bool>, Node,
+  typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
                          PairHashFunction< Node, bool,
-                                           NodeHashFunction, std::hash<int> > > BooleanTermCache;
+                                           NodeHashFunction, std::hash<size_t> > > BooleanTermCache;
+  /** The type of the Boolean term conversion type cache */
+  typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode,
+                         PairHashFunction< TypeNode, bool,
+                                           TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache;
+  /** The type of the Boolean term conversion datatype cache */
+  typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache;
 
   /** The SmtEngine to which we're associated */
   SmtEngine& d_smt;
 
+  /** The conversion for "false." */
+  Node d_ff;
+  /** The conversion for "true." */
+  Node d_tt;
+  /** The conversion for "false" when in datatypes contexts. */
+  Node d_ffDt;
+  /** The conversion for "true" when in datatypes contexts. */
+  Node d_ttDt;
+
   /** The cache used during Boolean term conversion */
-  BooleanTermCache d_booleanTermCache;
+  BooleanTermCache d_termCache;
+  /** The cache used during Boolean term type conversion */
+  BooleanTermTypeCache d_typeCache;
+  /** The cache used during Boolean term datatype conversion */
+  BooleanTermDatatypeCache d_datatypeCache;
 
   /**
    * Scan a datatype for and convert as necessary.
    */
-  const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw();
+  const Datatype& convertDatatype(const Datatype& dt) throw();
+
+  /**
+   * Convert a type.
+   */
+  TypeNode convertType(TypeNode type, bool datatypesContext);
 
-  Node rewriteBooleanTermsRec(TNode n, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw();
+  Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw();
 
 public:
 
-  BooleanTermConverter(SmtEngine& smt) :
-    d_smt(smt) {
-  }
+  /**
+   * Construct a Boolean-term converter associated to the given
+   * SmtEngine.
+   */
+  BooleanTermConverter(SmtEngine& smt);
 
   /**
-   * We rewrite Boolean terms in assertions as bitvectors of length 1.
+   * Rewrite Boolean terms under a node.  The node itself is not converted
+   * if boolParent is true, but its Boolean subterms appearing in a
+   * non-Boolean context will be rewritten.
    */
-  Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw() {
+  Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() {
     std::map<TNode, Node> quantBoolVars;
-    return rewriteBooleanTermsRec(n, boolParent, quantBoolVars);
+    Assert(!(boolParent && dtParent));
+    return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
   }
 
 };/* class BooleanTermConverter */
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 26f5c9c60..fb80b27f7 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -17,37 +17,170 @@
 #include "smt/model_postprocessor.h"
 #include "smt/boolean_terms.h"
 
+using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
 
+Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
+  if(n.getType().isSubtypeOf(asType)) {
+    // good to go, we have the right type
+    return n;
+  }
+  if(!n.isConst()) {
+    // we don't handle non-const right now
+    return n;
+  }
+  if(asType.isBoolean()) {
+    if(n.getType().isBitVector(1u)) {
+      // type mismatch: should only happen for Boolean-term conversion under
+      // datatype constructor applications; rewrite from BV(1) back to Boolean
+      bool tf = (n.getConst<BitVector>().getValue() == 1);
+      return NodeManager::currentNM()->mkConst(tf);
+    }
+    if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) {
+      // type mismatch: should only happen for Boolean-term conversion under
+      // datatype constructor applications; rewrite from datatype back to Boolean
+      Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
+      Assert(n.getNumChildren() == 0);
+      // we assume (by construction) false is first; see boolean_terms.cpp
+      bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1);
+      Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl;
+      return NodeManager::currentNM()->mkConst(tf);
+    }
+  }
+  Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
+  if(n.getType().isArray()) {
+    Assert(asType.isArray());
+    if(n.getKind() == kind::STORE) {
+      return NodeManager::currentNM()->mkNode(kind::STORE,
+                                              rewriteAs(n[0], asType),
+                                              rewriteAs(n[1], asType[0]),
+                                              rewriteAs(n[2], asType[1]));
+    }
+    Assert(n.getKind() == kind::STORE_ALL);
+    const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
+    Node val = rewriteAs(asa.getExpr(), asType[1]);
+    return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
+  }
+  if(asType.getNumChildren() != n.getNumChildren() ||
+     n.getMetaKind() == kind::metakind::CONSTANT) {
+    return n;
+  }
+  NodeBuilder<> b(n.getKind());
+  TypeNode::iterator t = asType.begin();
+  for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
+    Assert(t != asType.end());
+    b << rewriteAs(*i, *t);
+  }
+  Assert(t == asType.end());
+  Debug("boolean-terms") << "+++ constructing " << b << endl;
+  Node out = b;
+  return out;
+}
+
 void ModelPostprocessor::visit(TNode current, TNode parent) {
-  Debug("tuprec") << "visiting " << current << std::endl;
+  Debug("tuprec") << "visiting " << current << endl;
   Assert(!alreadyVisited(current, TNode::null()));
   if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+    TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
     NodeBuilder<> b(kind::TUPLE);
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+    TypeNode::iterator t = expectType.begin();
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
       Assert(alreadyVisited(*i, TNode::null()));
+      Assert(t != expectType.end());
       TNode n = d_nodes[*i];
-      b << (n.isNull() ? *i : n);
+      n = n.isNull() ? *i : n;
+      if(!n.getType().isSubtypeOf(*t)) {
+        Assert(n.getType().isBitVector(1u) ||
+               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+        Assert(n.isConst());
+        Assert((*t).isBoolean());
+        if(n.getType().isBitVector(1u)) {
+          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+        } else {
+          // we assume (by construction) false is first; see boolean_terms.cpp
+          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+        }
+      } else {
+        b << n;
+      }
     }
+    Assert(t == expectType.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Assert(d_nodes[current].getType() == expectType);
   } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+    TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
+    const Record& expectRec = expectType.getConst<Record>();
     NodeBuilder<> b(kind::RECORD);
     b << current.getType().getAttribute(expr::DatatypeRecordAttr());
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+    Record::const_iterator t = expectRec.begin();
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
       Assert(alreadyVisited(*i, TNode::null()));
+      Assert(t != expectRec.end());
       TNode n = d_nodes[*i];
-      b << (n.isNull() ? *i : n);
+      n = n.isNull() ? *i : n;
+      if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
+        Assert(n.getType().isBitVector(1u) ||
+               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+        Assert(n.isConst());
+        Assert((*t).second.isBoolean());
+        if(n.getType().isBitVector(1u)) {
+          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+        } else {
+          // we assume (by construction) false is first; see boolean_terms.cpp
+          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+        }
+      } else {
+        b << n;
+      }
     }
+    Assert(t == expectRec.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Assert(d_nodes[current].getType() == expectType);
+  } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
+            ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
+              ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
+                current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
+    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+    Node realOp;
+    if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) {
+      TNode oldAsc = current.getOperator().getOperator();
+      Debug("boolean-terms") << "old asc: " << oldAsc << endl;
+      Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr());
+      Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType()));
+      Debug("boolean-terms") << "new asc: " << newAsc << endl;
+      if(newCons.getType().getRangeType().isParametricDatatype()) {
+        vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes();
+        vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes();
+        Assert(oldParams.size() == newParams.size() && oldParams.size() > 0);
+        newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType()));
+      }
+      realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons);
+    } else {
+      realOp = current.getOperator().getAttribute(BooleanTermAttr());
+    }
+    b << realOp;
+    Debug("boolean-terms") << "+ op " << b.getOperator() << endl;
+    TypeNode::iterator j = realOp.getType().begin();
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) {
+      Assert(j != realOp.getType().end());
+      Assert(alreadyVisited(*i, TNode::null()));
+      TNode repl = d_nodes[*i];
+      repl = repl.isNull() ? *i : repl;
+      Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl;
+      b << rewriteAs(repl, *j);
+    }
+    Node n = b;
+    Debug("boolean-terms") << "model-post: " << current << endl
+                           << "- returning " << n << endl;
+    d_nodes[current] = n;
   } else {
-    Debug("tuprec") << "returning self" << std::endl;
+    Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
     // rewrite to self
     d_nodes[current] = Node::null();
   }
 }/* ModelPostprocessor::visit() */
-
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
index 08e6168d9..f727a3483 100644
--- a/src/smt/model_postprocessor.h
+++ b/src/smt/model_postprocessor.h
@@ -25,9 +25,12 @@ namespace CVC4 {
 namespace smt {
 
 class ModelPostprocessor {
+  std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
 public:
   typedef Node return_type;
-  std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
+  Node rewriteAs(TNode n, TypeNode asType);
 
   bool alreadyVisited(TNode current, TNode parent) {
     return d_nodes.find(current) != d_nodes.end();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e98bffc1e..147cea85b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -63,6 +63,8 @@
 #include "theory/logic_info.h"
 #include "theory/options.h"
 #include "theory/booleans/circuit_propagator.h"
+#include "theory/booleans/boolean_term_conversion_mode.h"
+#include "theory/booleans/options.h"
 #include "util/ite_removal.h"
 #include "theory/model.h"
 #include "printer/printer.h"
@@ -586,11 +588,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_cumulativeTimeUsed(0),
   d_cumulativeResourceUsed(0),
   d_status(),
-  d_private(new smt::SmtEnginePrivate(*this)),
-  d_statisticsRegistry(new StatisticsRegistry()),
+  d_private(NULL),
+  d_statisticsRegistry(NULL),
   d_stats(NULL) {
 
   SmtScope smts(this);
+  d_private = new smt::SmtEnginePrivate(*this);
+  d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
 
   // We have mutual dependency here, so we add the prop engine to the theory
@@ -2636,10 +2640,26 @@ void SmtEnginePrivate::processAssertions() {
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
     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] && !d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
-        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-        d_smt.d_logic.enableTheory(theory::THEORY_BV);
-        d_smt.d_logic.lock();
+      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::THEORY_BV)) {
+            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+            d_smt.d_logic.enableTheory(theory::THEORY_BV);
+            d_smt.d_logic.lock();
+          }
+          break;
+        case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+          if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+            d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES);
+            d_smt.d_logic.lock();
+          }
+          break;
+        default:
+          Unhandled(mode);
+        }
       }
       d_assertionsToPreprocess[i] = n;
     }
@@ -3046,10 +3066,14 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   return quickCheck().asValidityResult();
 }
 
-Node SmtEngine::postprocess(TNode node) {
+Node SmtEngine::postprocess(TNode node, TypeNode expectedType) {
   ModelPostprocessor mpost;
   NodeVisitor<ModelPostprocessor> visitor;
-  return visitor.run(mpost, node);
+  Node value = visitor.run(mpost, node);
+  Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
+  Node realValue = mpost.rewriteAs(value, expectedType);
+  Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
+  return realValue;
 }
 
 Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
@@ -3071,7 +3095,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
   // Make sure all preprocessing is done
   d_private->processAssertions();
   Node n = d_private->simplify(Node::fromExpr(e));
-  n = postprocess(n);
+  n = postprocess(n, TypeNode::fromType(e.getType()));
   return n.toExpr();
 }
 
@@ -3093,7 +3117,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   }
   hash_map<Node, Node, NodeHashFunction> cache;
   Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
-  n = postprocess(n);
+  n = postprocess(n, TypeNode::fromType(e.getType()));
   return n.toExpr();
 }
 
@@ -3140,8 +3164,10 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingExcep
     resultNode = m->getValue(n);
   }
   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
-  resultNode = postprocess(resultNode);
+  resultNode = postprocess(resultNode, n.getType());
   Trace("smt") << "--- model-post returned " << resultNode << endl;
+  Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
+  Trace("smt") << "--- model-post expected " << n.getType() << endl;
 
   // type-check the result we got
   Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
@@ -3356,7 +3382,9 @@ void SmtEngine::checkModel(bool hardFailure) {
       // function symbol (since then the definition is recursive)
       if (val.getKind() == kind::LAMBDA) {
         // first apply the model substitutions we have so far
+        Debug("boolean-terms") << "applying subses to " << val[1] << endl;
         Node n = substitutions.apply(val[1]);
+        Debug("boolean-terms") << "++ got " << n << endl;
         // now check if n contains func by doing a substitution
         // [func->func2] and checking equality of the Nodes.
         // (this just a way to check if func is in n.)
@@ -3391,6 +3419,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       }
 
       // (3) checks complete, add the substitution
+      Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
       substitutions.addSubstitution(func, val);
     }
   }
@@ -3408,7 +3437,9 @@ void SmtEngine::checkModel(bool hardFailure) {
     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
 
     // Apply our model value substitutions.
+    Debug("boolean-terms") << "applying subses to " << n << endl;
     n = substitutions.apply(n);
+    Debug("boolean-terms") << "++ got " << n << endl;
     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
 
     // Simplify the result.
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fecfba14a..525f90ffe 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine {
    * like turning datatypes back into tuples, length-1-bitvectors back
    * into booleans, etc.
    */
-  Node postprocess(TNode n);
+  Node postprocess(TNode n, TypeNode expectedType);
 
   /**
    * This is something of an "init" procedure, but is idempotent; call
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 8cb32de18..9d58ffa75 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -13,7 +13,10 @@ libbooleans_la_SOURCES = \
 	theory_bool_rewriter.h \
 	theory_bool_rewriter.cpp \
 	circuit_propagator.h \
-	circuit_propagator.cpp
+	circuit_propagator.cpp \
+	boolean_term_conversion_mode.h \
+	boolean_term_conversion_mode.cpp
 
 EXTRA_DIST = \
-	kinds
+	kinds \
+	options_handlers.h
diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp
new file mode 100644
index 000000000..f9d80835c
--- /dev/null
+++ b/src/theory/booleans/boolean_term_conversion_mode.cpp
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file boolean_term_conversion_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <iostream>
+#include "theory/booleans/boolean_term_conversion_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
+  switch(mode) {
+  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+    out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS";
+    break;
+  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+    out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES";
+    break;
+  case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+    out << "BOOLEAN_TERM_CONVERT_NATIVE";
+    break;
+  default:
+    out << "BooleanTermConversionMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h
new file mode 100644
index 000000000..6ca908df4
--- /dev/null
+++ b/src/theory/booleans/boolean_term_conversion_mode.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file boolean_term_conversion_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
+#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+typedef enum {
+  /**
+   * Convert Boolean terms to bitvectors of size 1.
+   */
+  BOOLEAN_TERM_CONVERT_TO_BITVECTORS,
+  /**
+   * Convert Boolean terms to enumerations in the Datatypes theory.
+   */
+  BOOLEAN_TERM_CONVERT_TO_DATATYPES,
+  /**
+   * Convert Boolean terms to enumerations in the Datatypes theory IF
+   * used in a datatypes context, otherwise to a bitvector of size 1.
+   */
+  BOOLEAN_TERM_CONVERT_NATIVE
+
+} BooleanTermConversionMode;
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
diff --git a/src/theory/booleans/options b/src/theory/booleans/options
index ae14de58b..6c571f30e 100644
--- a/src/theory/booleans/options
+++ b/src/theory/booleans/options
@@ -5,4 +5,7 @@
 
 module BOOLEANS "theory/booleans/options.h" Boolean theory
 
+option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h"
+ policy for converting Boolean terms
+
 endmodule
diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h
new file mode 100644
index 000000000..2bf53b3d2
--- /dev/null
+++ b/src/theory/booleans/options_handlers.h
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+static const std::string booleanTermConversionModeHelp = "\
+Boolean term conversion modes currently supported by the\n\
+--boolean-term-conversion-mode option:\n\
+\n\
+bitvectors [default]\n\
++ Boolean terms are converted to bitvectors of size 1.\n\
+\n\
+datatypes\n\
++ Boolean terms are converted to enumerations in the Datatype theory.\n\
+\n\
+native\n\
++ Boolean terms are converted in a \"natural\" way depending on where they\n\
+  are used.  If in a datatype context, they are converted to an enumeration.\n\
+  Elsewhere, they are converted to a bitvector of size 1.\n\
+";
+
+inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "bitvectors") {
+    return BOOLEAN_TERM_CONVERT_TO_BITVECTORS;
+  } else if(optarg ==  "datatypes") {
+    return BOOLEAN_TERM_CONVERT_TO_DATATYPES;
+  } else if(optarg ==  "native") {
+    return BOOLEAN_TERM_CONVERT_NATIVE;
+  } else if(optarg ==  "help") {
+    puts(booleanTermConversionModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") +
+                          optarg + "'.  Try --boolean-term-conversion-mode help.");
+  }
+}
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 352868f7b..a369fb572 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -79,7 +79,7 @@ class EqualityTypeRule {
 
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
-        ss << "Subtypes must have a common type:" << std::endl;
+        ss << "Subexpressions must have a common base type:" << std::endl;
         ss << "Equation: " << n << std::endl;
         ss << "Type 1: " << lhsType << std::endl;
         ss << "Type 2: " << rhsType << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9e4f0de75..a3bec7af0 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -24,6 +24,7 @@
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/model.h"
 #include "smt/options.h"
+#include "smt/boolean_terms.h"
 #include "theory/quantifiers/options.h"
 
 #include <map>
@@ -311,15 +312,28 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
   }
 
+  TypeNode t = in.getType();
+
   // we only care about tuples and records here
   if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
      in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
+    if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
+      Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
+      Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
+      if(t.isTuple()) {
+        Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
+        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
+        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
+      } else {
+        Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
+        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
+        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
+      }
+    }
     // nothing to do
     return in;
   }
 
-  TypeNode t = in.getType();
-
   if(t.hasAttribute(expr::DatatypeTupleAttr())) {
     t = t.getAttribute(expr::DatatypeTupleAttr());
   } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 2a74f6d15..a4facdefe 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -176,7 +176,7 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
   void newEnumerators() {
     d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
     for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-      d_enumerators[i] = NULL;
+      d_enumerators[i] = new TypeEnumerator(getType()[i]);
     }
   }
 
@@ -205,9 +205,7 @@ public:
     if(te.d_enumerators != NULL) {
       newEnumerators();
       for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        if(te.d_enumerators[i] != NULL) {
-          d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]);
-        }
+        *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]);
       }
     }
   }
@@ -292,9 +290,7 @@ public:
     if(re.d_enumerators != NULL) {
       newEnumerators();
       for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        if(re.d_enumerators[i] != NULL) {
-          d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]);
-        }
+        *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]);
       }
     }
   }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index bbc51c9e0..42a5380e4 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -57,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{
 Expr TheoryModel::getValue( Expr expr ) const{
   Node n = Node::fromExpr( expr );
   Node ret = getValue( n );
-  return d_smt.postprocess(ret).toExpr();
+  return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
 }
 
 /** get cardinality for sort */
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 18ecbc316..574a57f19 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -820,7 +820,18 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   // can only output datatypes in the CVC4 native language
   Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
 
-  os << "DATATYPE " << dt.getName() << " =" << endl;
+  os << "DATATYPE " << dt.getName();
+  if(dt.isParametric()) {
+    os << '[';
+    for(size_t i = 0; i < dt.getNumParameters(); ++i) {
+      if(i > 0) {
+        os << ',';
+      }
+      os << dt.getParameter(i);
+    }
+    os << ']';
+  }
+  os << " =" << endl;
   Datatype::const_iterator i = dt.begin(), i_end = dt.end();
   if(i != i_end) {
     os << "  ";
diff --git a/src/util/datatype.h b/src/util/datatype.h
index de38d8835..4b6894ef8 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -450,7 +450,7 @@ public:
    * Create a new Datatype of the given name, with the given
    * parameterization.
    */
-  inline Datatype(std::string name, std::vector<Type>& params);
+  inline Datatype(std::string name, const std::vector<Type>& params);
 
   /**
    * Add a constructor to this Datatype.  Constructor names need not
@@ -620,7 +620,7 @@ inline Datatype::Datatype(std::string name) :
   d_self() {
 }
 
-inline Datatype::Datatype(std::string name, std::vector<Type>& params) :
+inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
   d_name(name),
   d_params(params),
   d_constructors(),
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 08462d51b..8e992c03e 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -38,6 +38,12 @@ TESTS =	\
 	typed_v2l30079.cvc \
 	typed_v3l20092.cvc \
 	typed_v5l30069.cvc \
+	boolean-terms-datatype.cvc \
+	boolean-terms-parametric-datatype-1.cvc \
+	boolean-terms-parametric-datatype-2.cvc \
+	boolean-terms-tuple.cvc \
+	boolean-terms-record.cvc \
+	some-boolean-tests.cvc \
 	v10l40099.cvc \
 	v2l40025.cvc \
 	v3l60006.cvc \
@@ -48,6 +54,7 @@ TESTS =	\
 	wrong-sel-simp.cvc
 
 FAILING_TESTS = \
+	pair-real-bool.smt2 \
 	datatype-dump.cvc
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/datatypes/boolean-terms-datatype.cvc b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc
new file mode 100644
index 000000000..490574b35
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE List =
+  cons(car:BOOLEAN, cdr:List) | nil
+END;
+
+x : List;
+
+ASSERT x /= nil;
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
new file mode 100644
index 000000000..b667d0bbc
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+  node(left:BOOLEAN, right:RightistTree[T]) |
+  leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc
new file mode 100644
index 000000000..b667d0bbc
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+  node(left:BOOLEAN, right:RightistTree[T]) |
+  leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-record.cvc b/test/regress/regress0/datatypes/boolean-terms-record.cvc
new file mode 100644
index 000000000..ec757d042
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-record.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [# i:INT, b:BOOLEAN #];
+
+ASSERT x /= (# i := 0, b := FALSE #);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc
new file mode 100644
index 000000000..c2d95ce8f
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [ INT, BOOLEAN ];
+
+ASSERT x /= ( 0, FALSE );
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2
new file mode 100644
index 000000000..5d028d723
--- /dev/null
+++ b/test/regress/regress0/datatypes/pair-real-bool.smt2
@@ -0,0 +1,25 @@
+;(set-option :produce-models true)
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () (
+  ( RealTree 
+    ( Node 
+      (left RealTree) 
+		  (elem Real) 
+		  (right RealTree)) 
+    (Leaf)
+   )
+))
+
+(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
+
+( declare-fun SumeAndPositiveTree ( RealTree ) (Pair Real Bool) )
+
+(declare-fun l1 () RealTree)
+(declare-fun l2 () RealTree)
+(declare-const result (Pair Real Bool))
+(assert (= l1 (Node l2 5.0 l2)))
+(assert (= result (SumeAndPositiveTree l1)))
+(assert (= (first result) 5))
+(assert (= (second result) true))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc b/test/regress/regress0/datatypes/some-boolean-tests.cvc
new file mode 100644
index 000000000..ac6ef1137
--- /dev/null
+++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+DATATYPE list[T] = cons(car:T, care:BOOLEAN, cdr:list[T]) | nil END;
+x : list[REAL];
+
+y : [INT,BOOLEAN,INT];
+ASSERT y = (5,TRUE,4);
+
+ASSERT y.1;
+
+ASSERT x = cons(1.1,TRUE,nil::list[REAL])::list[REAL];
+CHECKSAT;