diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-05-13 17:29:52 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-14 00:29:52 +0000 |
commit | b59deea057513448d98f54629c78a38a81f99b27 (patch) | |
tree | 4f4458795bc505173710786a932c3babf9a1b5d4 /src/theory | |
parent | d7b74a33e3722dd123ecfb79603538cc5ac889a0 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bv_solver_bitblast.cpp | 66 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_bitblast.h | 13 | ||||
-rw-r--r-- | src/theory/valuation.cpp | 12 | ||||
-rw-r--r-- | src/theory/valuation.h | 16 |
4 files changed, 96 insertions, 11 deletions
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<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) + 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<Node> 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<Node> 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<prop::NullRegistrar> d_nullRegistrar; + std::unique_ptr<context::Context> d_nullContext; /** SAT solver back end (configured via options::bvSatSolver. */ @@ -108,9 +111,19 @@ class BVSolverBitblast : public BVSolver */ context::CDQueue<Node> d_bbFacts; + /** + * Bit-blast queue for user-level 0 input facts sent to this solver. + * + * Get populated on preNotifyFact(). + */ + context::CDQueue<Node> d_bbInputFacts; + /** Corresponds to the SAT literals of the currently asserted facts. */ context::CDList<prop::SatLiteral> d_assumptions; + /** Stores the current input assertions. */ + context::CDList<Node> d_assertions; + /** Flag indicating whether `d_modelCache` should be invalidated. */ context::CDO<bool> 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 @@ -185,6 +185,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. */ unsigned getAssertionLevel() const; |