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

Fix for mid-solving clause adding

Browse source
This commit is contained in:
Guillaume Bury 2014-11-23 20:49:16 +01:00
parent be4ce92d08
commit ff83cb70e9
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
sat/solver.ml
View file

@ -268,6 +268,7 @@ module Make (F : Formula_intf.S)
let enqueue a lvl reason =
assert (not a.is_true && not a.neg.is_true &&
a.var.level < 0 && a.var.reason = None && lvl >= 0);
assert (lvl = decision_level ());
(* keep the reason for proof/unsat-core *)
(*let reason = if lvl = 0 then None else reason in*)
a.is_true <- true;
@ -408,7 +409,7 @@ module Make (F : Formula_intf.S)
match atoms with
| [] ->
report_unsat init0;
| a::_::_ ->
| a::b::_ ->
let name = fresh_name () in
let clause = make_clause name atoms size (history <> History []) history in
Log.debug 10 "New clause : %a" St.pp_clause init0;
@ -418,6 +419,10 @@ module Make (F : Formula_intf.S)
let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
cancel_until lvl;
add_boolean_conflict clause
end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
cancel_until lvl;
enqueue a lvl (Some clause)
end
| [a] ->
cancel_until 0;