Remove Record object and convert to Node-level API (#5575)

Required for detangling NodeManager from the Expr layer.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 748a1ce067fc570a80a0039920fb7009ffdd9f53..36edfdb468f04b31363a03a94efdbfa496556b58 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3650,7 +3650,7 @@ Sort Solver::mkRecordSort(
 {
   NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  std::vector<std::pair<std::string, Type>> f;
+  std::vector<std::pair<std::string, TypeNode>> f;
   size_t i = 0;
   for (const auto& p : fields)
   {
@@ -3661,10 +3661,10 @@ Sort Solver::mkRecordSort(
         this == p.second.d_solver, "parameter sort", p.second, i)
         << "sort associated to this solver object";
     i += 1;
-    f.emplace_back(p.first, p.second.d_type->toType());
+    f.emplace_back(p.first, *p.second.d_type);
   }
 
-  return Sort(this, getNodeManager()->mkRecordType(Record(f)));
+  return Sort(this, getNodeManager()->mkRecordType(f));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c70cfce3b1e34a98b5886847e169c8b7b4a871e2..fde92c4e1cbeaaf47ba7f5faa4f359d35294376a 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -736,13 +736,14 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto
 }
 
 TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) {
-  if( index==rec.getNumFields() ){
+  if (index == rec.size())
+  {
     if( d_data.isNull() ){
-      const Record::FieldVector& fields = rec.getFields();
       std::stringstream sst;
       sst << "__cvc4_record";
-      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-        sst << "_" << (*i).first << "_" << (*i).second;
+      for (const std::pair<std::string, TypeNode>& i : rec)
+      {
+        sst << "_" << i.first << "_" << i.second;
       }
       DType dt(sst.str());
       dt.setRecord();
@@ -750,17 +751,18 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
       ssc << sst.str() << "_ctor";
       std::shared_ptr<DTypeConstructor> c =
           std::make_shared<DTypeConstructor>(ssc.str());
-      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-        c->addArg((*i).first, TypeNode::fromType((*i).second));
+      for (const std::pair<std::string, TypeNode>& i : rec)
+      {
+        c->addArg(i.first, i.second);
       }
       dt.addConstructor(c);
       d_data = nm->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 );
   }
+  return d_children[rec[index].second][rec[index].first].getRecordType(
+      nm, rec, index + 1);
 }
 
 TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts)

diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index f4004d2e7845be5103500c9443f48aafb94a6415..08944912a1bf43894a2146bbe7247ade1ac1ebae 100644 (file)
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -18,109 +18,12 @@
 
 #include "base/check.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, const 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);
-  PrettyCheckArgument(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;
-  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 << ", ";
-    }
-    os << (*i).first << ":" << (*i).second;
-    first = false;
-  }
-  os << " #]";
-
-  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 RecordUpdate& t) {
   return out << "[" << t.getField() << "]";
 }
 
-
-const std::pair<std::string, Type>& Record::operator[](size_t index) const {
-  PrettyCheckArgument(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 62ccd42db1296b456aca05ec186ddec98b8899e9..a0d545a56800b5d1fa25e847d584813e8e95df66 100644 (file)
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -29,7 +29,7 @@
 namespace CVC4 {
 // This forward delcartion is required to resolve a cicular dependency with
 // Record which is a referenced in a Kind file.
-class Type;
+class TypeNode;
 } /* namespace CVC4 */
 
 namespace CVC4 {
@@ -53,40 +53,7 @@ struct CVC4_PUBLIC RecordUpdateHashFunction {
 
 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
 
-// now an actual record definition
-class CVC4_PUBLIC Record {
- 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;
-
-  Record(const FieldVector& fields);
-  Record(const Record& other);
-  ~Record();
-  Record& operator=(const Record& r);
-
-  bool contains(const std::string &name) const;
-
-  size_t getIndex(std::string name) const;
-  size_t getNumFields() const;
-
-  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 {
-  size_t operator()(const Record& r) const;
-};/* struct RecordHashFunction */
-
-std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
+using Record = std::vector<std::pair<std::string, TypeNode>>;
 
 }/* CVC4 namespace */