From b59deea057513448d98f54629c78a38a81f99b27 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 13 May 2021 17:29:52 -0700 Subject: [PATCH] bv: Assert input facts on user-level 0. (#6515) The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default. --- src/options/bv_options.toml | 8 ++++ src/prop/minisat/core/Solver.h | 6 +-- src/prop/minisat/minisat.cpp | 10 +++++ src/prop/minisat/minisat.h | 4 ++ src/prop/prop_engine.cpp | 14 ++++++ src/prop/prop_engine.h | 16 +++++++ src/prop/sat_solver.h | 10 +++++ src/theory/bv/bv_solver_bitblast.cpp | 66 +++++++++++++++++++++++----- src/theory/bv/bv_solver_bitblast.h | 13 ++++++ src/theory/valuation.cpp | 12 +++++ src/theory/valuation.h | 16 +++++++ 11 files changed, 161 insertions(+), 14 deletions(-) diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 3172f8d5f..34bdfcdaa 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -243,3 +243,11 @@ name = "Bitvector theory" name = "simple" help = "Enables simple bitblasting solver with proof support." +[[option]] + name = "bvAssertInput" + category = "regular" + long = "bv-assert-input" + type = "bool" + default = "false" + help = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver" + diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index a9ee25c11..f4aa04e4d 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -531,12 +531,12 @@ protected: bool isPropagated (Var x) const; // Does the variable have a propagated variables bool isPropagatedBy (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C - int level (Var x) const; - int user_level (Var x) const; // User level at which this variable was asserted - int intro_level (Var x) const; // User level at which this variable was created int trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... public: + int level (Var x) const; + int user_level (Var x) const; // User level at which this variable was asserted + int intro_level (Var x) const; // User level at which this variable was created bool withinBudget (uint64_t amount) const; bool withinBudget(Resource r) const; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index b09ffd685..293e7175b 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -259,6 +259,16 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const { return d_minisat->isDecision( decn ); } +int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const +{ + return d_minisat->level(v); +} + +int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const +{ + return d_minisat->intro_level(v); +} + SatProofManager* MinisatSatSolver::getProofManager() { return d_minisat->getProofManager(); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index a4bd1e7a0..0e6ca28b8 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -85,6 +85,10 @@ class MinisatSatSolver : public CDCLTSatSolverInterface bool isDecision(SatVariable decn) const override; + int32_t getDecisionLevel(SatVariable v) const override; + + int32_t getIntroLevel(SatVariable v) const override; + /** Retrieve a pointer to the unerlying solver. */ Minisat::SimpSolver* getSolver() { return d_minisat; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 70401c56d..63591e74b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -340,6 +340,20 @@ bool PropEngine::isDecision(Node lit) const { return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable()); } +int32_t PropEngine::getDecisionLevel(Node lit) const +{ + Assert(isSatLiteral(lit)); + return d_satSolver->getDecisionLevel( + d_cnfStream->getLiteral(lit).getSatVariable()); +} + +int32_t PropEngine::getIntroLevel(Node lit) const +{ + Assert(isSatLiteral(lit)); + return d_satSolver->getIntroLevel( + d_cnfStream->getLiteral(lit).getSatVariable()); +} + void PropEngine::printSatisfyingAssignment(){ const CnfStream::NodeToLiteralMap& transCache = d_cnfStream->getTranslationCache(); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 631317c2d..a12816906 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -156,6 +156,22 @@ class PropEngine */ bool isDecision(Node lit) const; + /** + * Return the current decision level of `lit`. + * + * @param lit: The node in question, must have an associated SAT literal. + * @return Decision level of the SAT variable of `lit` (phase is disregarded), + * or -1 if `lit` has not been assigned yet. + */ + int32_t getDecisionLevel(Node lit) const; + + /** + * Return the user-context level when `lit` was introduced.. + * + * @return User-context level or -1 if not yet introduced. + */ + int32_t getIntroLevel(Node lit) const; + /** * Checks the current context for satisfiability. * diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 1c64c92c2..963810594 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -168,6 +168,16 @@ class CDCLTSatSolverInterface : public SatSolver virtual bool isDecision(SatVariable decn) const = 0; + /** + * Return the current decision level of `lit`. + */ + virtual int32_t getDecisionLevel(SatVariable v) const { return -1; } + + /** + * Return the user-context level when `lit` was introduced.. + */ + virtual int32_t getIntroLevel(SatVariable v) const { return -1; } + virtual std::shared_ptr getProof() = 0; }; /* class CDCLTSatSolverInterface */ diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index ecf2bafb6..b01ba2580 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -34,7 +34,9 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, d_nullRegistrar(new prop::NullRegistrar()), d_nullContext(new context::Context()), d_bbFacts(s->getSatContext()), + d_bbInputFacts(s->getSatContext()), d_assumptions(s->getSatContext()), + d_assertions(s->getSatContext()), d_invalidateModelCache(s->getSatContext(), true), d_inSatMode(s->getSatContext(), false), d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "") @@ -76,6 +78,23 @@ void BVSolverBitblast::postCheck(Theory::Effort level) } } + NodeManager* nm = NodeManager::currentNM(); + + /* Process input assertions bit-blast queue. */ + while (!d_bbInputFacts.empty()) + { + Node fact = d_bbInputFacts.front(); + d_bbInputFacts.pop(); + /* 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); + } + d_assertions.push_back(fact); + } + /* Process bit-blast queue and store SAT literals. */ while (!d_bbFacts.empty()) { @@ -87,7 +106,6 @@ void BVSolverBitblast::postCheck(Theory::Effort level) d_bitblaster->bbAtom(fact); Node bb_fact = d_bitblaster->getStoredBBAtom(fact); d_cnfStream->ensureLiteral(bb_fact); - prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact); d_factLiteralCache[fact] = lit; d_literalFactCache[lit] = fact; @@ -106,25 +124,51 @@ void BVSolverBitblast::postCheck(Theory::Effort level) { std::vector unsat_assumptions; d_satSolver->getUnsatAssumptions(unsat_assumptions); - Assert(unsat_assumptions.size() > 0); - std::vector conflict; - for (const prop::SatLiteral& lit : unsat_assumptions) + Node conflict; + // Unsat assumptions produce conflict. + if (unsat_assumptions.size() > 0) { - conflict.push_back(d_literalFactCache[lit]); - Debug("bv-bitblast") << "unsat assumption (" << lit - << "): " << conflict.back() << std::endl; + std::vector conf; + for (const prop::SatLiteral& lit : unsat_assumptions) + { + conf.push_back(d_literalFactCache[lit]); + Debug("bv-bitblast") + << "unsat assumption (" << lit << "): " << conf.back() << std::endl; + } + conflict = nm->mkAnd(conf); } - - NodeManager* nm = NodeManager::currentNM(); - d_im.conflict(nm->mkAnd(conflict), InferenceId::BV_BITBLAST_CONFLICT); + else // Input assertions produce conflict. + { + std::vector assertions(d_assertions.begin(), d_assertions.end()); + conflict = nm->mkAnd(assertions); + } + d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT); } } bool BVSolverBitblast::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) { - d_bbFacts.push_back(fact); + Valuation& val = d_state.getValuation(); + + /** + * Check whether `fact` is an input assertion on user-level 0. + * + * If this is the case we can assert `fact` to the SAT solver instead of + * using assumptions. + */ + if (options::bvAssertInput() && val.isSatLiteral(fact) + && !val.isDecision(fact) && val.getDecisionLevel(fact) == 0 + && val.getIntroLevel(fact) == 0) + { + d_bbInputFacts.push_back(fact); + } + else + { + d_bbFacts.push_back(fact); + } + return false; // Return false to enable equality engine reasoning in Theory. } diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 36c06209a..f98121a63 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -33,6 +33,8 @@ namespace cvc5 { namespace theory { namespace bv { +class BBRegistrar; + /** * Bit-blasting solver with support for different SAT back ends. */ @@ -94,6 +96,7 @@ class BVSolverBitblast : public BVSolver /** Used for initializing `d_cnfStream`. */ std::unique_ptr d_nullRegistrar; + std::unique_ptr d_nullContext; /** SAT solver back end (configured via options::bvSatSolver. */ @@ -108,9 +111,19 @@ class BVSolverBitblast : public BVSolver */ context::CDQueue d_bbFacts; + /** + * Bit-blast queue for user-level 0 input facts sent to this solver. + * + * Get populated on preNotifyFact(). + */ + context::CDQueue d_bbInputFacts; + /** Corresponds to the SAT literals of the currently asserted facts. */ context::CDList d_assumptions; + /** Stores the current input assertions. */ + context::CDList d_assertions; + /** Flag indicating whether `d_modelCache` should be invalidated. */ context::CDO d_invalidateModelCache; diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 937fcd5fa..621f89539 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -188,6 +188,18 @@ bool Valuation::isDecision(Node lit) const { return d_engine->getPropEngine()->isDecision(lit); } +int32_t Valuation::getDecisionLevel(Node lit) const +{ + Assert(d_engine != nullptr); + return d_engine->getPropEngine()->getDecisionLevel(lit); +} + +int32_t Valuation::getIntroLevel(Node lit) const +{ + Assert(d_engine != nullptr); + return d_engine->getPropEngine()->getIntroLevel(lit); +} + unsigned Valuation::getAssertionLevel() const{ Assert(d_engine != nullptr); return d_engine->getPropEngine()->getAssertionLevel(); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index a1a3db706..7438279b1 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -184,6 +184,22 @@ public: */ bool isDecision(Node lit) const; + /** + * Return the current decision level of `lit`. + * + * @param lit: The node in question, must have an associated SAT literal. + * @return Decision level of the SAT variable of `lit` (phase is disregarded), + * or -1 if `lit` has not been assigned yet. + */ + int32_t getDecisionLevel(Node lit) const; + + /** + * Return the user-context level when `lit` was introduced.. + * + * @return User-context level or -1 if not yet introduced. + */ + int32_t getIntroLevel(Node lit) const; + /** * Get the assertion level of the SAT solver. */ -- 2.30.2