BVQuickCheck::~BVQuickCheck() {
clearSolver();
- delete d_bitblaster;
}
QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
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();
}
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)
{
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);
~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 */
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);
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)
void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
d_bitblaster->setProofLog( bvp );
- bvp->setBitblaster(d_bitblaster);
+ bvp->setBitblaster(d_bitblaster.get());
}
}/* namespace CVC4::theory::bv */
~Statistics();
};
/** Bitblaster */
- TLazyBitblaster* d_bitblaster;
+ std::unique_ptr<TLazyBitblaster> d_bitblaster;
/** Nodes that still need to be bit-blasted */
context::CDQueue<TNode> d_bitblastQueue;
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:
d_equalityEngine.addFunctionKind(kind::INT_TO_BITVECTOR);
}
-CoreSolver::~CoreSolver() {
- delete d_slicer;
-}
+CoreSolver::~CoreSolver() {}
+
void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
/** new equivalence class */
void eqNotifyNewClass(TNode t);
- Slicer* d_slicer;
+ std::unique_ptr<Slicer> d_slicer;
context::CDO<bool> d_isComplete;
unsigned d_lemmaThreshold;
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) {
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:
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;
projects / cvc5.git / commitdiff