Change Record to shared_ptr (#3778)

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4d2467f84543d9af4ed8d4bdd5dac3d451d0eaae..5f43fb24fcb2b68acc3bc80e859772265d0981a3 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -42,7 +42,6 @@ Datatype::~Datatype()
   ExprManagerScope ems(*d_em);
   d_internal.reset();
   d_constructors.clear();
-  delete d_record;
 }
 
 Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
@@ -207,7 +206,7 @@ void Datatype::resolve(const std::map<std::string, DatatypeType>& resolutions,
     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);
+    d_record.reset(new Record(fields));
   }
 }
 
@@ -911,7 +910,7 @@ bool Datatype::isTuple() const
 
 bool Datatype::isRecord() const { return d_isRecord; }
 
-Record* Datatype::getRecord() const { return d_record; }
+Record* Datatype::getRecord() const { return d_record.get(); }
 bool Datatype::operator!=(const Datatype& other) const
 {
   return !(*this == other);

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 1ae59f00c8d53f199f06bdc1bb2f2b4e8f3ab8f7..f9edb998fe2b7fd2c258bc35b16414759f2be8be 100644 (file)
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -899,7 +899,7 @@ class CVC4_PUBLIC Datatype {
   /** self type */
   Type d_self;
   /** the data of the record for this datatype (if applicable) */
-  Record* d_record;
+  std::shared_ptr<Record> d_record;
   /** whether the datatype is a record */
   bool d_isRecord;
   /** the constructors of this datatype */

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index e53b989f0275cca3ebba4ee8f9088b1fc5803a3c..bf992d2d5807c44346b186c07c604431043f6ebb 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -247,6 +247,8 @@ void SolverBlack::testMkRecordSort()
   std::vector<std::pair<std::string, Sort>> empty;
   TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(fields));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
+  Sort recSort = d_solver->mkRecordSort(fields);
+  TS_ASSERT_THROWS_NOTHING(recSort.getDatatype());
 }
 
 void SolverBlack::testMkSetSort()