Use std::unique_ptr instead of std::shared_ptr for inference manager (#5003)

We now use std::unique_ptr instead of std::shared_ptr when storing TheoryInference objects.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index f026aa37422d18070d0da278aa5a2bc530bcb4a4..bb0bb494e1a9fff023c1c80d1dc29f0e77340ce8 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -29,7 +29,7 @@ InferenceManager::InferenceManager(TheoryArith& ta,
 {
 }
 
-void InferenceManager::addPendingArithLemma(std::shared_ptr<ArithLemma> lemma,
+void InferenceManager::addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
                                             bool isWaiting)
 {
   lemma->d_node = Rewriter::rewrite(lemma->d_node);
@@ -55,20 +55,21 @@ void InferenceManager::addPendingArithLemma(std::shared_ptr<ArithLemma> lemma,
   }
   else
   {
-    addPendingLemma(std::move(lemma));
+    d_pendingLem.emplace_back(std::move(lemma));
   }
 }
 void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
                                             bool isWaiting)
 {
-  addPendingArithLemma(std::make_shared<ArithLemma>(lemma), isWaiting);
+  addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(lemma)),
+                       isWaiting);
 }
 void InferenceManager::addPendingArithLemma(const Node& lemma,
                                             nl::Inference inftype,
                                             bool isWaiting)
 {
-  addPendingArithLemma(std::make_shared<ArithLemma>(
-                           lemma, LemmaProperty::NONE, nullptr, inftype),
+  addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(
+                           lemma, LemmaProperty::NONE, nullptr, inftype)),
                        isWaiting);
 }
 
@@ -76,7 +77,7 @@ void InferenceManager::flushWaitingLemmas()
 {
   for (auto& lem : d_waitingLem)
   {
-    addPendingLemma(std::move(lem));
+    d_pendingLem.emplace_back(std::move(lem));
   }
   d_waitingLem.clear();
 }

diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 3b71908265832c6781f811af051fda85abc6b82b..1c0678e605a451a913af5ce553a30806bd2b97fc 100644 (file)
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -55,7 +55,7 @@ class InferenceManager : public InferenceManagerBuffered
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
-  void addPendingArithLemma(std::shared_ptr<ArithLemma> lemma,
+  void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
                             bool isWaiting = false);
   /**
    * Add a lemma as pending lemma to the this inference manager.
@@ -102,7 +102,7 @@ class InferenceManager : public InferenceManagerBuffered
   bool isEntailedFalse(const ArithLemma& lem);
 
   /** The waiting lemmas. */
-  std::vector<std::shared_ptr<ArithLemma>> d_waitingLem;
+  std::vector<std::unique_ptr<ArithLemma>> d_waitingLem;
 
   /** cache of all preprocessed lemmas sent on the output channel
    * (user-context-dependent) */

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 762cdfd8be4286712dfca7d6da232bd5654a21ec..1faf71aa9c379ef47ea4b298dd6e9a19a32e6068 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -97,7 +97,7 @@ void InferenceManager::addPendingInference(Node conc,
                                            Node exp,
                                            ProofGenerator* pg)
 {
-  d_pendingFact.push_back(std::make_shared<DatatypesInference>(conc, exp, pg));
+  d_pendingFact.emplace_back(new DatatypesInference(conc, exp, pg));
 }
 
 void InferenceManager::process()

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index df01b4e93c69cbf90addf49809f0976760d7a9c4..8d7dd2abc798ee1f08eb80e0431c884d9e5b8889 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -50,11 +50,11 @@ void InferenceManagerBuffered::addPendingLemma(Node lem,
                                                ProofGenerator* pg)
 {
   // make the simple theory lemma
-  d_pendingLem.push_back(std::make_shared<SimpleTheoryLemma>(lem, p, pg));
+  d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg));
 }
 
 void InferenceManagerBuffered::addPendingLemma(
-    std::shared_ptr<TheoryInference> lemma)
+    std::unique_ptr<TheoryInference> lemma)
 {
   d_pendingLem.emplace_back(std::move(lemma));
 }
@@ -65,12 +65,11 @@ void InferenceManagerBuffered::addPendingFact(Node conc,
 {
   // make a simple theory internal fact
   Assert(conc.getKind() != AND && conc.getKind() != OR);
-  d_pendingFact.push_back(
-      std::make_shared<SimpleTheoryInternalFact>(conc, exp, pg));
+  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(conc, exp, pg));
 }
 
 void InferenceManagerBuffered::addPendingFact(
-    std::shared_ptr<TheoryInference> fact)
+    std::unique_ptr<TheoryInference> fact)
 {
   d_pendingFact.emplace_back(std::move(fact));
 }
@@ -97,7 +96,7 @@ void InferenceManagerBuffered::doPendingFacts()
 
 void InferenceManagerBuffered::doPendingLemmas()
 {
-  for (const std::shared_ptr<TheoryInference>& plem : d_pendingLem)
+  for (const std::unique_ptr<TheoryInference>& plem : d_pendingLem)
   {
     // process this lemma
     plem->process(this);

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 762b7d4e02274647e188c36d19aab495da01c1b9..62c3c9b55f6da4a9d4f42e0a915ac3059d1493c4 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -62,7 +62,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    * Add pending lemma, where lemma can be a (derived) class of the
    * theory inference base class.
    */
-  void addPendingLemma(std::shared_ptr<TheoryInference> lemma);
+  void addPendingLemma(std::unique_ptr<TheoryInference> lemma);
   /**
    * Add pending fact, which adds a fact on the pending fact queue. It must
    * be the case that:
@@ -78,7 +78,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    * Add pending fact, where fact can be a (derived) class of the
    * theory inference base class.
    */
-  void addPendingFact(std::shared_ptr<TheoryInference> fact);
+  void addPendingFact(std::unique_ptr<TheoryInference> fact);
   /** Add pending phase requirement
    *
    * This method is called to indicate this class should send a phase
@@ -131,9 +131,9 @@ class InferenceManagerBuffered : public TheoryInferenceManager
 
  protected:
   /** A set of pending inferences to be processed as lemmas */
-  std::vector<std::shared_ptr<TheoryInference>> d_pendingLem;
+  std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;
   /** A set of pending inferences to be processed as facts */
-  std::vector<std::shared_ptr<TheoryInference>> d_pendingFact;
+  std::vector<std::unique_ptr<TheoryInference>> d_pendingFact;
   /** A map from literals to their pending phase requirement */
   std::map<Node, bool> d_pendingReqPhase;
 };