From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Jul 2019 16:59:39 +0000 (-0500)
Subject: Use unique_ptr for UF modules (#3080)
X-Git-Tag: cvc5-1.0.0~4095
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2c289524f23a2ec481224b2ea569397acbb5e39e;p=cvc5.git

Use unique_ptr for UF modules (#3080)
---

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 393d9f640..7ea3f8370 100644
--- 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 df1cc232b..248f46900 100644
--- 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; }