summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/minisat/core/Solver.cc17
-rw-r--r--src/prop/minisat/core/Solver.h6
-rw-r--r--src/prop/minisat/minisat.cpp2
-rw-r--r--src/prop/minisat/minisat.h2
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc2
-rw-r--r--src/prop/prop_engine.cpp6
-rw-r--r--src/prop/prop_engine.h6
-rw-r--r--src/prop/sat_solver.h6
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress0/push-pop/bug1990.smt214
11 files changed, 53 insertions, 11 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 2136f22df..aa59f18e1 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -344,8 +344,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
// Fit to size
ps.shrink(i - j);
- // If we are in solve or decision level > 0
- if (minisat_busy || decisionLevel() > 0) {
+ // If we are in solve_ or propagate
+ if (minisat_busy)
+ {
Debug("pf::sat") << "Add clause adding a new lemma: ";
for (int k = 0; k < ps.size(); ++k) {
Debug("pf::sat") << ps[k] << " ";
@@ -369,6 +370,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
// Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
// lemmas_proof_id.push(proof_id);
} else {
+ assert(decisionLevel() == 0);
+
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
if(PROOF_ON()) {
@@ -534,9 +537,7 @@ void Solver::cancelUntil(int level) {
}
}
-void Solver::popTrail() {
- cancelUntil(0);
-}
+void Solver::resetTrail() { cancelUntil(0); }
//=================================================================================================
// Major methods:
@@ -1391,7 +1392,7 @@ lbool Solver::solve_()
ScopedBool scoped_bool(minisat_busy, true);
- popTrail();
+ assert(decisionLevel() == 0);
model.clear();
conflict.clear();
@@ -1580,8 +1581,8 @@ void Solver::garbageCollect()
void Solver::push()
{
assert(enable_incremental);
+ assert(decisionLevel() == 0);
- popTrail();
++assertionLevel;
Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
trail_ok.push(ok);
@@ -1596,8 +1597,6 @@ void Solver::pop()
{
assert(enable_incremental);
- // Pop the trail to 0 level
- popTrail();
assert(decisionLevel() == 0);
// Pop the trail below the user level
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 99c47e045..c27d8a18b 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -169,6 +169,11 @@ public:
void push ();
void pop ();
+ /*
+ * Reset the decisions in the DPLL(T) SAT solver at the current assertion
+ * level.
+ */
+ void resetTrail();
// addClause returns the ClauseId corresponding to the clause added in the
// reference parameter id.
bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); // Add a clause to the solver.
@@ -393,7 +398,6 @@ protected:
void theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Adds lemmas.
CRef updateLemmas (); // Add the lemmas, backtraking if necessary and return a conflict if there is one
void cancelUntil (int level); // Backtrack until a certain level.
- void popTrail (); // Backtrack the trail to the previous push position
int analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - true if p is redundant
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 514338fd9..73a6f0d5e 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -232,6 +232,8 @@ void MinisatSatSolver::pop() {
d_minisat->pop();
}
+void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
+
/// Statistics for MinisatSatSolver
MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) :
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 58e02179c..ea673a15d 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -74,6 +74,8 @@ public:
void pop() override;
+ void resetTrail() override;
+
void requirePhase(SatLiteral lit) override;
bool flipDecision() override;
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 9b551fa70..96fea2147 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -120,7 +120,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
toDimacs();
return l_Undef;
}
- popTrail();
+ assert(decisionLevel() == 0);
vec<Var> extra_frozen;
lbool result = l_True;
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 23f7ea6b5..b09e7a088 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -281,6 +281,12 @@ void PropEngine::pop() {
Debug("prop") << "pop()" << endl;
}
+void PropEngine::resetTrail()
+{
+ d_satSolver->resetTrail();
+ Debug("prop") << "resetTrail()" << endl;
+}
+
unsigned PropEngine::getAssertionLevel() const {
return d_satSolver->getAssertionLevel();
}
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index f3a69be96..edc828418 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -213,6 +213,12 @@ public:
*/
void pop();
+ /*
+ * Reset the decisions in the DPLL(T) SAT solver at the current assertion
+ * level.
+ */
+ void resetTrail();
+
/**
* Get the assertion level of the SAT solver.
*/
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 4dc95e060..86e0f1577 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -148,6 +148,12 @@ public:
virtual void pop() = 0;
+ /*
+ * Reset the decisions in the DPLL(T) SAT solver at the current assertion
+ * level.
+ */
+ virtual void resetTrail() = 0;
+
virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
virtual void requirePhase(SatLiteral lit) = 0;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2836f73b4..69cea8b06 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4709,6 +4709,8 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
}
}
+ d_propEngine->resetTrail();
+
// Pop the context
if (didInternalPush)
{
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 4a7267a60..d25da1b62 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -570,6 +570,7 @@ REG0_TESTS = \
regress0/push-pop/boolean/fuzz_48.smt2 \
regress0/push-pop/boolean/fuzz_49.smt2 \
regress0/push-pop/boolean/fuzz_50.smt2 \
+ regress0/push-pop/bug1990.smt2 \
regress0/push-pop/bug233.cvc \
regress0/push-pop/bug654-dd.smt2 \
regress0/push-pop/bug691.smt2 \
diff --git a/test/regress/regress0/push-pop/bug1990.smt2 b/test/regress/regress0/push-pop/bug1990.smt2
new file mode 100644
index 000000000..f0cde3113
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug1990.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic QF_SAT)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(assert (or v1 v2))
+(check-sat)
+(assert false)
+(push)
+(check-sat)
+(pop)
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback