From 5d3126cf3b3edb0dac89dac7566332f29f80fa06 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 9 Sep 2021 18:54:12 -0700 Subject: [PATCH] bv: Use EnvObj::rewrite() and EnvObj::options() in BvSolver. (#7171) --- src/theory/bv/bv_solver.h | 8 ++-- src/theory/bv/bv_solver_bitblast.cpp | 17 ++++---- src/theory/bv/bv_solver_bitblast.h | 3 +- src/theory/bv/bv_solver_bitblast_internal.cpp | 7 ++- src/theory/bv/bv_solver_bitblast_internal.h | 3 +- src/theory/bv/bv_solver_layered.cpp | 43 ++++++++++--------- src/theory/bv/bv_solver_layered.h | 1 + src/theory/bv/theory_bv.cpp | 20 +++++---- 8 files changed, 57 insertions(+), 45 deletions(-) diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index c959fb648..510c8a29a 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -20,17 +20,19 @@ #ifndef CVC5__THEORY__BV__BV_SOLVER_H #define CVC5__THEORY__BV__BV_SOLVER_H +#include "smt/env.h" +#include "smt/env_obj.h" #include "theory/theory.h" namespace cvc5 { namespace theory { namespace bv { -class BVSolver +class BVSolver : protected EnvObj { public: - BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr) - : d_state(state), d_im(inferMgr){}; + BVSolver(Env& env, TheoryState& state, TheoryInferenceManager& inferMgr) + : EnvObj(env), d_state(state), d_im(inferMgr){}; virtual ~BVSolver() {} diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index ecd42e4a0..9d316e91e 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -108,10 +108,11 @@ class BBRegistrar : public prop::Registrar std::unordered_set d_registeredAtoms; }; -BVSolverBitblast::BVSolverBitblast(TheoryState* s, +BVSolverBitblast::BVSolverBitblast(Env& env, + TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) - : BVSolver(*s, inferMgr), + : BVSolver(env, *s, inferMgr), d_bitblaster(new NodeBitblaster(s)), d_bbRegistrar(new BBRegistrar(d_bitblaster.get())), d_nullContext(new context::Context()), @@ -123,7 +124,7 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, : nullptr), d_factLiteralCache(s->getSatContext()), d_literalFactCache(s->getSatContext()), - d_propagate(options::bitvectorPropagate()), + d_propagate(options().bv.bitvectorPropagate), d_resetNotify(new NotifyResetAssertions(s->getUserContext())) { if (pnm != nullptr) @@ -147,7 +148,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level) // If we permanently added assertions to the SAT solver and the assertions // were reset, we have to reset the SAT solver and the CNF stream. - if (options::bvAssertInput() && d_resetNotify->doneResetAssertions()) + if (options().bv.bvAssertInput && d_resetNotify->doneResetAssertions()) { d_satSolver.reset(nullptr); d_cnfStream.reset(nullptr); @@ -248,7 +249,7 @@ bool BVSolverBitblast::preNotifyFact( * If this is the case we can assert `fact` to the SAT solver instead of * using assumptions. */ - if (options::bvAssertInput() && val.isSatLiteral(fact) + if (options().bv.bvAssertInput && val.isSatLiteral(fact) && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0) { Assert(!val.isDecision(fact)); @@ -277,7 +278,7 @@ void BVSolverBitblast::computeRelevantTerms(std::set& termSet) * in BitblastMode::EAGER and therefore add all variables from the * bit-blaster to `termSet`. */ - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { d_bitblaster->computeRelevantTerms(termSet); } @@ -303,7 +304,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m, // In eager bitblast mode we also have to collect the model values for // Boolean variables in the CNF stream. - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { NodeManager* nm = NodeManager::currentNM(); std::vector vars; @@ -327,7 +328,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m, void BVSolverBitblast::initSatSolver() { - switch (options::bvSatSolver()) + switch (options().bv.bvSatSolver) { case options::SatSolverMode::CRYPTOMINISAT: d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 3f4ab5025..e8931acff 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -42,7 +42,8 @@ class BBRegistrar; class BVSolverBitblast : public BVSolver { public: - BVSolverBitblast(TheoryState* state, + BVSolverBitblast(Env& env, + TheoryState* state, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm); ~BVSolverBitblast() = default; diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp index 1b606a0e9..71a29f472 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -68,8 +68,11 @@ void collectBVAtoms(TNode n, std::unordered_set& atoms) } // namespace BVSolverBitblastInternal::BVSolverBitblastInternal( - TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) - : BVSolver(*s, inferMgr), + Env& env, + TheoryState* s, + TheoryInferenceManager& inferMgr, + ProofNodeManager* pnm) + : BVSolver(env, *s, inferMgr), d_pnm(pnm), d_bitblaster(new BBProof(s, pnm, false)) { diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h index 2fc7173d1..cc365e109 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -37,7 +37,8 @@ namespace bv { class BVSolverBitblastInternal : public BVSolver { public: - BVSolverBitblastInternal(TheoryState* state, + BVSolverBitblastInternal(Env& env, + TheoryState* state, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm); ~BVSolverBitblastInternal() = default; diff --git a/src/theory/bv/bv_solver_layered.cpp b/src/theory/bv/bv_solver_layered.cpp index 40daf1cb4..bf76ed2f9 100644 --- a/src/theory/bv/bv_solver_layered.cpp +++ b/src/theory/bv/bv_solver_layered.cpp @@ -38,11 +38,12 @@ namespace theory { namespace bv { BVSolverLayered::BVSolverLayered(TheoryBV& bv, + Env& env, context::Context* c, context::UserContext* u, ProofNodeManager* pnm, std::string name) - : BVSolver(bv.d_state, bv.d_im), + : BVSolver(env, bv.d_state, bv.d_im), d_bv(bv), d_context(c), d_alreadyPropagatedSet(c), @@ -61,32 +62,32 @@ BVSolverLayered::BVSolverLayered(TheoryBV& bv, d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))), d_calledPreregister(false) { - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { d_eagerSolver.reset(new EagerBitblastSolver(c, this)); return; } - if (options::bitvectorEqualitySolver()) + if (options().bv.bitvectorEqualitySolver) { d_subtheories.emplace_back(new CoreSolver(c, this)); d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); } - if (options::bitvectorInequalitySolver()) + if (options().bv.bitvectorInequalitySolver) { d_subtheories.emplace_back(new InequalitySolver(c, u, this)); d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); } - if (options::bitvectorAlgebraicSolver()) + if (options().bv.bitvectorAlgebraicSolver) { 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()) + if (options().bv.bvAbstraction) { bb_solver->setAbstraction(d_abstractionModule.get()); } @@ -141,7 +142,7 @@ void BVSolverLayered::preRegisterTerm(TNode node) Debug("bitvector-preregister") << "BVSolverLayered::preRegister(" << node << ")" << std::endl; - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { // the aig bit-blaster option is set heuristically // if bv abstraction is used @@ -235,7 +236,7 @@ void BVSolverLayered::check(Theory::Effort e) // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); // if we are using the eager solver - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { // this can only happen on an empty benchmark if (!d_eagerSolver->isInitialized()) @@ -322,7 +323,7 @@ bool BVSolverLayered::collectModelValues(TheoryModel* m, const std::set& termSet) { Assert(!inConflict()); - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { if (!d_eagerSolver->collectModelInfo(m, true)) { @@ -355,7 +356,7 @@ Node BVSolverLayered::getModelValue(TNode var) void BVSolverLayered::propagate(Theory::Effort e) { Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl; - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { return; } @@ -394,15 +395,15 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) { Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n"; Node res = t; - if (options::bitwiseEq() && RewriteRule::applies(t)) + if (options().bv.bitwiseEq && RewriteRule::applies(t)) { Node result = RewriteRule::run(t); - res = Rewriter::rewrite(result); + res = rewrite(result); } else if (RewriteRule::applies(t)) { Node result = RewriteRule::run(t); - res = Rewriter::rewrite(result); + res = rewrite(result); } else if (res.getKind() == kind::EQUAL && ((res[0].getKind() == kind::BITVECTOR_ADD @@ -419,7 +420,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) Node rewr_eq = RewriteRule::run(new_eq); if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) { - res = Rewriter::rewrite(rewr_eq); + res = rewrite(rewr_eq); } else { @@ -451,7 +452,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) // if (RewriteRule::applies(mult)) { // Node new_mult = RewriteRule::run(mult); // Node new_eq = - // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, + // rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, // new_mult, add)); // // the simplification can cause the formula to blow up @@ -475,7 +476,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) // } // } - if (options::bvAbstraction() && t.getType().isBoolean()) + if (options().bv.bvAbstraction && t.getType().isBoolean()) { d_abstractionModule->addInputAtom(res); } @@ -595,9 +596,9 @@ void BVSolverLayered::notifySharedTerm(TNode t) EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b) { - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) return EQUALITY_UNKNOWN; - Assert(options::bitblastMode() == options::BitblastMode::LAZY); + Assert(options().bv.bitblastMode == options::BitblastMode::LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); @@ -665,8 +666,8 @@ bool BVSolverLayered::applyAbstraction(const std::vector& assertions, { bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); - if (changed && options::bitblastMode() == options::BitblastMode::EAGER - && options::bitvectorAig()) + if (changed && options().bv.bitblastMode == options::BitblastMode::EAGER + && options().bv.bitvectorAig) { // disable AIG mode AlwaysAssert(!d_eagerSolver->isInitialized()); @@ -678,7 +679,7 @@ bool BVSolverLayered::applyAbstraction(const std::vector& assertions, void BVSolverLayered::setConflict(Node conflict) { - if (options::bvAbstraction()) + if (options().bv.bvAbstraction) { NodeManager* const nm = NodeManager::currentNM(); Node new_conflict = d_abstractionModule->simplifyConflict(conflict); diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h index 023ff5a46..325f2fc72 100644 --- a/src/theory/bv/bv_solver_layered.h +++ b/src/theory/bv/bv_solver_layered.h @@ -58,6 +58,7 @@ class BVSolverLayered : public BVSolver public: BVSolverLayered(TheoryBV& bv, + Env& env, context::Context* c, context::UserContext* u, ProofNodeManager* pnm = nullptr, diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7493a54c7..96eccea57 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,20 +43,22 @@ TheoryBV::TheoryBV(Env& env, d_invalidateModelCache(context(), true), d_stats("theory::bv::") { - switch (options::bvSolver()) + switch (options().bv.bvSolver) { case options::BVSolver::BITBLAST: - d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm)); + d_internal.reset(new BVSolverBitblast(d_env, &d_state, d_im, d_pnm)); break; case options::BVSolver::LAYERED: - d_internal.reset( - new BVSolverLayered(*this, context(), userContext(), d_pnm, name)); + d_internal.reset(new BVSolverLayered( + *this, d_env, context(), userContext(), d_pnm, name)); break; default: - AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL); - d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm)); + AlwaysAssert(options().bv.bvSolver + == options::BVSolver::BITBLAST_INTERNAL); + d_internal.reset( + new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm)); } d_theoryState = &d_state; d_inferManager = &d_im; @@ -68,7 +70,7 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; } ProofRuleChecker* TheoryBV::getProofChecker() { - if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL) + if (options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL) { return static_cast(d_internal.get()) ->getProofChecker(); @@ -222,7 +224,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert( * x = c::sk2 if h == bw(x)-1, where bw(sk2) = l * x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l */ - Node node = Rewriter::rewrite(in); + Node node = rewrite(in); if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) || (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) @@ -391,7 +393,7 @@ Node TheoryBV::getValue(TNode node) Assert(iit->second.isConst()); nb << iit->second; } - it->second = Rewriter::rewrite(nb.constructNode()); + it->second = rewrite(nb.constructNode()); } } while (!visit.empty()); -- 2.30.2