diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 16:01:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 16:01:48 +0000 |
commit | 6d4822f197ccd235175669f199e922aa12eda4b1 (patch) | |
tree | 4da9f061921d35f27658e817ac411205fbecb2b6 /src/prop/minisat | |
parent | 1a890e13218be6e87dbf0124b03a73420631d816 (diff) |
removing duplicate literals in explanations of propagations
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 6ee508eba..71f252291 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -199,6 +199,7 @@ CRef Solver::reason(Var x) { // Compute the assertion level for this clause int explLevel = 0; int i, j; + Lit prev = lit_Undef; for (i = 0, j = 0; i < explanation.size(); ++ i) { int varLevel = intro_level(var(explanation[i])); if (varLevel > explLevel) { @@ -207,8 +208,8 @@ CRef Solver::reason(Var x) { Assert(value(explanation[i]) != l_Undef); Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); // ignore zero level literals - if (i == 0 || level(var(explanation[i])) > 0) { - explanation[j++] = explanation[i]; + if (i == 0 || (level(var(explanation[i])) > 0 && explanation[i] != prev)) { + prev = explanation[j++] = explanation[i]; } } explanation.shrink(i - j); |