This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.
theory/bv/bv_solver.h
theory/bv/bv_solver_lazy.cpp
theory/bv/bv_solver_lazy.h
+ theory/bv/bv_solver_simple.cpp
+ theory/bv/bv_solver_simple.h
theory/bv/bv_subtheory.h
theory/bv/bv_subtheory_algebraic.cpp
theory/bv/bv_subtheory_algebraic.h
type = "bool"
default = "false"
help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"
+
+[[option]]
+ name = "bvSolver"
+ category = "regular"
+ long = "bv-solver=MODE"
+ type = "BVSolver"
+ default = "LAZY"
+ help = "choose bit-vector solver, see --bv-solver=help"
+ help_mode = "Bit-vector solvers."
+[[option.mode.LAZY]]
+ name = "lazy"
+ help = "Enables the lazy BV solver infrastructure."
+[[option.mode.SIMPLE]]
+ name = "simple"
+ help = "Enables simple bitblasting solver with proof support."
+
}
}
+ /* BVSolver::SIMPLE does not natively support int2bv and nat2bv, they need to
+ * to be eliminated eagerly. */
+ if (options::bvSolver() == options::BVSolver::SIMPLE)
+ {
+ options::bvLazyReduceExtf.set(false);
+ options::bvLazyRewriteExtf.set(false);
+ }
+
if (options::solveIntAsBV() > 0)
{
// not compatible with incremental
*/
virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
- virtual bool needsCheckLastEffort() = 0;
+ virtual bool needsCheckLastEffort() { return false; }
virtual void propagate(Theory::Effort e){};
/** Called by abstraction preprocessing pass. */
virtual bool applyAbstraction(const std::vector<Node>& assertions,
- std::vector<Node>& new_assertions) = 0;
+ std::vector<Node>& new_assertions)
+ {
+ new_assertions.insert(
+ new_assertions.end(), assertions.begin(), assertions.end());
+ return false;
+ };
protected:
TheoryState& d_state;
--- /dev/null
+/********************* */
+/*! \file bv_solver_simple.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 Simple bit-blast solver
+ **
+ ** Simple bit-blast solver that sends bitblast lemmas directly to MiniSat.
+ **/
+
+#include "theory/bv/bv_solver_simple.h"
+
+#include "theory/bv/bitblast/lazy_bitblaster.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 {
+
+/**
+ * Implementation of a simple Node-based bit-blaster.
+ *
+ * Implements the bare minimum to bit-blast bit-vector atoms/terms.
+ */
+class BBSimple : public TBitblaster<Node>
+{
+ using Bits = std::vector<Node>;
+
+ public:
+ BBSimple(TheoryState& state);
+ ~BBSimple() = default;
+
+ /** Bit-blast term 'node' and return bit-blasted 'bits'. */
+ void bbTerm(TNode node, Bits& bits) override;
+ /** Bit-blast atom 'node'. */
+ void bbAtom(TNode node) override;
+ /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */
+ Node getBBAtom(TNode atom) const override;
+ /** Store Boolean node representing the bit-blasted atom. */
+ void storeBBAtom(TNode atom, Node atom_bb) override;
+ /** Store bits of bit-blasted term. */
+ void storeBBTerm(TNode node, const Bits& bits) override;
+ /** Check if atom was already bit-blasted. */
+ bool hasBBAtom(TNode atom) const override;
+ /** Get bit-blasted node stored for atom. */
+ Node getStoredBBAtom(TNode node);
+ /** Create 'bits' for variable 'var'. */
+ void makeVariable(TNode var, Bits& bits) override;
+
+ /** Collect model values for all relevant terms given in 'relevantTerms'. */
+ bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
+
+ prop::SatSolver* getSatSolver() override { Unreachable(); }
+
+ private:
+ /** Query SAT solver for assignment of node 'a'. */
+ Node getModelFromSatSolver(TNode a, bool fullModel) override;
+
+ /** Caches variables for which we already created bits. */
+ TNodeSet d_variables;
+ /** Stores bit-blasted atoms. */
+ std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms;
+ /** Theory state. */
+ TheoryState& d_state;
+};
+
+BBSimple::BBSimple(TheoryState& s) : TBitblaster<Node>(), d_state(s) {}
+
+void BBSimple::bbAtom(TNode node)
+{
+ node = node.getKind() == kind::NOT ? node[0] : node;
+
+ if (hasBBAtom(node))
+ {
+ return;
+ }
+
+ Node normalized = Rewriter::rewrite(node);
+ Node atom_bb =
+ normalized.getKind() != kind::CONST_BOOLEAN
+ && normalized.getKind() != kind::BITVECTOR_BITOF
+ ? d_atomBBStrategies[normalized.getKind()](normalized, this)
+ : normalized;
+
+ storeBBAtom(node, atom_bb);
+}
+
+void BBSimple::storeBBAtom(TNode atom, Node atom_bb)
+{
+ d_bbAtoms.emplace(atom, atom_bb);
+}
+
+void BBSimple::storeBBTerm(TNode node, const Bits& bits)
+{
+ d_termCache.emplace(node, bits);
+}
+
+bool BBSimple::hasBBAtom(TNode atom) const
+{
+ return d_bbAtoms.find(atom) != d_bbAtoms.end();
+}
+
+void BBSimple::makeVariable(TNode var, Bits& bits)
+{
+ Assert(bits.size() == 0);
+ for (unsigned i = 0; i < utils::getSize(var); ++i)
+ {
+ bits.push_back(utils::mkBitOf(var, i));
+ }
+ d_variables.insert(var);
+}
+
+Node BBSimple::getBBAtom(TNode node) const { return node; }
+
+void BBSimple::bbTerm(TNode node, Bits& bits)
+{
+ Assert(node.getType().isBitVector());
+ if (hasBBTerm(node))
+ {
+ getBBTerm(node, bits);
+ return;
+ }
+ d_termBBStrategies[node.getKind()](node, bits, this);
+ Assert(bits.size() == utils::getSize(node));
+ storeBBTerm(node, bits);
+}
+
+Node BBSimple::getStoredBBAtom(TNode node)
+{
+ bool negated = false;
+ if (node.getKind() == kind::NOT)
+ {
+ node = node[0];
+ negated = true;
+ }
+
+ Assert(hasBBAtom(node));
+ Node atom_bb = d_bbAtoms.at(node);
+ return negated ? atom_bb.negate() : atom_bb;
+}
+
+Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
+{
+ if (!hasBBTerm(a))
+ {
+ return utils::mkConst(utils::getSize(a), 0u);
+ }
+
+ bool assignment;
+ Bits bits;
+ getBBTerm(a, bits);
+ Integer value(0);
+ Integer one(1), zero(0);
+ for (int i = bits.size() - 1; i >= 0; --i)
+ {
+ Integer bit;
+ if (d_state.hasSatValue(bits[i], assignment))
+ {
+ bit = assignment ? one : zero;
+ }
+ else
+ {
+ bit = zero;
+ }
+ value = value * 2 + bit;
+ }
+ return utils::mkConst(bits.size(), value);
+}
+
+bool BBSimple::collectModelValues(TheoryModel* m,
+ const std::set<Node>& relevantTerms)
+{
+ for (const auto& var : relevantTerms)
+ {
+ if (d_variables.find(var) == d_variables.end()) continue;
+
+ Node const_value = getModelFromSatSolver(var, true);
+ Assert(const_value.isNull() || const_value.isConst());
+ if (!const_value.isNull())
+ {
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+/* -------------------------------------------------------------------------- */
+
+namespace {
+
+bool isBVAtom(TNode n)
+{
+ return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
+ || n.getKind() == kind::BITVECTOR_ULT
+ || n.getKind() == kind::BITVECTOR_ULE
+ || n.getKind() == kind::BITVECTOR_SLT
+ || n.getKind() == kind::BITVECTOR_SLE;
+}
+
+/* Traverse Boolean nodes and collect BV atoms. */
+void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms)
+{
+ std::vector<TNode> visit;
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+
+ visit.push_back(n);
+
+ do
+ {
+ TNode cur = visit.back();
+ visit.pop_back();
+
+ if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
+ continue;
+
+ visited.insert(cur);
+ if (isBVAtom(cur))
+ {
+ atoms.insert(cur);
+ continue;
+ }
+
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ } while (!visit.empty());
+}
+
+} // namespace
+
+BVSolverSimple::BVSolverSimple(TheoryState& s, TheoryInferenceManager& inferMgr)
+ : BVSolver(s, inferMgr), d_bitblaster(new BBSimple(s))
+{
+}
+
+void BVSolverSimple::addBBLemma(TNode fact)
+{
+ if (!d_bitblaster->hasBBAtom(fact))
+ {
+ d_bitblaster->bbAtom(fact);
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Node atom_bb = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
+ Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
+ d_inferManager.lemma(lemma);
+}
+
+bool BVSolverSimple::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ if (fact.getKind() == kind::NOT)
+ {
+ fact = fact[0];
+ }
+
+ if (isBVAtom(fact))
+ {
+ addBBLemma(fact);
+ }
+ else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
+ {
+ TNode n = fact[0];
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node lemma = nm->mkNode(kind::EQUAL, fact, n);
+ d_inferManager.lemma(lemma);
+
+ std::unordered_set<Node, NodeHashFunction> bv_atoms;
+ collectBVAtoms(n, bv_atoms);
+ for (const Node& nn : bv_atoms)
+ {
+ addBBLemma(nn);
+ }
+ }
+
+ return true;
+}
+
+bool BVSolverSimple::collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet)
+{
+ return d_bitblaster->collectModelValues(m, termSet);
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file bv_solver_simple.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 Simple bit-blast solver
+ **
+ ** Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
+#define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
+
+#include <unordered_map>
+
+#include "theory/bv/bv_solver.h"
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+class BBSimple;
+
+/**
+ * Simple bit-blasting solver that sends bit-blasting lemmas directly to the
+ * internal MiniSat. It is also ablo to handle atoms of kind
+ * BITVECTOR_EAGER_ATOM.
+ *
+ * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
+ */
+class BVSolverSimple : public BVSolver
+{
+ public:
+ BVSolverSimple(TheoryState& state, TheoryInferenceManager& inferMgr);
+ ~BVSolverSimple() = default;
+
+ void preRegisterTerm(TNode n) override {}
+
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+
+ std::string identify() const override { return "BVSolverSimple"; };
+
+ Theory::PPAssertStatus ppAssert(TNode in,
+ SubstitutionMap& outSubstitutions) override
+ {
+ return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
+ }
+
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
+
+ private:
+ /**
+ * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
+ * inference manager.
+ */
+ void addBBLemma(TNode fact);
+
+ /** Bit-blaster used to bit-blast atoms/terms. */
+ std::unique_ptr<BBSimple> d_bitblaster;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "options/bv_options.h"
#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_simple.h"
#include "theory/bv/theory_bv_utils.h"
namespace CVC4 {
d_state(c, u, valuation),
d_inferMgr(*this, d_state, pnm)
{
- d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
+ switch (options::bvSolver())
+ {
+ case options::BVSolver::LAZY:
+ d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
+ break;
+
+ default:
+ AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
+ d_internal.reset(new BVSolverSimple(d_state, d_inferMgr));
+ }
d_theoryState = &d_state;
d_inferManager = &d_inferMgr;
}
bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
+void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
+
+bool TheoryBV::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
+}
+
+void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
+{
+ d_internal->notifyFact(atom, pol, fact, isInternal);
+}
+
bool TheoryBV::needsCheckLastEffort()
{
return d_internal->needsCheckLastEffort();
bool preCheck(Effort e) override;
+ void postCheck(Effort e) override;
+
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+
bool needsCheckLastEffort() override;
void propagate(Effort e) override;
ConcatToMult,
IsPowerOfTwo,
MultSltMult,
+ BitOfConst,
};
inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
case MultSltMult: out << "MultSltMult"; return out;
case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out;
+ case BitOfConst: out << "BitOfConst"; return out;
default:
Unreachable();
}
namespace theory {
namespace bv {
+/* -------------------------------------------------------------------------- */
+
+/**
+ * BitOfConst
+ */
+template <>
+inline bool RewriteRule<BitOfConst>::applies(TNode node)
+{
+ return node.getKind() == kind::BITVECTOR_BITOF && node[0].isConst();
+}
+
+template <>
+inline Node RewriteRule<BitOfConst>::apply(TNode node)
+{
+ size_t pos = node.getOperator().getConst<BitVectorBitOf>().d_bitIndex;
+ return utils::getBit(node[0], pos) ? utils::mkTrue() : utils::mkFalse();
+}
/* -------------------------------------------------------------------------- */
return res;
}
+RewriteResponse TheoryBVRewriter::RewriteBitOf(TNode node, bool prerewrite)
+{
+ Node resultNode = LinearRewriteStrategy<RewriteRule<BitOfConst>>::apply(node);
+ return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) {
// reduce common subexpressions on both sides
Node resultNode = LinearRewriteStrategy
}
d_rewriteTable [ kind::EQUAL ] = RewriteEqual;
+ d_rewriteTable[kind::BITVECTOR_BITOF] = RewriteBitOf;
d_rewriteTable [ kind::BITVECTOR_ULT ] = RewriteUlt;
d_rewriteTable [ kind::BITVECTOR_SLT ] = RewriteSlt;
d_rewriteTable [ kind::BITVECTOR_ULE ] = RewriteUle;
private:
static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
- static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
-
+ static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
+
+ static RewriteResponse RewriteBitOf(TNode node, bool prerewrite = false);
static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false);
TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
+bool TheoryState::hasSatValue(TNode n, bool& value) const
+{
+ return d_valuation.hasSatValue(n, value);
+}
+
} // namespace theory
} // namespace CVC4
*/
TheoryModel* getModel();
+ /** Returns true if n has a current SAT assignment and stores it in value. */
+ virtual bool hasSatValue(TNode n, bool& value) const;
+
protected:
/** Pointer to the SAT context object used by the theory. */
context::Context* d_context;
; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models --no-check-unsat-cores
; EXPECT: sat
(set-logic QF_UFBV)
(set-info :smt-lib-version 2.0)
; COMMAND-LINE: --bitblast=eager
+; COMMAND-LINE: --bitblast=eager --bv-solver=simple
(set-info :status sat)
(set-logic QF_BV)
(declare-fun x () Bool)
; COMMAND-LINE: --bool-to-bv=ite
+; COMMAND-LINE: --bool-to-bv=ite --bv-solver=simple
; EXPECT: sat
(set-logic QF_BV)
(declare-fun x2 () (_ BitVec 3))
; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --bv-solver=simple
; EXPECT: sat
; EXPECT: sat
(set-logic QF_BV)
; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --bv-solver=simple
; EXPECT: sat
; EXPECT: sat
(set-logic ALL)
; COMMAND-LINE: --no-bv-div-zero-const --no-check-unsat-cores
+; COMMAND-LINE: --bv-solver=simple --no-bv-div-zero-const --no-check-unsat-cores
(set-logic QF_BV)
(set-info :status sat)
(declare-const x (_ BitVec 4))
; COMMAND-LINE: --bitblast=lazy
; COMMAND-LINE: --bitblast=eager --no-check-models
+; COMMAND-LINE: --bv-solver=simple
; EXPECT: sat
; Automatically generated by SBV. Do not edit.
(set-logic QF_UFBV)
projects / cvc5.git / commitdiff