9 files changed, 169 insertions, 97 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1b9bfcd10..17524a3c0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -447,8 +447,8 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
 TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
   Assert(t.isTuple() || t.isRecord());
 
-  //AJR: not sure why .getBaseType() was used in two cases below, 
-  //     disabling this, which is necessary to fix bug 605/667, 
+  //AJR: not sure why .getBaseType() was used in two cases below,
+  //     disabling this, which is necessary to fix bug 605/667,
   //     which involves records of INT which were mapped to records of REAL below.
   TypeNode tOrig = t;
   if(t.isTuple()) {
@@ -472,7 +472,8 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
     const Record& r = t.getRecord();
     std::vector< std::pair<std::string, Type> > v;
     bool changed = false;
-    for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+    const Record::FieldVector& fields = r.getFields();
+    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
       Type tn = (*i).second;
       Type base;
       if(tn.isTuple() || tn.isRecord()) {
@@ -503,9 +504,10 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dtt.setAttribute(DatatypeTupleAttr(), tOrig);
     } else {
       const Record& rec = t.getRecord();
+      const Record::FieldVector& fields = rec.getFields();
       Datatype dt("__cvc4_record");
       DatatypeConstructor c("__cvc4_record_ctor");
-      for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
+      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
         c.addArg((*i).first, (*i).second);
       }
       dt.addConstructor(c);
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index dfcba0d46..2dee03dbf 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -16,12 +16,74 @@
 
 #include "expr/record.h"
 
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+
+
 namespace CVC4 {
 
+static Record::FieldVector::const_iterator find(const Record::FieldVector& fields, std::string name){
+  for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){
+    if((*i).first == name) {
+      return i;
+    }
+  }
+  return fields.end();
+}
+
+Record::Record(const FieldVector& fields)
+    : d_fields(new FieldVector(fields))
+{
+  Debug("record") << "making " << this << " " << d_fields << std::endl;
+}
+
+Record::Record(const Record& other)
+    : d_fields(new FieldVector(other.getFields()))
+{
+  Debug("record") << "copy constructor " << this << " " << d_fields << std::endl;
+}
+
+Record::~Record() {
+  Debug("record") << "deleting " << this << " " << d_fields << std::endl;
+  delete d_fields;
+}
+
+Record& Record::operator=(const Record& r) {
+  Debug("record") << "setting " << this << " " << d_fields << std::endl;
+  Record::FieldVector& local = *d_fields;
+  local = r.getFields();
+  return *this;
+}
+
+const Record::FieldVector& Record::getFields() const {
+  return *d_fields;
+}
+
+bool Record::contains(const std::string& name) const {
+  return find(*d_fields, name) != d_fields->end();
+}
+
+
+size_t Record::getIndex(std::string name) const {
+  FieldVector::const_iterator i = find(*d_fields, name);
+  CheckArgument(i != d_fields->end(), name,
+                  "requested field `%s' does not exist in record", name.c_str());
+  return i - d_fields->begin();
+}
+
+size_t Record::getNumFields() const {
+  return d_fields->size();
+}
+
+
 std::ostream& operator<<(std::ostream& os, const Record& r) {
   os << "[# ";
   bool first = true;
-  for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+  const Record::FieldVector& fields = r.getFields();
+  for(Record::FieldVector::const_iterator i = fields.begin(),
+      i_end = fields.end(); i != i_end; ++i) {
     if(!first) {
       os << ", ";
     }
@@ -33,4 +95,32 @@ std::ostream& operator<<(std::ostream& os, const Record& r) {
   return os;
 }
 
+size_t RecordHashFunction::operator()(const Record& r) const {
+  size_t n = 0;
+  const Record::FieldVector& fields = r.getFields();
+  for(Record::FieldVector::const_iterator i = fields.begin(),
+      i_end = fields.end(); i != i_end; ++i) {
+    n = (n << 3) ^ TypeHashFunction()((*i).second);
+  }
+  return n;
+}
+
+std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
+  return out << "[" << t.getField() << "]";
+}
+
+std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
+  return out << "[" << t.getField() << "]";
+}
+
+
+const std::pair<std::string, Type>& Record::operator[](size_t index) const {
+  CheckArgument(index < d_fields->size(), index, "index out of bounds for record type");
+  return (*d_fields)[index];
+}
+
+bool Record::operator==(const Record& r) const {
+  return (*d_fields) == *(r.d_fields);
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/record.h b/src/expr/record.h
index a255649da..2cd7defe9 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -25,9 +25,14 @@
 #include <utility>
 #include "util/hash.h"
 
+// Forward Declarations
 namespace CVC4 {
+// This forward delcartion is required to resolve a cicular dependency with
+// Record which is a referenced in a Kind file.
+class CVC4_PUBLIC Type;
+} /* namespace CVC4 */
 
-class CVC4_PUBLIC Record;
+namespace CVC4 {
 
 // operators for record select and update
 
@@ -64,87 +69,37 @@ struct CVC4_PUBLIC RecordUpdateHashFunction {
 std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
 
-inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
-  return out << "[" << t.getField() << "]";
-}
-
-inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
-  return out << "[" << t.getField() << "]";
-}
-
-}/* CVC4 namespace */
-
-#warning "TODO: Address circular dependence in Record."
-#include "expr/expr.h"
-#include "expr/type.h"
-
-namespace CVC4 {
-
 // now an actual record definition
-
 class CVC4_PUBLIC Record {
-  std::vector< std::pair<std::string, Type> > d_fields;
-
 public:
+  // Type must stay as incomplete types throughout this header!
+  // Everything containing a Type must be a pointer or a reference.
+  typedef std::vector< std::pair<std::string, Type> > FieldVector;
 
-  typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator;
-  typedef const_iterator iterator;
-
-  Record(const std::vector< std::pair<std::string, Type> >& fields) :
-    d_fields(fields) {
-  }
-
-  const_iterator find(std::string name) const {
-    const_iterator i;
-    for(i = begin(); i != end(); ++i) {
-      if((*i).first == name) {
-        break;
-      }
-    }
-    return i;
-  }
-
-  size_t getIndex(std::string name) const {
-    const_iterator i = find(name);
-    CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str());
-    return i - begin();
-  }
-
-  size_t getNumFields() const {
-    return d_fields.size();
-  }
-
-  const_iterator begin() const {
-    return d_fields.begin();
-  }
+  Record(const FieldVector& fields);
+  Record(const Record& other);
+  ~Record();
+  Record& operator=(const Record& r);
 
-  const_iterator end() const {
-    return d_fields.end();
-  }
+  bool contains(const std::string &name) const;
 
-  std::pair<std::string, Type> operator[](size_t index) const {
-    CheckArgument(index < d_fields.size(), index, "index out of bounds for record type");
-    return d_fields[index];
-  }
+  size_t getIndex(std::string name) const;
+  size_t getNumFields() const;
 
-  bool operator==(const Record& r) const {
-    return d_fields == r.d_fields;
-  }
+  const FieldVector& getFields() const;
+  const std::pair<std::string, Type>& operator[](size_t index) const;
 
+  bool operator==(const Record& r) const;
   bool operator!=(const Record& r) const {
     return !(*this == r);
   }
 
+private:
+  FieldVector* d_fields;
 };/* class Record */
 
 struct CVC4_PUBLIC RecordHashFunction {
-  inline size_t operator()(const Record& r) const {
-    size_t n = 0;
-    for(Record::iterator i = r.begin(); i != r.end(); ++i) {
-      n = (n << 3) ^ TypeHashFunction()((*i).second);
-    }
-    return n;
-  }
+  size_t operator()(const Record& r) const;
 };/* struct RecordHashFunction */
 
 std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 869304c0a..659e80550 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -114,9 +114,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
       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::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+      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;
         }
@@ -125,7 +127,7 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     return true;
   }
   if(isFunction()) {
-    // A function is a subtype of another if the args are the same type, and 
+    // 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).
@@ -189,7 +191,9 @@ bool TypeNode::isComparableTo(TypeNode t) const {
         }
         // r1's fields must be comparable to r2's, in order
         // names must match also
-        for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+        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;
           }
@@ -474,8 +478,10 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
     }
     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::const_iterator i = r0.begin(), j = r1.begin(); i != r0.end(); ++i, ++j) {
+    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
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 460b1ee03..ff3753a67 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1559,8 +1559,7 @@ recordStore[CVC4::Expr& f]
         PARSER_STATE->parseError(ss.str());
       }
       const Record& rec = RecordType(t).getRecord();
-      Record::const_iterator fld = rec.find(id);
-      if(fld == rec.end()) {
+      if(! rec.contains(id)) {
         PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
       }
       f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f);
@@ -1687,8 +1686,7 @@ postfixTerm[CVC4::Expr& f]
             PARSER_STATE->parseError("record-select applied to non-record");
           }
           const Record& rec = RecordType(t).getRecord();
-          Record::const_iterator fld = rec.find(id);
-          if(fld == rec.end()) {
+          if(!rec.contains(id)){
             PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
           }
           f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index d33b97d66..db4558af6 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -390,7 +390,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << "(# ";
       TNode::iterator i = n.begin();
       bool first = true;
-      for(Record::const_iterator j = rec.begin(); j != rec.end(); ++i, ++j) {
+      const Record::FieldVector& fields = rec.getFields();
+      for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
         if(!first) {
           out << ", ";
         }
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index f7dfdb410..4372c0c18 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -389,8 +389,9 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext)
   }
   if(type.isRecord()) {
     const Record& rec = type.getConst<Record>();
+    const Record::FieldVector& fields = rec.getFields();
     vector< pair<string, Type> > flds;
-    for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
+    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
       TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
       if(TypeNode::fromType((*i).second) != converted) {
         flds.push_back(make_pair((*i).first, converted.toType()));
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 485b2c9a9..f9e449be3 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -15,12 +15,15 @@
  **/
 
 #include "smt/model_postprocessor.h"
-#include "smt/boolean_terms.h"
+
 #include "expr/node_manager_attributes.h"
+#include "expr/record.h"
+#include "smt/boolean_terms.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::smt;
+
+namespace CVC4 {
+namespace smt {
 
 Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
   if(n.getType().isSubtypeOf(asType)) {
@@ -191,10 +194,11 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     const Record& expectRec = expectType.getConst<Record>();
     NodeBuilder<> b(kind::RECORD);
     b << current.getType().getAttribute(expr::DatatypeRecordAttr());
-    Record::const_iterator t = expectRec.begin();
+    const Record::FieldVector& fields = expectRec.getFields();
+    Record::FieldVector::const_iterator t = fields.begin();
     for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
       Assert(alreadyVisited(*i, TNode::null()));
-      Assert(t != expectRec.end());
+      Assert(t != fields.end());
       TNode n = d_nodes[*i];
       n = n.isNull() ? *i : n;
       if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
@@ -212,7 +216,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
         b << n;
       }
     }
-    Assert(t == expectRec.end());
+    Assert(t == fields.end());
     d_nodes[current] = b;
     Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     Assert(d_nodes[current].getType() == expectType);
@@ -298,3 +302,6 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     d_nodes[current] = Node::null();
   }
 }/* ModelPostprocessor::visit() */
+
+} /* namespace smt */
+} /* namespace CVC4 */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 23e68a6a8..8b723f43e 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -35,6 +35,7 @@ namespace datatypes {
 
 typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
 
+
 struct DatatypeConstructorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate, AssertionException) {
@@ -401,12 +402,13 @@ struct RecordTypeRule {
     Assert(n.getKind() == kind::RECORD);
     NodeManagerScope nms(nodeManager);
     const Record& rec = n.getOperator().getConst<Record>();
+    const Record::FieldVector& fields = rec.getFields();
     if(check) {
-      Record::iterator i = rec.begin();
+      Record::FieldVector::const_iterator i = fields.begin();
       for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
           child_it != child_it_end;
           ++child_it, ++i) {
-        if(i == rec.end()) {
+        if(i == fields.end()) {
           throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
         }
         if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
@@ -415,7 +417,7 @@ struct RecordTypeRule {
           throw TypeCheckingExceptionPrivate(n, ss.str());
         }
       }
-      if(i != rec.end()) {
+      if(i != fields.end()) {
         throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
       }
     }
@@ -424,6 +426,15 @@ struct RecordTypeRule {
 };/* struct RecordTypeRule */
 
 struct RecordSelectTypeRule {
+  inline static Record::FieldVector::const_iterator record_find(const Record::FieldVector& fields, std::string name){
+    for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){
+      if((*i).first == name) {
+        return i;
+      }
+    }
+    return fields.end();
+  }
+
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
     Assert(n.getKind() == kind::RECORD_SELECT);
     NodeManagerScope nms(nodeManager);
@@ -439,8 +450,9 @@ struct RecordSelectTypeRule {
       recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
     }
     const Record& rec = recordType.getRecord();
-    Record::const_iterator field = rec.find(rs.getField());
-    if(field == rec.end()) {
+    const Record::FieldVector& fields = rec.getFields();
+    Record::FieldVector::const_iterator field = record_find(fields, rs.getField());
+    if(field == fields.end()) {
       std::stringstream ss;
       ss << "Record-select field `" << rs.getField()
          << "' is not a valid field name for the record type";
@@ -465,8 +477,7 @@ struct RecordUpdateTypeRule {
         recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
       }
       const Record& rec = recordType.getRecord();
-      Record::const_iterator field = rec.find(ru.getField());
-      if(field == rec.end()) {
+      if(!rec.contains(ru.getField())) {
         std::stringstream ss;
         ss << "Record-update field `" << ru.getField()
            << "' is not a valid field name for the record type";
@@ -482,9 +493,10 @@ struct RecordProperties {
     Assert(type.getKind() == kind::RECORD_TYPE);
 
     const Record& rec = type.getRecord();
+    const Record::FieldVector& fields = rec.getFields();
     std::vector<Node> children;
-    for(Record::iterator i = rec.begin(),
-          i_end = rec.end();
+    for(Record::FieldVector::const_iterator i = fields.begin(),
+          i_end = fields.end();
         i != i_end;
         ++i) {
       children.push_back((*i).second.mkGroundTerm());