Use std:unique_ptr instead of raw pointers in theory/bv. (#2385)

This should also fix CIDs 1465687, 1465695, 1465696, and 1465701.

10 files changed, 96 insertions, 107 deletions

diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index cc007bef4..d81300b84 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -145,7 +145,6 @@ bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel)
 
 BVQuickCheck::~BVQuickCheck() {
   clearSolver();
-  delete d_bitblaster;
 }
 
 QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index ec4eb9f4f..b2c31edcb 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -40,7 +40,7 @@ class TheoryBV;
 
 class BVQuickCheck {
   context::Context d_ctx;
-  TLazyBitblaster* d_bitblaster;
+  std::unique_ptr<TLazyBitblaster> d_bitblaster;
   Node d_conflict;
   context::CDO<bool> d_inConflict;
   void setConflict();
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 0150264fd..df7ba29b5 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -228,30 +228,28 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
 }
 
 AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
-  : SubtheorySolver(c, bv)
-  , d_modelMap(NULL)
-  , d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv))
-  , d_isComplete(c, false)
-  , d_isDifficult(c, false)
-  , d_budget(options::bitvectorAlgebraicBudget())
-  , d_explanations()
-  , d_inputAssertions()
-  , d_ids()
-  , d_numSolved(0)
-  , d_numCalls(0)
-  , d_ctx(new context::Context())
-  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("theory::bv::algebraic", d_quickSolver) : NULL)
-  , d_statistics()
-{}
-
-AlgebraicSolver::~AlgebraicSolver() {
-  if(d_modelMap != NULL) { delete d_modelMap; }
-  delete d_quickXplain;
-  delete d_quickSolver;
-  delete d_ctx;
+    : SubtheorySolver(c, bv),
+      d_modelMap(),
+      d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)),
+      d_isComplete(c, false),
+      d_isDifficult(c, false),
+      d_budget(options::bitvectorAlgebraicBudget()),
+      d_explanations(),
+      d_inputAssertions(),
+      d_ids(),
+      d_numSolved(0),
+      d_numCalls(0),
+      d_quickXplain(),
+      d_statistics()
+{
+  if (options::bitvectorQuickXplain())
+  {
+    d_quickXplain.reset(
+        new QuickXPlain("theory::bv::algebraic", d_quickSolver.get()));
+  }
 }
 
-
+AlgebraicSolver::~AlgebraicSolver() {}
 
 bool AlgebraicSolver::check(Theory::Effort e)
 {
@@ -298,16 +296,15 @@ bool AlgebraicSolver::check(Theory::Effort e)
 
   Assert (d_explanations.size() == worklist.size());
 
-  delete d_modelMap;
-  d_modelMap = new SubstitutionMap(d_context);
-  SubstitutionEx subst(d_modelMap);
+  d_modelMap.reset(new SubstitutionMap(d_context));
+  SubstitutionEx subst(d_modelMap.get());
 
   // first round of substitutions
   processAssertions(worklist, subst);
 
   if (!d_isDifficult.get()) {
     // skolemize all possible extracts
-    ExtractSkolemizer skolemizer(d_modelMap);
+    ExtractSkolemizer skolemizer(d_modelMap.get());
     skolemizer.skolemize(worklist);
     // second round of substitutions
     processAssertions(worklist, subst);
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 09d958f25..42f5faa7c 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -169,8 +169,8 @@ class AlgebraicSolver : public SubtheorySolver {
     ~Statistics();
   };
 
-  SubstitutionMap* d_modelMap;
-  BVQuickCheck* d_quickSolver;
+  std::unique_ptr<SubstitutionMap> d_modelMap;
+  std::unique_ptr<BVQuickCheck> d_quickSolver;
   context::CDO<bool> d_isComplete; 
   context::CDO<bool> d_isDifficult; /**< flag to indicate whether the current assertions contain expensive BV operators */
   
@@ -181,9 +181,9 @@ class AlgebraicSolver : public SubtheorySolver {
   uint64_t d_numSolved;
   uint64_t d_numCalls;
 
-  context::Context* d_ctx;
-  QuickXPlain* d_quickXplain;   /**< separate quickXplain module as it can reuse the current SAT solver */
-  
+  /** separate quickXplain module as it can reuse the current SAT solver */
+  std::unique_ptr<QuickXPlain> d_quickXplain;
+
   Statistics d_statistics;
   bool useHeuristic();
   void setConflict(TNode conflict);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index cdbf2f955..ea2f8e4bf 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -35,24 +35,25 @@ namespace theory {
 namespace bv {
 
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
-  : SubtheorySolver(c, bv),
-    d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
-    d_bitblastQueue(c),
-    d_statistics(),
-    d_validModelCache(c, true),
-    d_lemmaAtomsQueue(c),
-    d_useSatPropagation(options::bitvectorPropagate()),
-    d_abstractionModule(NULL),
-    d_quickCheck(options::bitvectorQuickXplain() ? new BVQuickCheck("bb", bv) : NULL),
-    d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("bb", d_quickCheck) :  NULL)
+    : SubtheorySolver(c, bv),
+      d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
+      d_bitblastQueue(c),
+      d_statistics(),
+      d_validModelCache(c, true),
+      d_lemmaAtomsQueue(c),
+      d_useSatPropagation(options::bitvectorPropagate()),
+      d_abstractionModule(NULL),
+      d_quickCheck(),
+      d_quickXplain()
 {
+  if (options::bitvectorQuickXplain())
+  {
+    d_quickCheck.reset(new BVQuickCheck("bb", bv));
+    d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
+  }
 }
 
-BitblastSolver::~BitblastSolver() {
-  delete d_quickXplain;
-  delete d_quickCheck;
-  delete d_bitblaster;
-}
+BitblastSolver::~BitblastSolver() {}
 
 BitblastSolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
@@ -278,7 +279,7 @@ void BitblastSolver::setConflict(TNode conflict) {
 
 void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
   d_bitblaster->setProofLog( bvp );
-  bvp->setBitblaster(d_bitblaster);
+  bvp->setBitblaster(d_bitblaster.get());
 }
 
 }/* namespace CVC4::theory::bv */
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 350baae41..ac0d38815 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -42,7 +42,7 @@ class BitblastSolver : public SubtheorySolver {
     ~Statistics();
   };
   /** Bitblaster */
-  TLazyBitblaster* d_bitblaster;
+  std::unique_ptr<TLazyBitblaster> d_bitblaster;
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
@@ -56,8 +56,8 @@ class BitblastSolver : public SubtheorySolver {
   context::CDQueue<TNode> d_lemmaAtomsQueue;
   bool  d_useSatPropagation;
   AbstractionModule* d_abstractionModule;
-  BVQuickCheck* d_quickCheck;
-  QuickXPlain* d_quickXplain;
+  std::unique_ptr<BVQuickCheck> d_quickCheck;
+  std::unique_ptr<QuickXPlain> d_quickXplain;
   //  Node getModelValueRec(TNode node);
   void setConflict(TNode conflict);
 public:
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index b3c3f73f3..9285141a0 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -79,9 +79,8 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   d_equalityEngine.addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
-CoreSolver::~CoreSolver() {
-  delete d_slicer;
-}
+CoreSolver::~CoreSolver() {}
+
 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 2ef18e613..ce570d531 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -82,7 +82,7 @@ class CoreSolver : public SubtheorySolver {
   /** new equivalence class */
   void eqNotifyNewClass(TNode t);
 
-  Slicer* d_slicer;
+  std::unique_ptr<Slicer> d_slicer;
   context::CDO<bool> d_isComplete;
   unsigned d_lemmaThreshold;
   
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 1b7eeddac..d08405ef3 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -44,79 +44,72 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
-                   OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, std::string name)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
-    d_context(c),
-    d_alreadyPropagatedSet(c),
-    d_sharedTermsSet(c),
-    d_subtheories(),
-    d_subtheoryMap(),
-    d_statistics(),
-    d_staticLearnCache(),
-    d_BVDivByZero(),
-    d_BVRemByZero(),
-    d_lemmasAdded(c, false),
-    d_conflict(c, false),
-    d_invalidateModelCache(c, true),
-    d_literalsToPropagate(c),
-    d_literalsToPropagateIndex(c, 0),
-    d_propagatedBy(c),
-    d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
-    d_isCoreTheory(false),
-    d_calledPreregister(false),
-    d_needsLastCallCheck(false),
-    d_extf_range_infer(u),
-    d_extf_collapse_infer(u)
+TheoryBV::TheoryBV(context::Context* c,
+                   context::UserContext* u,
+                   OutputChannel& out,
+                   Valuation valuation,
+                   const LogicInfo& logicInfo,
+                   std::string name)
+    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
+      d_context(c),
+      d_alreadyPropagatedSet(c),
+      d_sharedTermsSet(c),
+      d_subtheories(),
+      d_subtheoryMap(),
+      d_statistics(),
+      d_staticLearnCache(),
+      d_BVDivByZero(),
+      d_BVRemByZero(),
+      d_lemmasAdded(c, false),
+      d_conflict(c, false),
+      d_invalidateModelCache(c, true),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_propagatedBy(c),
+      d_eagerSolver(),
+      d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
+      d_isCoreTheory(false),
+      d_calledPreregister(false),
+      d_needsLastCallCheck(false),
+      d_extf_range_infer(u),
+      d_extf_collapse_infer(u)
 {
   setupExtTheory();
   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver = new EagerBitblastSolver(c, this);
+    d_eagerSolver.reset(new EagerBitblastSolver(c, this));
     return;
   }
 
   if (options::bitvectorEqualitySolver() && !options::proof())
   {
-    SubtheorySolver* core_solver = new CoreSolver(c, this);
-    d_subtheories.push_back(core_solver);
-    d_subtheoryMap[SUB_CORE] = core_solver;
+    d_subtheories.emplace_back(new CoreSolver(c, this));
+    d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
   }
 
   if (options::bitvectorInequalitySolver() && !options::proof())
   {
-    SubtheorySolver* ineq_solver = new InequalitySolver(c, u, this);
-    d_subtheories.push_back(ineq_solver);
-    d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
+    d_subtheories.emplace_back(new InequalitySolver(c, u, this));
+    d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
   }
 
   if (options::bitvectorAlgebraicSolver() && !options::proof())
   {
-    SubtheorySolver* alg_solver = new AlgebraicSolver(c, this);
-    d_subtheories.push_back(alg_solver);
-    d_subtheoryMap[SUB_ALGEBRAIC] = alg_solver;
+    d_subtheories.emplace_back(new AlgebraicSolver(c, this));
+    d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
   }
 
   BitblastSolver* bb_solver = new BitblastSolver(c, this);
-  if (options::bvAbstraction()) {
-    bb_solver->setAbstraction(d_abstractionModule);
+  if (options::bvAbstraction())
+  {
+    bb_solver->setAbstraction(d_abstractionModule.get());
   }
-  d_subtheories.push_back(bb_solver);
+  d_subtheories.emplace_back(bb_solver);
   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
 }
 
-TheoryBV::~TheoryBV() {
-  if (d_eagerSolver) {
-    delete d_eagerSolver;
-  }
-  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    delete d_subtheories[i];
-  }
-  delete d_abstractionModule;
-}
+TheoryBV::~TheoryBV() {}
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 05bb695e5..d5e3ad02e 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -53,7 +53,7 @@ class TheoryBV : public Theory {
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
 
-  std::vector<SubtheorySolver*> d_subtheories;
+  std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
 public:
@@ -172,8 +172,8 @@ private:
   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
-  EagerBitblastSolver* d_eagerSolver;
-  AbstractionModule* d_abstractionModule;
+  std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
+  std::unique_ptr<AbstractionModule> d_abstractionModule;
   bool d_isCoreTheory;
   bool d_calledPreregister;