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

refactor: remove proof printing code

Browse source
This commit is contained in:
Simon Cruanes 2019-02-16 13:38:54 -06:00
parent c06e4025fa
commit 1f68753121
2 changed files with 1 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/smt/Solver.ml
View file

@ -17,32 +17,7 @@ let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
module Atom = Sat_solver.Atom
module Proof = struct
type t = Sat_solver.Proof.t
let check = Sat_solver.Proof.check
let pp out (p:t) : unit =
let pp_step_res out p =
let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in
Sat_solver.Clause.pp out conclusion
in
let pp_step out = function
| Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
| Sat_solver.Proof.Resolution (p1, p2, _) ->
Format.fprintf out "(@[<1>resolution@ %a@ %a@])"
pp_step_res p1 pp_step_res p2
| _ -> Fmt.string out "<other>"
in
Format.fprintf out "(@[<v>";
Sat_solver.Proof.fold
(fun () {Sat_solver.Proof.conclusion; step } ->
Format.fprintf out "(@[<hv1>step@ %a@ @[<1>from:@ %a@]@])@,"
Sat_solver.Clause.pp conclusion pp_step step)
() p;
Format.fprintf out "@])";
()
end
module Proof = Sat_solver.Proof
(* main solver state *)
type t = {

2
src/smt/Solver.mli
View file

@ -18,9 +18,7 @@ module Atom = Sat_solver.Atom
module Proof : sig
type t = Sat_solver.Proof.t
val check : t -> unit
val pp : t CCFormat.printer
end
type unknown =