From de0401e53e4baab30a5e78d5bd51048348b1e1ce Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 2 Jul 2021 15:13:17 -0700 Subject: [PATCH] Fix bv assert input reset assertions (#6820) If reset-assertions was called it will now reset the SAT solver and the CNF stream if clauses were permanently added to the SAT solver via option --bv-assert-input. --- src/theory/bv/bv_solver_bitblast.cpp | 92 +++++++++++++++---- src/theory/bv/bv_solver_bitblast.h | 7 ++ test/regress/CMakeLists.txt | 1 + .../bv/reset-assertions-assert-input.smt2 | 18 ++++ 4 files changed, 100 insertions(+), 18 deletions(-) create mode 100644 test/regress/regress0/bv/reset-assertions-assert-input.smt2 diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index a5d89e371..613ba47bf 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -26,6 +26,46 @@ namespace cvc5 { namespace theory { namespace bv { +/** + * Notifies the BV solver when assertions were reset. + * + * This class is notified after every user-context pop and maintains a flag + * that indicates whether assertions have been reset. If the user-context level + * reaches level 0 it means that the assertions were reset. + */ +class NotifyResetAssertions : public context::ContextNotifyObj +{ + public: + NotifyResetAssertions(context::Context* c) + : context::ContextNotifyObj(c, false), + d_context(c), + d_doneResetAssertions(false) + { + } + + bool doneResetAssertions() { return d_doneResetAssertions; } + + void reset() { d_doneResetAssertions = false; } + + protected: + void contextNotifyPop() override + { + // If the user-context level reaches 0 it means that reset-assertions was + // called. + if (d_context->getLevel() == 0) + { + d_doneResetAssertions = true; + } + } + + private: + /** The user-context. */ + context::Context* d_context; + + /** Flag to notify whether reset assertions was called. */ + bool d_doneResetAssertions; +}; + /** * Bit-blasting registrar. * @@ -85,30 +125,15 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, : nullptr), d_factLiteralCache(s->getSatContext()), d_literalFactCache(s->getSatContext()), - d_propagate(options::bitvectorPropagate()) + d_propagate(options::bitvectorPropagate()), + d_resetNotify(new NotifyResetAssertions(s->getUserContext())) { if (pnm != nullptr) { d_bvProofChecker.registerTo(pnm->getChecker()); } - switch (options::bvSatSolver()) - { - case options::SatSolverMode::CRYPTOMINISAT: - d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); - break; - default: - d_satSolver.reset(prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); - } - d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), - d_bbRegistrar.get(), - d_nullContext.get(), - nullptr, - smt::currentResourceManager(), - prop::FormulaLitPolicy::INTERNAL, - "theory::bv::BVSolverBitblast")); + initSatSolver(); } void BVSolverBitblast::postCheck(Theory::Effort level) @@ -122,6 +147,16 @@ void BVSolverBitblast::postCheck(Theory::Effort level) } } + // If we permanently added assertions to the SAT solver and the assertions + // were reset, we have to reset the SAT solver and the CNF stream. + if (options::bvAssertInput() && d_resetNotify->doneResetAssertions()) + { + d_satSolver.reset(nullptr); + d_cnfStream.reset(nullptr); + initSatSolver(); + d_resetNotify->reset(); + } + NodeManager* nm = NodeManager::currentNM(); /* Process input assertions bit-blast queue. */ @@ -316,6 +351,27 @@ EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b) return EQUALITY_FALSE_IN_MODEL; } +void BVSolverBitblast::initSatSolver() +{ + switch (options::bvSatSolver()) + { + case options::SatSolverMode::CRYPTOMINISAT: + d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); + break; + default: + d_satSolver.reset(prop::SatSolverFactory::createCadical( + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); + } + d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), + d_bbRegistrar.get(), + d_nullContext.get(), + nullptr, + smt::currentResourceManager(), + prop::FormulaLitPolicy::INTERNAL, + "theory::bv::BVSolverBitblast")); +} + Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize) { if (node.isConst()) diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index c5134c6fc..1fb721deb 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -33,6 +33,7 @@ namespace cvc5 { namespace theory { namespace bv { +class NotifyResetAssertions; class BBRegistrar; /** @@ -70,6 +71,9 @@ class BVSolverBitblast : public BVSolver const std::set& termSet) override; private: + /** Initialize SAT solver and CNF stream. */ + void initSatSolver(); + /** * Get value of `node` from SAT solver. * @@ -153,6 +157,9 @@ class BVSolverBitblast : public BVSolver /** Option to enable/disable bit-level propagation. */ bool d_propagate; + + /** Notifies when reset-assertion was called. */ + std::unique_ptr d_resetNotify; }; } // namespace bv diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6cf5c76c1..00a50a69c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -429,6 +429,7 @@ set(regress_0_tests regress0/bv/mult-pow2-negative.smt2 regress0/bv/pr4993-bvugt-bvurem-a.smt2 regress0/bv/pr4993-bvugt-bvurem-b.smt2 + regress0/bv/reset-assertions-assert-input.smt2 regress0/bv/sizecheck.cvc regress0/bv/smtcompbug.smtv1.smt2 regress0/bv/test-bv_intro_pow2.smt2 diff --git a/test/regress/regress0/bv/reset-assertions-assert-input.smt2 b/test/regress/regress0/bv/reset-assertions-assert-input.smt2 new file mode 100644 index 000000000..6a77ae078 --- /dev/null +++ b/test/regress/regress0/bv/reset-assertions-assert-input.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i --bv-solver=bitblast --bv-assert-input +(set-logic QF_BV) +(set-option :global-declarations true) + +(declare-const a (_ BitVec 8)) +(declare-const b (_ BitVec 8)) +(declare-const c (_ BitVec 8)) +(declare-const d (_ BitVec 8)) + +(assert (distinct (bvadd a d) (bvadd b c))) +(set-info :status sat) +(check-sat) + +(reset-assertions) + +(assert (= (bvadd a d) (bvadd b c))) +(set-info :status sat) +(check-sat) -- 2.30.2