simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -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 eb23644195
commit ed114f8abe
2 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/main/main.ml
View file

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

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 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;