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.

2 files changed, 81 insertions, 18 deletions

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
@@ -27,6 +27,46 @@ 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.
  *
  * The CnfStream calls preRegister() if it encounters a theory atom.
@@ -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<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