Fix issue with reset-assertions. (#3988)

Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index a6b6cbd8f6831d24e8e9dc4ccd7cbdde38b87f9f..ce79d6ca08f0406313eb9dd8cf0770868fa85b52 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -29,27 +29,28 @@
 namespace CVC4 {
 
 JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
-                                               context::UserContext *uc,
-                                               context::Context *c):
-  ITEDecisionStrategy(de, c),
-  d_justified(c),
-  d_exploredThreshold(c),
-  d_prvsIndex(c, 0),
-  d_threshPrvsIndex(c, 0),
-  d_helfulness("decision::jh::helpfulness", 0),
-  d_giveup("decision::jh::giveup", 0),
-  d_timestat("decision::jh::time"),
-  d_assertions(uc),
-  d_iteAssertions(uc),
-  d_iteCache(uc),
-  d_visited(),
-  d_visitedComputeITE(),
-  d_curDecision(),
-  d_curThreshold(0),
-  d_childCache(uc),
-  d_weightCache(uc),
-  d_startIndexCache(c) {
-  smtStatisticsRegistry()->registerStat(&d_helfulness);
+                                               context::UserContext* uc,
+                                               context::Context* c)
+    : ITEDecisionStrategy(de, c),
+      d_justified(c),
+      d_exploredThreshold(c),
+      d_prvsIndex(c, 0),
+      d_threshPrvsIndex(c, 0),
+      d_helpfulness("decision::jh::helpfulness", 0),
+      d_giveup("decision::jh::giveup", 0),
+      d_timestat("decision::jh::time"),
+      d_assertions(uc),
+      d_iteAssertions(uc),
+      d_iteCache(uc),
+      d_visited(),
+      d_visitedComputeITE(),
+      d_curDecision(),
+      d_curThreshold(0),
+      d_childCache(uc),
+      d_weightCache(uc),
+      d_startIndexCache(c)
+{
+  smtStatisticsRegistry()->registerStat(&d_helpfulness);
   smtStatisticsRegistry()->registerStat(&d_giveup);
   smtStatisticsRegistry()->registerStat(&d_timestat);
   Trace("decision") << "Justification heuristic enabled" << std::endl;
@@ -57,7 +58,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
 
 JustificationHeuristic::~JustificationHeuristic()
 {
-  smtStatisticsRegistry()->unregisterStat(&d_helfulness);
+  smtStatisticsRegistry()->unregisterStat(&d_helpfulness);
   smtStatisticsRegistry()->unregisterStat(&d_giveup);
   smtStatisticsRegistry()->unregisterStat(&d_timestat);
 }
@@ -109,7 +110,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
     if(litDecision != undefSatLiteral) {
       setPrvsIndex(i);
       Trace("decision") << "jh: splitting on " << litDecision << std::endl;
-      ++d_helfulness;
+      ++d_helpfulness;
       return litDecision;
     }
   }

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index b2c32562893863bea03dc47fd48303b9a07014d9..bb426ad1e9f7d1a1b38ece71e5cc7ef150f07eb7 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -57,7 +57,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   context::CDO<unsigned>  d_prvsIndex;
   context::CDO<unsigned>  d_threshPrvsIndex;
 
-  IntStat d_helfulness;
+  IntStat d_helpfulness;
   IntStat d_giveup;
   TimerStat d_timestat;
 

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index b32a2a86fd139099b03be78c5cc2e5c58e17f685..106b1aadbd1076927e1895fd895b3f91d0e21629 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -45,7 +45,7 @@ class PreprocessingPassContext
 
   SmtEngine* getSmt() { return d_smt; }
   TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
-  prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
+  prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
   context::Context* getUserContext() { return d_smt->d_userContext; }
   context::Context* getDecisionContext() { return d_smt->d_context; }
   RemoveTermFormulas* getIteRemover() { return d_iteRemover; }

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 3cc0ed120c837518ad8cc37d229a27ddd7655732..f00bba000677cd1fac3443a2e54f4ed437151f5a 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -27,8 +27,7 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
 public:
 
   MinisatSatSolver(StatisticsRegistry* registry);
-  virtual ~MinisatSatSolver();
-;
+  ~MinisatSatSolver() override;
 
   static SatVariable     toSatVariable(Minisat::Var var);
   static Minisat::Lit    toMinisatLit(SatLiteral lit);

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 546567b98fe347560ba7d146257be5a9c49bc61f..19ee2919166457c73c3a7b8d7b8758be1340a169 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -120,6 +120,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 PropEngine::~PropEngine() {
   Debug("prop") << "Destructing the PropEngine" << endl;
   d_decisionEngine->shutdown();
+  d_decisionEngine.reset(nullptr);
   delete d_cnfStream;
   delete d_registrar;
   delete d_satSolver;

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 9898f3f872e35ccbd441b04b10b7e538c1910a5f..b9c518fd6af20a93952a4cb9cfb4094ba10ab10c 100644 (file)
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -132,10 +132,13 @@ public:
 
 };/* class BVSatSolverInterface */
 
+class DPLLSatSolverInterface : public SatSolver
+{
+ public:
+  virtual ~DPLLSatSolverInterface(){};
 
-class DPLLSatSolverInterface: public SatSolver {
-public:
-  virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0;
+  virtual void initialize(context::Context* context,
+                          prop::TheoryProxy* theoryProxy) = 0;
 
   virtual void push() = 0;
 
@@ -152,7 +155,7 @@ public:
   virtual void requirePhase(SatLiteral lit) = 0;
 
   virtual bool isDecision(SatVariable decn) const = 0;
-};/* class DPLLSatSolverInterface */
+}; /* class DPLLSatSolverInterface */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ec16409a711740772f14ead84a5ce90daedec7f7..bfb126e9e7622118e1fdbc0cfb4cadaae76a1636 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -851,8 +851,8 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_userLevels(),
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
-      d_theoryEngine(NULL),
-      d_propEngine(NULL),
+      d_theoryEngine(nullptr),
+      d_propEngine(nullptr),
       d_proofManager(NULL),
       d_definedFunctions(NULL),
       d_fmfRecFunctionsDefined(NULL),
@@ -936,14 +936,18 @@ void SmtEngine::finishInit()
   Trace("smt-debug") << "Making decision engine..." << std::endl;
 
   Trace("smt-debug") << "Making prop engine..." << std::endl;
-  d_propEngine = new PropEngine(d_theoryEngine,
-                                d_context,
-                                d_userContext,
-                                d_private->getReplayLog(),
-                                d_replayStream);
+  /* force destruction of referenced PropEngine to enforce that statistics
+   * are unregistered by the obsolete PropEngine object before registered
+   * again by the new PropEngine object */
+  d_propEngine.reset(nullptr);
+  d_propEngine.reset(new PropEngine(d_theoryEngine,
+                                    d_context,
+                                    d_userContext,
+                                    d_private->getReplayLog(),
+                                    d_replayStream));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
-  d_theoryEngine->setPropEngine(d_propEngine);
+  d_theoryEngine->setPropEngine(getPropEngine());
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
 
@@ -1022,10 +1026,12 @@ void SmtEngine::shutdown() {
     internalPop(true);
   }
 
-  if(d_propEngine != NULL) {
+  if (d_propEngine != nullptr)
+  {
     d_propEngine->shutdown();
   }
-  if(d_theoryEngine != NULL) {
+  if (d_theoryEngine != nullptr)
+  {
     d_theoryEngine->shutdown();
   }
 }
@@ -1082,8 +1088,7 @@ SmtEngine::~SmtEngine()
 
     delete d_theoryEngine;
     d_theoryEngine = NULL;
-    delete d_propEngine;
-    d_propEngine = NULL;
+    d_propEngine.reset(nullptr);
 
     delete d_stats;
     d_stats = NULL;
@@ -5546,24 +5551,49 @@ void SmtEngine::reset()
 void SmtEngine::resetAssertions()
 {
   SmtScope smts(this);
+
+  if (!d_fullyInited)
+  {
+    // We're still in Start Mode, nothing asserted yet, do nothing.
+    // (see solver execution modes in the SMT-LIB standard)
+    Assert(d_context->getLevel() == 0);
+    Assert(d_userContext->getLevel() == 0);
+    DeleteAndClearCommandVector(d_modelGlobalCommands);
+    return;
+  }
+
   doPendingPops();
 
   Trace("smt") << "SMT resetAssertions()" << endl;
-  if(Dump.isOn("benchmark")) {
+  if (Dump.isOn("benchmark"))
+  {
     Dump("benchmark") << ResetAssertionsCommand();
   }
 
-  while(!d_userLevels.empty()) {
+  while (!d_userLevels.empty())
+  {
     pop();
   }
 
-  // Also remember the global push/pop around everything.
+  // Remember the global push/pop around everything when beyond Start mode
+  // (see solver execution modes in the SMT-LIB standard)
   Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
   d_context->popto(0);
   d_userContext->popto(0);
   DeleteAndClearCommandVector(d_modelGlobalCommands);
   d_userContext->push();
   d_context->push();
+
+  /* Create new PropEngine.
+   * First force destruction of referenced PropEngine to enforce that
+   * statistics are unregistered by the obsolete PropEngine object before
+   * registered again by the new PropEngine object */
+  d_propEngine.reset(nullptr);
+  d_propEngine.reset(new PropEngine(d_theoryEngine,
+                                    d_context,
+                                    d_userContext,
+                                    d_private->getReplayLog(),
+                                    d_replayStream));
 }
 
 void SmtEngine::interrupt()

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1424352ef64cd9782d38cd1dac0bbcc2a01c41e2..61f8b75405b00032651c21bad6b202d5098707c7 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -859,6 +859,9 @@ class CVC4_PUBLIC SmtEngine
   SmtEngine(const SmtEngine&) = delete;
   SmtEngine& operator=(const SmtEngine&) = delete;
 
+  /** Get a pointer to the PropEngine owned by this SmtEngine. */
+  prop::PropEngine* getPropEngine() { return d_propEngine.get(); }
+
   /**
    * Check that a generated proof (via getProof()) checks.
    */
@@ -1063,7 +1066,7 @@ class CVC4_PUBLIC SmtEngine
   /** The theory engine */
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */
-  prop::PropEngine* d_propEngine;
+  std::unique_ptr<prop::PropEngine> d_propEngine;
 
   /** The proof manager */
   ProofManager* d_proofManager;

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 7f93a690e0dd21ca046c1ee8a7cd38dc3444c718..ee7d1bb8721cc2f8b8851d487fb3ed76bc52ea67 100644 (file)
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -157,9 +157,11 @@ StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
 void StatisticsRegistry::registerStat(Stat* s)
 {
 #ifdef CVC4_STATISTICS_ON
-  PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
-                "Statistic `%s' was not registered with this registry.",
-                s->getName().c_str());
+  PrettyCheckArgument(
+      d_stats.find(s) == d_stats.end(),
+      s,
+      "Statistic `%s' is already registered with this registry.",
+      s->getName().c_str());
   d_stats.insert(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat_() */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6579894e9489afafd91f5a8cd4354ba137b3e5e8..a9017ac2005950f5accb592ca028b5cfc2b249f7 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -816,7 +816,6 @@ set(regress_0_tests
   regress0/rels/rel_transpose_7.cvc
   regress0/rels/relations-ops.smt2
   regress0/rels/rels-sharing-simp.cvc
-  regress0/reset-assertions.smt2
   regress0/sep/dispose-1.smt2
   regress0/sep/dup-nemp.smt2
   regress0/sep/issue3720-check-model.smt2
@@ -897,6 +896,9 @@ set(regress_0_tests
   regress0/smtlib/get-unsat-assumptions.smt2
   regress0/smtlib/global-decls.smt2
   regress0/smtlib/reason-unknown.smt2
+  regress0/smtlib/reset-assertions1.smt2
+  regress0/smtlib/reset-assertions2.smt2
+  regress0/smtlib/reset-assertions-global.smt2
   regress0/smtlib/reset-force-logic.smt2
   regress0/smtlib/reset-set-logic.smt2
   regress0/smtlib/set-info-status.smt2

diff --git a/test/regress/regress0/reset-assertions.smt2 b/test/regress/regress0/reset-assertions.smt2
deleted file mode 100644 (file)
index 3c37f2c..0000000
--- a/test/regress/regress0/reset-assertions.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-; EXPECT: sat
-; EXPECT: sat
-(set-logic QF_ALL)
-(set-option :incremental true)
-(set-option :produce-models true)
-
-(declare-fun x () Real)
-(declare-fun y () Real)
-(assert (> x 0.0))
-(assert (> y 0.0))
-(assert (= (+ (* 2 x) y) 4))
-(check-sat)
-(reset-assertions)
-
-(declare-fun a () (Array Int Int))
-(assert (= (select a 4) 10))
-(check-sat)

diff --git a/test/regress/regress0/smtlib/reset-assertions-global.smt2 b/test/regress/regress0/smtlib/reset-assertions-global.smt2
new file mode 100644 (file)
index 0000000..f6e2aae
--- /dev/null
+++ b/test/regress/regress0/smtlib/reset-assertions-global.smt2
@@ -0,0 +1,18 @@
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+(set-option :global-declarations true)
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(assert (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))
+(assert (= #b000 x2))
+(check-sat)
+(reset-assertions)
+(assert (= x2 x1))
+(check-sat)
+(reset-assertions)
+(assert (distinct x1 x1))
+(check-sat)

diff --git a/test/regress/regress0/smtlib/reset-assertions1.smt2 b/test/regress/regress0/smtlib/reset-assertions1.smt2
new file mode 100644 (file)
index 0000000..7b4006c
--- /dev/null
+++ b/test/regress/regress0/smtlib/reset-assertions1.smt2
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun v0 () (_ BitVec 4))
+(set-option :produce-models true)
+(reset-assertions)
+(set-option :incremental true)
+(assert (and (= v0 (_ bv0 4)) (distinct v0 (_ bv0 4))))
+(check-sat)
+(reset-assertions)
+(check-sat)

diff --git a/test/regress/regress0/smtlib/reset-assertions2.smt2 b/test/regress/regress0/smtlib/reset-assertions2.smt2
new file mode 100644 (file)
index 0000000..3c37f2c
--- /dev/null
+++ b/test/regress/regress0/smtlib/reset-assertions2.smt2
@@ -0,0 +1,17 @@
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_ALL)
+(set-option :incremental true)
+(set-option :produce-models true)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (> x 0.0))
+(assert (> y 0.0))
+(assert (= (+ (* 2 x) y) 4))
+(check-sat)
+(reset-assertions)
+
+(declare-fun a () (Array Int Int))
+(assert (= (select a 4) 10))
+(check-sat)