Use unique_ptr for UF modules (#3080)

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 393d9f6409a69fe0857769d5b48530de694dea85..7ea3f8370f9cede8296513af86d168811e4fa4e8 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -50,7 +50,8 @@ TheoryUF::TheoryUF(context::Context* c,
       d_notify(*this),
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
-      d_thss(NULL),
+      d_thss(nullptr),
+      d_ho(nullptr),
       d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
       d_conflict(c, false),
       d_functionsTerms(c),
@@ -63,7 +64,6 @@ TheoryUF::TheoryUF(context::Context* c,
 }
 
 TheoryUF::~TheoryUF() {
-  delete d_thss;
 }
 
 void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -81,12 +81,13 @@ void TheoryUF::finishInit() {
   if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind()
       && options::ufssMode() != UF_SS_NONE)
   {
-    d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);
+    d_thss.reset(new StrongSolverTheoryUF(
+        getSatContext(), getUserContext(), *d_out, this));
   }
   if (options::ufHo())
   {
     d_equalityEngine.addFunctionKind(kind::HO_APPLY);
-    d_ho = new HoExtension(*this, getSatContext(), getUserContext());
+    d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext()));
   }
 }
 

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index df1cc232bb1c2c852eba2916719d55e8d0988b3d..248f4690082857a9ad2d7e7cb71e729586866b90 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -120,8 +120,10 @@ private:
   /** The notify class */
   NotifyClass d_notify;
 
-  /** The associated theory strong solver (or NULL if none) */
-  StrongSolverTheoryUF* d_thss;
+  /** The associated theory strong solver (or nullptr if it does not exist) */
+  std::unique_ptr<StrongSolverTheoryUF> d_thss;
+  /** the higher-order solver extension (or nullptr if it does not exist) */
+  std::unique_ptr<HoExtension> d_ho;
 
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
@@ -132,8 +134,6 @@ private:
   /** The conflict node */
   Node d_conflictNode;
 
-  /** the higher-order solver extension */
-  HoExtension* d_ho;
 
   /** node for true */
   Node d_true;
@@ -218,9 +218,8 @@ private:
 
   eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 
-  StrongSolverTheoryUF* getStrongSolver() {
-    return d_thss;
-  }
+  /** get a pointer to the strong solver (uf with cardinality) */
+  StrongSolverTheoryUF* getStrongSolver() const { return d_thss.get(); }
   /** are we in conflict? */
   bool inConflict() const { return d_conflict; }