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

Do not decide on unused variables

Browse source
This commit is contained in:
Guillaume Bury 2017-01-17 12:29:39 +01:00
parent c77c997ab8
commit e8e619f3c7
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/core/internal.ml
View file

@ -369,6 +369,7 @@ module Make
let attach_clause c = let attach_clause c =
assert (not c.attached); assert (not c.attached);
Log.debugf debug "Attaching %a" (fun k -> k St.pp_clause c); Log.debugf debug "Attaching %a" (fun k -> k St.pp_clause c);
Array.iter (fun a -> a.var.used <- a.var.used + 1) c.atoms;
Vec.push c.atoms.(0).neg.watched c; Vec.push c.atoms.(0).neg.watched c;
Vec.push c.atoms.(1).neg.watched c; Vec.push c.atoms.(1).neg.watched c;
c.attached <- true; c.attached <- true;
@ -986,7 +987,10 @@ module Make
(* Decide on a new literal, and enqueue it into the trail *) (* Decide on a new literal, and enqueue it into the trail *)
let rec pick_branch_aux atom: unit = let rec pick_branch_aux atom: unit =
let v = atom.var in let v = atom.var in
if v.v_level >= 0 then begin if v.used <= 0 then begin
assert (v.used = 0);
pick_branch_lit ()
end else if v.v_level >= 0 then begin
assert (v.pa.is_true || v.na.is_true); assert (v.pa.is_true || v.na.is_true);
pick_branch_lit () pick_branch_lit ()
end else match Plugin.eval atom.lit with end else match Plugin.eval atom.lit with