From: Gereon Kremer Date: Wed, 2 Sep 2020 15:21:03 +0000 (+0200) Subject: Use std::unique_ptr instead of std::shared_ptr for inference manager (#5003) X-Git-Tag: cvc5-1.0.0~2920 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e93736643667d7b8e4ff9fa5f86596ce1ec31d3;p=cvc5.git 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 f026aa374..bb0bb494e 100644 --- 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 lemma, +void InferenceManager::addPendingArithLemma(std::unique_ptr lemma, bool isWaiting) { lemma->d_node = Rewriter::rewrite(lemma->d_node); @@ -55,20 +55,21 @@ void InferenceManager::addPendingArithLemma(std::shared_ptr 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(lemma), isWaiting); + addPendingArithLemma(std::unique_ptr(new ArithLemma(lemma)), + isWaiting); } void InferenceManager::addPendingArithLemma(const Node& lemma, nl::Inference inftype, bool isWaiting) { - addPendingArithLemma(std::make_shared( - lemma, LemmaProperty::NONE, nullptr, inftype), + addPendingArithLemma(std::unique_ptr(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 3b7190826..1c0678e60 100644 --- 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 lemma, + void addPendingArithLemma(std::unique_ptr 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> d_waitingLem; + std::vector> 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 762cdfd8b..1faf71aa9 100644 --- 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(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 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(lem, p, pg)); + d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg)); } void InferenceManagerBuffered::addPendingLemma( - std::shared_ptr lemma) + std::unique_ptr 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(conc, exp, pg)); + d_pendingFact.emplace_back(new SimpleTheoryInternalFact(conc, exp, pg)); } void InferenceManagerBuffered::addPendingFact( - std::shared_ptr fact) + std::unique_ptr fact) { d_pendingFact.emplace_back(std::move(fact)); } @@ -97,7 +96,7 @@ void InferenceManagerBuffered::doPendingFacts() void InferenceManagerBuffered::doPendingLemmas() { - for (const std::shared_ptr& plem : d_pendingLem) + for (const std::unique_ptr& 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 762b7d4e0..62c3c9b55 100644 --- 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 lemma); + void addPendingLemma(std::unique_ptr 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 fact); + void addPendingFact(std::unique_ptr 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> d_pendingLem; + std::vector> d_pendingLem; /** A set of pending inferences to be processed as facts */ - std::vector> d_pendingFact; + std::vector> d_pendingFact; /** A map from literals to their pending phase requirement */ std::map d_pendingReqPhase; };