This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
theory/bv/bv_quick_check.cpp
theory/bv/bv_quick_check.h
theory/bv/bv_solver.h
+ theory/bv/bv_solver_bitblast.cpp
+ theory/bv/bv_solver_bitblast.h
theory/bv/bv_solver_lazy.cpp
theory/bv/bv_solver_lazy.h
theory/bv/bv_solver_simple.cpp
default = "LAZY"
help = "choose bit-vector solver, see --bv-solver=help"
help_mode = "Bit-vector solvers."
+[[option.mode.BITBLAST]]
+ name = "bitblast"
+ help = "Enables bitblasting solver."
[[option.mode.LAZY]]
name = "lazy"
help = "Enables the lazy BV solver infrastructure."
throw OptionException(ss.str());
}
- if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
- || m == SatSolverMode::KISSAT)
+ if (options::bvSolver() != options::BVSolver::BITBLAST
+ && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
+ || m == SatSolverMode::KISSAT))
{
if (options::bitblastMode() == options::BitblastMode::LAZY
&& options::bitblastMode.wasSetByUser())
SatValue CadicalSolver::solve()
{
+ d_assumptions.clear();
TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
SatValue res = toSatValue(d_solver->solve());
d_okay = (res == SAT_VALUE_TRUE);
SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
{
+ d_assumptions.clear();
TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
for (const SatLiteral& lit : assumptions)
{
d_solver->assume(toCadicalLit(lit));
+ d_assumptions.push_back(lit);
}
SatValue res = toSatValue(d_solver->solve());
d_okay = (res == SAT_VALUE_TRUE);
return res;
}
+void CadicalSolver::getUnsatAssumptions(std::vector<SatLiteral>& assumptions)
+{
+ for (const SatLiteral& lit : d_assumptions)
+ {
+ if (d_solver->failed(toCadicalLit(lit)))
+ {
+ assumptions.push_back(lit);
+ }
+ }
+}
+
void CadicalSolver::interrupt() { d_solver->terminate(); }
SatValue CadicalSolver::value(SatLiteral l)
SatValue solve() override;
SatValue solve(long unsigned int&) override;
SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+ void getUnsatAssumptions(std::vector<SatLiteral>& assumptions) override;
void interrupt() override;
void init();
std::unique_ptr<CaDiCaL::Solver> d_solver;
+ /**
+ * Stores the current set of assumptions provided via solve() and is used to
+ * query the solver if a given assumption is false.
+ */
+ std::vector<SatLiteral> d_assumptions;
unsigned d_nextVarIdx;
bool d_okay;
return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
}
+SatLiteral toSatLiteral(CMSat::Lit lit)
+{
+ if (lit == CMSat::lit_Undef)
+ {
+ return undefSatLiteral;
+ }
+ return SatLiteral(lit.var(), lit.sign());
+}
+
SatValue toSatLiteralValue(CMSat::lbool res)
{
if (res == CMSat::l_True) return SAT_VALUE_TRUE;
return toSatLiteralValue(d_solver->solve(&assumpts));
}
+void CryptoMinisatSolver::getUnsatAssumptions(
+ std::vector<SatLiteral>& assumptions)
+{
+ for (const CMSat::Lit& lit : d_solver->get_conflict())
+ {
+ assumptions.push_back(toSatLiteral(~lit));
+ }
+}
+
SatValue CryptoMinisatSolver::value(SatLiteral l){
const std::vector<CMSat::lbool> model = d_solver->get_model();
CMSatVar var = l.getSatVariable();
SatValue solve() override;
SatValue solve(long unsigned int&) override;
SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+ void getUnsatAssumptions(std::vector<SatLiteral>& assumptions) override;
bool ok() const override;
SatValue value(SatLiteral l) override;
/** Check if the solver is in an inconsistent state */
virtual bool ok() const = 0;
+ /**
+ * Get list of unsatisfiable assumptions.
+ *
+ * The returned assumptions are a subset of the assumptions provided to
+ * the solve method.
+ * Can only be called if satisfiability check under assumptions was used and
+ * if it returned SAT_VALUE_FALSE.
+ */
+ virtual void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions)
+ {
+ Unimplemented() << "getUnsatAssumptions not implemented";
+ }
+
};/* class SatSolver */
"Incremental eager bit-blasting is currently "
"only supported for QF_BV. Try --bitblast=lazy.");
}
+
+ // Force lazy solver since we don't handle EAGER_ATOMS in the
+ // BVSolver::BITBLAST solver.
+ options::bvSolver.set(options::BVSolver::LAZY);
}
- /* BVSolver::SIMPLE does not natively support int2bv and nat2bv, they need to
- * to be eliminated eagerly. */
- if (options::bvSolver() == options::BVSolver::SIMPLE)
+ /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers
+ * we need to eagerly eliminate the operators. */
+ if (options::bvSolver() == options::BVSolver::SIMPLE
+ || options::bvSolver() == options::BVSolver::BITBLAST)
{
options::bvLazyReduceExtf.set(false);
options::bvLazyRewriteExtf.set(false);
unsigned size = utils::getSize(node);
unsigned log2_size = std::ceil(log2((double)size));
Node a_size = utils::mkConst(size, size);
- Node b_ult_a_size_node = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
- // ensure that the inequality is bit-blasted
- bb->bbAtom(b_ult_a_size_node);
- T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+ std::vector<T> a_size_bits;
+ DefaultConstBB(a_size, a_size_bits, bb);
+ T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
+
std::vector<T> prev_res;
res = a;
// we only need to look at the bits bellow log2_a_size
unsigned size = utils::getSize(node);
unsigned log2_size = std::ceil(log2((double)size));
Node a_size = utils::mkConst(size, size);
- Node b_ult_a_size_node = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
- // ensure that the inequality is bit-blasted
- bb->bbAtom(b_ult_a_size_node);
- T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+ std::vector<T> a_size_bits;
+ DefaultConstBB(a_size, a_size_bits, bb);
+ T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
+
res = a;
std::vector<T> prev_res;
unsigned size = utils::getSize(node);
unsigned log2_size = std::ceil(log2((double)size));
Node a_size = utils::mkConst(size, size);
- Node b_ult_a_size_node = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
- // ensure that the inequality is bit-blasted
- bb->bbAtom(b_ult_a_size_node);
- T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+ std::vector<T> a_size_bits;
+ DefaultConstBB(a_size, a_size_bits, bb);
+ T b_ult_a_size = uLessThanBB(b, a_size_bits, false);
res = a;
T sign_bit = a.back();
d_termCache.emplace(node, bits);
}
-bool BBSimple::hasBBAtom(TNode atom) const
+bool BBSimple::hasBBAtom(TNode lit) const
{
- return d_bbAtoms.find(atom) != d_bbAtoms.end();
+ if (lit.getKind() == kind::NOT)
+ {
+ lit = lit[0];
+ }
+ return d_bbAtoms.find(lit) != d_bbAtoms.end();
}
void BBSimple::makeVariable(TNode var, Bits& bits)
return true;
}
+bool BBSimple::isVariable(TNode node)
+{
+ return d_variables.find(node) != d_variables.end();
+}
+
} // namespace bv
} // namespace theory
} // namespace CVC4
prop::SatSolver* getSatSolver() override { Unreachable(); }
+ /** Checks whether node is a variable introduced via `makeVariable`.*/
+ bool isVariable(TNode node);
+
private:
/** Query SAT solver for assignment of node 'a'. */
Node getModelFromSatSolver(TNode a, bool fullModel) override;
--- /dev/null
+/********************* */
+/*! \file bv_solver_bitblast.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bit-blasting solver
+ **
+ ** Bit-blasting solver that supports multiple SAT backends.
+ **/
+
+#include "theory/bv/bv_solver_bitblast.h"
+
+#include "options/bv_options.h"
+#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+BVSolverBitblast::BVSolverBitblast(TheoryState* s,
+ TheoryInferenceManager& inferMgr,
+ ProofNodeManager* pnm)
+ : BVSolver(*s, inferMgr),
+ d_bitblaster(new BBSimple(s)),
+ d_nullRegistrar(new prop::NullRegistrar()),
+ d_nullContext(new context::Context()),
+ d_facts(s->getSatContext()),
+ d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
+ : nullptr)
+{
+ if (pnm != nullptr)
+ {
+ d_bvProofChecker.registerTo(pnm->getChecker());
+ }
+
+ switch (options::bvSatSolver())
+ {
+ case options::SatSolverMode::CRYPTOMINISAT:
+ d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
+ smtStatisticsRegistry(), "BVSolverBitblast"));
+ break;
+ default:
+ d_satSolver.reset(prop::SatSolverFactory::createCadical(
+ smtStatisticsRegistry(), "BVSolverBitblast"));
+ }
+ d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+ d_nullRegistrar.get(),
+ d_nullContext.get(),
+ nullptr,
+ smt::currentResourceManager()));
+}
+
+void BVSolverBitblast::postCheck(Theory::Effort level)
+{
+ if (level != Theory::Effort::EFFORT_FULL)
+ {
+ return;
+ }
+
+ std::vector<prop::SatLiteral> assumptions;
+ std::unordered_map<prop::SatLiteral, TNode, prop::SatLiteralHashFunction>
+ node_map;
+ for (const TNode fact : d_facts)
+ {
+ /* Bitblast fact */
+ d_bitblaster->bbAtom(fact);
+ Node bb_fact = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
+ d_cnfStream->ensureLiteral(bb_fact);
+
+ prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
+ assumptions.push_back(lit);
+ node_map.emplace(lit, fact);
+ }
+
+ prop::SatValue val = d_satSolver->solve(assumptions);
+
+ if (val == prop::SatValue::SAT_VALUE_FALSE)
+ {
+ std::vector<prop::SatLiteral> unsat_assumptions;
+ d_satSolver->getUnsatAssumptions(unsat_assumptions);
+ Assert(unsat_assumptions.size() > 0);
+
+ std::vector<Node> conflict;
+ for (const prop::SatLiteral& lit : unsat_assumptions)
+ {
+ conflict.push_back(node_map[lit]);
+ }
+
+ NodeManager* nm = NodeManager::currentNM();
+ d_inferManager.conflict(nm->mkAnd(conflict));
+ }
+}
+
+bool BVSolverBitblast::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ d_facts.push_back(fact);
+ return false; // Return false to enable equality engine reasoning in Theory.
+}
+
+bool BVSolverBitblast::collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet)
+{
+ for (const auto& term : termSet)
+ {
+ if (!d_bitblaster->isVariable(term))
+ {
+ continue;
+ }
+
+ Node value = getValueFromSatSolver(term);
+ Assert(value.isConst());
+ if (!m->assertEquality(term, value, true))
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+Node BVSolverBitblast::getValueFromSatSolver(TNode node)
+{
+ /* If node was not bit-blasted return zero-initialized bit-vector. */
+ if (!d_bitblaster->hasBBTerm(node))
+ {
+ return utils::mkConst(utils::getSize(node), 0u);
+ }
+
+ std::vector<Node> bits;
+ d_bitblaster->getBBTerm(node, bits);
+ Integer value(0), one(1), zero(0), bit;
+ for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
+ {
+ if (d_cnfStream->hasLiteral(bits[j]))
+ {
+ prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
+ prop::SatValue val = d_satSolver->modelValue(lit);
+ bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
+ }
+ else
+ {
+ bit = zero;
+ }
+ value = value * 2 + bit;
+ }
+ return utils::mkConst(bits.size(), value);
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file bv_solver_bitblast.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bit-blasting solver
+ **
+ ** Bit-blasting solver that supports multiple SAT back ends.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
+#define CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
+
+#include <unordered_map>
+
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/bitblast/simple_bitblaster.h"
+#include "theory/bv/bv_solver.h"
+#include "theory/bv/proof_checker.h"
+#include "theory/eager_proof_generator.h"
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+/**
+ * Bit-blasting solver with support for different SAT back ends.
+ */
+class BVSolverBitblast : public BVSolver
+{
+ public:
+ BVSolverBitblast(TheoryState* state,
+ TheoryInferenceManager& inferMgr,
+ ProofNodeManager* pnm);
+ ~BVSolverBitblast() = default;
+
+ bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
+
+ void preRegisterTerm(TNode n) override {}
+
+ void postCheck(Theory::Effort level) override;
+
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+
+ std::string identify() const override { return "BVSolverBitblast"; };
+
+ Theory::PPAssertStatus ppAssert(
+ TrustNode in, TrustSubstitutionMap& outSubstitutions) override
+ {
+ return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
+ }
+
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
+
+ private:
+ /** Get value of `node` from SAT solver. */
+ Node getValueFromSatSolver(TNode node);
+
+ /** Bit-blaster used to bit-blast atoms/terms. */
+ std::unique_ptr<BBSimple> d_bitblaster;
+
+ /** Used for initializing CnfStream> */
+ std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+ std::unique_ptr<context::Context> d_nullContext;
+
+ /** SAT solver back end (configured via options::bvSatSolver. */
+ std::unique_ptr<prop::SatSolver> d_satSolver;
+ /** CNF stream. */
+ std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+ /** Facts sent to this solver. */
+ context::CDList<Node> d_facts;
+
+ /** Proof generator that manages proofs for lemmas generated by this class. */
+ std::unique_ptr<EagerProofGenerator> d_epg;
+
+ BVProofRuleChecker d_bvProofChecker;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "options/bv_options.h"
#include "options/smt_options.h"
+#include "theory/bv/bv_solver_bitblast.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/bv_solver_simple.h"
#include "theory/bv/theory_bv_utils.h"
{
switch (options::bvSolver())
{
+ case options::BVSolver::BITBLAST:
+ d_internal.reset(new BVSolverBitblast(&d_state, d_inferMgr, pnm));
+ break;
+
case options::BVSolver::LAZY:
d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
break;
getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
d_internal->finishInit();
+
+ eq::EqualityEngine* ee = getEqualityEngine();
+ if (ee)
+ {
+ // The kinds we are treating as function application in congruence
+ ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
+ // ee->addFunctionKind(kind::BITVECTOR_AND);
+ // ee->addFunctionKind(kind::BITVECTOR_OR);
+ // ee->addFunctionKind(kind::BITVECTOR_XOR);
+ // ee->addFunctionKind(kind::BITVECTOR_NOT);
+ // ee->addFunctionKind(kind::BITVECTOR_NAND);
+ // ee->addFunctionKind(kind::BITVECTOR_NOR);
+ // ee->addFunctionKind(kind::BITVECTOR_XNOR);
+ // ee->addFunctionKind(kind::BITVECTOR_COMP);
+ ee->addFunctionKind(kind::BITVECTOR_MULT, true);
+ ee->addFunctionKind(kind::BITVECTOR_PLUS, true);
+ ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+ // ee->addFunctionKind(kind::BITVECTOR_SUB);
+ // ee->addFunctionKind(kind::BITVECTOR_NEG);
+ // ee->addFunctionKind(kind::BITVECTOR_UDIV);
+ // ee->addFunctionKind(kind::BITVECTOR_UREM);
+ // ee->addFunctionKind(kind::BITVECTOR_SDIV);
+ // ee->addFunctionKind(kind::BITVECTOR_SREM);
+ // ee->addFunctionKind(kind::BITVECTOR_SMOD);
+ // ee->addFunctionKind(kind::BITVECTOR_SHL);
+ // ee->addFunctionKind(kind::BITVECTOR_LSHR);
+ // ee->addFunctionKind(kind::BITVECTOR_ASHR);
+ // ee->addFunctionKind(kind::BITVECTOR_ULT);
+ // ee->addFunctionKind(kind::BITVECTOR_ULE);
+ // ee->addFunctionKind(kind::BITVECTOR_UGT);
+ // ee->addFunctionKind(kind::BITVECTOR_UGE);
+ // ee->addFunctionKind(kind::BITVECTOR_SLT);
+ // ee->addFunctionKind(kind::BITVECTOR_SLE);
+ // ee->addFunctionKind(kind::BITVECTOR_SGT);
+ // ee->addFunctionKind(kind::BITVECTOR_SGE);
+ ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
+ ee->addFunctionKind(kind::INT_TO_BITVECTOR);
+ }
}
Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
void TheoryBV::presolve() { d_internal->presolve(); }
+EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+{
+ return d_internal->getEqualityStatus(a, b);
+}
+
TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
void TheoryBV::notifySharedTerm(TNode t)
void presolve() override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+
/** Called by abstraction preprocessing pass. */
bool applyAbstraction(const std::vector<Node>& assertions,
std::vector<Node>& new_assertions);
projects / cvc5.git / commitdiff