From: Mathias Preiner Date: Wed, 3 Feb 2021 20:38:09 +0000 (-0800) Subject: Add BV solver bitblast. (#5851) X-Git-Tag: cvc5-1.0.0~2325 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac998a45ae64c589aeb79c5fd72234468e40451c;p=cvc5.git Add BV solver bitblast. (#5851) 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. --- 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& 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& assumptions) return res; } +void CadicalSolver::getUnsatAssumptions(std::vector& 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& assumptions) override; + void getUnsatAssumptions(std::vector& assumptions) override; void interrupt() override; @@ -74,6 +75,11 @@ class CadicalSolver : public SatSolver void init(); std::unique_ptr 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 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& assumptions) return toSatLiteralValue(d_solver->solve(&assumpts)); } +void CryptoMinisatSolver::getUnsatAssumptions( + std::vector& assumptions) +{ + for (const CMSat::Lit& lit : d_solver->get_conflict()) + { + assumptions.push_back(toSatLiteral(~lit)); + } +} + SatValue CryptoMinisatSolver::value(SatLiteral l){ const std::vector 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& assumptions) override; + void getUnsatAssumptions(std::vector& 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& 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& res, TBitblaster* 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 a_size_bits; + DefaultConstBB(a_size, a_size_bits, bb); + T b_ult_a_size = uLessThanBB(b, a_size_bits, false); + std::vector 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& res, TBitblaster* 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 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 prev_res; @@ -727,11 +727,10 @@ void DefaultAshrBB(TNode node, std::vector& res, TBitblaster* 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 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 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 assumptions; + std::unordered_map + 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 unsat_assumptions; + d_satSolver->getUnsatAssumptions(unsat_assumptions); + Assert(unsat_assumptions.size() > 0); + + std::vector 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& 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 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 + +#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& 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 d_bitblaster; + + /** Used for initializing CnfStream> */ + std::unique_ptr d_nullRegistrar; + std::unique_ptr d_nullContext; + + /** SAT solver back end (configured via options::bvSatSolver. */ + std::unique_ptr d_satSolver; + /** CNF stream. */ + std::unique_ptr d_cnfStream; + + /** Facts sent to this solver. */ + context::CDList d_facts; + + /** Proof generator that manages proofs for lemmas generated by this class. */ + std::unique_ptr 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& assertions, std::vector& new_assertions);