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.

1 files changed, 5 insertions, 6 deletions

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index df01b4e93..8d7dd2abc 100644
--- 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);