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

Fixed bug in if_sat

Browse source 
The trick using a bool ref to see if a new clause has been pushed
did not detect cases where new clauses were added using assume.
This commit is contained in:
Guillaume Bury 2015-12-08 13:11:05 +01:00
parent 9f421e6b1d
commit 3168d4ae2b
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
solver/internal.ml
View file

@ -682,11 +682,11 @@ module Make
propagate = slice_propagate; propagate = slice_propagate;
}) })
let full_slice tag = Th.({ let full_slice () = Th.({
start = 0; start = 0;
length = Vec.size env.elt_queue; length = Vec.size env.elt_queue;
get = slice_get; get = slice_get;
push = (fun cl proof -> tag := true; slice_push cl proof); push = slice_push;
propagate = (fun _ -> assert false); propagate = (fun _ -> assert false);
}) })
@ -887,9 +887,11 @@ module Make
n_of_conflicts := !n_of_conflicts *. env.restart_inc; n_of_conflicts := !n_of_conflicts *. env.restart_inc;
n_of_learnts := !n_of_learnts *. env.learntsize_inc n_of_learnts := !n_of_learnts *. env.learntsize_inc
| Sat -> | Sat ->
let tag = ref false in let nbc = env.nb_init_clauses in
Th.if_sat (full_slice tag); Th.if_sat (full_slice ());
if not !tag then raise Sat if env.nb_init_clauses = nbc &&
env.elt_head = Vec.size env.elt_queue then
raise Sat
end end
done done
with with