summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/justification_heuristic.cpp47
-rw-r--r--src/decision/justification_heuristic.h2
-rw-r--r--src/preprocessing/preprocessing_pass_context.h2
-rw-r--r--src/prop/minisat/minisat.h3
-rw-r--r--src/prop/prop_engine.cpp1
-rw-r--r--src/prop/sat_solver.h11
-rw-r--r--src/smt/smt_engine.cpp60
-rw-r--r--src/smt/smt_engine.h5
-rw-r--r--src/util/statistics_registry.cpp8
-rw-r--r--test/regress/CMakeLists.txt4
-rw-r--r--test/regress/regress0/smtlib/reset-assertions-global.smt218
-rw-r--r--test/regress/regress0/smtlib/reset-assertions1.smt211
-rw-r--r--test/regress/regress0/smtlib/reset-assertions2.smt2 (renamed from test/regress/regress0/reset-assertions.smt2)0
13 files changed, 121 insertions, 51 deletions
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<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 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<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 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
index 3c37f2cba..3c37f2cba 100644
--- a/test/regress/regress0/reset-assertions.smt2
+++ b/test/regress/regress0/smtlib/reset-assertions2.smt2
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback