From: Mathias Preiner Date: Mon, 27 Aug 2018 23:19:34 +0000 (-0700) Subject: Use std:unique_ptr instead of raw pointers in theory/bv. (#2385) X-Git-Tag: cvc5-1.0.0~4714 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a442b02d9a695a04f12d58fee71f7e1afbfa1473;p=cvc5.git Use std:unique_ptr instead of raw pointers in theory/bv. (#2385) This should also fix CIDs 1465687, 1465695, 1465696, and 1465701. --- 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 d_bitblaster; Node d_conflict; context::CDO 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 d_modelMap; + std::unique_ptr d_quickSolver; context::CDO d_isComplete; context::CDO 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 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 d_bitblaster; /** Nodes that still need to be bit-blasted */ context::CDQueue d_bitblastQueue; @@ -56,8 +56,8 @@ class BitblastSolver : public SubtheorySolver { context::CDQueue d_lemmaAtomsQueue; bool d_useSatPropagation; AbstractionModule* d_abstractionModule; - BVQuickCheck* d_quickCheck; - QuickXPlain* d_quickXplain; + std::unique_ptr d_quickCheck; + std::unique_ptr 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 d_slicer; context::CDO 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 d_alreadyPropagatedSet; context::CDHashSet d_sharedTermsSet; - std::vector d_subtheories; + std::vector> d_subtheories; std::unordered_map > d_subtheoryMap; public: @@ -172,8 +172,8 @@ private: typedef context::CDHashMap PropagatedMap; PropagatedMap d_propagatedBy; - EagerBitblastSolver* d_eagerSolver; - AbstractionModule* d_abstractionModule; + std::unique_ptr d_eagerSolver; + std::unique_ptr d_abstractionModule; bool d_isCoreTheory; bool d_calledPreregister;