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
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"
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"
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"
[[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"
#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"
namespace theory {
namespace bv {
-EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
+EagerBitblaster::EagerBitblaster(BVSolverLayered* theory_bv,
+ context::Context* c)
: TBitblaster<Node>(),
d_context(c),
d_satSolver(),
namespace bv {
class BitblastingRegistrar;
-class BVSolverLazy;
+class BVSolverLayered;
class EagerBitblaster : public TBitblaster<Node>
{
public:
- EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context);
+ EagerBitblaster(BVSolverLayered* theory_bv, context::Context* context);
~EagerBitblaster();
void addAtom(TNode atom);
std::unique_ptr<prop::SatSolver> d_satSolver;
std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
- BVSolverLazy* d_bv;
+ BVSolverLayered* d_bv;
TNodeSet d_bbAtoms;
TNodeSet d_variables;
* directory for licensing information.
* ****************************************************************************
*
- * Bitblaster for the lazy bv solver.
+ * Bitblaster for the layered BV solver.
*/
#include "theory/bv/bitblast/lazy_bitblaster.h"
#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"
}
TLazyBitblaster::TLazyBitblaster(context::Context* c,
- bv::BVSolverLazy* bv,
+ bv::BVSolverLayered* bv,
const std::string name,
bool emptyNotify)
: TBitblaster<Node>(),
}
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);
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);
}
}
namespace theory {
namespace bv {
-class BVSolverLazy;
+class BVSolverLayered;
class TLazyBitblaster : public TBitblaster<Node>
{
bool hasBBAtom(TNode atom) const override;
TLazyBitblaster(context::Context* c,
- BVSolverLazy* bv,
+ BVSolverLayered* bv,
const std::string name = "",
bool emptyNotify = false);
~TLazyBitblaster();
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)
{
}
void safePoint(Resource r) override;
};
- BVSolverLazy* d_bv;
+ BVSolverLayered* d_bv;
context::Context* d_ctx;
std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
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),
#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 {
*/
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);
std::unique_ptr<AigBitblaster> d_aigBitblaster;
bool d_useAig;
- BVSolverLazy* d_bv;
+ BVSolverLayered* d_bv;
}; // class EagerBitblastSolver
} // namespace bv
#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;
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(),
namespace bv {
class TLazyBitblaster;
-class BVSolverLazy;
+class BVSolverLayered;
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; }
--- /dev/null
+/******************************************************************************
+ * 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<TNode> 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<Node>& 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<BitwiseEq>::applies(t))
+ {
+ Node result = RewriteRule<BitwiseEq>::run<false>(t);
+ res = Rewriter::rewrite(result);
+ }
+ else if (RewriteRule<UltAddOne>::applies(t))
+ {
+ Node result = RewriteRule<UltAddOne>::run<false>(t);
+ res = Rewriter::rewrite(result);
+ }
+ else if (res.getKind() == kind::EQUAL
+ && ((res[0].getKind() == kind::BITVECTOR_ADD
+ && RewriteRule<ConcatToMult>::applies(res[1]))
+ || (res[1].getKind() == kind::BITVECTOR_ADD
+ && RewriteRule<ConcatToMult>::applies(res[0]))))
+ {
+ Node mult = RewriteRule<ConcatToMult>::applies(res[0])
+ ? RewriteRule<ConcatToMult>::run<false>(res[0])
+ : RewriteRule<ConcatToMult>::run<true>(res[1]);
+ Node factor = mult[0];
+ Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
+ Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
+ Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
+ if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
+ {
+ res = Rewriter::rewrite(rewr_eq);
+ }
+ else
+ {
+ res = t;
+ }
+ }
+ else if (RewriteRule<SignExtendEqConst>::applies(t))
+ {
+ res = RewriteRule<SignExtendEqConst>::run<false>(t);
+ }
+ else if (RewriteRule<ZeroExtendEqConst>::applies(t))
+ {
+ res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
+ }
+ else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
+ {
+ res = RewriteRule<NormalizeEqAddNeg>::run<false>(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<MultSlice>::applies(mult)) {
+ // Node new_mult = RewriteRule<MultSlice>::run<false>(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<TNode>& 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<TNode> 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<Node>& assertions,
+ std::vector<Node>& 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<Node> 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
--- /dev/null
+/******************************************************************************
+ * 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 <unordered_map>
+#include <unordered_set>
+
+#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<Node> d_alreadyPropagatedSet;
+ context::CDHashSet<Node> d_sharedTermsSet;
+
+ std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
+ std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
+ 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<Node>& 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<Node>& assertions,
+ std::vector<Node>& 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<TNode> TNodeSet;
+ typedef std::unordered_set<Node> NodeSet;
+ NodeSet d_staticLearnCache;
+
+ typedef std::unordered_map<Node, Node> NodeToNode;
+
+ context::CDO<bool> d_lemmasAdded;
+
+ // Are we in conflict?
+ context::CDO<bool> d_conflict;
+
+ // Invalidate the model cache if check was called
+ context::CDO<bool> d_invalidateModelCache;
+
+ /** The conflict node */
+ Node d_conflictNode;
+
+ /** Literals to propagate */
+ context::CDList<Node> d_literalsToPropagate;
+
+ /** Index of the next literal to propagate */
+ context::CDO<unsigned> d_literalsToPropagateIndex;
+
+ /**
+ * Keeps a map from nodes to the subtheory that propagated it so that we can
+ * explain it properly.
+ */
+ typedef context::CDHashMap<Node, SubTheory> PropagatedMap;
+ PropagatedMap d_propagatedBy;
+
+ std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
+ std::unique_ptr<AbstractionModule> 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<TNode>& 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 */
+++ /dev/null
-/******************************************************************************
- * 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<TNode> 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<Node>& 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<BitwiseEq>::applies(t))
- {
- Node result = RewriteRule<BitwiseEq>::run<false>(t);
- res = Rewriter::rewrite(result);
- }
- else if (RewriteRule<UltAddOne>::applies(t))
- {
- Node result = RewriteRule<UltAddOne>::run<false>(t);
- res = Rewriter::rewrite(result);
- }
- else if (res.getKind() == kind::EQUAL
- && ((res[0].getKind() == kind::BITVECTOR_ADD
- && RewriteRule<ConcatToMult>::applies(res[1]))
- || (res[1].getKind() == kind::BITVECTOR_ADD
- && RewriteRule<ConcatToMult>::applies(res[0]))))
- {
- Node mult = RewriteRule<ConcatToMult>::applies(res[0])
- ? RewriteRule<ConcatToMult>::run<false>(res[0])
- : RewriteRule<ConcatToMult>::run<true>(res[1]);
- Node factor = mult[0];
- Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
- Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
- Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
- if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
- {
- res = Rewriter::rewrite(rewr_eq);
- }
- else
- {
- res = t;
- }
- }
- else if (RewriteRule<SignExtendEqConst>::applies(t))
- {
- res = RewriteRule<SignExtendEqConst>::run<false>(t);
- }
- else if (RewriteRule<ZeroExtendEqConst>::applies(t))
- {
- res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
- }
- else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
- {
- res = RewriteRule<NormalizeEqAddNeg>::run<false>(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<MultSlice>::applies(mult)) {
- // Node new_mult = RewriteRule<MultSlice>::run<false>(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<TNode>& 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<TNode> 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<Node>& assertions,
- std::vector<Node>& 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<Node> 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
+++ /dev/null
-/******************************************************************************
- * 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 <unordered_map>
-#include <unordered_set>
-
-#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<Node> d_alreadyPropagatedSet;
- context::CDHashSet<Node> d_sharedTermsSet;
-
- std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
- std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
- 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<Node>& 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<Node>& assertions,
- std::vector<Node>& 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<TNode> TNodeSet;
- typedef std::unordered_set<Node> NodeSet;
- NodeSet d_staticLearnCache;
-
- typedef std::unordered_map<Node, Node> NodeToNode;
-
- context::CDO<bool> d_lemmasAdded;
-
- // Are we in conflict?
- context::CDO<bool> d_conflict;
-
- // Invalidate the model cache if check was called
- context::CDO<bool> d_invalidateModelCache;
-
- /** The conflict node */
- Node d_conflictNode;
-
- /** Literals to propagate */
- context::CDList<Node> d_literalsToPropagate;
-
- /** Index of the next literal to propagate */
- context::CDO<unsigned> d_literalsToPropagateIndex;
-
- /**
- * Keeps a map from nodes to the subtheory that propagated it so that we can
- * explain it properly.
- */
- typedef context::CDHashMap<Node, SubTheory> PropagatedMap;
- PropagatedMap d_propagatedBy;
-
- std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
- std::unique_ptr<AbstractionModule> 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<TNode>& 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 */
}
// forward declaration
-class BVSolverLazy;
+class BVSolverLayered;
using AssertionQueue = context::CDQueue<Node>;
*/
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)
{
}
context::Context* d_context;
/** The bit-vector theory */
- BVSolverLazy* d_bv;
+ BVSolverLayered* d_bv;
AssertionQueue d_assertionQueue;
context::CDO<uint32_t> d_assertionIndex;
}; /* class SubtheorySolver */
#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"
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)),
bool quickCheck(std::vector<Node>& facts);
public:
- AlgebraicSolver(context::Context* c, BVSolverLazy* bv);
+ AlgebraicSolver(context::Context* c, BVSolverLayered* bv);
~AlgebraicSolver();
void preRegister(TNode node) override {}
#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;
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),
void setConflict(TNode conflict);
public:
- BitblastSolver(context::Context* c, BVSolverLazy* bv);
+ BitblastSolver(context::Context* c, BVSolverLayered* bv);
~BitblastSolver();
void preRegister(TNode node) override;
#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"
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),
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;
Statistics d_statistics;
public:
- CoreSolver(context::Context* c, BVSolverLazy* bv);
+ CoreSolver(context::Context* c, BVSolverLayered* bv);
~CoreSolver();
bool needsEqualityEngine(EeSetupInfo& esi);
void finishInit();
#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"
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),
#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"
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:
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,
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";
// ---------------------------------- 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
#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"
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
d_smtEngine->finishInit();
TheoryBV* tbv = dynamic_cast<TheoryBV*>(
d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]);
- BVSolverLazy* bvsl = dynamic_cast<BVSolverLazy*>(tbv->d_internal.get());
+ BVSolverLayered* bvsl = dynamic_cast<BVSolverLayered*>(tbv->d_internal.get());
std::unique_ptr<EagerBitblaster> bb(
new EagerBitblaster(bvsl, d_smtEngine->getContext()));
projects / cvc5.git / commitdiff