diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-03 17:30:41 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-03 17:30:41 -0700 |
| commit | fee2021bb7419630853cbd0b20afa1af5e2eb1e9 (patch) | |
| tree | e4d6ff6757bfffb11cb1f101cf1fb6d1b16f784f | |
| parent | 5248998baff098d6b28a80f7bd2f286dfa942148 (diff) | |
[BVMiniSat] Avoid duplicates in conflicts (#1745)
If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.
The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.
| -rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 2d6e318f2..885e429f0 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -675,7 +675,10 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) if (reason(x) == CRef_Undef) { assert(marker[x] == 2); assert(level(x) > 0); - out_conflict.push(~trail[i]); + if (~trail[i] != p) + { + out_conflict.push(~trail[i]); + } } else { Clause& c = ca[reason(x)]; if(d_bvp){ |