From 97f1e4592b617a5682a8e990b4f82d3cbb6ee037 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 27 Mar 2020 16:37:14 -0700 Subject: 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. --- src/proof/proof_manager.cpp | 83 +++++++++++++++-------------- src/proof/proof_manager.h | 13 +++-- src/prop/prop_engine.cpp | 5 ++ src/smt/smt_engine.cpp | 3 -- test/regress/CMakeLists.txt | 1 + test/regress/regress0/smtlib/issue4151.smt2 | 13 +++++ 6 files changed, 67 insertions(+), 51 deletions(-) create mode 100644 test/regress/regress0/smtlib/issue4151.smt2 diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 14556708b..f9e3293fa 100644 --- 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(getSatProof()), + getSatProof(), static_cast(getCnfProof()), static_cast(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(true); Node false_node = NodeManager::currentNM()->mkConst(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 ec845e41d..a59f36858 100644 --- 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 d_satProof; + std::unique_ptr d_cnfProof; + std::unique_ptr 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 19ee29191..2436aed04 100644 --- 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 299cc357b..30c1cd0f5 100644 --- 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(true)); - d_propEngine->assertFormula(NodeManager::currentNM()->mkConst(false).notNode()); } void SmtEngine::shutdown() { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8382e40fc..a5acd62fb 100644 --- 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 index 000000000..629ec48b6 --- /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) -- cgit v1.2.3