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

refactor: return optional proof, do not store if if -no-check was given

Browse source
This commit is contained in:
Simon Cruanes 2019-02-10 16:59:27 -06:00
parent 62ea8fd0cb
commit 5865151247
4 changed files with 27 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/main/main.ml
View file

@ -107,7 +107,7 @@ let main () =
| Smtlib ->
[Sidekick_th_bool.th] (* TODO: more theories *)
in
Sidekick_smt.Solver.create ~theories ()
Sidekick_smt.Solver.create ~store_proof:!check ~theories ()
in
let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
begin match syn with

16
src/smt/Solver.ml
View file

@ -63,10 +63,10 @@ let[@inline] mk_atom_t self ?sign t : Atom.t =
let lit = Lit.atom ?sign t in
mk_atom_lit self lit
let create ?size ?(config=Config.empty) ~theories () : t =
let create ?size ?(config=Config.empty) ?store_proof ~theories () : t =
let th_combine = Theory_combine.create() in
let self = {
solver=Sat_solver.create ?size th_combine;
solver=Sat_solver.create ?store_proof ?size th_combine;
stat=Stat.create ();
config;
} in
@ -168,7 +168,7 @@ let pp_model = Model.pp
type res =
| Sat of model
| Unsat of Proof.t
| Unsat of Proof.t option
| Unknown of unknown
(** {2 Main} *)
@ -221,7 +221,7 @@ let check_model (_s:t) : unit =
(* TODO: main loop with iterative deepening of the unrolling limit
(not the value depth limit) *)
let solve ?(on_exit=[]) ?check:(_=true) ~assumptions (self:t) : res =
let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
let r = Sat_solver.solve ~assumptions (solver self) in
match r with
| Sat_solver.Sat st ->
@ -237,7 +237,13 @@ let solve ?(on_exit=[]) ?check:(_=true) ~assumptions (self:t) : res =
Unknown U_incomplete (* TODO *)
*)
| Sat_solver.Unsat us ->
let pr = us.get_proof () in
let pr =
try
let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr;
Some pr
with Msat.Solver_intf.No_proof -> None
in
do_on_exit ~on_exit;
Unsat pr

3
src/smt/Solver.mli
View file

@ -30,7 +30,7 @@ type unknown =
type res =
| Sat of Model.t
| Unsat of Proof.t
| Unsat of Proof.t option
| Unknown of unknown
(** {2 Main} *)
@ -41,6 +41,7 @@ type t
val create :
?size:[`Big | `Tiny | `Small] ->
?config:Config.t ->
?store_proof:bool ->
theories:Theory.t list ->
unit -> t

24
src/smtlib/Process.ml
View file

@ -287,20 +287,22 @@ let solve
);
let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat p ->
| Solver.Unsat None ->
Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
| Solver.Unsat (Some p) ->
if check then (
Solver.Proof.check p;
begin match dot_proof with
| None -> ()
| Some file ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.pp fmt p;
Format.pp_print_flush fmt (); flush oc)
end
);
begin match dot_proof with
| None -> ()
| Some file ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.pp fmt p;
Format.pp_print_flush fmt (); flush oc)
end;
let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unknown reas ->