From bb6813731ef1059ab38cedcc5af026b6e75bd6be Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 14 Jul 2021 18:54:33 -0700 Subject: [PATCH] bv: Rename lazy solver to layered solver. (#6889) --- src/CMakeLists.txt | 4 +- src/options/bv_options.toml | 12 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 5 +- src/theory/bv/bitblast/eager_bitblaster.h | 6 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 16 +-- src/theory/bv/bitblast/lazy_bitblaster.h | 12 +- src/theory/bv/bv_eager_solver.cpp | 3 +- src/theory/bv/bv_eager_solver.h | 6 +- src/theory/bv/bv_quick_check.cpp | 4 +- src/theory/bv/bv_quick_check.h | 4 +- ..._solver_lazy.cpp => bv_solver_layered.cpp} | 110 +++++++++--------- .../{bv_solver_lazy.h => bv_solver_layered.h} | 29 ++--- src/theory/bv/bv_subtheory.h | 6 +- src/theory/bv/bv_subtheory_algebraic.cpp | 4 +- src/theory/bv/bv_subtheory_algebraic.h | 2 +- src/theory/bv/bv_subtheory_bitblast.cpp | 4 +- src/theory/bv/bv_subtheory_bitblast.h | 2 +- src/theory/bv/bv_subtheory_core.cpp | 4 +- src/theory/bv/bv_subtheory_core.h | 4 +- src/theory/bv/bv_subtheory_inequality.cpp | 2 +- src/theory/bv/bv_subtheory_inequality.h | 4 +- src/theory/bv/theory_bv.cpp | 6 +- src/theory/bv/theory_bv.h | 6 +- src/theory/inference_id.cpp | 4 +- src/theory/inference_id.h | 4 +- test/unit/theory/theory_bv_white.cpp | 6 +- 26 files changed, 139 insertions(+), 130 deletions(-) rename src/theory/bv/{bv_solver_lazy.cpp => bv_solver_layered.cpp} (84%) rename src/theory/bv/{bv_solver_lazy.h => bv_solver_layered.h} (90%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8dc1f986f..015f00f8f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -591,8 +591,8 @@ libcvc5_add_sources( theory/bv/bv_solver_bitblast.h theory/bv/bv_solver_bitblast_internal.cpp theory/bv/bv_solver_bitblast_internal.h - theory/bv/bv_solver_lazy.cpp - theory/bv/bv_solver_lazy.h + theory/bv/bv_solver_layered.cpp + theory/bv/bv_solver_layered.h theory/bv/bv_subtheory.h theory/bv/bv_subtheory_algebraic.cpp theory/bv/bv_subtheory_algebraic.h diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 3faf9a111..05ea7f512 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -66,7 +66,7 @@ name = "Bitvector Theory" long = "bv-eq-solver" type = "bool" default = "true" - help = "use the equality engine for the bit-vector theory (only if --bitblast=lazy)" + help = "use the equality engine for the bit-vector theory (only if --bv-solver=layered)" [[option]] name = "bitvectorInequalitySolver" @@ -74,7 +74,7 @@ name = "Bitvector Theory" long = "bv-inequality-solver" type = "bool" default = "true" - help = "turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)" + help = "turn on the inequality solver for the bit-vector theory (only if --bv-solver=layered)" [[option]] name = "bitvectorAlgebraicSolver" @@ -82,7 +82,7 @@ name = "Bitvector Theory" long = "bv-algebraic-solver" type = "bool" default = "false" - help = "turn on experimental algebraic solver for the bit-vector theory (only if --bitblast=lazy)" + help = "turn on experimental algebraic solver for the bit-vector theory (only if --bv-solver=layered)" [[option]] name = "bitvectorAlgebraicBudget" @@ -217,12 +217,12 @@ name = "Bitvector Theory" [[option.mode.BITBLAST]] name = "bitblast" help = "Enables bitblasting solver." -[[option.mode.LAZY]] - name = "lazy" - help = "Enables the lazy BV solver infrastructure." [[option.mode.BITBLAST_INTERNAL]] name = "bitblast-internal" help = "Enables bitblasting to internal SAT solver with proof support." +[[option.mode.LAYERED]] + name = "layered" + help = "Enables the layered BV solver." [[option]] name = "bvAssertInput" diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 55ed6c41d..dd3a3e9ce 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -23,7 +23,7 @@ #include "prop/sat_solver_factory.h" #include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -31,7 +31,8 @@ namespace cvc5 { namespace theory { namespace bv { -EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) +EagerBitblaster::EagerBitblaster(BVSolverLayered* theory_bv, + context::Context* c) : TBitblaster(), d_context(c), d_satSolver(), diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 9e5ace9d8..71bf50dd0 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -30,12 +30,12 @@ namespace theory { namespace bv { class BitblastingRegistrar; -class BVSolverLazy; +class BVSolverLayered; class EagerBitblaster : public TBitblaster { public: - EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context); + EagerBitblaster(BVSolverLayered* theory_bv, context::Context* context); ~EagerBitblaster(); void addAtom(TNode atom); @@ -60,7 +60,7 @@ class EagerBitblaster : public TBitblaster std::unique_ptr d_satSolver; std::unique_ptr d_bitblastingRegistrar; - BVSolverLazy* d_bv; + BVSolverLayered* d_bv; TNodeSet d_bbAtoms; TNodeSet d_variables; diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 6a5372e04..3eb2eebe7 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Bitblaster for the lazy bv solver. + * Bitblaster for the layered BV solver. */ #include "theory/bv/bitblast/lazy_bitblaster.h" @@ -23,7 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -58,7 +58,7 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen) } TLazyBitblaster::TLazyBitblaster(context::Context* c, - bv::BVSolverLazy* bv, + bv::BVSolverLayered* bv, const std::string name, bool emptyNotify) : TBitblaster(), @@ -294,10 +294,10 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { } Debug("bitvector-bb") - << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom - << "\n"; + << "BVSolverLayered::TLazyBitblaster::assertToSat asserting node: " + << atom << "\n"; Debug("bitvector-bb") - << "BVSolverLazy::TLazyBitblaster::assertToSat with literal: " + << "BVSolverLayered::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n"; prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); @@ -404,9 +404,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { lemmab << d_cnf->getNode(clause[i]); } Node lemma = lemmab; - d_bv->d_im.lemma(lemma, InferenceId::BV_LAZY_LEMMA); + d_bv->d_im.lemma(lemma, InferenceId::BV_LAYERED_LEMMA); } else { - d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAZY_LEMMA); + d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAYERED_LEMMA); } } diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 15cbe1558..8d8723522 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -33,7 +33,7 @@ class NullRegistrat; namespace theory { namespace bv { -class BVSolverLazy; +class BVSolverLayered; class TLazyBitblaster : public TBitblaster { @@ -46,7 +46,7 @@ class TLazyBitblaster : public TBitblaster bool hasBBAtom(TNode atom) const override; TLazyBitblaster(context::Context* c, - BVSolverLazy* bv, + BVSolverLayered* bv, const std::string name = "", bool emptyNotify = false); ~TLazyBitblaster(); @@ -109,11 +109,13 @@ class TLazyBitblaster : public TBitblaster class MinisatNotify : public prop::BVSatSolverNotify { prop::CnfStream* d_cnf; - BVSolverLazy* d_bv; + BVSolverLayered* d_bv; TLazyBitblaster* d_lazyBB; public: - MinisatNotify(prop::CnfStream* cnf, BVSolverLazy* bv, TLazyBitblaster* lbv) + MinisatNotify(prop::CnfStream* cnf, + BVSolverLayered* bv, + TLazyBitblaster* lbv) : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv) { } @@ -124,7 +126,7 @@ class TLazyBitblaster : public TBitblaster void safePoint(Resource r) override; }; - BVSolverLazy* d_bv; + BVSolverLayered* d_bv; context::Context* d_ctx; std::unique_ptr d_nullRegistrar; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index b0082b992..23b98ca54 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -27,7 +27,8 @@ namespace cvc5 { namespace theory { namespace bv { -EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv) +EagerBitblastSolver::EagerBitblastSolver(context::Context* c, + BVSolverLayered* bv) : d_assertionSet(c), d_assumptionSet(c), d_context(c), diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index ab51ea844..fec4edee9 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__BV__BV_EAGER_SOLVER_H #include "expr/node.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/theory_model.h" namespace cvc5 { @@ -34,7 +34,7 @@ class AigBitblaster; */ class EagerBitblastSolver { public: - EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLazy* bv); + EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLayered* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -54,7 +54,7 @@ class EagerBitblastSolver { std::unique_ptr d_aigBitblaster; bool d_useAig; - BVSolverLazy* d_bv; + BVSolverLayered* d_bv; }; // class EagerBitblastSolver } // namespace bv diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 5d3e99253..dd9c1849d 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -17,7 +17,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/bitblast/lazy_bitblaster.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv_utils.h" using namespace cvc5::prop; @@ -27,7 +27,7 @@ namespace theory { namespace bv { BVQuickCheck::BVQuickCheck(const std::string& name, - theory::bv::BVSolverLazy* bv) + theory::bv::BVSolverLayered* bv) : d_ctx(), d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)), d_conflict(), diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index d1411d784..b8274ce80 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -35,7 +35,7 @@ class TheoryModel; namespace bv { class TLazyBitblaster; -class BVSolverLazy; +class BVSolverLayered; class BVQuickCheck { @@ -46,7 +46,7 @@ class BVQuickCheck void setConflict(); public: - BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv); + BVQuickCheck(const std::string& name, theory::bv::BVSolverLayered* bv); ~BVQuickCheck(); bool inConflict(); Node getConflict() { return d_conflict; } diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_layered.cpp similarity index 84% rename from src/theory/bv/bv_solver_lazy.cpp rename to src/theory/bv/bv_solver_layered.cpp index 5210117b8..40daf1cb4 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_layered.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * Lazy bit-vector solver. + * Layered bit-vector solver. */ -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "expr/node_algorithm.h" #include "options/bv_options.h" @@ -37,11 +37,11 @@ namespace cvc5 { namespace theory { namespace bv { -BVSolverLazy::BVSolverLazy(TheoryBV& bv, - context::Context* c, - context::UserContext* u, - ProofNodeManager* pnm, - std::string name) +BVSolverLayered::BVSolverLayered(TheoryBV& bv, + context::Context* c, + context::UserContext* u, + ProofNodeManager* pnm, + std::string name) : BVSolver(bv.d_state, bv.d_im), d_bv(bv), d_context(c), @@ -94,9 +94,9 @@ BVSolverLazy::BVSolverLazy(TheoryBV& bv, d_subtheoryMap[SUB_BITBLAST] = bb_solver; } -BVSolverLazy::~BVSolverLazy() {} +BVSolverLayered::~BVSolverLayered() {} -bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi) +bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi) { CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; if (core) @@ -107,7 +107,7 @@ bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi) return false; } -void BVSolverLazy::finishInit() +void BVSolverLayered::finishInit() { CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; if (core) @@ -117,12 +117,9 @@ void BVSolverLazy::finishInit() } } -void BVSolverLazy::spendResource(Resource r) -{ - d_im.spendResource(r); -} +void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); } -BVSolverLazy::Statistics::Statistics() +BVSolverLayered::Statistics::Statistics() : d_avgConflictSize(smtStatisticsRegistry().registerAverage( "theory::bv::lazy::AvgBVConflictSize")), d_solveTimer(smtStatisticsRegistry().registerTimer( @@ -138,11 +135,11 @@ BVSolverLazy::Statistics::Statistics() { } -void BVSolverLazy::preRegisterTerm(TNode node) +void BVSolverLayered::preRegisterTerm(TNode node) { d_calledPreregister = true; Debug("bitvector-preregister") - << "BVSolverLazy::preRegister(" << node << ")" << std::endl; + << "BVSolverLayered::preRegister(" << node << ")" << std::endl; if (options::bitblastMode() == options::BitblastMode::EAGER) { @@ -171,7 +168,7 @@ void BVSolverLazy::preRegisterTerm(TNode node) // d_bv.d_extTheory->registerTermRec( node ); } -void BVSolverLazy::sendConflict() +void BVSolverLayered::sendConflict() { Assert(d_conflict); if (d_conflictNode.isNull()) @@ -180,15 +177,15 @@ void BVSolverLazy::sendConflict() } else { - Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict " + Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict " << d_conflictNode << std::endl; - d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT); + d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT); d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren(); d_conflictNode = Node::null(); } } -void BVSolverLazy::checkForLemma(TNode fact) +void BVSolverLayered::checkForLemma(TNode fact) { if (fact.getKind() == kind::EQUAL) { @@ -220,20 +217,20 @@ void BVSolverLazy::checkForLemma(TNode fact) } } -bool BVSolverLazy::preCheck(Theory::Effort e) +bool BVSolverLayered::preCheck(Theory::Effort e) { check(e); return true; } -void BVSolverLazy::check(Theory::Effort e) +void BVSolverLayered::check(Theory::Effort e) { if (done() && e < Theory::EFFORT_FULL) { return; } - Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl; + Debug("bitvector") << "BVSolverLayered::check(" << e << ")" << std::endl; TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); @@ -261,11 +258,11 @@ void BVSolverLazy::check(Theory::Effort e) { if (assertions.size() == 1) { - d_im.conflict(assertions[0], InferenceId::BV_LAZY_CONFLICT); + d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT); return; } Node conflict = utils::mkAnd(assertions); - d_im.conflict(conflict, InferenceId::BV_LAZY_CONFLICT); + d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT); return; } return; @@ -321,8 +318,8 @@ void BVSolverLazy::check(Theory::Effort e) } } -bool BVSolverLazy::collectModelValues(TheoryModel* m, - const std::set& termSet) +bool BVSolverLayered::collectModelValues(TheoryModel* m, + const std::set& termSet) { Assert(!inConflict()); if (options::bitblastMode() == options::BitblastMode::EAGER) @@ -342,7 +339,7 @@ bool BVSolverLazy::collectModelValues(TheoryModel* m, return true; } -Node BVSolverLazy::getModelValue(TNode var) +Node BVSolverLayered::getModelValue(TNode var) { Assert(!inConflict()); for (unsigned i = 0; i < d_subtheories.size(); ++i) @@ -355,9 +352,9 @@ Node BVSolverLazy::getModelValue(TNode var) Unreachable(); } -void BVSolverLazy::propagate(Theory::Effort e) +void BVSolverLayered::propagate(Theory::Effort e) { - Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl; + Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl; if (options::bitblastMode() == options::BitblastMode::EAGER) { return; @@ -378,7 +375,7 @@ void BVSolverLazy::propagate(Theory::Effort e) if (d_state.isSatLiteral(literal)) { Debug("bitvector::propagate") - << "BVSolverLazy:: propagating " << literal << "\n"; + << "BVSolverLayered:: propagating " << literal << "\n"; ok = d_im.propagateLit(literal); } } @@ -386,15 +383,16 @@ void BVSolverLazy::propagate(Theory::Effort e) if (!ok) { Debug("bitvector::propagate") - << indent() << "BVSolverLazy::propagate(): conflict from theory engine" + << indent() + << "BVSolverLayered::propagate(): conflict from theory engine" << std::endl; setConflict(); } } -TrustNode BVSolverLazy::ppRewrite(TNode t) +TrustNode BVSolverLayered::ppRewrite(TNode t) { - Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n"; + Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n"; Node res = t; if (options::bitwiseEq() && RewriteRule::applies(t)) { @@ -489,25 +487,26 @@ TrustNode BVSolverLazy::ppRewrite(TNode t) return TrustNode::null(); } -void BVSolverLazy::presolve() +void BVSolverLayered::presolve() { - Debug("bitvector") << "BVSolverLazy::presolve" << std::endl; + Debug("bitvector") << "BVSolverLayered::presolve" << std::endl; } static int prop_count = 0; -bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory) +bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory) { - Debug("bitvector::propagate") << indent() << d_context->getLevel() << " " - << "BVSolverLazy::storePropagation(" << literal - << ", " << subtheory << ")" << std::endl; + Debug("bitvector::propagate") + << indent() << d_context->getLevel() << " " + << "BVSolverLayered::storePropagation(" << literal << ", " << subtheory + << ")" << std::endl; prop_count++; // If already in conflict, no more propagation if (d_conflict) { Debug("bitvector::propagate") - << indent() << "BVSolverLazy::storePropagation(" << literal << ", " + << indent() << "BVSolverLayered::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl; return false; } @@ -552,19 +551,19 @@ bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory) } return ok; -} /* BVSolverLazy::propagate(TNode) */ +} /* BVSolverLayered::propagate(TNode) */ -void BVSolverLazy::explain(TNode literal, std::vector& assumptions) +void BVSolverLayered::explain(TNode literal, std::vector& assumptions) { Assert(wasPropagatedBySubtheory(literal)); SubTheory sub = getPropagatingSubtheory(literal); d_subtheoryMap[sub]->explain(literal, assumptions); } -TrustNode BVSolverLazy::explain(TNode node) +TrustNode BVSolverLayered::explain(TNode node) { Debug("bitvector::explain") - << "BVSolverLazy::explain(" << node << ")" << std::endl; + << "BVSolverLayered::explain(" << node << ")" << std::endl; std::vector assumptions; // Ask for the explanation @@ -580,20 +579,21 @@ TrustNode BVSolverLazy::explain(TNode node) // return the explanation explanation = utils::mkAnd(assumptions); } - Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => " + Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => " << explanation << std::endl; - Debug("bitvector::explain") << "BVSolverLazy::explain done. \n"; + Debug("bitvector::explain") << "BVSolverLayered::explain done. \n"; return TrustNode::mkTrustPropExp(node, explanation, nullptr); } -void BVSolverLazy::notifySharedTerm(TNode t) +void BVSolverLayered::notifySharedTerm(TNode t) { Debug("bitvector::sharing") - << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl; + << indent() << "BVSolverLayered::notifySharedTerm(" << t << ")" + << std::endl; d_sharedTermsSet.insert(t); } -EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) +EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b) { if (options::bitblastMode() == options::BitblastMode::EAGER) return EQUALITY_UNKNOWN; @@ -610,7 +610,7 @@ EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) ; } -void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned) +void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned) { if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) { @@ -660,8 +660,8 @@ void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned) } } -bool BVSolverLazy::applyAbstraction(const std::vector& assertions, - std::vector& new_assertions) +bool BVSolverLayered::applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) { bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); @@ -676,7 +676,7 @@ bool BVSolverLazy::applyAbstraction(const std::vector& assertions, return changed; } -void BVSolverLazy::setConflict(Node conflict) +void BVSolverLayered::setConflict(Node conflict) { if (options::bvAbstraction()) { diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_layered.h similarity index 90% rename from src/theory/bv/bv_solver_lazy.h rename to src/theory/bv/bv_solver_layered.h index 4f73354bc..023ff5a46 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_layered.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * Lazy bit-vector solver. + * Layered bit-vector solver. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H -#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H +#ifndef CVC5__THEORY__BV__BV_SOLVER_LAYERED_H +#define CVC5__THEORY__BV__BV_SOLVER_LAYERED_H #include #include @@ -40,7 +40,7 @@ class BitblastSolver; class EagerBitblastSolver; class AbstractionModule; -class BVSolverLazy : public BVSolver +class BVSolverLayered : public BVSolver { /** Back reference to TheoryBV */ TheoryBV& d_bv; @@ -57,13 +57,13 @@ class BVSolverLazy : public BVSolver d_subtheoryMap; public: - BVSolverLazy(TheoryBV& bv, - context::Context* c, - context::UserContext* u, - ProofNodeManager* pnm = nullptr, - std::string name = ""); + BVSolverLayered(TheoryBV& bv, + context::Context* c, + context::UserContext* u, + ProofNodeManager* pnm = nullptr, + std::string name = ""); - ~BVSolverLazy(); + ~BVSolverLayered(); //--------------------------------- initialization @@ -89,7 +89,10 @@ class BVSolverLazy : public BVSolver bool collectModelValues(TheoryModel* m, const std::set& termSet) override; - std::string identify() const override { return std::string("BVSolverLazy"); } + std::string identify() const override + { + return std::string("BVSolverLayered"); + } TrustNode ppRewrite(TNode t) override; @@ -197,7 +200,7 @@ class BVSolverLazy : public BVSolver void lemma(TNode node) { - d_im.lemma(node, InferenceId::BV_LAZY_LEMMA); + d_im.lemma(node, InferenceId::BV_LAYERED_LEMMA); d_lemmasAdded = true; } @@ -218,7 +221,7 @@ class BVSolverLazy : public BVSolver friend class InequalitySolver; friend class AlgebraicSolver; friend class EagerBitblastSolver; -}; /* class BVSolverLazy */ +}; /* class BVSolverLayered */ } // namespace bv } // namespace theory diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 8a81a5ef8..6c887424a 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -54,7 +54,7 @@ inline std::ostream& operator<<(std::ostream& out, SubTheory subtheory) { } // forward declaration -class BVSolverLazy; +class BVSolverLayered; using AssertionQueue = context::CDQueue; @@ -64,7 +64,7 @@ using AssertionQueue = context::CDQueue; */ class SubtheorySolver { public: - SubtheorySolver(context::Context* c, BVSolverLazy* bv) + SubtheorySolver(context::Context* c, BVSolverLayered* bv) : d_context(c), d_bv(bv), d_assertionQueue(c), d_assertionIndex(c, 0) { } @@ -99,7 +99,7 @@ class SubtheorySolver { context::Context* d_context; /** The bit-vector theory */ - BVSolverLazy* d_bv; + BVSolverLayered* d_bv; AssertionQueue d_assertionQueue; context::CDO d_assertionIndex; }; /* class SubtheorySolver */ diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 65c1ec79c..d6e60d1f4 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -25,7 +25,7 @@ #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -232,7 +232,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) { d_cache[from] = SubstitutionElement(to, reason); } -AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLazy* bv) +AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLayered* bv) : SubtheorySolver(c, bv), d_modelMap(), d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)), diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index b93ff235f..16cf3d53b 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -222,7 +222,7 @@ class AlgebraicSolver : public SubtheorySolver bool quickCheck(std::vector& facts); public: - AlgebraicSolver(context::Context* c, BVSolverLazy* bv); + AlgebraicSolver(context::Context* c, BVSolverLayered* bv); ~AlgebraicSolver(); void preRegister(TNode node) override {} diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index b86809a91..cdc2fc143 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -22,7 +22,7 @@ #include "theory/bv/abstraction.h" #include "theory/bv/bitblast/lazy_bitblaster.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv_utils.h" using namespace std; @@ -32,7 +32,7 @@ namespace cvc5 { namespace theory { namespace bv { -BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv) +BitblastSolver::BitblastSolver(context::Context* c, BVSolverLayered* bv) : SubtheorySolver(c, bv), d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")), d_bitblastQueue(c), diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 439bd33ed..3ad707482 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -63,7 +63,7 @@ class BitblastSolver : public SubtheorySolver void setConflict(TNode conflict); public: - BitblastSolver(context::Context* c, BVSolverLazy* bv); + BitblastSolver(context::Context* c, BVSolverLayered* bv); ~BitblastSolver(); void preRegister(TNode node) override; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index fa71641ad..3f3384257 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -19,7 +19,7 @@ #include "options/bv_options.h" #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" @@ -32,7 +32,7 @@ using namespace cvc5::theory; using namespace cvc5::theory::bv; using namespace cvc5::theory::bv::utils; -CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv) +CoreSolver::CoreSolver(context::Context* c, BVSolverLayered* bv) : SubtheorySolver(c, bv), d_notify(*this), d_isComplete(c, true), diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 46c4559ea..2e6312144 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -74,7 +74,7 @@ class CoreSolver : public SubtheorySolver { bool d_checkCalled; /** Pointer to the parent theory solver that owns this */ - BVSolverLazy* d_bv; + BVSolverLayered* d_bv; /** Pointer to the equality engine of the parent */ eq::EqualityEngine* d_equalityEngine; @@ -87,7 +87,7 @@ class CoreSolver : public SubtheorySolver { Statistics d_statistics; public: - CoreSolver(context::Context* c, BVSolverLazy* bv); + CoreSolver(context::Context* c, BVSolverLayered* bv); ~CoreSolver(); bool needsEqualityEngine(EeSetupInfo& esi); void finishInit(); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index aa93008c2..3bd3e9c3e 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -17,7 +17,7 @@ #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index f8a7bf113..8a76a6bf1 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -62,7 +62,9 @@ class InequalitySolver : public SubtheorySolver Statistics d_statistics; public: - InequalitySolver(context::Context* c, context::Context* u, BVSolverLazy* bv) + InequalitySolver(context::Context* c, + context::Context* u, + BVSolverLayered* bv) : SubtheorySolver(c, bv), d_assertionSet(c), d_inequalityGraph(c, u), diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b3cf6da59..37881f9b2 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -21,7 +21,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" #include "theory/bv/bv_solver_bitblast_internal.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ee_setup_info.h" #include "theory/trust_substitutions.h" @@ -51,8 +51,8 @@ TheoryBV::TheoryBV(context::Context* c, d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm)); break; - case options::BVSolver::LAZY: - d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name)); + case options::BVSolver::LAYERED: + d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name)); break; default: diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index e884f621c..f2d6bb47e 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -34,9 +34,9 @@ class BVSolver; class TheoryBV : public Theory { - /* BVSolverLazy accesses methods from theory in a way that is deprecated and - * will be removed in the future. For now we allow direct access. */ - friend class BVSolverLazy; + /* BVSolverLayered accesses methods from theory in a way that is deprecated + * and will be removed in the future. For now we allow direct access. */ + friend class BVSolverLayered; public: TheoryBV(context::Context* c, diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 612c99d82..a26147f09 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -110,12 +110,12 @@ const char* toString(InferenceId i) case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL"; case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT"; - case InferenceId::BV_LAZY_CONFLICT: return "BV_LAZY_CONFLICT"; - case InferenceId::BV_LAZY_LEMMA: return "BV_LAZY_LEMMA"; case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA: return "BV_BITBLAST_EAGER_LEMMA"; case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA: return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA"; + case InferenceId::BV_LAYERED_CONFLICT: return "BV_LAYERED_CONFLICT"; + case InferenceId::BV_LAYERED_LEMMA: return "BV_LAYERED_LEMMA"; case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA"; case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index ebbccfd54..f32c80b68 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -173,10 +173,10 @@ enum class InferenceId // ---------------------------------- bitvector theory BV_BITBLAST_CONFLICT, - BV_LAZY_CONFLICT, - BV_LAZY_LEMMA, BV_BITBLAST_INTERNAL_EAGER_LEMMA, BV_BITBLAST_INTERNAL_BITBLAST_LEMMA, + BV_LAYERED_CONFLICT, + BV_LAYERED_LEMMA, BV_EXTF_LEMMA, BV_EXTF_COLLAPSE, // ---------------------------------- end bitvector theory diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 150320824..4cf695609 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -22,7 +22,7 @@ #include "expr/node.h" #include "test_smt.h" #include "theory/bv/bitblast/eager_bitblaster.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -45,7 +45,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) d_smtEngine->setLogic("QF_BV"); d_smtEngine->setOption("bitblast", "eager"); - d_smtEngine->setOption("bv-solver", "lazy"); + d_smtEngine->setOption("bv-solver", "layered"); d_smtEngine->setOption("incremental", "false"); // Notice that this unit test uses the theory engine of a created SMT // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized @@ -53,7 +53,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) d_smtEngine->finishInit(); TheoryBV* tbv = dynamic_cast( d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]); - BVSolverLazy* bvsl = dynamic_cast(tbv->d_internal.get()); + BVSolverLayered* bvsl = dynamic_cast(tbv->d_internal.get()); std::unique_ptr bb( new EagerBitblaster(bvsl, d_smtEngine->getContext())); -- 2.30.2