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

feat(sat): check proofs if asked to

Browse source
This commit is contained in:
Simon Cruanes 2021-08-02 23:13:18 -04:00
parent 2d081c554b
commit a205c429e7
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/main/main.ml
View file

@ -149,8 +149,9 @@ let main_cnf () : _ result =
~on_new_atom:(fun _ -> incr n_atoms) ~on_new_atom:(fun _ -> incr n_atoms)
~size:`Big () ~size:`Big ()
in in
S.Dimacs.parse_file solver !file >>= fun () -> S.Dimacs.parse_file solver !file >>= fun () ->
let r = S.solve solver in let r = S.solve ~check:!check solver in
if !p_stat then ( if !p_stat then (
Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d@.\ Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d@.\
; n-restarts: %d n-atoms: %d@." ; n-restarts: %d n-atoms: %d@."

9
src/main/pure_sat_solver.ml
View file

@ -40,7 +40,7 @@ module Dimacs = struct
E.of_exn_trace e E.of_exn_trace e
end end
let solve (solver:SAT.t) : (unit, string) result = let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
let res = let res =
Profile.with_ "solve" (fun () -> SAT.solve solver) Profile.with_ "solve" (fun () -> SAT.solve solver)
in in
@ -50,7 +50,12 @@ let solve (solver:SAT.t) : (unit, string) result =
| SAT.Sat _ -> | SAT.Sat _ ->
let t3 = Sys.time () -. t2 in let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f)@." t2 t3; Format.printf "Sat (%.3f/%.3f)@." t2 t3;
| SAT.Unsat _ -> | SAT.Unsat (module US) ->
if check then (
let pr = US.get_proof() in
SAT.Proof.check (SAT.store solver) pr;
);
let t3 = Sys.time () -. t2 in let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f)@." t2 t3; Format.printf "Unsat (%.3f/%.3f)@." t2 t3;