Fix issues with unsat cores and reset-assertions (#4159)

Fixes #4151. Commit e9f4cec2cad02e270747759223090c16b9d2d44c fixed how
`(reset-assertions)` is handled by destroying and recreating the
`PropEngine` owned by `SmtEngine`. When unsat cores are enabled,
creating a `PropEngine` triggers the creation of a SAT proof and a CNF
proof. In the `ProofManager`, we had assertions that checked that those
kinds of proofs were only created once, which is not true anymore. This
commit removes the assertions, cleans up the memory management in
`ProofManager` to use `std::unique_ptr` and makes all the
`ProofManager::init*` methods non-static for consistency.

The commit also fixes an additional issue that I encountered while
testing the fix: When creating the new `PropEngine`, we were not
asserting `true` and `(not false)`, which lead to an error if we tried
to get the unsat core after a `(reset-assertion)` command and we had
asserted `(assert false)`. The commit fixes this by asserting `true` and
`(not false)` in the constructor of `PropEngine`.

The regression test is an extension of the example in #4151 and covers
both issues.

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 14556708bb12f2b1b86a5304971e29edeb11ab71..f9e3293fa4a2dce0116b493c6fcd6927b6fbfc67 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -60,9 +60,9 @@ std::string append(const std::string& str, uint64_t num) {
 
 ProofManager::ProofManager(context::Context* context, ProofFormat format)
     : d_context(context),
-      d_satProof(NULL),
-      d_cnfProof(NULL),
-      d_theoryProof(NULL),
+      d_satProof(nullptr),
+      d_cnfProof(nullptr),
+      d_theoryProof(nullptr),
       d_inputFormulas(),
       d_inputCoreFormulas(context),
       d_outputCoreFormulas(context),
@@ -73,11 +73,7 @@ ProofManager::ProofManager(context::Context* context, ProofFormat format)
 {
 }
 
-ProofManager::~ProofManager() {
-  if (d_satProof) delete d_satProof;
-  if (d_cnfProof) delete d_cnfProof;
-  if (d_theoryProof) delete d_theoryProof;
-}
+ProofManager::~ProofManager() {}
 
 ProofManager* ProofManager::currentPM() {
   return smt::currentProofManager();
@@ -89,26 +85,29 @@ const Proof& ProofManager::getProof(SmtEngine* smt)
     Assert(currentPM()->d_format == LFSC);
     currentPM()->d_fullProof.reset(new LFSCProof(
         smt,
-        static_cast<CoreSatProof*>(getSatProof()),
+        getSatProof(),
         static_cast<LFSCCnfProof*>(getCnfProof()),
         static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine())));
   }
   return *(currentPM()->d_fullProof);
 }
 
-CoreSatProof* ProofManager::getSatProof() {
+CoreSatProof* ProofManager::getSatProof()
+{
   Assert(currentPM()->d_satProof);
-  return currentPM()->d_satProof;
+  return currentPM()->d_satProof.get();
 }
 
-CnfProof* ProofManager::getCnfProof() {
+CnfProof* ProofManager::getCnfProof()
+{
   Assert(currentPM()->d_cnfProof);
-  return currentPM()->d_cnfProof;
+  return currentPM()->d_cnfProof.get();
 }
 
-TheoryProofEngine* ProofManager::getTheoryProofEngine() {
+TheoryProofEngine* ProofManager::getTheoryProofEngine()
+{
   Assert(currentPM()->d_theoryProof != NULL);
-  return currentPM()->d_theoryProof;
+  return currentPM()->d_theoryProof.get();
 }
 
 UFProof* ProofManager::getUfProof() {
@@ -141,43 +140,45 @@ SkolemizationManager* ProofManager::getSkolemizationManager() {
   return &(currentPM()->d_skolemizationManager);
 }
 
-void ProofManager::initSatProof(Minisat::Solver* solver) {
-  Assert(currentPM()->d_satProof == NULL);
-  Assert(currentPM()->d_format == LFSC);
-  currentPM()->d_satProof = new CoreSatProof(solver, d_context, "");
+void ProofManager::initSatProof(Minisat::Solver* solver)
+{
+  Assert(d_format == LFSC);
+  // Destroy old instance before initializing new one to avoid issues with
+  // registering stats
+  d_satProof.reset();
+  d_satProof.reset(new CoreSatProof(solver, d_context, ""));
 }
 
 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
-                                context::Context* ctx) {
-  ProofManager* pm = currentPM();
-  Assert(pm->d_satProof != NULL);
-  Assert(pm->d_cnfProof == NULL);
-  Assert(pm->d_format == LFSC);
-  CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, "");
-  pm->d_cnfProof = cnf;
+                                context::Context* ctx)
+{
+  Assert(d_satProof != nullptr);
+  Assert(d_format == LFSC);
+
+  d_cnfProof.reset(new LFSCCnfProof(cnfStream, ctx, ""));
 
   // true and false have to be setup in a special way
   Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
   Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
 
-  pm->d_cnfProof->pushCurrentAssertion(true_node);
-  pm->d_cnfProof->pushCurrentDefinition(true_node);
-  pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getTrueUnit());
-  pm->d_cnfProof->popCurrentAssertion();
-  pm->d_cnfProof->popCurrentDefinition();
-
-  pm->d_cnfProof->pushCurrentAssertion(false_node);
-  pm->d_cnfProof->pushCurrentDefinition(false_node);
-  pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getFalseUnit());
-  pm->d_cnfProof->popCurrentAssertion();
-  pm->d_cnfProof->popCurrentDefinition();
+  d_cnfProof->pushCurrentAssertion(true_node);
+  d_cnfProof->pushCurrentDefinition(true_node);
+  d_cnfProof->registerConvertedClause(d_satProof->getTrueUnit());
+  d_cnfProof->popCurrentAssertion();
+  d_cnfProof->popCurrentDefinition();
 
+  d_cnfProof->pushCurrentAssertion(false_node);
+  d_cnfProof->pushCurrentDefinition(false_node);
+  d_cnfProof->registerConvertedClause(d_satProof->getFalseUnit());
+  d_cnfProof->popCurrentAssertion();
+  d_cnfProof->popCurrentDefinition();
 }
 
-void ProofManager::initTheoryProofEngine() {
-  Assert(currentPM()->d_theoryProof == NULL);
-  Assert(currentPM()->d_format == LFSC);
-  currentPM()->d_theoryProof = new LFSCTheoryProofEngine();
+void ProofManager::initTheoryProofEngine()
+{
+  Assert(d_theoryProof == NULL);
+  Assert(d_format == LFSC);
+  d_theoryProof.reset(new LFSCTheoryProofEngine());
 }
 
 std::string ProofManager::getInputClauseName(ClauseId id,

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index ec845e41d750eda4a2e209c3953e90f0380584ad..a59f3685866e1c35189d55c136f9a9b8b3aa270d 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -143,9 +143,9 @@ private:
 class ProofManager {
   context::Context* d_context;
 
-  CoreSatProof*  d_satProof;
-  CnfProof*      d_cnfProof;
-  TheoryProofEngine* d_theoryProof;
+  std::unique_ptr<CoreSatProof> d_satProof;
+  std::unique_ptr<CnfProof> d_cnfProof;
+  std::unique_ptr<TheoryProofEngine> d_theoryProof;
 
   // information that will need to be shared across proofs
   ExprSet    d_inputFormulas;
@@ -179,10 +179,9 @@ public:
   static ProofManager* currentPM();
 
   // initialization
-  void         initSatProof(Minisat::Solver* solver);
-  static void         initCnfProof(CVC4::prop::CnfStream* cnfStream,
-                                   context::Context* ctx);
-  static void         initTheoryProofEngine();
+  void initSatProof(Minisat::Solver* solver);
+  void initCnfProof(CVC4::prop::CnfStream* cnfStream, context::Context* ctx);
+  void initTheoryProofEngine();
 
   // getting various proofs
   static const Proof& getProof(SmtEngine* smt);

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 19ee2919166457c73c3a7b8d7b8758be1340a169..2436aed04cb539f8d057a02124a944b3508972b4 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -115,6 +115,11 @@ PropEngine::PropEngine(TheoryEngine* te,
   PROOF (
          ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
          );
+
+  NodeManager* nm = NodeManager::currentNM();
+  d_cnfStream->convertAndAssert(nm->mkConst(true), false, false, RULE_GIVEN);
+  d_cnfStream->convertAndAssert(
+      nm->mkConst(false).notNode(), false, false, RULE_GIVEN);
 }
 
 PropEngine::~PropEngine() {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 299cc357ba88896a8ec93f21c470c002553a5688..30c1cd0f55783d54dffd4f30dddd0c2a5e2f207b 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1017,9 +1017,6 @@ void SmtEngine::finalOptionsAreSet() {
 
   d_fullyInited = true;
   Assert(d_logic.isLocked());
-
-  d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
-  d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
 }
 
 void SmtEngine::shutdown() {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8382e40fce80ae9faa6ba060dbfdc1b57ce95e20..a5acd62fb5ee7b6bff98d787161858bc552fc7a1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -902,6 +902,7 @@ set(regress_0_tests
   regress0/smtlib/global-decls.smt2
   regress0/smtlib/issue4028.smt2
   regress0/smtlib/issue4077.smt2
+  regress0/smtlib/issue4151.smt2
   regress0/smtlib/reason-unknown.smt2
   regress0/smtlib/reset.smt2
   regress0/smtlib/reset-assertions1.smt2

diff --git a/test/regress/regress0/smtlib/issue4151.smt2 b/test/regress/regress0/smtlib/issue4151.smt2
new file mode 100644 (file)
index 0000000..629ec48
--- /dev/null
+++ b/test/regress/regress0/smtlib/issue4151.smt2
@@ -0,0 +1,13 @@
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: (
+; EXPECT: )
+(set-logic ALL)
+(set-option :incremental true)
+(set-option :produce-unsat-assumptions true)
+(set-option :produce-unsat-cores true)
+(check-sat)
+(reset-assertions)
+(assert false)
+(check-sat)
+(get-unsat-core)