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

Fixed incomplete proofs due to level 0 propagation

Browse source
This commit is contained in:
Guillaume Bury 2014-11-15 20:23:11 +01:00
parent c6dd201014
commit bfce3e54a2
2 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
sat/solver.ml
View file

@ -624,7 +624,7 @@ module Make (F : Formula_intf.S)
exception Trivial exception Trivial
(* TODO: could be more efficient than [@] everywhere? *) (* TODO: could be more efficient than [@] everywhere? *)
let partition atoms init = let partition atoms init0 =
let rec partition_aux trues unassigned falses init = function let rec partition_aux trues unassigned falses init = function
| [] -> trues @ unassigned @ falses, init | [] -> trues @ unassigned @ falses, init
| a::r -> | a::r ->
@ -634,13 +634,13 @@ module Make (F : Formula_intf.S)
else if a.neg.is_true then else if a.neg.is_true then
if a.var.level = 0 then match a.var.vpremise with if a.var.level = 0 then match a.var.vpremise with
| History v -> | History v ->
partition_aux trues unassigned falses partition_aux trues unassigned falses [init0] r
(List.rev_append v init) r
| Lemma _ -> assert false | Lemma _ -> assert false
else partition_aux trues unassigned (a::falses) init r else
partition_aux trues unassigned (a::falses) init r
else partition_aux trues (a::unassigned) falses init r else partition_aux trues (a::unassigned) falses init r
in in
partition_aux [] [] [] init atoms partition_aux [] [] [] [] atoms
let add_clause ~cnumber atoms = let add_clause ~cnumber atoms =
@ -655,12 +655,12 @@ module Make (F : Formula_intf.S)
(fun (atoms, init) a -> (fun (atoms, init) a ->
if a.is_true then raise Trivial; if a.is_true then raise Trivial;
if a.neg.is_true then match a.var.vpremise with if a.neg.is_true then match a.var.vpremise with
| History v -> atoms, (List.rev_append v init) | History v -> atoms, [init0]
| Lemma p -> assert false | Lemma p -> assert false
else a::atoms, init else a::atoms, init
) ([], [init0]) atoms in ) ([], []) atoms in
List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
else partition atoms [init0] else partition atoms init0
in in
let size = List.length atoms in let size = List.length atoms in
match atoms with match atoms with
@ -669,7 +669,7 @@ module Make (F : Formula_intf.S)
| a::_::_ -> | a::_::_ ->
let name = fresh_name () in let name = fresh_name () in
let clause = make_clause name atoms size false (History init) in let clause = make_clause name atoms size (init <> []) (History init) in
attach_clause clause; attach_clause clause;
Vec.push env.clauses clause; Vec.push env.clauses clause;
if a.neg.is_true then begin if a.neg.is_true then begin
@ -681,7 +681,7 @@ module Make (F : Formula_intf.S)
| [a] -> | [a] ->
cancel_until 0; cancel_until 0;
a.var.vpremise <- History init; a.var.vpremise <- History init;
enqueue a 0 None; enqueue a 0 (match init with [init0] -> Some init0 | _ -> None);
match propagate () with match propagate () with
None -> () | Some confl -> report_unsat confl None -> () | Some confl -> report_unsat confl
with Trivial -> () with Trivial -> ()

2
tests/unsat/test-010.smt2 Normal file
View file

@ -0,0 +1,2 @@
(assert (and a (=> a b) (not b)))
(check-sat)