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

fix warnings

Browse source
This commit is contained in:
Simon Cruanes 2023-06-23 20:44:01 -04:00
parent 7fbfb8439b
commit 619da6fbcb
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 7 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/main/pure_sat_solver.ml
View file

@ -104,7 +104,9 @@ let tracer ~(sink : Tr.Sink.t) () : SAT.Tracer.t =
dict_of_list dict_of_list
[ [
"id", int id; "id", int id;
"c", list (lits |> Iter.map self#sat_encode_lit |> Iter.to_rev_list); ( "c",
list (lits |> Iter.map self#sat_encode_lit |> Iter.to_rev_list)
);
]) ])
in in
Tr.Sink.emit sink ~tag:"AssCSat" v Tr.Sink.emit sink ~tag:"AssCSat" v
@ -147,8 +149,7 @@ let tracer ~(sink : Tr.Sink.t) () : SAT.Tracer.t =
let start = Sys.time () let start = Sys.time ()
let solve ?(check = false) (solver : SAT.t) : let solve ?check:(_ = false) (solver : SAT.t) : (unit, string) result =
(unit, string) result =
let res = Profile.with_ "solve" (fun () -> SAT.solve solver) in let res = Profile.with_ "solve" (fun () -> SAT.solve solver) in
let t2 = Sys.time () in let t2 = Sys.time () in
Printf.printf "\r"; Printf.printf "\r";
@ -158,9 +159,7 @@ let solve ?(check = false) (solver : SAT.t) :
let t3 = Sys.time () in let t3 = Sys.time () in
Format.printf "Sat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2) Format.printf "Sat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2)
| SAT.Unsat _ -> | SAT.Unsat _ ->
(* TODO: extract proof from trace; use check_proof *)
(* TODO: extract proof from trace; use check_proof *)
let t3 = Sys.time () in let t3 = Sys.time () in
Format.printf "Unsat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2)); Format.printf "Unsat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2));
Ok () Ok ()

4
src/smtlib/Driver.ml
View file

@ -120,10 +120,10 @@ let solve (self : t) ~assumptions () : Solver.res =
*); *);
(match self.proof_file with (match self.proof_file with
| Some file -> | Some _file ->
(match unsat_proof () with (match unsat_proof () with
| None -> () | None -> ()
| Some step_id -> | Some _step_id ->
(* TODO: read trace; emit proof (* TODO: read trace; emit proof
let proof = Solver.proof self.solver in let proof = Solver.proof self.solver in
let proof_quip = let proof_quip =

1
src/smtlib/build_model.mli
View file

@ -1,4 +1,3 @@
open Common_
open! Sidekick_base open! Sidekick_base
type t type t