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

refactor(main): catch resolution errors properly; style

Browse source
This commit is contained in:
Simon Cruanes 2019-02-16 12:16:00 -06:00 • committed by Guillaume Bury
parent e30c54e11b
commit 92ca9c328f
1 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/main/main.ml
View file

@ -48,14 +48,16 @@ module Process() = struct
let t' = Sys.time () -. t in let t' = Sys.time () -. t in
Format.printf "Sat (%f/%f)@." t t' Format.printf "Sat (%f/%f)@." t t'
| S.Unsat state -> | S.Unsat state ->
if !p_check then begin if !p_check then (
let p = state.Msat.get_proof () in let p = state.Msat.get_proof () in
S.Proof.check p; S.Proof.check p;
if !p_dot_proof <> "" then begin if !p_dot_proof <> "" then (
let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in let oc = open_out !p_dot_proof in
D.pp fmt p let fmt = Format.formatter_of_out_channel oc in
end Format.fprintf fmt "%a@?" D.pp p;
end; flush oc; close_out_noerr oc;
)
);
let t' = Sys.time () -. t in let t' = Sys.time () -. t in
Format.printf "Unsat (%f/%f)@." t t' Format.printf "Unsat (%f/%f)@." t t'
end end
@ -171,4 +173,7 @@ let () =
| Incorrect_model -> | Incorrect_model ->
Format.printf "Internal error : incorrect *sat* model@."; Format.printf "Internal error : incorrect *sat* model@.";
exit 4 exit 4
| S.Proof.Resolution_error msg ->
Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg;
exit 5