update from the master

59 files changed, 633 insertions, 565 deletions

diff --git a/src/expr/array.h b/src/expr/array.h
index ab554171f..cf050e077 100644
--- a/src/expr/array.h
+++ b/src/expr/array.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file array.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Array types.
  **
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 6ac07c81d..c8e346e48 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file array_store_all.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of a constant array (an array in which the
  ** element is the same for all indices)
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 293b785a9..0a9c8344a 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file array_store_all.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of a constant array (an array in which the
  ** element is the same for all indices)
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index 42906e557..46d2871ff 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file ascription_type.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A class representing a type ascription
  **
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index cd5b35384..3cf242988 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file attribute.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Tim King
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief AttributeManager implementation.
  **
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 432fbbac9..13bedeaf8 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file attribute.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Node attributes.
  **
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index dae11fd74..60d2069e7 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file attribute_internals.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Node attributes' internals.
  **
diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
index 45dc368a5..4875bdf50 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file attribute_unique_id.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/expr/chain.h b/src/expr/chain.h
index e052a2ed8..703aa76ed 100644
--- a/src/expr/chain.h
+++ b/src/expr/chain.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file chain.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h
index 0c3b690b2..611a88e6f 100644
--- a/src/expr/convenience_node_builders.h
+++ b/src/expr/convenience_node_builders.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file convenience_node_builders.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Convenience node builders.
  **
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 32c0bb6dd..d14ac26d4 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file datatype.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A class representing a Datatype definition
  **
@@ -51,6 +51,10 @@ typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFin
 typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
 typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
 
+Datatype::~Datatype(){
+  delete d_record;
+}
+
 const Datatype& Datatype::datatypeOf(Expr item) {
   ExprManagerScope ems(item);
   TypeNode t = Node::fromExpr(item).getType();
@@ -133,6 +137,14 @@ void Datatype::resolve(ExprManager* em,
       d_involvesUt =  true;
     }
   }
+
+  if( d_isRecord ){
+    std::vector< std::pair<std::string, Type> > fields;
+    for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
+      fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
+    }
+    d_record = new Record(fields);
+  }
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -152,10 +164,12 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
 }
 
 void Datatype::setTuple() {
+  PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
   d_isTuple = true;
 }
 
 void Datatype::setRecord() {
+  PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
   d_isRecord = true;
 }
 
@@ -185,20 +199,24 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons
 bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( d_card_rec_singleton==0 ){
-    Assert( d_card_u_assume.empty() );
-    std::vector< Type > processing;
-    if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
-      d_card_rec_singleton = 1;
+    if( isCodatatype() ){
+      Assert( d_card_u_assume.empty() );
+      std::vector< Type > processing;
+      if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
+        d_card_rec_singleton = 1;
+      }else{
+        d_card_rec_singleton = -1;
+      }
+      if( d_card_rec_singleton==1 ){
+        Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
+        for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
+          Trace("dt-card") << "  " << d_card_u_assume [i] << std::endl;
+        }
+        Trace("dt-card") << std::endl;
+      }
     }else{
       d_card_rec_singleton = -1;
     }
-    if( d_card_rec_singleton==1 ){
-      Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
-      for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
-        Trace("dt-card") << "  " << d_card_u_assume [i] << std::endl;
-      }
-      Trace("dt-card") << std::endl;
-    }
   }
   return d_card_rec_singleton==1;
 }
@@ -288,10 +306,11 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) {
   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
     return self.getAttribute(DatatypeUFiniteAttr());
   }
+  //start by assuming it is not
+  self.setAttribute(DatatypeUFiniteComputedAttr(), true);
+  self.setAttribute(DatatypeUFiniteAttr(), false);
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
     if(! (*i).isUFinite()) {
-      self.setAttribute(DatatypeUFiniteComputedAttr(), true);
-      self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;
     }
   }
@@ -820,7 +839,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
     return self.getAttribute(DatatypeFiniteAttr());
   }
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) {
+    if(! (*i).getRangeType().getCardinality().isFinite()) {
       self.setAttribute(DatatypeFiniteComputedAttr(), true);
       self.setAttribute(DatatypeFiniteAttr(), false);
       return false;
@@ -840,9 +859,18 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
     return self.getAttribute(DatatypeUFiniteAttr());
   }
+  bool success = true;
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type t = SelectorType((*i).getSelector().getType()).getRangeType();
-    if(!t.isSort() && !t.getCardinality().isFinite()) {
+    Type t = (*i).getRangeType();
+    if( t.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)t).getDatatype();
+      if( !dt.isUFinite() ){
+        success = false;
+      }
+    }else if(!t.isSort() && !t.getCardinality().isFinite()) {
+      success = false;
+    }
+    if(!success ){
       self.setAttribute(DatatypeUFiniteComputedAttr(), true);
       self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;
@@ -974,6 +1002,10 @@ SelectorType DatatypeConstructorArg::getType() const {
   return getSelector().getType();
 }
 
+Type DatatypeConstructorArg::getRangeType() const {
+  return getType().getRangeType();
+}
+
 bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
   return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
 }
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 625fbb5d4..1197b4a3b 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file datatype.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A class representing a Datatype definition
  **
@@ -155,6 +155,11 @@ public:
   SelectorType getType() const;
 
   /**
+   * Get the range type of this argument.
+   */
+  Type getRangeType() const;
+
+  /**
    * Get the name of the type of this constructor argument
    * (Datatype field).  Can be used for not-yet-resolved Datatypes
    * (in which case the name of the unresolved type, or "[self]"
@@ -474,6 +479,7 @@ private:
   bool d_isCo;
   bool d_isTuple;
   bool d_isRecord;
+  Record * d_record;
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
@@ -553,6 +559,8 @@ public:
    */
   inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
 
+  ~Datatype();
+
   /**
    * Add a constructor to this Datatype.  Constructor names need not
    * be unique; they are for convenience and pretty-printing only.
@@ -602,6 +610,9 @@ public:
   /** is this a record datatype? */
   inline bool isRecord() const;
 
+  /** get the record representation for this datatype */
+  inline Record * getRecord() const;
+
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
@@ -772,6 +783,7 @@ inline Datatype::Datatype(std::string name, bool isCo) :
   d_isCo(isCo),
   d_isTuple(false),
   d_isRecord(false),
+  d_record(NULL),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -788,6 +800,7 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo
   d_isCo(isCo),
   d_isTuple(false),
   d_isRecord(false),
+  d_record(NULL),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -844,6 +857,10 @@ inline bool Datatype::isRecord() const {
   return d_isRecord;
 }
 
+inline Record * Datatype::getRecord() const {
+  return d_record;
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index a6e2c1ece..23e6df7dc 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file emptyset.cpp
  ** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Kshitij Bansal, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index cf9d050f8..a606951f0 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file emptyset.h
  ** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Kshitij Bansal, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/expr/expr.i b/src/expr/expr.i
index b50686f52..354cacdc0 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -130,7 +130,13 @@ namespace CVC4 {
 
 %include "expr/expr.h"
 
+#ifdef SWIGPYTHON
+/* The python bindings on Mac OS X have trouble with this one - leave it
+ * out for now. */
+//%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+#else
 %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+#endif
 %template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>;
 %template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
 %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
index 4c7ab3c8b..1d6df2a4e 100644
--- a/src/expr/expr_iomanip.cpp
+++ b/src/expr/expr_iomanip.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_iomanip.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2015  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Expr IO manipulation classes.
  **
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index b3370e75a..94e2b46ea 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_iomanip.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2015  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Expr IO manipulation classes.
  **
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 66930cf55..11c1e284d 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -40,7 +40,6 @@
 
 %include "expr/expr_manager.h"
 
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
@@ -67,10 +66,7 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
@@ -78,6 +74,25 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RegExp>;
+#ifdef SWIGPYTHON
+/* The python bindings cannot differentiate between bool and other basic
+ * types like enum and int. Therefore, we rename mkConst for the bool
+ * case into mkBoolConst.
+*/
+%template(mkBoolConst) CVC4::ExprManager::mkConst<bool>;
+
+// These cases have trouble too.  Remove them for now.
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
+
+#else
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<bool>;
+#endif
 
 %include "expr/expr_manager.h"
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index a8e8f04be..cd4c274e5 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_manager_scope.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index ce7a92b48..84f674d2b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_manager_template.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Christopher L. Conway
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Public-facing expression manager interface, implementation
  **
@@ -142,6 +142,11 @@ StringType ExprManager::stringType() const {
   return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
 }
 
+RegExpType ExprManager::regExpType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType())));
+}
+
 RealType ExprManager::realType() const {
   NodeManagerScope nms(d_nodeManager);
   return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
@@ -791,7 +796,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
         j != j_end;
         ++j) {
       const DatatypeConstructorArg& a = *j;
-      Type selectorType = a.getSelector().getType();
+      Type selectorType = a.getType();
       Assert(a.isResolved() &&
              selectorType.isSelector() &&
              SelectorType(selectorType).getDomain() == dtt,
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 37ef128f4..04f2f4289 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_manager_template.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Public-facing expression manager interface
  **
@@ -121,6 +121,9 @@ public:
   /** Get the type for strings. */
   StringType stringType() const;
 
+  /** Get the type for regular expressions. */
+  RegExpType regExpType() const;
+
   /** Get the type for reals. */
   RealType realType() const;
 
diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h
index 20977011c..d3dbd2902 100644
--- a/src/expr/expr_stream.h
+++ b/src/expr/expr_stream.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_stream.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A stream interface for expressions
  **
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index a6cdedd00..43e4a7b76 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_template.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Kshitij Bansal
- ** Minor contributors (to current version): Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Morgan Deters, Kshitij Bansal, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Public-facing expression interface, implementation.
  **
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index d037a6bb9..5c3f89e9c 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file expr_template.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Public-facing expression interface.
  **
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index 02e9728f0..6858f8ab9 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file kind_map.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A bitmap of Kinds
  **
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 799d1ac33..440d6b586 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file kind_template.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Template for the Node kind header
  **
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
index 8cb092a64..308ad06df 100644
--- a/src/expr/matcher.h
+++ b/src/expr/matcher.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file matcher.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A class representing a type matcher
  **
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 539db1c91..9025aa02a 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file metakind_template.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Template for the metakind header.
  **
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index cf9a772b7..793b6af97 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Reference-counted encapsulation of a pointer to node information.
  **
diff --git a/src/expr/node.h b/src/expr/node.h
index a51de6d66..998294da3 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot, Clark Barrett, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Reference-counted encapsulation of a pointer to node information
  **
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index e1a083a78..0dd4e44e8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_builder.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A builder interface for Nodes.
  **
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e6e44928d..0809a0331 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_manager.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): ACSYS, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Expression manager implementation.
  **
@@ -170,7 +170,9 @@ NodeManager::~NodeManager() {
     d_operators[i] = Node::null();
   }
 
-  d_tupleAndRecordTypes.clear();
+  //d_tupleAndRecordTypes.clear();
+  d_tt_cache.d_children.clear();
+  d_rt_cache.d_children.clear();
 
   Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
@@ -461,6 +463,47 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
   return TypeNode(mkTypeConst(bounds));
 }
 
+TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
+  if( index==types.size() ){
+    if( d_data.isNull() ){
+      Datatype dt("__cvc4_tuple");
+      dt.setTuple();
+      DatatypeConstructor c("__cvc4_tuple_ctor");
+      for (unsigned i = 0; i < types.size(); ++ i) {
+        std::stringstream ss;
+        ss << "__cvc4_tuple_stor_" << i;
+        c.addArg(ss.str().c_str(), types[i].toType());
+      }
+      dt.addConstructor(c);
+      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
+    }
+    return d_data;
+  }else{
+    return d_children[types[index]].getTupleType( nm, types, index+1 );
+  }
+}
+
+TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) {
+  if( index==rec.getNumFields() ){
+    if( d_data.isNull() ){
+      const Record::FieldVector& fields = rec.getFields();
+      Datatype dt("__cvc4_record");
+      dt.setRecord();
+      DatatypeConstructor c("__cvc4_record_ctor");
+      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
+        c.addArg((*i).first, (*i).second);
+      }
+      dt.addConstructor(c);
+      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
+    }
+    return d_data;
+  }else{
+    return d_children[TypeNode::fromType( rec[index].second )][rec[index].first].getRecordType( nm, rec, index+1 );
+  }
+}
+
 TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   std::vector< TypeNode > ts;
   Debug("tuprec-debug") << "Make tuple type : ";
@@ -470,60 +513,11 @@ TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
     Debug("tuprec-debug") << types[i] << " ";
   }
   Debug("tuprec-debug") << std::endl;
-  //index based on function type
-  TypeNode tindex;
-  if( types.empty() ){
-    //do nothing (will index on null type)
-  }else if( types.size()==1 ){
-    tindex = types[0];
-  }else{
-    TypeNode tt = ts.back();
-    ts.pop_back();
-    tindex = mkFunctionType( ts, tt );
-    ts.push_back( tt );
-  }
-  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
-  if(dtt.isNull()) {
-    Datatype dt("__cvc4_tuple");
-    dt.setTuple();
-    DatatypeConstructor c("__cvc4_tuple_ctor");
-    for (unsigned i = 0; i < ts.size(); ++ i) {
-      std::stringstream ss;
-      ss << "__cvc4_tuple_stor_" << i;
-      c.addArg(ss.str().c_str(), ts[i].toType());
-    }
-    dt.addConstructor(c);
-    dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-    dtt.setAttribute(DatatypeTupleAttr(), tindex);
-    Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
-  }else{
-    Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
-  }
-  Assert(!dtt.isNull());
-  return dtt;
+  return d_tt_cache.getTupleType( this, ts );
 }
 
 TypeNode NodeManager::mkRecordType(const Record& rec) {
-  //index based on type constant
-  TypeNode tindex = mkTypeConst(rec);
-  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
-  if(dtt.isNull()) {
-    const Record::FieldVector& fields = rec.getFields();
-    Datatype dt("__cvc4_record");
-    dt.setRecord();
-    DatatypeConstructor c("__cvc4_record_ctor");
-    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-      c.addArg((*i).first, (*i).second);
-    }
-    dt.addConstructor(c);
-    dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-    dtt.setAttribute(DatatypeRecordAttr(), tindex);
-    Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
-  }else{
-    Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
-  }
-  Assert(!dtt.isNull());
-  return dtt;
+  return d_rt_cache.getRecordType( this, rec );
 }
 
 void NodeManager::reclaimAllZombies(){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 45c9afbde..7d2b13e4c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_manager.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Christopher L. Conway, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A manager for Nodes
  **
@@ -166,7 +166,20 @@ class NodeManager {
   /**
    * A map of tuple and record types to their corresponding datatype.
    */
-  std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
+  class TupleTypeCache {
+  public:
+    std::map< TypeNode, TupleTypeCache > d_children;
+    TypeNode d_data;
+    TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 );
+  };
+  class RecTypeCache {
+  public:
+    std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children;
+    TypeNode d_data;
+    TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 );
+  };
+  TupleTypeCache d_tt_cache;
+  RecTypeCache d_rt_cache;
 
   /**
    * Keep a count of all abstract values produced by this NodeManager.
@@ -692,7 +705,7 @@ public:
   inline TypeNode stringType();
 
   /** Get the (singleton) type for RegExp. */
-  inline TypeNode regexpType();
+  inline TypeNode regExpType();
 
   /** Get the (singleton) type for rounding modes. */
   inline TypeNode roundingModeType();
@@ -988,7 +1001,7 @@ inline TypeNode NodeManager::stringType() {
 }
 
 /** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regexpType() {
+inline TypeNode NodeManager::regExpType() {
   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
 }
 
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index 41086ac21..20e1c6c50 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_manager_attributes.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -28,8 +28,6 @@ namespace attr {
   struct VarNameTag { };
   struct GlobalVarTag { };
   struct SortArityTag { };
-  struct DatatypeTupleTag { };
-  struct DatatypeRecordTag { };
   struct TypeTag { };
   struct TypeCheckedTag { };
 }/* CVC4::expr::attr namespace */
@@ -37,10 +35,6 @@ namespace attr {
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
 typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
 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;
 typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
 typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
 
diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp
index ec2de105a..3915aa9bd 100644
--- a/src/expr/node_manager_listeners.cpp
+++ b/src/expr/node_manager_listeners.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file node_manager_listeners.h
+/*! \file node_manager_listeners.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Listeners that NodeManager registers to its Options object.
  **
diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h
index fc7c2f65f..caff3a545 100644
--- a/src/expr/node_manager_listeners.h
+++ b/src/expr/node_manager_listeners.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_manager_listeners.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Listeners that NodeManager registers to its Options object.
  **
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 77fc05e3b..9d37f6e6e 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_self_iterator.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Iterator supporting Node "self-iteration"
  **
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index ab18973cb..a40075ca9 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_value.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief An expression node.
  **
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index c39c14604..fbf3ff76e 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file node_value.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Christopher L. Conway, Tim King, Dejan Jovanovic
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief An expression node.
  **
diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp
index e273bcece..2050d2d15 100644
--- a/src/expr/pickle_data.cpp
+++ b/src/expr/pickle_data.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file pickle_data.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief This is a "pickle" for expressions, CVC4-internal view
  **
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h
index acf0dccdd..6c283719a 100644
--- a/src/expr/pickle_data.h
+++ b/src/expr/pickle_data.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file pickle_data.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief This is a "pickle" for expressions, CVC4-internal view
  **
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index d0501ca2b..ab8037a9a 100644
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file pickler.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King, Kshitij Bansal
+ ** Top contributors (to current version):
+ **   Morgan Deters, Kshitij Bansal, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief This is a "pickler" for expressions
  **
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index cf1754d93..abd927788 100644
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file pickler.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief This is a "pickler" for expressions
  **
diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
index 5ccc3484a..52b580148 100644
--- a/src/expr/predicate.cpp
+++ b/src/expr/predicate.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file predicate.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of predicates for predicate subtyping
  **
diff --git a/src/expr/predicate.h b/src/expr/predicate.h
index 669ecc29f..a7003fbd1 100644
--- a/src/expr/predicate.h
+++ b/src/expr/predicate.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file predicate.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of predicates for predicate subtyping
  **
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index ec5ef96f1..0d2fd6527 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file record.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A class representing a record definition
  **
diff --git a/src/expr/record.h b/src/expr/record.h
index d30536fb0..84feb7e1d 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file record.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A class representing a Record definition
  **
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index c0a80b7ce..185006e73 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file symbol_table.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
+ ** Top contributors (to current version):
+ **   Morgan Deters, Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Convenience class for scoping variable and type
  ** declarations (implementation)
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 451a482dc..efd0f1a13 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file symbol_table.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
+ ** Top contributors (to current version):
+ **   Morgan Deters, Christopher L. Conway, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Convenience class for scoping variable and type declarations.
  **
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 6b5bdf07c..0c4d554ef 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type.cpp
  ** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Dejan Jovanovic, Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of expression types
  **
@@ -223,6 +223,12 @@ bool Type::isString() const {
   return d_typeNode->isString();
 }
 
+/** Is this the regexp type? */
+bool Type::isRegExp() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isRegExp();
+}
+
 /** Is this the rounding mode type? */
 bool Type::isRoundingMode() const {
   NodeManagerScope nms(d_nodeManager);
@@ -427,6 +433,11 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) :
   PrettyCheckArgument(isNull() || isString(), this);
 }
 
+RegExpType::RegExpType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  PrettyCheckArgument(isNull() || isRegExp(), this);
+}
+
 RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   PrettyCheckArgument(isNull() || isRoundingMode(), this);
diff --git a/src/expr/type.h b/src/expr/type.h
index 67d259fec..43cb3ffbf 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type.h
  ** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Dejan Jovanovic, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Martin Brain
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Interface for expression types.
  **
@@ -47,6 +47,7 @@ class BooleanType;
 class IntegerType;
 class RealType;
 class StringType;
+class RegExpType;
 class RoundingModeType;
 class BitVectorType;
 class ArrayType;
@@ -258,6 +259,12 @@ public:
   bool isString() const;
 
   /**
+   * Is this the regexp type?
+   * @return true if the type is the regexp type
+   */
+  bool isRegExp() const;
+
+  /**
    * Is this the rounding mode type?
    * @return true if the type is the rounding mode type
    */
@@ -424,6 +431,18 @@ public:
 };/* class StringType */
 
 /**
+ * Singleton class encapsulating the string type.
+ */
+class CVC4_PUBLIC RegExpType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  RegExpType(const Type& type) throw(IllegalArgumentException);
+};/* class RegExpType */
+
+
+/**
  * Singleton class encapsulating the rounding mode type.
  */
 class CVC4_PUBLIC RoundingModeType : public Type {
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 4b04adfc9..3df73b268 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type_checker.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A type checker
  **
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 061e1b4e0..8ed894a22 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type_checker_template.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief TypeChecker implementation
  **
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 755b16e46..5d672e6ac 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type_node.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Reference-counted encapsulation of a pointer to node information.
  **
@@ -93,46 +93,28 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
           t.getConst<TypeConstant>() == REAL_TYPE );
     }
   }
-  if(isTuple() || isRecord()) {
-    if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
+  if(isTuple() && t.isTuple()) {
+    const Datatype& dt1 = getDatatype();
+    const Datatype& dt2 = t.getDatatype();
+    if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
       return false;
     }
-    if(isTuple()) {
-      if(getNumChildren() != t.getNumChildren()) {
+    // r1's fields must be subtypes of r2's, in order
+    for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+      if( !dt1[0][i].getRangeType().isSubtypeOf( dt2[0][i].getRangeType() ) ){
         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 = getRecord();
-      const Record& r2 = t.getRecord();
-      if(r1.getNumFields() != r2.getNumFields()) {
-        return false;
-      }
-      const Record::FieldVector& fields1 = r1.getFields();
-      const Record::FieldVector& fields2 = r2.getFields();
-      // r1's fields must be subtypes of r2's, in order
-      // names must match also
-      for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) {
-        if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
-          return false;
-        }
-      }
     }
     return true;
+  }else if( t.isRecord() && t.isRecord() ){
+    //records are not subtypes of each other in current implementation
   }
   if(isFunction()) {
     // A function is a subtype of another if the args are the same type, and
     // the return type is a subtype of the other's.  This is enough for now
     // (and it's necessary for model generation, since a Real-valued function
     // might return a constant Int and thus the model value is typed differently).
-    return t.isFunction() &&
-           getArgTypes() == t.getArgTypes() &&
-           getRangeType().isSubtypeOf(t.getRangeType());
+    return t.isFunction() && getArgTypes() == t.getArgTypes() && getRangeType().isSubtypeOf(t.getRangeType());
   }
   if(isParametricDatatype() && t.isParametricDatatype()) {
     Assert(getKind() == kind::PARAMETRIC_DATATYPE);
@@ -153,6 +135,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
   if(isSet() && t.isSet()) {
     return getSetElementType().isSubtypeOf(t.getSetElementType());
   }
+  if(isArray() && t.isArray()) {
+    //reverse for index type
+    return t.getArrayIndexType().isSubtypeOf(getArrayIndexType()) && 
+           getArrayConstituentType().isSubtypeOf(t.getArrayConstituentType());
+  }
   return false;
 }
 
@@ -163,39 +150,21 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
     return t.isSubtypeOf(NodeManager::currentNM()->realType());
   }
-  if(isTuple() || isRecord()) {
-    if(t.isTuple() || t.isRecord()) {
-      if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
+  if(isTuple() && t.isTuple()) {
+    const Datatype& dt1 = getDatatype();
+    const Datatype& dt2 = t.getDatatype();
+    if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
+      return false;
+    }
+    // r1's fields must be subtypes of r2's, in order
+    for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+      if( !dt1[0][i].getRangeType().isComparableTo( dt2[0][i].getRangeType() ) ){
         return false;
       }
-      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 = getRecord();
-        const Record& r2 = t.getRecord();
-        if(r1.getNumFields() != r2.getNumFields()) {
-          return false;
-        }
-        // r1's fields must be comparable to r2's, in order
-        // names must match also
-        const Record::FieldVector& fields1 = r1.getFields();
-        const Record::FieldVector& fields2 = r2.getFields();
-        for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) {
-          if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
-            return false;
-          }
-        }
-      }
-      return true;
     }
+    return true;
+  //}else if( isRecord() && t.isRecord() ){
+    //record types are incomparable in current implementation
   } else if(isParametricDatatype() && t.isParametricDatatype()) {
     Assert(getKind() == kind::PARAMETRIC_DATATYPE);
     Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
@@ -211,10 +180,12 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   } else if(isSet() && t.isSet()) {
     return getSetElementType().isComparableTo(t.getSetElementType());
   }
-
-  if(isPredicateSubtype()) {
-    return t.isComparableTo(getSubtypeParentType());
+  if(isArray() && t.isArray()) {
+    return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
   }
+  //if(isPredicateSubtype()) {
+  //  return t.isComparableTo(getSubtypeParentType());
+  //}
   return false;
 }
 
@@ -271,13 +242,13 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
 
 /** Is this a tuple type? */
 bool TypeNode::isTuple() const {
-  return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) ||
+  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) ||
     ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
 }
 
 /** Is this a record type? */
 bool TypeNode::isRecord() const {
-  return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) )  ||
+  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() )  ||
     ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
 }
 
@@ -294,14 +265,16 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(dt.getNumConstructors()==1);
   vector<TypeNode> types;
   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
-    types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType()));
+    types.push_back(TypeNode::fromType(dt[0][i].getRangeType()));
   }
   return types;
 }
 
 const Record& TypeNode::getRecord() const {
   Assert(isRecord());
-  return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
+  const Datatype & dt = getDatatype();
+  return *(dt.getRecord());
+  //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
 }
 
 vector<TypeNode> TypeNode::getSExprTypes() const {
@@ -341,6 +314,14 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
 }
 
 TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
+  return commonTypeNode( t0, t1, true );
+}
+
+TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
+  return commonTypeNode( t0, t1, false );
+}
+
+TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
@@ -361,65 +342,75 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
         return t0; //IntegerType
       } else if(t1.isReal()) {
         // t0 == IntegerType && t1.isReal() && !t1.isInteger()
-        return NodeManager::currentNM()->realType(); // RealType
+        return isLeast ? t1 : t0; // RealType
       } else {
         return TypeNode(); // null type
       }
     case REAL_TYPE:
       if(t1.isReal()) {
-        return t0; // RealType
+        return isLeast ? t0 : t1; // RealType
       } else {
         return TypeNode(); // null type
       }
     default:
-      if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
-        return t0; // t0 is a constant type
-      } else {
+      //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
+      //  return t0; // t0 is a constant type
+      //} else {
         return TypeNode(); // null type
-      }
+      //}
     }
   } else if(t1.getKind() == kind::TYPE_CONSTANT) {
-    return leastCommonTypeNode(t1, t0); // decrease the number of special cases
+    return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
   }
 
   // t0 != t1 &&
   // t0.getKind() == kind::TYPE_CONSTANT &&
   // t1.getKind() == kind::TYPE_CONSTANT
   switch(t0.getKind()) {
-  case kind::ARRAY_TYPE:
   case kind::BITVECTOR_TYPE:
   case kind::SORT_TYPE:
   case kind::CONSTRUCTOR_TYPE:
   case kind::SELECTOR_TYPE:
   case kind::TESTER_TYPE:
-    if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
-      return t0;
-    } else {
+    //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
+    //  return t0;
+    //} else {
       return TypeNode();
-    }
+    //}
   case kind::FUNCTION_TYPE:
     return TypeNode(); // Not sure if this is right
   case kind::SET_TYPE: {
     // take the least common subtype of element types
     TypeNode elementType;
-    if(t1.isSet() &&
-       ! (elementType = leastCommonTypeNode(t0[0], t1[0])).isNull() ) {
+    if(t1.isSet() && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull() ) {
       return NodeManager::currentNM()->mkSetType(elementType);
     } else {
       return TypeNode();
     }
   }
+  case kind::ARRAY_TYPE: {
+    TypeNode indexType, elementType;
+    if(t1.isArray() &&
+       ! (indexType = commonTypeNode(t0[0], t1[0], !isLeast)).isNull() && 
+       ! (elementType = commonTypeNode(t0[1], t1[1], isLeast)).isNull() ) {
+      return NodeManager::currentNM()->mkArrayType(indexType, elementType);
+    } else {
+      return TypeNode();
+    }
+  }
   case kind::SEXPR_TYPE:
     Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
     return TypeNode();
   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
-      return leastCommonTypeNode(t1, t0); //decrease the number of special cases
-    }
+    //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
+    //  return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases
+    //}
+    return TypeNode();
   case kind::SUBRANGE_TYPE:
+    /*
     if(t1.isSubrange()) {
       const SubrangeBounds& t0SR = t0.getSubrangeBounds();
       const SubrangeBounds& t1SR = t1.getSubrangeBounds();
@@ -449,62 +440,28 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       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>();
-    const Record::FieldVector& fields0 = r0.getFields();
-    const Record::FieldVector& fields1 = r1.getFields();
-    // construct childwise leastCommonType, if one exists
-    for(Record::FieldVector::const_iterator i = fields0.begin(), j = fields1.begin(); i != fields0.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));
-  }
 */
+    return TypeNode();
   case kind::DATATYPE_TYPE:
-    // t1 might be a subtype tuple or record
-    if(t1.getBaseType() == t0) {
-      return t0;
+    if( t0.isTuple() && t1.isTuple() ){
+      const Datatype& dt1 = t0.getDatatype();
+      const Datatype& dt2 = t1.getDatatype();
+      if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
+        std::vector< TypeNode > lc_types;
+        for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+          TypeNode tc = commonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ), isLeast );
+          if( tc.isNull() ){
+            return tc;
+          }else{
+            lc_types.push_back( tc );
+          }
+        }
+        return NodeManager::currentNM()->mkTupleType( lc_types );
+      }
     }
+    //else if( t0.isRecord() && t1.isRecord() ){
+      //record types are not related in current implementation
+    //}
     // otherwise no common ancestor
     return TypeNode();
   case kind::PARAMETRIC_DATATYPE: {
@@ -519,12 +476,12 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
     }
     vector<Type> v;
     for(size_t i = 1; i < t0.getNumChildren(); ++i) {
-      v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType());
+      v.push_back(commonTypeNode(t0[i], t1[i], isLeast).toType());
     }
     return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v));
   }
   default:
-    Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
+    Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
     return TypeNode();
   }
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 4c48cc3ca..cfb61a085 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type_node.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tianyi Liang, Kshitij Bansal, Tim King
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Martin Brain
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Reference-counted encapsulation of a pointer to node information.
  **
@@ -642,8 +642,10 @@ public:
    * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice
    */
   static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
+  static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
 
 private:
+  static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
 
   /**
    * Returns the leastUpperBound in the extended type lattice of two
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index bc780a7e5..4874a84b8 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file type_properties_template.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Template for the Type properties header
  **
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 97bc3ae4b..c88c3b591 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file uninterpreted_constant.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of constants of uninterpreted sorts
  **
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 5b2293df6..7d7a3759b 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file uninterpreted_constant.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of constants of uninterpreted sorts
  **
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
index 59ce5c606..00d2c3eac 100644
--- a/src/expr/variable_type_map.h
+++ b/src/expr/variable_type_map.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file variable_type_map.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **