summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/options/bv_options.toml3
-rw-r--r--src/options/options_handler.cpp5
-rw-r--r--src/prop/cadical.cpp14
-rw-r--r--src/prop/cadical.h6
-rw-r--r--src/prop/cryptominisat.cpp18
-rw-r--r--src/prop/cryptominisat.h1
-rw-r--r--src/prop/sat_solver.h13
-rw-r--r--src/smt/set_defaults.cpp11
-rw-r--r--src/theory/bv/bitblast/bitblast_strategies_template.h29
-rw-r--r--src/theory/bv/bitblast/simple_bitblaster.cpp13
-rw-r--r--src/theory/bv/bitblast/simple_bitblaster.h3
-rw-r--r--src/theory/bv/bv_solver_bitblast.cpp161
-rw-r--r--src/theory/bv/bv_solver_bitblast.h99
-rw-r--r--src/theory/bv/theory_bv.cpp48
-rw-r--r--src/theory/bv/theory_bv.h2
16 files changed, 406 insertions, 22 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0929b6625..c5673a396 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -525,6 +525,8 @@ libcvc4_add_sources(
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
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 6a0ca913b..acb010a2e 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -236,6 +236,9 @@ header = "options/bv_options.h"
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."
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index fe37e9363..ac33d9c51 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -145,8 +145,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
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())
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 6410552ba..b3563bf28 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -111,6 +111,7 @@ SatVariable CadicalSolver::falseVar() { return d_false; }
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);
@@ -125,10 +126,12 @@ SatValue CadicalSolver::solve(long unsigned int&)
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);
@@ -136,6 +139,17 @@ SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
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)
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index bb7b7aa9f..6a7258091 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -50,6 +50,7 @@ class CadicalSolver : public SatSolver
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;
@@ -74,6 +75,11 @@ class CadicalSolver : public SatSolver
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;
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 1072003d2..d375388ef 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -39,6 +39,15 @@ CMSat::Lit toInternalLit(SatLiteral lit)
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;
@@ -181,6 +190,15 @@ SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
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();
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 8861daf61..eebe4de29 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -61,6 +61,7 @@ class CryptoMinisatSolver : public SatSolver
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;
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 10ee843df..896233f41 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -96,6 +96,19 @@ public:
/** 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 */
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 26f5745ca..cb4c99a2e 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -117,11 +117,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
"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);
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index a4e1757e2..8bab969c5 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -611,11 +611,11 @@ void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
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
@@ -669,11 +669,11 @@ void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
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;
@@ -727,11 +727,10 @@ void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
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();
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 36e115e5e..8eb209b53 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -51,9 +51,13 @@ void BBSimple::storeBBTerm(TNode node, const Bits& bits)
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)
@@ -143,6 +147,11 @@ bool BBSimple::collectModelValues(TheoryModel* m,
return true;
}
+bool BBSimple::isVariable(TNode node)
+{
+ return d_variables.find(node) != d_variables.end();
+}
+
} // namespace bv
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 8a625b5e1..72a2fb0d8 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -58,6 +58,9 @@ class BBSimple : public TBitblaster<Node>
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;
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
new file mode 100644
index 000000000..68192e1d4
--- /dev/null
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -0,0 +1,161 @@
+/********************* */
+/*! \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
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
new file mode 100644
index 000000000..df0f2e085
--- /dev/null
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -0,0 +1,99 @@
+/********************* */
+/*! \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
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 227df458a..b27bd04e1 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -17,6 +17,7 @@
#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"
@@ -42,6 +43,10 @@ TheoryBV::TheoryBV(context::Context* c,
{
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;
@@ -70,6 +75,44 @@ void TheoryBV::finishInit()
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)
@@ -199,6 +242,11 @@ TrustNode TheoryBV::ppRewrite(TNode t)
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)
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 093a35a1b..306b1ff93 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -96,6 +96,8 @@ class TheoryBV : public Theory
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback