diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-24 19:41:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-24 19:41:33 +0000 |
commit | baf045ed88c2f72f435547e2de6424992b8c0810 (patch) | |
tree | 39598bfc0bf118e96bba6f076882829d6b0bd5f5 /src/prop/minisat | |
parent | 6809eb4a11f5cf2188f6492c683c9183045419a3 (diff) |
fix for bug 429
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fbaef61f2..b5d524c31 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -265,11 +265,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); ) - if(assertionLevel > 0) { - // remember to unset it on user pop - Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl; - trail_user.push(ps[0]); - } return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); } else return ok; } else { @@ -686,6 +681,11 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) // Enqueue to the theory proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); } + if (from == CRef_Undef) { + if (assertionLevel > 0) { + trail_user.push(p); + } + } } @@ -1620,12 +1620,6 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; uncheckedEnqueue(lemma[0], lemma_ref); - if(lemma.size() == 1 && assertionLevel > 0) { - assert(decisionLevel() == 0); - // remember to unset it on user pop - Debug("minisat") << "got new unit (survived downward during updateLemmas()) " << lemma[0] << " at assertion level " << assertionLevel << std::endl; - trail_user.push(lemma[0]); - } } } } |