From e9f4cec2cad02e270747759223090c16b9d2d44c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 10 Mar 2020 14:51:32 -0700 Subject: [PATCH] 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. --- src/decision/justification_heuristic.cpp | 47 ++++++++------- src/decision/justification_heuristic.h | 2 +- .../preprocessing_pass_context.h | 2 +- src/prop/minisat/minisat.h | 3 +- src/prop/prop_engine.cpp | 1 + src/prop/sat_solver.h | 11 ++-- src/smt/smt_engine.cpp | 60 ++++++++++++++----- src/smt/smt_engine.h | 5 +- src/util/statistics_registry.cpp | 8 ++- test/regress/CMakeLists.txt | 4 +- .../smtlib/reset-assertions-global.smt2 | 18 ++++++ .../regress0/smtlib/reset-assertions1.smt2 | 11 ++++ .../reset-assertions2.smt2} | 0 13 files changed, 121 insertions(+), 51 deletions(-) create mode 100644 test/regress/regress0/smtlib/reset-assertions-global.smt2 create mode 100644 test/regress/regress0/smtlib/reset-assertions1.smt2 rename test/regress/regress0/{reset-assertions.smt2 => smtlib/reset-assertions2.smt2} (100%) diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index a6b6cbd8f..ce79d6ca0 100644 --- 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 b2c325628..bb426ad1e 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -57,7 +57,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { context::CDO d_prvsIndex; context::CDO 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 b32a2a86f..106b1aadb 100644 --- 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 3cc0ed120..f00bba000 100644 --- 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 546567b98..19ee29191 100644 --- 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 9898f3f87..b9c518fd6 100644 --- 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 ec16409a7..bfb126e9e 100644 --- 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 1424352ef..61f8b7540 100644 --- 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 d_propEngine; /** The proof manager */ ProofManager* d_proofManager; diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 7f93a690e..ee7d1bb87 100644 --- 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 6579894e9..a9017ac20 100644 --- 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/smtlib/reset-assertions-global.smt2 b/test/regress/regress0/smtlib/reset-assertions-global.smt2 new file mode 100644 index 000000000..f6e2aaed2 --- /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 index 000000000..7b4006c5d --- /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/reset-assertions.smt2 b/test/regress/regress0/smtlib/reset-assertions2.smt2 similarity index 100% rename from test/regress/regress0/reset-assertions.smt2 rename to test/regress/regress0/smtlib/reset-assertions2.smt2 -- 2.30.2