Tuples and records merge. Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 files changed, 330 insertions, 64 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index cacfa9215..7cb5eb459 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -517,6 +517,11 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 }
 
+RecordType ExprManager::mkRecordType(const Record& rec) {
+  NodeManagerScope nms(d_nodeManager);
+  return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+}
+
 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
   std::vector<TypeNode> typeNodes;
@@ -804,20 +809,20 @@ Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
   return t;
 }
 
-Expr ExprManager::mkVar(const std::string& name, Type type) {
+Expr ExprManager::mkVar(const std::string& name, Type type, bool isGlobal) {
   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
+  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, isGlobal);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
   INC_STAT_VAR(type, false);
   return Expr(this, n);
 }
 
-Expr ExprManager::mkVar(Type type) {
+Expr ExprManager::mkVar(Type type, bool isGlobal) {
   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
-  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
+  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, isGlobal));
 }
 
 Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 561d99392..b9cae9431 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -359,6 +359,11 @@ public:
   TupleType mkTupleType(const std::vector<Type>& types);
 
   /**
+   * Make a record type with types from the rec parameter.
+   */
+  RecordType mkRecordType(const Record& rec);
+
+  /**
    * Make a symbolic expressiontype with types from
    * <code>types[0..types.size()-1]</code>.  <code>types</code> may
    * have any number of elements.
@@ -464,8 +469,8 @@ public:
     throw(TypeCheckingException);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const std::string& name, Type type);
-  Expr mkVar(Type type);
+  Expr mkVar(const std::string& name, Type type, bool isGlobal = false);
+  Expr mkVar(Type type, bool isGlobal = false);
   Expr mkBoundVar(const std::string& name, Type type);
   Expr mkBoundVar(Type type);
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 28a47d84d..ec8d0d12f 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -136,7 +136,9 @@ function typerule {
   lineno=${BASH_LINENO[0]}
   check_theory_seen
   typerules="${typerules}
+#line $lineno \"$kf\"
   case kind::$1:
+#line $lineno \"$kf\"
     typeNode = $2::computeType(nodeManager, n, check);
     break;
 "
@@ -147,7 +149,9 @@ function construle {
   lineno=${BASH_LINENO[0]}
   check_theory_seen
   construles="${construles}
+#line $lineno \"$kf\"
   case kind::$1:
+#line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
 "
 }
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 11e889ca2..e580b6348 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -27,6 +27,9 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
                                                            std::string message) throw() :
   Exception(message),
   d_node(new Node(node)) {
+#ifdef CVC4_DEBUG
+  s_debugLastException = toString().c_str();
+#endif /* CVC4_DEBUG */
 }
 
 TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
diff --git a/src/expr/node.h b/src/expr/node.h
index d36953054..a3b8853a0 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -67,10 +67,6 @@ private:
   /** The node responsible for the failure */
   NodeTemplate<true>* d_node;
 
-protected:
-
-  TypeCheckingExceptionPrivate() throw() : Exception() {}
-
 public:
 
   /**
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0a13222dd..f040c7c72 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -320,7 +320,7 @@ Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const
   }
   if((flags & SKOLEM_NO_NOTIFY) == 0) {
     for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-      (*i)->nmNotifyNewSkolem(n, comment);
+      (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL);
     }
   }
   return n;
@@ -395,4 +395,38 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
   return TypeNode(mkTypeConst(bounds));
 }
 
+TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
+  Assert(t.isTuple() || t.isRecord());
+
+  // if the type doesn't have an associated datatype, then make one for it
+  TypeNode& dtt = d_tupleAndRecordTypes[t];
+  if(dtt.isNull()) {
+    if(t.isTuple()) {
+      Datatype dt("__cvc4_tuple");
+      DatatypeConstructor c("__cvc4_tuple_ctor");
+      for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) {
+        c.addArg("__cvc4_tuple_stor", (*i).toType());
+      }
+      dt.addConstructor(c);
+      dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
+      Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
+    } else {
+      const Record& rec = t.getRecord();
+      Datatype dt("__cvc4_record");
+      DatatypeConstructor c("__cvc4_record_ctor");
+      for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
+        c.addArg((*i).first, (*i).second);
+      }
+      dt.addConstructor(c);
+      dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
+      Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
+    }
+    dtt.setAttribute(DatatypeRecordAttr(), t);
+  } else {
+    Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
+  }
+  Assert(!dtt.isNull());
+  return dtt;
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ea733e771..6e08a9bc2 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -53,10 +53,16 @@ class TypeChecker;
 namespace attr {
   struct VarNameTag { };
   struct SortArityTag { };
+  struct DatatypeTupleTag { };
+  struct DatatypeRecordTag { };
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
 typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
+/** Attribute true for datatype types that are replacements for tuple types */
+typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr;
+/** Attribute true for datatype types that are replacements for record types */
+typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr;
 
 }/* CVC4::expr namespace */
 
@@ -71,8 +77,8 @@ public:
   virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
   virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
   virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
-  virtual void nmNotifyNewVar(TNode n) { }
-  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment) { }
+  virtual void nmNotifyNewVar(TNode n, bool isGlobal) { }
+  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { }
 };/* class NodeManagerListener */
 
 class NodeManager {
@@ -82,8 +88,8 @@ class NodeManager {
   friend class expr::TypeChecker;
 
   // friends so they can access mkVar() here, which is private
-  friend Expr ExprManager::mkVar(const std::string&, Type);
-  friend Expr ExprManager::mkVar(Type);
+  friend Expr ExprManager::mkVar(const std::string&, Type, bool isGlobal);
+  friend Expr ExprManager::mkVar(Type, bool isGlobal);
 
   // friend so it can access NodeManager's d_listeners and notify clients
   friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
@@ -158,6 +164,11 @@ class NodeManager {
   std::vector<NodeManagerListener*> d_listeners;
 
   /**
+   * A map of tuple and record types to their corresponding datatype.
+   */
+  std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
+
+  /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
    * NodeValue.  In particular, "non-inlined" constants are permitted
@@ -288,12 +299,12 @@ class NodeManager {
    * version of this is private to avoid internal uses of mkVar() from
    * within CVC4.  Such uses should employ mkSkolem() instead.
    */
-  Node mkVar(const std::string& name, const TypeNode& type);
-  Node* mkVarPtr(const std::string& name, const TypeNode& type);
+  Node mkVar(const std::string& name, const TypeNode& type, bool isGlobal = false);
+  Node* mkVarPtr(const std::string& name, const TypeNode& type, bool isGlobal = false);
 
   /** Create a variable with the given type. */
-  Node mkVar(const TypeNode& type);
-  Node* mkVarPtr(const TypeNode& type);
+  Node mkVar(const TypeNode& type, bool isGlobal = false);
+  Node* mkVarPtr(const TypeNode& type, bool isGlobal = false);
 
 public:
 
@@ -413,7 +424,8 @@ public:
   enum SkolemFlags {
     SKOLEM_DEFAULT = 0,   /**< default behavior */
     SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
-    SKOLEM_EXACT_NAME = 2 /**< do not make the name unique by adding the id */
+    SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
+    SKOLEM_IS_GLOBAL = 4  /**< global vars appear in models even after a pop */
   };/* enum SkolemFlags */
 
   /**
@@ -717,6 +729,14 @@ public:
   inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
 
   /**
+   * Make a record type with the description from rec.
+   *
+   * @param rec a description of the record
+   * @returns the record type
+   */
+  inline TypeNode mkRecordType(const Record& rec);
+
+  /**
    * Make a symbolic expression type with types from
    * <code>types</code>. <code>types</code> may have any number of
    * elements.
@@ -780,6 +800,12 @@ public:
     throw(TypeCheckingExceptionPrivate);
 
   /**
+   * Given a tuple or record type, get the internal datatype used for
+   * it.  Makes the DatatypeType if necessary.
+   */
+  TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
+
+  /**
    * Get the type for the given node and optionally do type checking.
    *
    * Initial type computation will be near-constant time if
@@ -1067,6 +1093,10 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
 }
 
+inline TypeNode NodeManager::mkRecordType(const Record& rec) {
+  return mkTypeConst(rec);
+}
+
 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
@@ -1456,25 +1486,25 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 }
 
 
-inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
+inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bool isGlobal) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n);
+    (*i)->nmNotifyNewVar(n, isGlobal);
   }
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const std::string& name,
-                                   const TypeNode& type) {
+                                   const TypeNode& type, bool isGlobal) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   setAttribute(*n, expr::VarNameAttr(), name);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n);
+    (*i)->nmNotifyNewVar(*n, isGlobal);
   }
   return n;
 }
@@ -1492,22 +1522,22 @@ inline Node* NodeManager::mkBoundVarPtr(const std::string& name,
   return n;
 }
 
-inline Node NodeManager::mkVar(const TypeNode& type) {
+inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n);
+    (*i)->nmNotifyNewVar(n, isGlobal);
   }
   return n;
 }
 
-inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
+inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n);
+    (*i)->nmNotifyNewVar(*n, isGlobal);
   }
   return n;
 }
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index cb1e829c4..cc52b11b9 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -350,6 +350,19 @@ Type::operator TupleType() const throw(IllegalArgumentException) {
   return TupleType(*this);
 }
 
+/** Is this a record type? */
+bool Type::isRecord() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isRecord();
+}
+
+/** Cast to a record type */
+Type::operator RecordType() const throw(IllegalArgumentException) {
+  NodeManagerScope nms(d_nodeManager);
+  CheckArgument(isNull() || isRecord(), this);
+  return RecordType(*this);
+}
+
 /** Is this a symbolic expression type? */
 bool Type::isSExpr() const {
   NodeManagerScope nms(d_nodeManager);
@@ -449,6 +462,10 @@ Type FunctionType::getRangeType() const {
   return makeType(d_typeNode->getRangeType());
 }
 
+size_t TupleType::getLength() const {
+  return d_typeNode->getTupleLength();
+}
+
 vector<Type> TupleType::getTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> types;
@@ -461,6 +478,11 @@ vector<Type> TupleType::getTypes() const {
   return types;
 }
 
+const Record& RecordType::getRecord() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getRecord();
+}
+
 vector<Type> SExprType::getTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> types;
@@ -565,6 +587,11 @@ TupleType::TupleType(const Type& t) throw(IllegalArgumentException) :
   CheckArgument(isNull() || isTuple(), this);
 }
 
+RecordType::RecordType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  CheckArgument(isNull() || isRecord(), this);
+}
+
 SExprType::SExprType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   CheckArgument(isNull() || isSExpr(), this);
@@ -633,12 +660,13 @@ std::vector<Type> ConstructorType::getArgTypes() const {
 }
 
 const Datatype& DatatypeType::getDatatype() const {
+  NodeManagerScope nms(d_nodeManager);
   if( d_typeNode->isParametricDatatype() ) {
     CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
     const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
     return dt;
   } else {
-    return d_typeNode->getConst<Datatype>();
+    return d_typeNode->getDatatype();
   }
 }
 
diff --git a/src/expr/type.h b/src/expr/type.h
index e5590aa59..4223d71ab 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -38,6 +38,7 @@ class ExprManagerMapCollection;
 class SmtEngine;
 
 class Datatype;
+class Record;
 
 template <bool ref_count>
 class NodeTemplate;
@@ -54,6 +55,7 @@ class SelectorType;
 class TesterType;
 class FunctionType;
 class TupleType;
+class RecordType;
 class SExprType;
 class SortType;
 class SortConstructorType;
@@ -323,6 +325,18 @@ public:
   operator TupleType() const throw(IllegalArgumentException);
 
   /**
+   * Is this a record type?
+   * @return true if the type is a record type
+   */
+  bool isRecord() const;
+
+  /**
+   * Cast this type to a record type
+   * @return the RecordType
+   */
+  operator RecordType() const throw(IllegalArgumentException);
+
+  /**
    * Is this a symbolic expression type?
    * @return true if the type is a symbolic expression type
    */
@@ -527,11 +541,29 @@ public:
   /** Construct from the base type */
   TupleType(const Type& type = Type()) throw(IllegalArgumentException);
 
+  /** Get the length of the tuple.  The same as getTypes().size(). */
+  size_t getLength() const;
+
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
+
 };/* class TupleType */
 
 /**
+ * Class encapsulating a record type.
+ */
+class CVC4_PUBLIC RecordType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  RecordType(const Type& type = Type()) throw(IllegalArgumentException);
+
+  /** Get the constituent types */
+  const Record& getRecord() const;
+};/* class RecordType */
+
+/**
  * Class encapsulating a tuple type.
  */
 class CVC4_PUBLIC SExprType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index ae870b1c2..236f48017 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -90,6 +90,22 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
           t.getConst<TypeConstant>() == REAL_TYPE );
     }
   }
+  if(isTuple() || isRecord()) {
+    if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
+      return true;
+    }
+    if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
+       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;
+      }
+    }
+    return true;
+  }
   if(isPredicateSubtype()) {
     return getSubtypeParentType().isSubtypeOf(t);
   }
@@ -103,6 +119,30 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
     return t.isSubtypeOf(NodeManager::currentNM()->realType());
   }
+  if(t.isDatatype() && (isTuple() || isRecord())) {
+    if(t.isTuple() || t.isRecord()) {
+      if(NodeManager::currentNM()->getDatatypeForTupleRecord(t) ==
+         NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
+        return true;
+      }
+      if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
+         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;
+        }
+      }
+      return true;
+    } else {
+      return t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this);
+    }
+  } else if(isDatatype() && (t.isTuple() || t.isRecord())) {
+    Assert(!isTuple() && !isRecord());// should have been handled above
+    return *this == NodeManager::currentNM()->getDatatypeForTupleRecord(t);
+  }
   if(isPredicateSubtype()) {
     return t.isComparableTo(getSubtypeParentType());
   }
@@ -123,6 +163,8 @@ TypeNode TypeNode::getBaseType() const {
   TypeNode realt = NodeManager::currentNM()->realType();
   if (isSubtypeOf(realt)) {
     return realt;
+  } else if (isTuple() || isRecord()) {
+    return NodeManager::currentNM()->getDatatypeForTupleRecord(*this);
   } else if (isPredicateSubtype()) {
     return getSubtypeParentType().getBaseType();
   }
@@ -152,6 +194,11 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
+size_t TypeNode::getTupleLength() const {
+  Assert(isTuple());
+  return getNumChildren();
+}
+
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
   vector<TypeNode> types;
@@ -161,6 +208,11 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   return types;
 }
 
+const Record& TypeNode::getRecord() const {
+  Assert(isRecord());
+  return getConst<Record>();
+}
+
 vector<TypeNode> TypeNode::getSExprTypes() const {
   Assert(isSExpr());
   vector<TypeNode> types;
@@ -205,41 +257,41 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
   Assert(!t0.isNull());
   Assert(!t1.isNull());
 
-  if(EXPECT_TRUE(t0 == t1)){
+  if(EXPECT_TRUE(t0 == t1)) {
     return t0;
-  }else{ // t0 != t1
-    if(t0.getKind()== kind::TYPE_CONSTANT){
+  } else { // t0 != t1
+    if(t0.getKind()== kind::TYPE_CONSTANT) {
       switch(t0.getConst<TypeConstant>()) {
       case INTEGER_TYPE:
-        if(t1.isInteger()){
+        if(t1.isInteger()) {
           // t0 == IntegerType && t1.isInteger()
           return t0; //IntegerType
-        }else if(t1.isReal()){
+        } else if(t1.isReal()) {
           // t0 == IntegerType && t1.isReal() && !t1.isInteger()
           return NodeManager::currentNM()->realType(); // RealType
-        }else{
-          return TypeNode(); //null type
+        } else {
+          return TypeNode(); // null type
         }
       case REAL_TYPE:
-        if(t1.isReal()){
+        if(t1.isReal()) {
           return t0; // RealType
-        }else{
+        } else {
           return TypeNode(); // null type
         }
       default:
-        if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){
+        if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
           return t0; // t0 is a constant type
-        }else{
+        } else {
           return TypeNode(); // null type
         }
       }
-    }else if(t1.getKind() == kind::TYPE_CONSTANT){
+    } else if(t1.getKind() == kind::TYPE_CONSTANT) {
       return leastCommonTypeNode(t1, t0); //decrease the number of special cases
-    }else{
+    } else {
       // t0 != t1 &&
       // t0.getKind() == kind::TYPE_CONSTANT &&
       // t1.getKind() == kind::TYPE_CONSTANT
-      switch(t0.getKind()){
+      switch(t0.getKind()) {
       case kind::ARRAY_TYPE:
       case kind::BITVECTOR_TYPE:
       case kind::SORT_TYPE:
@@ -247,9 +299,9 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       case kind::CONSTRUCTOR_TYPE:
       case kind::SELECTOR_TYPE:
       case kind::TESTER_TYPE:
-        if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){
+        if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
           return t0;
-        }else{
+        } else {
           return TypeNode();
         }
       case kind::FUNCTION_TYPE:
@@ -257,48 +309,96 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       case kind::SEXPR_TYPE:
         Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
         return TypeNode(); // Not sure if this is right
-      case kind::TUPLE_TYPE:
-        Unimplemented("haven't implemented leastCommonType for tuples yet");
-        return TypeNode(); // Not sure if this is right
       case kind::SUBTYPE_TYPE:
         if(t1.isPredicateSubtype()){
           // This is the case where both t0 and t1 are predicate subtypes.
           return leastCommonPredicateSubtype(t0, t1);
-        }else{ //t0 is a predicate subtype and t1 is not
+        }else{ // t0 is a predicate subtype and t1 is not
           return leastCommonTypeNode(t1, t0); //decrease the number of special cases
         }
       case kind::SUBRANGE_TYPE:
-        if(t1.isSubrange()){
-          const SubrangeBounds& t0SR= t0.getSubrangeBounds();
+        if(t1.isSubrange()) {
+          const SubrangeBounds& t0SR = t0.getSubrangeBounds();
           const SubrangeBounds& t1SR = t1.getSubrangeBounds();
-          if(SubrangeBounds::joinIsBounded(t0SR, t1SR)){
+          if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) {
             SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR);
             return NodeManager::currentNM()->mkSubrangeType(j);
-          }else{
+          } else {
             return NodeManager::currentNM()->integerType();
           }
-        }else if(t1.isPredicateSubtype()){
-          //t0 is a subrange
-          //t1 is not a subrange
-          //t1 is a predicate subtype
-          if(t1.isInteger()){
+        } else if(t1.isPredicateSubtype()) {
+          // t0 is a subrange
+          // t1 is not a subrange
+          // t1 is a predicate subtype
+          if(t1.isInteger()) {
             return NodeManager::currentNM()->integerType();
-          }else if(t1.isReal()){
+          } else if(t1.isReal()) {
             return NodeManager::currentNM()->realType();
-          }else{
+          } else {
             return TypeNode();
           }
-        }else{
-          //t0 is a subrange
-          //t1 is not a subrange
+        } else {
+          // t0 is a subrange
+          // t1 is not a subrange
           // t1 is not a type constant && is not a predicate subtype
           // t1 cannot be real subtype or integer.
           Assert(t1.isReal());
           Assert(t1.isInteger());
           return TypeNode();
         }
+      case kind::TUPLE_TYPE: {
+        // if the other == this one, we returned already, above
+        if(t0.getBaseType() == t1) {
+          return t1;
+        }
+        if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) {
+          // no compatibility between t0, t1
+          return TypeNode();
+        }
+        std::vector<TypeNode> types;
+        // construct childwise leastCommonType, if one exists
+        for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) {
+          TypeNode kid = leastCommonTypeNode(*i, *j);
+          if(kid.isNull()) {
+            // no common supertype: types t0, t1 not compatible
+            return TypeNode();
+          }
+          types.push_back(kid);
+        }
+        // if we make it here, we constructed the least common type
+        return NodeManager::currentNM()->mkTupleType(types);
+      }
+      case kind::RECORD_TYPE: {
+        // if the other == this one, we returned already, above
+        if(t0.getBaseType() == t1) {
+          return t1;
+        }
+        const Record& r0 = t0.getConst<Record>();
+        if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) {
+          // no compatibility between t0, t1
+          return TypeNode();
+        }
+        std::vector< std::pair<std::string, Type> > fields;
+        const Record& r1 = t1.getConst<Record>();
+        // construct childwise leastCommonType, if one exists
+        for(Record::const_iterator i = r0.begin(), j = r1.begin(); i != r0.end(); ++i, ++j) {
+          TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second));
+          if((*i).first != (*j).first || kid.isNull()) {
+            // if field names differ, or no common supertype, then
+            // types t0, t1 not compatible
+            return TypeNode();
+          }
+          fields.push_back(std::make_pair((*i).first, kid.toType()));
+        }
+        // if we make it here, we constructed the least common type
+        return NodeManager::currentNM()->mkRecordType(Record(fields));
+      }
       case kind::DATATYPE_TYPE:
-        // two datatypes that aren't == have no common ancestors
+        // t1 might be a subtype tuple or record
+        if(t1.getBaseType() == t0) {
+          return t0;
+        }
+        // otherwise no common ancestor
         return TypeNode();
       default:
         Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index fc142191d..93e9f1ca7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -536,9 +536,18 @@ public:
   /** Is this a tuple type? */
   bool isTuple() const;
 
+  /** Get the length of a tuple type */
+  size_t getTupleLength() const;
+
   /** Get the constituent types of a tuple type */
   std::vector<TypeNode> getTupleTypes() const;
 
+  /** Is this a record type? */
+  bool isRecord() const;
+
+  /** Get the description of the record type */
+  const Record& getRecord() const;
+
   /** Is this a symbolic expression type? */
   bool isSExpr() const;
 
@@ -572,6 +581,9 @@ public:
   /** Is this a tester type */
   bool isTester() const;
 
+  /** Get the Datatype specification from a datatype type */
+  const Datatype& getDatatype() const;
+
   /** Get the size of this bit-vector type */
   unsigned getBitVectorSize() const;
 
@@ -883,6 +895,12 @@ inline bool TypeNode::isTuple() const {
     ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
 }
 
+/** Is this a record type? */
+inline bool TypeNode::isRecord() const {
+  return getKind() == kind::RECORD_TYPE ||
+    ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
+}
+
 /** Is this a symbolic expression type? */
 inline bool TypeNode::isSExpr() const {
   return getKind() == kind::SEXPR_TYPE ||
@@ -920,6 +938,7 @@ inline bool TypeNode::isBitVector() const {
 /** Is this a datatype type */
 inline bool TypeNode::isDatatype() const {
   return getKind() == kind::DATATYPE_TYPE ||
+    getKind() == kind::TUPLE_TYPE || getKind() == kind::RECORD_TYPE ||
     ( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
 }
 
@@ -951,6 +970,16 @@ inline bool TypeNode::isBitVector(unsigned size) const {
     ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) );
 }
 
+/** Get the datatype specification from a datatype type */
+inline const Datatype& TypeNode::getDatatype() const {
+  Assert(isDatatype());
+  if(getKind() == kind::DATATYPE_TYPE) {
+    return getConst<Datatype>();
+  } else {
+    return NodeManager::currentNM()->getDatatypeForTupleRecord(*this).getConst<Datatype>();
+  }
+}
+
 /** Get the size of this bit-vector type */
 inline unsigned TypeNode::getBitVectorSize() const {
   Assert(isBitVector());