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.

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index a5d89e37146c29721fb267ca9c6581b142fe6764..613ba47bfcc339c852e575acc97c037a3996f381 100644 (file)
--- 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 c5134c6fceef3b9bb5f3ea21cfb67b965b8ed2d1..1fb721deb1fa05795d2554ae12403820e2f2d486 100644 (file)
--- 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<Node>& 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<NotifyResetAssertions> d_resetNotify;
 };
 
 }  // namespace bv

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6cf5c76c19db5ef991bcea4aea38ccd949cb52d0..00a50a69c5c1b1efbef820c2b12375a88b009350 100644 (file)
--- 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 (file)
index 0000000..6a77ae0
--- /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)