From: Mathias Preiner Date: Thu, 15 Jul 2021 01:54:33 +0000 (-0700) Subject: bv: Rename lazy solver to layered solver. (#6889) X-Git-Tag: cvc5-1.0.0~1484 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb6813731ef1059ab38cedcc5af026b6e75bd6be;p=cvc5.git bv: Rename lazy solver to layered solver. (#6889) --- 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_layered.cpp b/src/theory/bv/bv_solver_layered.cpp new file mode 100644 index 000000000..40daf1cb4 --- /dev/null +++ b/src/theory/bv/bv_solver_layered.cpp @@ -0,0 +1,700 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Layered bit-vector solver. + */ + +#include "theory/bv/bv_solver_layered.h" + +#include "expr/node_algorithm.h" +#include "options/bv_options.h" +#include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" +#include "theory/bv/abstraction.h" +#include "theory/bv/bv_eager_solver.h" +#include "theory/bv/bv_subtheory_algebraic.h" +#include "theory/bv/bv_subtheory_bitblast.h" +#include "theory/bv/bv_subtheory_core.h" +#include "theory/bv/bv_subtheory_inequality.h" +#include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#include "theory/bv/theory_bv_rewriter.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/theory_model.h" + +using namespace cvc5::theory::bv::utils; + +namespace cvc5 { +namespace theory { +namespace bv { + +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), + d_alreadyPropagatedSet(c), + d_sharedTermsSet(c), + d_subtheories(), + d_subtheoryMap(), + d_statistics(), + d_staticLearnCache(), + 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_calledPreregister(false) +{ + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + d_eagerSolver.reset(new EagerBitblastSolver(c, this)); + return; + } + + if (options::bitvectorEqualitySolver()) + { + d_subtheories.emplace_back(new CoreSolver(c, this)); + d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); + } + + if (options::bitvectorInequalitySolver()) + { + d_subtheories.emplace_back(new InequalitySolver(c, u, this)); + d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); + } + + if (options::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()) + { + bb_solver->setAbstraction(d_abstractionModule.get()); + } + d_subtheories.emplace_back(bb_solver); + d_subtheoryMap[SUB_BITBLAST] = bb_solver; +} + +BVSolverLayered::~BVSolverLayered() {} + +bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi) +{ + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if (core) + { + return core->needsEqualityEngine(esi); + } + // otherwise we don't use an equality engine + return false; +} + +void BVSolverLayered::finishInit() +{ + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if (core) + { + // must finish initialization in the core solver + core->finishInit(); + } +} + +void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); } + +BVSolverLayered::Statistics::Statistics() + : d_avgConflictSize(smtStatisticsRegistry().registerAverage( + "theory::bv::lazy::AvgBVConflictSize")), + d_solveTimer(smtStatisticsRegistry().registerTimer( + "theory::bv::lazy::solveTimer")), + d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumFullCheckCalls")), + d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumStandardCheckCalls")), + d_weightComputationTimer(smtStatisticsRegistry().registerTimer( + "theory::bv::lazy::weightComputationTimer")), + d_numMultSlice(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumMultSliceApplied")) +{ +} + +void BVSolverLayered::preRegisterTerm(TNode node) +{ + d_calledPreregister = true; + Debug("bitvector-preregister") + << "BVSolverLayered::preRegister(" << node << ")" << std::endl; + + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + // the aig bit-blaster option is set heuristically + // if bv abstraction is used + if (!d_eagerSolver->isInitialized()) + { + d_eagerSolver->initialize(); + } + + if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) + { + Node formula = node[0]; + d_eagerSolver->assertFormula(formula); + } + return; + } + + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + d_subtheories[i]->preRegister(node); + } + + // AJR : equality solver currently registers all terms to ExtTheory, if we + // want a lazy reduction without the bv equality solver, need to call this + // d_bv.d_extTheory->registerTermRec( node ); +} + +void BVSolverLayered::sendConflict() +{ + Assert(d_conflict); + if (d_conflictNode.isNull()) + { + return; + } + else + { + Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict " + << d_conflictNode << std::endl; + d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT); + d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren(); + d_conflictNode = Node::null(); + } +} + +void BVSolverLayered::checkForLemma(TNode fact) +{ + if (fact.getKind() == kind::EQUAL) + { + NodeManager* nm = NodeManager::currentNM(); + if (fact[0].getKind() == kind::BITVECTOR_UREM) + { + TNode urem = fact[0]; + TNode result = fact[1]; + TNode divisor = urem[1]; + Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = + nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); + Node split = nm->mkNode( + kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + if (fact[1].getKind() == kind::BITVECTOR_UREM) + { + TNode urem = fact[1]; + TNode result = fact[0]; + TNode divisor = urem[1]; + Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = + nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); + Node split = nm->mkNode( + kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + } +} + +bool BVSolverLayered::preCheck(Theory::Effort e) +{ + check(e); + return true; +} + +void BVSolverLayered::check(Theory::Effort e) +{ + if (done() && e < Theory::EFFORT_FULL) + { + return; + } + + 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); + // if we are using the eager solver + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + // this can only happen on an empty benchmark + if (!d_eagerSolver->isInitialized()) + { + d_eagerSolver->initialize(); + } + if (!Theory::fullEffort(e)) return; + + std::vector assertions; + while (!done()) + { + TNode fact = get().d_assertion; + Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); + assertions.push_back(fact); + d_eagerSolver->assertFormula(fact[0]); + } + + bool ok = d_eagerSolver->checkSat(); + if (!ok) + { + if (assertions.size() == 1) + { + d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT); + return; + } + Node conflict = utils::mkAnd(assertions); + d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT); + return; + } + return; + } + + if (Theory::fullEffort(e)) + { + ++(d_statistics.d_numCallsToCheckFullEffort); + } + else + { + ++(d_statistics.d_numCallsToCheckStandardEffort); + } + // if we are already in conflict just return the conflict + if (inConflict()) + { + sendConflict(); + return; + } + + while (!done()) + { + TNode fact = get().d_assertion; + + checkForLemma(fact); + + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + d_subtheories[i]->assertFact(fact); + } + } + + bool ok = true; + bool complete = false; + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + Assert(!inConflict()); + ok = d_subtheories[i]->check(e); + complete = d_subtheories[i]->isComplete(); + + if (!ok) + { + // if we are in a conflict no need to check with other theories + Assert(inConflict()); + sendConflict(); + return; + } + if (complete) + { + // if the last subtheory was complete we stop + break; + } + } +} + +bool BVSolverLayered::collectModelValues(TheoryModel* m, + const std::set& termSet) +{ + Assert(!inConflict()); + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + if (!d_eagerSolver->collectModelInfo(m, true)) + { + return false; + } + } + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + if (d_subtheories[i]->isComplete()) + { + return d_subtheories[i]->collectModelValues(m, termSet); + } + } + return true; +} + +Node BVSolverLayered::getModelValue(TNode var) +{ + Assert(!inConflict()); + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + if (d_subtheories[i]->isComplete()) + { + return d_subtheories[i]->getModelValue(var); + } + } + Unreachable(); +} + +void BVSolverLayered::propagate(Theory::Effort e) +{ + Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl; + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + return; + } + + if (inConflict()) + { + return; + } + + // go through stored propagations + bool ok = true; + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; + d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) + { + TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; + // temporary fix for incremental bit-blasting + if (d_state.isSatLiteral(literal)) + { + Debug("bitvector::propagate") + << "BVSolverLayered:: propagating " << literal << "\n"; + ok = d_im.propagateLit(literal); + } + } + + if (!ok) + { + Debug("bitvector::propagate") + << indent() + << "BVSolverLayered::propagate(): conflict from theory engine" + << std::endl; + setConflict(); + } +} + +TrustNode BVSolverLayered::ppRewrite(TNode t) +{ + Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n"; + Node res = t; + if (options::bitwiseEq() && RewriteRule::applies(t)) + { + Node result = RewriteRule::run(t); + res = Rewriter::rewrite(result); + } + else if (RewriteRule::applies(t)) + { + Node result = RewriteRule::run(t); + res = Rewriter::rewrite(result); + } + else if (res.getKind() == kind::EQUAL + && ((res[0].getKind() == kind::BITVECTOR_ADD + && RewriteRule::applies(res[1])) + || (res[1].getKind() == kind::BITVECTOR_ADD + && RewriteRule::applies(res[0])))) + { + Node mult = RewriteRule::applies(res[0]) + ? RewriteRule::run(res[0]) + : RewriteRule::run(res[1]); + Node factor = mult[0]; + Node sum = RewriteRule::applies(res[0]) ? res[1] : res[0]; + Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); + Node rewr_eq = RewriteRule::run(new_eq); + if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) + { + res = Rewriter::rewrite(rewr_eq); + } + else + { + res = t; + } + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + + // if(t.getKind() == kind::EQUAL && + // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == + // kind::BITVECTOR_ADD) || + // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == + // kind::BITVECTOR_ADD))) { + // // if we have an equality between a multiplication and addition + // // try to express multiplication in terms of addition + // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; + // Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1]; + // if (RewriteRule::applies(mult)) { + // Node new_mult = RewriteRule::run(mult); + // Node new_eq = + // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, + // new_mult, add)); + + // // the simplification can cause the formula to blow up + // // only apply if formula reduced + // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { + // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; + // uint64_t old_size = bv->computeAtomWeight(t); + // Assert (old_size); + // uint64_t new_size = bv->computeAtomWeight(new_eq); + // double ratio = ((double)new_size)/old_size; + // if (ratio <= 0.4) { + // ++(d_statistics.d_numMultSlice); + // return new_eq; + // } + // } + + // if (new_eq.getKind() == kind::CONST_BOOLEAN) { + // ++(d_statistics.d_numMultSlice); + // return new_eq; + // } + // } + // } + + if (options::bvAbstraction() && t.getType().isBoolean()) + { + d_abstractionModule->addInputAtom(res); + } + Debug("bv-pp-rewrite") << "to " << res << "\n"; + if (res != t) + { + return TrustNode::mkTrustRewrite(t, res, nullptr); + } + return TrustNode::null(); +} + +void BVSolverLayered::presolve() +{ + Debug("bitvector") << "BVSolverLayered::presolve" << std::endl; +} + +static int prop_count = 0; + +bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory) +{ + 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() << "BVSolverLayered::storePropagation(" << literal << ", " + << subtheory << "): already in conflict" << std::endl; + return false; + } + + // If propagated already, just skip + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + if (find != d_propagatedBy.end()) + { + return true; + } + else + { + bool polarity = literal.getKind() != kind::NOT; + Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0]; + find = d_propagatedBy.find(negatedLiteral); + if (find != d_propagatedBy.end() && (*find).second != subtheory) + { + // Safe to ignore this one, subtheory should produce a conflict + return true; + } + + d_propagatedBy[literal] = subtheory; + } + + // Propagate differs depending on the subtheory + // * bitblaster needs to be left alone until it's done, otherwise it doesn't + // know how to explain + // * equality engine can propagate eagerly + // TODO(2348): Determine if ok should be set by propagate. If not, remove ok. + constexpr bool ok = true; + if (subtheory == SUB_CORE) + { + d_im.propagateLit(literal); + if (!ok) + { + setConflict(); + } + } + else + { + d_literalsToPropagate.push_back(literal); + } + return ok; + +} /* BVSolverLayered::propagate(TNode) */ + +void BVSolverLayered::explain(TNode literal, std::vector& assumptions) +{ + Assert(wasPropagatedBySubtheory(literal)); + SubTheory sub = getPropagatingSubtheory(literal); + d_subtheoryMap[sub]->explain(literal, assumptions); +} + +TrustNode BVSolverLayered::explain(TNode node) +{ + Debug("bitvector::explain") + << "BVSolverLayered::explain(" << node << ")" << std::endl; + std::vector assumptions; + + // Ask for the explanation + explain(node, assumptions); + // this means that it is something true at level 0 + Node explanation; + if (assumptions.size() == 0) + { + explanation = utils::mkTrue(); + } + else + { + // return the explanation + explanation = utils::mkAnd(assumptions); + } + Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => " + << explanation << std::endl; + Debug("bitvector::explain") << "BVSolverLayered::explain done. \n"; + return TrustNode::mkTrustPropExp(node, explanation, nullptr); +} + +void BVSolverLayered::notifySharedTerm(TNode t) +{ + Debug("bitvector::sharing") + << indent() << "BVSolverLayered::notifySharedTerm(" << t << ")" + << std::endl; + d_sharedTermsSet.insert(t); +} + +EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b) +{ + if (options::bitblastMode() == options::BitblastMode::EAGER) + return EQUALITY_UNKNOWN; + Assert(options::bitblastMode() == options::BitblastMode::LAZY); + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); + if (status != EQUALITY_UNKNOWN) + { + return status; + } + } + return EQUALITY_UNKNOWN; + ; +} + +void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned) +{ + if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) + { + return; + } + d_staticLearnCache.insert(in); + + if (in.getKind() == kind::EQUAL) + { + if ((in[0].getKind() == kind::BITVECTOR_ADD + && in[1].getKind() == kind::BITVECTOR_SHL) + || (in[1].getKind() == kind::BITVECTOR_ADD + && in[0].getKind() == kind::BITVECTOR_SHL)) + { + TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1]; + TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0]; + + if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL + && p[1].getKind() == kind::BITVECTOR_SHL) + { + unsigned size = utils::getSize(s); + Node one = utils::mkConst(size, 1u); + if (s[0] == one && p[0][0] == one && p[1][0] == one) + { + Node zero = utils::mkConst(size, 0u); + TNode b = p[0]; + TNode c = p[1]; + // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) + Node b_eq_0 = b.eqNode(zero); + Node c_eq_0 = c.eqNode(zero); + Node b_eq_c = b.eqNode(c); + + Node dis = NodeManager::currentNM()->mkNode( + kind::OR, b_eq_0, c_eq_0, b_eq_c); + Node imp = in.impNode(dis); + learned << imp; + } + } + } + } + else if (in.getKind() == kind::AND) + { + for (size_t i = 0, N = in.getNumChildren(); i < N; ++i) + { + ppStaticLearn(in[i], learned); + } + } +} + +bool BVSolverLayered::applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) +{ + bool changed = + d_abstractionModule->applyAbstraction(assertions, new_assertions); + if (changed && options::bitblastMode() == options::BitblastMode::EAGER + && options::bitvectorAig()) + { + // disable AIG mode + AlwaysAssert(!d_eagerSolver->isInitialized()); + d_eagerSolver->turnOffAig(); + d_eagerSolver->initialize(); + } + return changed; +} + +void BVSolverLayered::setConflict(Node conflict) +{ + if (options::bvAbstraction()) + { + NodeManager* const nm = NodeManager::currentNM(); + Node new_conflict = d_abstractionModule->simplifyConflict(conflict); + + std::vector lemmas; + lemmas.push_back(new_conflict); + d_abstractionModule->generalizeConflict(new_conflict, lemmas); + for (unsigned i = 0; i < lemmas.size(); ++i) + { + lemma(nm->mkNode(kind::NOT, lemmas[i])); + } + } + d_conflict = true; + d_conflictNode = conflict; +} + +} // namespace bv +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h new file mode 100644 index 000000000..023ff5a46 --- /dev/null +++ b/src/theory/bv/bv_solver_layered.h @@ -0,0 +1,231 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Layered bit-vector solver. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__BV__BV_SOLVER_LAYERED_H +#define CVC5__THEORY__BV__BV_SOLVER_LAYERED_H + +#include +#include + +#include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/context.h" +#include "theory/bv/bv_solver.h" +#include "theory/bv/bv_subtheory.h" +#include "theory/bv/theory_bv.h" +#include "util/hash.h" + +namespace cvc5 { +namespace theory { +namespace bv { + +class CoreSolver; +class InequalitySolver; +class AlgebraicSolver; +class BitblastSolver; +class EagerBitblastSolver; +class AbstractionModule; + +class BVSolverLayered : public BVSolver +{ + /** Back reference to TheoryBV */ + TheoryBV& d_bv; + + /** The context we are using */ + context::Context* d_context; + + /** Context dependent set of atoms we already propagated */ + context::CDHashSet d_alreadyPropagatedSet; + context::CDHashSet d_sharedTermsSet; + + std::vector> d_subtheories; + std::unordered_map> + d_subtheoryMap; + + public: + BVSolverLayered(TheoryBV& bv, + context::Context* c, + context::UserContext* u, + ProofNodeManager* pnm = nullptr, + std::string name = ""); + + ~BVSolverLayered(); + + //--------------------------------- initialization + + /** + * Returns true if we need an equality engine. If so, we initialize the + * information regarding how it should be setup. For details, see the + * documentation in Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi) override; + + /** finish initialization */ + void finishInit() override; + //--------------------------------- end initialization + + void preRegisterTerm(TNode n) override; + + bool preCheck(Theory::Effort e) override; + + void propagate(Theory::Effort e) override; + + TrustNode explain(TNode n) override; + + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; + + std::string identify() const override + { + return std::string("BVSolverLayered"); + } + + TrustNode ppRewrite(TNode t) override; + + void ppStaticLearn(TNode in, NodeBuilder& learned) override; + + void presolve() override; + + bool applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) override; + + bool isLeaf(TNode node) { return d_bv.isLeaf(node); } + + private: + class Statistics + { + public: + AverageStat d_avgConflictSize; + TimerStat d_solveTimer; + IntStat d_numCallsToCheckFullEffort; + IntStat d_numCallsToCheckStandardEffort; + TimerStat d_weightComputationTimer; + IntStat d_numMultSlice; + Statistics(); + }; + + Statistics d_statistics; + + void check(Theory::Effort e); + void spendResource(Resource r); + + typedef std::unordered_set TNodeSet; + typedef std::unordered_set NodeSet; + NodeSet d_staticLearnCache; + + typedef std::unordered_map NodeToNode; + + context::CDO d_lemmasAdded; + + // Are we in conflict? + context::CDO d_conflict; + + // Invalidate the model cache if check was called + context::CDO d_invalidateModelCache; + + /** The conflict node */ + Node d_conflictNode; + + /** Literals to propagate */ + context::CDList d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO d_literalsToPropagateIndex; + + /** + * Keeps a map from nodes to the subtheory that propagated it so that we can + * explain it properly. + */ + typedef context::CDHashMap PropagatedMap; + PropagatedMap d_propagatedBy; + + std::unique_ptr d_eagerSolver; + std::unique_ptr d_abstractionModule; + bool d_calledPreregister; + + bool wasPropagatedBySubtheory(TNode literal) const + { + return d_propagatedBy.find(literal) != d_propagatedBy.end(); + } + + SubTheory getPropagatingSubtheory(TNode literal) const + { + Assert(wasPropagatedBySubtheory(literal)); + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + return (*find).second; + } + + /** Should be called to propagate the literal. */ + bool storePropagation(TNode literal, SubTheory subtheory); + + /** + * Explains why this literal (propagated by subtheory) is true by adding + * assumptions. + */ + void explain(TNode literal, std::vector& assumptions); + + void notifySharedTerm(TNode t) override; + + bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } + + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + + Node getModelValue(TNode var); + + inline std::string indent() + { + std::string indentStr(d_context->getLevel(), ' '); + return indentStr; + } + + void setConflict(Node conflict = Node::null()); + + bool inConflict() { return d_conflict; } + + void sendConflict(); + + void lemma(TNode node) + { + d_im.lemma(node, InferenceId::BV_LAYERED_LEMMA); + d_lemmasAdded = true; + } + + void checkForLemma(TNode node); + + size_t numAssertions() { return d_bv.numAssertions(); } + + theory::Assertion get() { return d_bv.get(); } + + bool done() { return d_bv.done(); } + + friend class LazyBitblaster; + friend class TLazyBitblaster; + friend class EagerBitblaster; + friend class BitblastSolver; + friend class EqualitySolver; + friend class CoreSolver; + friend class InequalitySolver; + friend class AlgebraicSolver; + friend class EagerBitblastSolver; +}; /* class BVSolverLayered */ + +} // namespace bv +} // namespace theory + +} // namespace cvc5 + +#endif /* CVC5__THEORY__BV__BV_SOLVER_LAZY_H */ diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp deleted file mode 100644 index 5210117b8..000000000 --- a/src/theory/bv/bv_solver_lazy.cpp +++ /dev/null @@ -1,700 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner, Liana Hadarean, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Lazy bit-vector solver. - */ - -#include "theory/bv/bv_solver_lazy.h" - -#include "expr/node_algorithm.h" -#include "options/bv_options.h" -#include "options/smt_options.h" -#include "smt/smt_statistics_registry.h" -#include "theory/bv/abstraction.h" -#include "theory/bv/bv_eager_solver.h" -#include "theory/bv/bv_subtheory_algebraic.h" -#include "theory/bv/bv_subtheory_bitblast.h" -#include "theory/bv/bv_subtheory_core.h" -#include "theory/bv/bv_subtheory_inequality.h" -#include "theory/bv/theory_bv_rewrite_rules_normalization.h" -#include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/bv/theory_bv_rewriter.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/theory_model.h" - -using namespace cvc5::theory::bv::utils; - -namespace cvc5 { -namespace theory { -namespace bv { - -BVSolverLazy::BVSolverLazy(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), - d_alreadyPropagatedSet(c), - d_sharedTermsSet(c), - d_subtheories(), - d_subtheoryMap(), - d_statistics(), - d_staticLearnCache(), - 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_calledPreregister(false) -{ - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - d_eagerSolver.reset(new EagerBitblastSolver(c, this)); - return; - } - - if (options::bitvectorEqualitySolver()) - { - d_subtheories.emplace_back(new CoreSolver(c, this)); - d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); - } - - if (options::bitvectorInequalitySolver()) - { - d_subtheories.emplace_back(new InequalitySolver(c, u, this)); - d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); - } - - if (options::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()) - { - bb_solver->setAbstraction(d_abstractionModule.get()); - } - d_subtheories.emplace_back(bb_solver); - d_subtheoryMap[SUB_BITBLAST] = bb_solver; -} - -BVSolverLazy::~BVSolverLazy() {} - -bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi) -{ - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - return core->needsEqualityEngine(esi); - } - // otherwise we don't use an equality engine - return false; -} - -void BVSolverLazy::finishInit() -{ - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - // must finish initialization in the core solver - core->finishInit(); - } -} - -void BVSolverLazy::spendResource(Resource r) -{ - d_im.spendResource(r); -} - -BVSolverLazy::Statistics::Statistics() - : d_avgConflictSize(smtStatisticsRegistry().registerAverage( - "theory::bv::lazy::AvgBVConflictSize")), - d_solveTimer(smtStatisticsRegistry().registerTimer( - "theory::bv::lazy::solveTimer")), - d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt( - "theory::bv::lazy::NumFullCheckCalls")), - d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt( - "theory::bv::lazy::NumStandardCheckCalls")), - d_weightComputationTimer(smtStatisticsRegistry().registerTimer( - "theory::bv::lazy::weightComputationTimer")), - d_numMultSlice(smtStatisticsRegistry().registerInt( - "theory::bv::lazy::NumMultSliceApplied")) -{ -} - -void BVSolverLazy::preRegisterTerm(TNode node) -{ - d_calledPreregister = true; - Debug("bitvector-preregister") - << "BVSolverLazy::preRegister(" << node << ")" << std::endl; - - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - // the aig bit-blaster option is set heuristically - // if bv abstraction is used - if (!d_eagerSolver->isInitialized()) - { - d_eagerSolver->initialize(); - } - - if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) - { - Node formula = node[0]; - d_eagerSolver->assertFormula(formula); - } - return; - } - - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - d_subtheories[i]->preRegister(node); - } - - // AJR : equality solver currently registers all terms to ExtTheory, if we - // want a lazy reduction without the bv equality solver, need to call this - // d_bv.d_extTheory->registerTermRec( node ); -} - -void BVSolverLazy::sendConflict() -{ - Assert(d_conflict); - if (d_conflictNode.isNull()) - { - return; - } - else - { - Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict " - << d_conflictNode << std::endl; - d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT); - d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren(); - d_conflictNode = Node::null(); - } -} - -void BVSolverLazy::checkForLemma(TNode fact) -{ - if (fact.getKind() == kind::EQUAL) - { - NodeManager* nm = NodeManager::currentNM(); - if (fact[0].getKind() == kind::BITVECTOR_UREM) - { - TNode urem = fact[0]; - TNode result = fact[1]; - TNode divisor = urem[1]; - Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); - Node divisor_eq_0 = - nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); - Node split = nm->mkNode( - kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); - lemma(split); - } - if (fact[1].getKind() == kind::BITVECTOR_UREM) - { - TNode urem = fact[1]; - TNode result = fact[0]; - TNode divisor = urem[1]; - Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); - Node divisor_eq_0 = - nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); - Node split = nm->mkNode( - kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); - lemma(split); - } - } -} - -bool BVSolverLazy::preCheck(Theory::Effort e) -{ - check(e); - return true; -} - -void BVSolverLazy::check(Theory::Effort e) -{ - if (done() && e < Theory::EFFORT_FULL) - { - return; - } - - Debug("bitvector") << "BVSolverLazy::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); - // if we are using the eager solver - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - // this can only happen on an empty benchmark - if (!d_eagerSolver->isInitialized()) - { - d_eagerSolver->initialize(); - } - if (!Theory::fullEffort(e)) return; - - std::vector assertions; - while (!done()) - { - TNode fact = get().d_assertion; - Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); - assertions.push_back(fact); - d_eagerSolver->assertFormula(fact[0]); - } - - bool ok = d_eagerSolver->checkSat(); - if (!ok) - { - if (assertions.size() == 1) - { - d_im.conflict(assertions[0], InferenceId::BV_LAZY_CONFLICT); - return; - } - Node conflict = utils::mkAnd(assertions); - d_im.conflict(conflict, InferenceId::BV_LAZY_CONFLICT); - return; - } - return; - } - - if (Theory::fullEffort(e)) - { - ++(d_statistics.d_numCallsToCheckFullEffort); - } - else - { - ++(d_statistics.d_numCallsToCheckStandardEffort); - } - // if we are already in conflict just return the conflict - if (inConflict()) - { - sendConflict(); - return; - } - - while (!done()) - { - TNode fact = get().d_assertion; - - checkForLemma(fact); - - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - d_subtheories[i]->assertFact(fact); - } - } - - bool ok = true; - bool complete = false; - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - Assert(!inConflict()); - ok = d_subtheories[i]->check(e); - complete = d_subtheories[i]->isComplete(); - - if (!ok) - { - // if we are in a conflict no need to check with other theories - Assert(inConflict()); - sendConflict(); - return; - } - if (complete) - { - // if the last subtheory was complete we stop - break; - } - } -} - -bool BVSolverLazy::collectModelValues(TheoryModel* m, - const std::set& termSet) -{ - Assert(!inConflict()); - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - if (!d_eagerSolver->collectModelInfo(m, true)) - { - return false; - } - } - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - if (d_subtheories[i]->isComplete()) - { - return d_subtheories[i]->collectModelValues(m, termSet); - } - } - return true; -} - -Node BVSolverLazy::getModelValue(TNode var) -{ - Assert(!inConflict()); - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - if (d_subtheories[i]->isComplete()) - { - return d_subtheories[i]->getModelValue(var); - } - } - Unreachable(); -} - -void BVSolverLazy::propagate(Theory::Effort e) -{ - Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl; - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - return; - } - - if (inConflict()) - { - return; - } - - // go through stored propagations - bool ok = true; - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; - d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) - { - TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - // temporary fix for incremental bit-blasting - if (d_state.isSatLiteral(literal)) - { - Debug("bitvector::propagate") - << "BVSolverLazy:: propagating " << literal << "\n"; - ok = d_im.propagateLit(literal); - } - } - - if (!ok) - { - Debug("bitvector::propagate") - << indent() << "BVSolverLazy::propagate(): conflict from theory engine" - << std::endl; - setConflict(); - } -} - -TrustNode BVSolverLazy::ppRewrite(TNode t) -{ - Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n"; - Node res = t; - if (options::bitwiseEq() && RewriteRule::applies(t)) - { - Node result = RewriteRule::run(t); - res = Rewriter::rewrite(result); - } - else if (RewriteRule::applies(t)) - { - Node result = RewriteRule::run(t); - res = Rewriter::rewrite(result); - } - else if (res.getKind() == kind::EQUAL - && ((res[0].getKind() == kind::BITVECTOR_ADD - && RewriteRule::applies(res[1])) - || (res[1].getKind() == kind::BITVECTOR_ADD - && RewriteRule::applies(res[0])))) - { - Node mult = RewriteRule::applies(res[0]) - ? RewriteRule::run(res[0]) - : RewriteRule::run(res[1]); - Node factor = mult[0]; - Node sum = RewriteRule::applies(res[0]) ? res[1] : res[0]; - Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); - Node rewr_eq = RewriteRule::run(new_eq); - if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) - { - res = Rewriter::rewrite(rewr_eq); - } - else - { - res = t; - } - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - - // if(t.getKind() == kind::EQUAL && - // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == - // kind::BITVECTOR_ADD) || - // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == - // kind::BITVECTOR_ADD))) { - // // if we have an equality between a multiplication and addition - // // try to express multiplication in terms of addition - // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; - // Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1]; - // if (RewriteRule::applies(mult)) { - // Node new_mult = RewriteRule::run(mult); - // Node new_eq = - // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, - // new_mult, add)); - - // // the simplification can cause the formula to blow up - // // only apply if formula reduced - // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { - // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; - // uint64_t old_size = bv->computeAtomWeight(t); - // Assert (old_size); - // uint64_t new_size = bv->computeAtomWeight(new_eq); - // double ratio = ((double)new_size)/old_size; - // if (ratio <= 0.4) { - // ++(d_statistics.d_numMultSlice); - // return new_eq; - // } - // } - - // if (new_eq.getKind() == kind::CONST_BOOLEAN) { - // ++(d_statistics.d_numMultSlice); - // return new_eq; - // } - // } - // } - - if (options::bvAbstraction() && t.getType().isBoolean()) - { - d_abstractionModule->addInputAtom(res); - } - Debug("bv-pp-rewrite") << "to " << res << "\n"; - if (res != t) - { - return TrustNode::mkTrustRewrite(t, res, nullptr); - } - return TrustNode::null(); -} - -void BVSolverLazy::presolve() -{ - Debug("bitvector") << "BVSolverLazy::presolve" << std::endl; -} - -static int prop_count = 0; - -bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory) -{ - Debug("bitvector::propagate") << indent() << d_context->getLevel() << " " - << "BVSolverLazy::storePropagation(" << literal - << ", " << subtheory << ")" << std::endl; - prop_count++; - - // If already in conflict, no more propagation - if (d_conflict) - { - Debug("bitvector::propagate") - << indent() << "BVSolverLazy::storePropagation(" << literal << ", " - << subtheory << "): already in conflict" << std::endl; - return false; - } - - // If propagated already, just skip - PropagatedMap::const_iterator find = d_propagatedBy.find(literal); - if (find != d_propagatedBy.end()) - { - return true; - } - else - { - bool polarity = literal.getKind() != kind::NOT; - Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0]; - find = d_propagatedBy.find(negatedLiteral); - if (find != d_propagatedBy.end() && (*find).second != subtheory) - { - // Safe to ignore this one, subtheory should produce a conflict - return true; - } - - d_propagatedBy[literal] = subtheory; - } - - // Propagate differs depending on the subtheory - // * bitblaster needs to be left alone until it's done, otherwise it doesn't - // know how to explain - // * equality engine can propagate eagerly - // TODO(2348): Determine if ok should be set by propagate. If not, remove ok. - constexpr bool ok = true; - if (subtheory == SUB_CORE) - { - d_im.propagateLit(literal); - if (!ok) - { - setConflict(); - } - } - else - { - d_literalsToPropagate.push_back(literal); - } - return ok; - -} /* BVSolverLazy::propagate(TNode) */ - -void BVSolverLazy::explain(TNode literal, std::vector& assumptions) -{ - Assert(wasPropagatedBySubtheory(literal)); - SubTheory sub = getPropagatingSubtheory(literal); - d_subtheoryMap[sub]->explain(literal, assumptions); -} - -TrustNode BVSolverLazy::explain(TNode node) -{ - Debug("bitvector::explain") - << "BVSolverLazy::explain(" << node << ")" << std::endl; - std::vector assumptions; - - // Ask for the explanation - explain(node, assumptions); - // this means that it is something true at level 0 - Node explanation; - if (assumptions.size() == 0) - { - explanation = utils::mkTrue(); - } - else - { - // return the explanation - explanation = utils::mkAnd(assumptions); - } - Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => " - << explanation << std::endl; - Debug("bitvector::explain") << "BVSolverLazy::explain done. \n"; - return TrustNode::mkTrustPropExp(node, explanation, nullptr); -} - -void BVSolverLazy::notifySharedTerm(TNode t) -{ - Debug("bitvector::sharing") - << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl; - d_sharedTermsSet.insert(t); -} - -EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) -{ - if (options::bitblastMode() == options::BitblastMode::EAGER) - return EQUALITY_UNKNOWN; - Assert(options::bitblastMode() == options::BitblastMode::LAZY); - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); - if (status != EQUALITY_UNKNOWN) - { - return status; - } - } - return EQUALITY_UNKNOWN; - ; -} - -void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned) -{ - if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) - { - return; - } - d_staticLearnCache.insert(in); - - if (in.getKind() == kind::EQUAL) - { - if ((in[0].getKind() == kind::BITVECTOR_ADD - && in[1].getKind() == kind::BITVECTOR_SHL) - || (in[1].getKind() == kind::BITVECTOR_ADD - && in[0].getKind() == kind::BITVECTOR_SHL)) - { - TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1]; - TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0]; - - if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL - && p[1].getKind() == kind::BITVECTOR_SHL) - { - unsigned size = utils::getSize(s); - Node one = utils::mkConst(size, 1u); - if (s[0] == one && p[0][0] == one && p[1][0] == one) - { - Node zero = utils::mkConst(size, 0u); - TNode b = p[0]; - TNode c = p[1]; - // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) - Node b_eq_0 = b.eqNode(zero); - Node c_eq_0 = c.eqNode(zero); - Node b_eq_c = b.eqNode(c); - - Node dis = NodeManager::currentNM()->mkNode( - kind::OR, b_eq_0, c_eq_0, b_eq_c); - Node imp = in.impNode(dis); - learned << imp; - } - } - } - } - else if (in.getKind() == kind::AND) - { - for (size_t i = 0, N = in.getNumChildren(); i < N; ++i) - { - ppStaticLearn(in[i], learned); - } - } -} - -bool BVSolverLazy::applyAbstraction(const std::vector& assertions, - std::vector& new_assertions) -{ - bool changed = - d_abstractionModule->applyAbstraction(assertions, new_assertions); - if (changed && options::bitblastMode() == options::BitblastMode::EAGER - && options::bitvectorAig()) - { - // disable AIG mode - AlwaysAssert(!d_eagerSolver->isInitialized()); - d_eagerSolver->turnOffAig(); - d_eagerSolver->initialize(); - } - return changed; -} - -void BVSolverLazy::setConflict(Node conflict) -{ - if (options::bvAbstraction()) - { - NodeManager* const nm = NodeManager::currentNM(); - Node new_conflict = d_abstractionModule->simplifyConflict(conflict); - - std::vector lemmas; - lemmas.push_back(new_conflict); - d_abstractionModule->generalizeConflict(new_conflict, lemmas); - for (unsigned i = 0; i < lemmas.size(); ++i) - { - lemma(nm->mkNode(kind::NOT, lemmas[i])); - } - } - d_conflict = true; - d_conflictNode = conflict; -} - -} // namespace bv -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h deleted file mode 100644 index 4f73354bc..000000000 --- a/src/theory/bv/bv_solver_lazy.h +++ /dev/null @@ -1,228 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner, Liana Hadarean, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Lazy bit-vector solver. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H -#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H - -#include -#include - -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/context.h" -#include "theory/bv/bv_solver.h" -#include "theory/bv/bv_subtheory.h" -#include "theory/bv/theory_bv.h" -#include "util/hash.h" - -namespace cvc5 { -namespace theory { -namespace bv { - -class CoreSolver; -class InequalitySolver; -class AlgebraicSolver; -class BitblastSolver; -class EagerBitblastSolver; -class AbstractionModule; - -class BVSolverLazy : public BVSolver -{ - /** Back reference to TheoryBV */ - TheoryBV& d_bv; - - /** The context we are using */ - context::Context* d_context; - - /** Context dependent set of atoms we already propagated */ - context::CDHashSet d_alreadyPropagatedSet; - context::CDHashSet d_sharedTermsSet; - - std::vector> d_subtheories; - std::unordered_map> - d_subtheoryMap; - - public: - BVSolverLazy(TheoryBV& bv, - context::Context* c, - context::UserContext* u, - ProofNodeManager* pnm = nullptr, - std::string name = ""); - - ~BVSolverLazy(); - - //--------------------------------- initialization - - /** - * Returns true if we need an equality engine. If so, we initialize the - * information regarding how it should be setup. For details, see the - * documentation in Theory::needsEqualityEngine. - */ - bool needsEqualityEngine(EeSetupInfo& esi) override; - - /** finish initialization */ - void finishInit() override; - //--------------------------------- end initialization - - void preRegisterTerm(TNode n) override; - - bool preCheck(Theory::Effort e) override; - - void propagate(Theory::Effort e) override; - - TrustNode explain(TNode n) override; - - bool collectModelValues(TheoryModel* m, - const std::set& termSet) override; - - std::string identify() const override { return std::string("BVSolverLazy"); } - - TrustNode ppRewrite(TNode t) override; - - void ppStaticLearn(TNode in, NodeBuilder& learned) override; - - void presolve() override; - - bool applyAbstraction(const std::vector& assertions, - std::vector& new_assertions) override; - - bool isLeaf(TNode node) { return d_bv.isLeaf(node); } - - private: - class Statistics - { - public: - AverageStat d_avgConflictSize; - TimerStat d_solveTimer; - IntStat d_numCallsToCheckFullEffort; - IntStat d_numCallsToCheckStandardEffort; - TimerStat d_weightComputationTimer; - IntStat d_numMultSlice; - Statistics(); - }; - - Statistics d_statistics; - - void check(Theory::Effort e); - void spendResource(Resource r); - - typedef std::unordered_set TNodeSet; - typedef std::unordered_set NodeSet; - NodeSet d_staticLearnCache; - - typedef std::unordered_map NodeToNode; - - context::CDO d_lemmasAdded; - - // Are we in conflict? - context::CDO d_conflict; - - // Invalidate the model cache if check was called - context::CDO d_invalidateModelCache; - - /** The conflict node */ - Node d_conflictNode; - - /** Literals to propagate */ - context::CDList d_literalsToPropagate; - - /** Index of the next literal to propagate */ - context::CDO d_literalsToPropagateIndex; - - /** - * Keeps a map from nodes to the subtheory that propagated it so that we can - * explain it properly. - */ - typedef context::CDHashMap PropagatedMap; - PropagatedMap d_propagatedBy; - - std::unique_ptr d_eagerSolver; - std::unique_ptr d_abstractionModule; - bool d_calledPreregister; - - bool wasPropagatedBySubtheory(TNode literal) const - { - return d_propagatedBy.find(literal) != d_propagatedBy.end(); - } - - SubTheory getPropagatingSubtheory(TNode literal) const - { - Assert(wasPropagatedBySubtheory(literal)); - PropagatedMap::const_iterator find = d_propagatedBy.find(literal); - return (*find).second; - } - - /** Should be called to propagate the literal. */ - bool storePropagation(TNode literal, SubTheory subtheory); - - /** - * Explains why this literal (propagated by subtheory) is true by adding - * assumptions. - */ - void explain(TNode literal, std::vector& assumptions); - - void notifySharedTerm(TNode t) override; - - bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - - EqualityStatus getEqualityStatus(TNode a, TNode b) override; - - Node getModelValue(TNode var); - - inline std::string indent() - { - std::string indentStr(d_context->getLevel(), ' '); - return indentStr; - } - - void setConflict(Node conflict = Node::null()); - - bool inConflict() { return d_conflict; } - - void sendConflict(); - - void lemma(TNode node) - { - d_im.lemma(node, InferenceId::BV_LAZY_LEMMA); - d_lemmasAdded = true; - } - - void checkForLemma(TNode node); - - size_t numAssertions() { return d_bv.numAssertions(); } - - theory::Assertion get() { return d_bv.get(); } - - bool done() { return d_bv.done(); } - - friend class LazyBitblaster; - friend class TLazyBitblaster; - friend class EagerBitblaster; - friend class BitblastSolver; - friend class EqualitySolver; - friend class CoreSolver; - friend class InequalitySolver; - friend class AlgebraicSolver; - friend class EagerBitblastSolver; -}; /* class BVSolverLazy */ - -} // namespace bv -} // namespace theory - -} // namespace cvc5 - -#endif /* CVC5__THEORY__BV__BV_SOLVER_LAZY_H */ 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()));