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

refactor: make proof production lazy

Browse source
This commit is contained in:
Simon Cruanes 2021-03-19 17:26:30 -04:00
parent d665f83c65
commit 3aadb055b6
3 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/core/Sidekick_core.ml
View file

@ -698,7 +698,7 @@ module type SOLVER = sig
type res = type res =
| Sat of Model.t | Sat of Model.t
| Unsat of { | Unsat of {
proof: proof option; proof: proof option lazy_t;
unsat_core: Atom.t list lazy_t; unsat_core: Atom.t list lazy_t;
} }
| Unknown of Unknown.t | Unknown of Unknown.t

6
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -593,7 +593,7 @@ module Make(A : ARG)
type res = type res =
| Sat of Model.t | Sat of Model.t
| Unsat of { | Unsat of {
proof: proof option; proof: proof option lazy_t;
unsat_core: Atom.t list lazy_t; unsat_core: Atom.t list lazy_t;
} }
| Unknown of Unknown.t | Unknown of Unknown.t
@ -653,13 +653,13 @@ module Make(A : ARG)
do_on_exit (); do_on_exit ();
Sat m Sat m
| Sat_solver.Unsat us -> | Sat_solver.Unsat us ->
let proof = let proof = lazy (
try try
let pr = us.get_proof () in let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr; if check then Sat_solver.Proof.check pr;
Some pr Some pr
with Msat.Solver_intf.No_proof -> None with Msat.Solver_intf.No_proof -> None
in ) in
let unsat_core = lazy (us.Msat.unsat_assumptions ()) in let unsat_core = lazy (us.Msat.unsat_assumptions ()) in
do_on_exit (); do_on_exit ();
Unsat {proof; unsat_core} Unsat {proof; unsat_core}

16
src/smtlib/Process.ml
View file

@ -178,15 +178,16 @@ let solve
*) *)
let t3 = Sys.time () -. t2 in let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat {proof=None;_} -> | Solver.Unsat {proof;_} ->
Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
| Solver.Unsat {proof=Some p;_} ->
if check then ( if check then (
Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p); match proof with
| lazy (Some p) ->
Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
| _ -> ()
); );
begin match dot_proof with begin match dot_proof, proof with
| None -> () | None, _ -> ()
| Some file -> | Some file, lazy (Some p) ->
Profile.with_ "dot.proof" @@ fun () -> Profile.with_ "dot.proof" @@ fun () ->
CCIO.with_out file CCIO.with_out file
(fun oc -> (fun oc ->
@ -194,6 +195,7 @@ let solve
let fmt = Format.formatter_of_out_channel oc in let fmt = Format.formatter_of_out_channel oc in
Solver.Proof.pp_dot fmt p; Solver.Proof.pp_dot fmt p;
Format.pp_print_flush fmt (); flush oc) Format.pp_print_flush fmt (); flush oc)
| _ -> ()
end; end;
let t3 = Sys.time () -. t2 in let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;