From ff5ecff78ade286f2836c6fa76b6c502fa8f3c3b Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 19 May 2021 10:21:42 -0700 Subject: [PATCH] bv: Add support for --bitblast=eager. (#6516) This PR adds support for handling --bitblast=eager in the new bitblast solver. --- src/smt/set_defaults.cpp | 4 -- src/theory/bv/bv_solver_bitblast.cpp | 102 ++++++++++++++++++++++++--- src/theory/bv/bv_solver_bitblast.h | 11 ++- 3 files changed, 102 insertions(+), 15 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index b97c99eae..7c5d775ed 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -162,10 +162,6 @@ 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. - opts.set(options::bvSolver, options::BVSolver::LAZY); } /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index b01ba2580..463a937fd 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -26,12 +26,54 @@ namespace cvc5 { namespace theory { namespace bv { +/** + * Bit-blasting registrar. + * + * The CnfStream calls preRegister() if it encounters a theory atom. + * This registrar bit-blasts given atom and remembers which bit-vector atoms + * were bit-blasted. + * + * This registrar is needed when --bitblast=eager is enabled. + */ +class BBRegistrar : public prop::Registrar +{ + public: + BBRegistrar(BBSimple* bb) : d_bitblaster(bb) {} + + void preRegister(Node n) override + { + if (d_registeredAtoms.find(n) != d_registeredAtoms.end()) + { + return; + } + /* We are only interested in bit-vector atoms. */ + if ((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) + { + d_registeredAtoms.insert(n); + d_bitblaster->bbAtom(n); + } + } + + std::unordered_set& getRegisteredAtoms() { return d_registeredAtoms; } + + private: + /** The bitblaster used. */ + BBSimple* d_bitblaster; + + /** Stores bit-vector atoms encounterd on preRegister(). */ + std::unordered_set d_registeredAtoms; +}; + BVSolverBitblast::BVSolverBitblast(TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) : BVSolver(*s, inferMgr), d_bitblaster(new BBSimple(s)), - d_nullRegistrar(new prop::NullRegistrar()), + d_bbRegistrar(new BBRegistrar(d_bitblaster.get())), d_nullContext(new context::Context()), d_bbFacts(s->getSatContext()), d_bbInputFacts(s->getSatContext()), @@ -61,7 +103,7 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); } d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), - d_nullRegistrar.get(), + d_bbRegistrar.get(), d_nullContext.get(), nullptr, smt::currentResourceManager())); @@ -88,9 +130,16 @@ void BVSolverBitblast::postCheck(Theory::Effort level) /* Bit-blast fact and cache literal. */ if (d_factLiteralCache.find(fact) == d_factLiteralCache.end()) { - d_bitblaster->bbAtom(fact); - Node bb_fact = d_bitblaster->getStoredBBAtom(fact); - d_cnfStream->convertAndAssert(bb_fact, false, false); + if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM) + { + handleEagerAtom(fact, true); + } + else + { + d_bitblaster->bbAtom(fact); + Node bb_fact = d_bitblaster->getStoredBBAtom(fact); + d_cnfStream->convertAndAssert(bb_fact, false, false); + } } d_assertions.push_back(fact); } @@ -103,10 +152,19 @@ void BVSolverBitblast::postCheck(Theory::Effort level) /* Bit-blast fact and cache literal. */ if (d_factLiteralCache.find(fact) == d_factLiteralCache.end()) { - d_bitblaster->bbAtom(fact); - Node bb_fact = d_bitblaster->getStoredBBAtom(fact); - d_cnfStream->ensureLiteral(bb_fact); - prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact); + prop::SatLiteral lit; + if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM) + { + handleEagerAtom(fact, false); + lit = d_cnfStream->getLiteral(fact[0]); + } + else + { + d_bitblaster->bbAtom(fact); + Node bb_fact = d_bitblaster->getStoredBBAtom(fact); + d_cnfStream->ensureLiteral(bb_fact); + lit = d_cnfStream->getLiteral(bb_fact); + } d_factLiteralCache[fact] = lit; d_literalFactCache[lit] = fact; } @@ -322,6 +380,32 @@ Node BVSolverBitblast::getValue(TNode node) return it->second; } +void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact) +{ + Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); + + if (assertFact) + { + d_cnfStream->convertAndAssert(fact[0], false, false); + } + else + { + d_cnfStream->ensureLiteral(fact[0]); + } + + /* convertAndAssert() does not make the connection between the bit-vector + * atom and it's bit-blasted form (it only calls preRegister() from the + * registrar). Thus, we add the equalities now. */ + auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms(); + for (auto atom : registeredAtoms) + { + Node bb_atom = d_bitblaster->getStoredBBAtom(atom); + d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false); + } + // Clear cache since we only need to do this once per bit-blasted atom. + registeredAtoms.clear(); +} + } // namespace bv } // namespace theory } // namespace cvc5 diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index f98121a63..3da08f868 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -83,6 +83,14 @@ class BVSolverBitblast : public BVSolver */ Node getValue(TNode node); + /** + * Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream. + * + * @param assertFact: Indicates whether the fact should be asserted (true) or + * assumed (false). + */ + void handleEagerAtom(TNode fact, bool assertFact); + /** * Cache for getValue() calls. * @@ -95,8 +103,7 @@ class BVSolverBitblast : public BVSolver std::unique_ptr d_bitblaster; /** Used for initializing `d_cnfStream`. */ - std::unique_ptr d_nullRegistrar; - + std::unique_ptr d_bbRegistrar; std::unique_ptr d_nullContext; /** SAT solver back end (configured via options::bvSatSolver. */ -- 2.30.2