From be2ee6f3ea202812a9ddecfad3a8eeddfd44db3e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2020 14:19:09 -0600 Subject: [PATCH] Change Record to shared_ptr (#3778) --- src/expr/datatype.cpp | 5 ++--- src/expr/datatype.h | 2 +- test/unit/api/solver_black.h | 2 ++ 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 4d2467f84..5f43fb24f 100644 --- 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& resolutions, for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){ fields.push_back( std::pair( (*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 1ae59f00c..f9edb998f 100644 --- 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 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 e53b989f0..bf992d2d5 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -247,6 +247,8 @@ void SolverBlack::testMkRecordSort() std::vector> 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() -- 2.30.2