simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Accept late conflict clauses, closes #4

Browse source
This commit is contained in:
Guillaume Bury 2016-08-04 21:31:51 +02:00
parent 12fed8a811
commit 7d57b3f1b5
1 changed files with 15 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/core/internal.ml
View file

@ -630,6 +630,9 @@ module Make
let size = ref 1 in let size = ref 1 in
let history = ref [] in let history = ref [] in
assert (decision_level () > 0); assert (decision_level () > 0);
let conflict_level =
Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
in
while !cond do while !cond do
begin match !c.cpremise with begin match !c.cpremise with
| History _ -> clause_bump_activity !c | History _ -> clause_bump_activity !c
@ -651,8 +654,8 @@ module Make
seen := q :: !seen; seen := q :: !seen;
if q.var.v_level > 0 then begin if q.var.v_level > 0 then begin
var_bump_activity q.var; var_bump_activity q.var;
if q.var.v_level >= decision_level () then begin if q.var.v_level >= conflict_level then begin
incr pathC incr pathC;
end else begin end else begin
learnt := q :: !learnt; learnt := q :: !learnt;
incr size; incr size;
@ -663,15 +666,23 @@ module Make
done; done;
(* look for the next node to expand *) (* look for the next node to expand *)
while not (get_atom !tr_ind).var.seen do decr tr_ind done; while
decr pathC; let q = get_atom !tr_ind in
(not q.var.seen) ||
(q.var.v_level < conflict_level)
do
decr tr_ind;
done;
let p = get_atom !tr_ind in let p = get_atom !tr_ind in
decr pathC;
decr tr_ind; decr tr_ind;
match !pathC, p.var.reason with match !pathC, p.var.reason with
| 0, _ -> | 0, _ ->
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
| n, Some Bcp cl -> | n, Some Bcp cl ->
assert (n > 0);
assert (p.var.v_level >= conflict_level);
c := cl c := cl
| n, _ -> assert false | n, _ -> assert false
done; done;