From 2c289524f23a2ec481224b2ea569397acbb5e39e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Jul 2019 11:59:39 -0500
Subject: Use unique_ptr for UF modules (#3080)

---
 src/theory/uf/theory_uf.h | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'src/theory/uf/theory_uf.h')

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; }
 
-- 
cgit v1.2.3