From 502dce503cc10de47f0a75f61645bd143f8a26d0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 25 Apr 2021 21:56:16 -0400 Subject: [PATCH] refactor(proof): merge proof and lemma, add composite proof constructor --- src/base-term/Proof.ml | 136 +++++++++++----- src/cc/Sidekick_cc.ml | 2 +- src/core/Sidekick_core.ml | 49 ++++-- src/lra/sidekick_arith_lra.ml | 4 +- src/msat-solver/Sidekick_msat_solver.ml | 148 +++++++++++------- src/smtlib/Process.ml | 12 +- src/th-bool-static/Sidekick_th_bool_static.ml | 2 +- 7 files changed, 230 insertions(+), 123 deletions(-) diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index 26626c01..f885a1e1 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -35,6 +35,7 @@ type t = | Unspecified | Sorry (* NOTE: v. bad as we don't even specify the return *) | Sorry_c of clause + | Named of string (* refers to previously defined clause *) | Refl of term | CC_lemma_imply of t list * term * term | CC_lemma of clause @@ -50,6 +51,23 @@ type t = | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term | LRA of clause + | Composite of { + (* some named (atomic) assumptions *) + assumptions: (string * lit) list; + steps: composite_step list; (* last step is the proof *) + } + +and composite_step = + | S_define_c of { + name: string; (* name *) + res: clause; (* result of [proof] *) + proof: t; (* sub-proof *) + } + + (* TODO: do we need that here? or is it only during printing + that it becomes important? + | S_define_t of string * term (* name this term *) + *) and hres_step = | R of { pivot: term; p: t} @@ -62,11 +80,15 @@ let r1 p = R1 p let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs } let p1 p = P1 p +let defc ~name res proof : composite_step = + S_define_c {proof;name;res} + let default=Unspecified let sorry_c c = Sorry_c (Iter.to_rev_list c) let sorry_c_l c = Sorry_c c let sorry = Sorry let refl t : t = Refl t +let ref_by_name name : t = Named name let make_cc iter : t = CC_lemma (Iter.to_rev_list iter) let cc_lemma c : t = CC_lemma (Iter.to_rev_list c) let cc_imply_l l t u : t = CC_lemma_imply (l, t, u) @@ -74,6 +96,11 @@ let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u) let assertion t = Assertion t let assertion_c c = Assertion_c (Iter.to_rev_list c) let assertion_c_l c = Assertion_c c +let composite_l ?(assms=[]) steps : t = + Composite {assumptions=assms; steps} +let composite_iter ?(assms=[]) steps : t = + let steps = Iter.to_list steps in + Composite {assumptions=assms; steps} let isa_split ty i = DT_isa_split (ty, Iter.to_rev_list i) let isa_disj ty t u = DT_isa_disj (ty, t, u) @@ -91,45 +118,72 @@ let hres_iter c i : t = Hres (c, Iter.to_list i) let lra_l c : t = LRA c let lra c = LRA (Iter.to_rev_list c) -let rec pp out (self:t) : unit = - let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l in - let pp_cl out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l pp_lit) c in - match self with - | Unspecified -> Fmt.string out "" - | CC_lemma l -> - Fmt.fprintf out "(@[cc-lemma@ %a@])" pp_cl l - | CC_lemma_imply (l,t,u) -> - Fmt.fprintf out "(@[cc-lemma-imply@ (@[%a@])@ (@[=@ %a@ %a@])@])" - (pp_l pp) l T.pp t T.pp u - | Refl t -> Fmt.fprintf out "(@[refl@ %a@])" T.pp t - | Sorry -> Fmt.string out "sorry" - | Sorry_c c -> Fmt.fprintf out "(@[sorry-c@ %a@])" pp_cl c - | Bool_true_is_true -> Fmt.string out "true-is-true" - | Bool_true_neq_false -> Fmt.string out "(@[!= T F@])" - | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" T.pp a T.pp b - | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" T.pp t - | Assertion_c c -> - Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c - | Hres (c, l) -> - Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp c - (pp_l pp_hres_step) l - | DT_isa_split (ty,l) -> - Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])" - Ty.pp ty (pp_l T.pp) l - | DT_isa_disj (ty,t,u) -> - Fmt.fprintf out "(@[dt.isa.disj@ (@[ty %a@])@ %a@ %a@])" Ty.pp ty T.pp t T.pp u - | DT_cstor_inj (c,i,ts,us) -> - Fmt.fprintf out "(@[dt.cstor.inj %d@ (@[%a@ %a@])@ (@[%a@ %a@])@])" - i Cstor.pp c (pp_l T.pp) ts Cstor.pp c (pp_l T.pp) us - | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" T.pp t - | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" T.pp t - | LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c +module Quip = struct + (* + TODO: make sure we print terms properly + TODO: define/use [deft] for printing shared terms + *) -and pp_hres_step out = function - | R {pivot; p} -> - Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" T.pp pivot pp p - | R1 p -> Fmt.fprintf out "(@[r1@ %a@])" pp p - | P {p; lhs; rhs} -> - Fmt.fprintf out "(@[r@ (@[lhs@ %a@])@ (@[rhs@ %a@])@ %a@])" - T.pp lhs T.pp rhs pp p - | P1 p -> Fmt.fprintf out "(@[p1@ %a@])" pp p + let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l + let pp_cl out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l pp_lit) c + + let rec pp_rec out (self:t) : unit = + match self with + | Unspecified -> Fmt.string out "" + | Named s -> Fmt.fprintf out "(ref %s)" s + | CC_lemma l -> + Fmt.fprintf out "(@[cc-lemma@ %a@])" pp_cl l + | CC_lemma_imply (l,t,u) -> + Fmt.fprintf out "(@[cc-lemma-imply@ (@[%a@])@ (@[=@ %a@ %a@])@])" + (pp_l pp_rec) l T.pp t T.pp u + | Refl t -> Fmt.fprintf out "(@[refl@ %a@])" T.pp t + | Sorry -> Fmt.string out "sorry" + | Sorry_c c -> Fmt.fprintf out "(@[sorry-c@ %a@])" pp_cl c + | Bool_true_is_true -> Fmt.string out "true-is-true" + | Bool_true_neq_false -> Fmt.string out "(@[!= T F@])" + | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" T.pp a T.pp b + | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" T.pp t + | Assertion_c c -> + Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c + | Hres (c, l) -> + Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp_rec c + (pp_l pp_hres_step) l + | DT_isa_split (ty,l) -> + Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])" + Ty.pp ty (pp_l T.pp) l + | DT_isa_disj (ty,t,u) -> + Fmt.fprintf out "(@[dt.isa.disj@ (@[ty %a@])@ %a@ %a@])" Ty.pp ty T.pp t T.pp u + | DT_cstor_inj (c,i,ts,us) -> + Fmt.fprintf out "(@[dt.cstor.inj %d@ (@[%a@ %a@])@ (@[%a@ %a@])@])" + i Cstor.pp c (pp_l T.pp) ts Cstor.pp c (pp_l T.pp) us + | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" T.pp t + | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" T.pp t + | LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c + | Composite {steps; assumptions} -> + let pp_ass out (n,a) = Fmt.fprintf out "(@[assuming@ (name %s) %a@])" n pp_lit a in + Fmt.fprintf out "(@[steps@ (@[%a@])@ (@[%a@])@])" + (pp_l pp_ass) assumptions (pp_l pp_composite_step) steps + + and pp_composite_step out = function + | S_define_c {name;res;proof} -> + Fmt.fprintf out "(@[defc %s %a@ %a@])" name pp_cl res pp_rec proof + (* + | S_define_t (name, t) -> + Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t + *) + + and pp_hres_step out = function + | R {pivot; p} -> + Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" T.pp pivot pp_rec p + | R1 p -> Fmt.fprintf out "(@[r1@ %a@])" pp_rec p + | P {p; lhs; rhs} -> + Fmt.fprintf out "(@[r@ (@[lhs@ %a@])@ (@[rhs@ %a@])@ %a@])" + T.pp lhs T.pp rhs pp_rec p + | P1 p -> Fmt.fprintf out "(@[p1@ %a@])" pp_rec p + + (* toplevel wrapper *) + let pp out self = + Fmt.fprintf out "(@[quip 1@ %a@])" pp_rec self +end + +let pp_debug = Quip.pp_rec diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index f87a23ff..a983a0d3 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -169,7 +169,7 @@ module Make (A: CC_ARG) | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b | E_merge_t (a,b) -> Fmt.fprintf out "(@[merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e - | E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp p + | E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp_debug p | E_and (a,b) -> Format.fprintf out "(@[and@ %a@ %a@])" pp a pp b diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 33bc1e8f..fb4dff34 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -149,7 +149,6 @@ module type PROOF = sig type term type ty type t - val pp : t Fmt.printer type hres_step (** hyper-resolution steps: resolution, unit resolution; @@ -178,8 +177,12 @@ module type PROOF = sig val neq : term -> term -> lit val not : lit -> lit + type composite_step + val defc : name:string -> lit list -> t -> composite_step + val assertion : term -> t val assertion_c : lit Iter.t -> t + val ref_by_name : string -> t (* named clause, see {!defc} *) val assertion_c_l : lit list -> t val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *) val hres_l : t -> hres_step list -> t (* hyper-res *) @@ -189,6 +192,8 @@ module type PROOF = sig val cc_lemma : lit Iter.t -> t (* equality tautology, unsigned *) val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *) val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *) + val composite_iter : ?assms:(string * lit) list -> composite_step Iter.t -> t + val composite_l : ?assms:(string * lit) list -> composite_step list -> t val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *) val sorry_c : lit Iter.t -> t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *) @@ -196,6 +201,13 @@ module type PROOF = sig val sorry_c_l : lit list -> t val default : t [@@alert cstor "do not use default constructor"] + + val pp_debug : t Fmt.printer + + module Quip : sig + val pp : t Fmt.printer + (** Printer in Quip format (experimental) *) + end end (** Literals @@ -810,7 +822,7 @@ module type SOLVER = sig type term = T.Term.t type ty = T.Ty.t type lit = Lit.t - type lemma = P.t + type proof = P.t (** {3 A theory} @@ -915,19 +927,6 @@ module type SOLVER = sig *) end - (** {3 Proof type} - - The representation of a full proof, including toplevel steps - with intermediate, named, clauses. Each clause is justified by - a {!P.t} lemma. *) - module Proof : sig - type t - val check : t -> unit - val pp_dot : t Fmt.printer - val pp : t Fmt.printer - end - type proof = Proof.t - (** {3 Main API} *) val stats : t -> Stat.t @@ -980,11 +979,29 @@ module type SOLVER = sig val add_clause_l : t -> Atom.t list -> P.t -> unit (** Same as {!add_clause} but with a list of atoms. *) + (** {2 Internal representation of proofs} + + A type or state convertible into {!P.t} *) + module Pre_proof : sig + type t + + val pp : t Fmt.printer + + val pp_dot : t Fmt.printer option + (** Optional printer into DOT/graphviz *) + + val check : t -> unit + (** Check the proof (to an unspecified level of confidence; + this can be a no-op). May fail. *) + + val to_proof : t -> P.t + end + (** Result of solving for the current set of clauses *) type res = | Sat of Model.t (** Satisfiable *) | Unsat of { - proof: proof option lazy_t; (** proof of unsat *) + proof: Pre_proof.t option lazy_t; (** proof of unsat *) unsat_core: Atom.t list lazy_t; (** subset of assumptions responsible for unsat *) } (** Unsatisfiable *) | Unknown of Unknown.t diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 81b50bfe..fcb5563b 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -58,8 +58,8 @@ module type ARG = sig (** Does this term have the type [Real] *) (** TODO: more accurate certificates *) - val proof_lra : S.P.lit Iter.t -> S.lemma - val proof_lra_l : S.P.lit list -> S.lemma + val proof_lra : S.P.lit Iter.t -> S.P.t + val proof_lra_l : S.P.lit list -> S.P.t module Gensym : sig type t diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index c4941ae2..298e0be9 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -36,7 +36,7 @@ module Make(A : ARG) module Term = T.Term type term = Term.t type ty = Ty.t - type lemma = P.t + type proof = P.t module Lit_ = struct module T = T @@ -344,7 +344,7 @@ module Make(A : ARG) let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in Log.debugf 10 (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])" - Lit.pp lit Lit.pp lit' P.pp p); + Lit.pp lit Lit.pp lit' P.Quip.pp p); lit', p (* add a clause using [acts] *) @@ -504,92 +504,128 @@ module Make(A : ARG) module Sat_solver = Msat.Make_cdcl_t(Solver_internal) module Atom = Sat_solver.Atom - module Proof = struct - include Sat_solver.Proof + + module Pre_proof = struct + module SP = Sat_solver.Proof module SC = Sat_solver.Clause + type t = { + msat: Sat_solver.proof; + p: P.t lazy_t; + } + + let to_proof (self:t) : P.t = Lazy.force self.p + let pp_dot = let module Dot = Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in - Dot.pp + let pp out self = Dot.pp out self.msat in + Some pp - (* TODO: instead export to regular proof, which must get: + (* export to proof {!P.t}, translating Msat-level proof ising: - [defc name cl proof] to bind [name] to given clause and proof - [deft name t] to define [name] as a shortcut for [t] (tseitin, etc.). - Checker will always expand these. + Checker will always expand these. (TODO) - [steps +] for a structure proof with definitions, returning last one - [subproof (assms * ) (proof)] which uses [proof] to get clause [c] under given assumptions (each assm is a lit), and return [-a1 \/ … \/ -an \/ c], discharging assumptions - - proof must provide a mutable builder for "steps" which is passed along - in main solver context so that theories can use it for their global - definitions. This is also what resolution should use to translate the proof. *) - let pp out (self:t) : unit = - let n_step = ref 0 in - let n_tbl_ = SC.Tbl.create 32 in (* node.concl -> unique idx *) + let conv_proof (msat:Sat_solver.proof) : P.t = + let assms = ref [] in + let steps = ref [] in - let find_idx_of_proof_ (p:t) : int = - try SC.Tbl.find n_tbl_ (conclusion p) + let n_step = ref 0 in + let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *) + + (* name of an already processed proof node *) + let find_proof_name (p:Sat_solver.proof) : string = + try SC.Tbl.find n_tbl_ (SP.conclusion p) with Not_found -> - Error.errorf "proof print: cannot find proof step with conclusion %a" SC.pp (conclusion p) + Error.errorf + "msat-solver.pre-proof.to_proof: cannot find proof step with conclusion %a" + SC.pp (SP.conclusion p) in - let pp_node () n_init : unit = - let {conclusion=c; step} = n_init in + let add_step s = steps := s :: !steps in + + (* convert [n_init] into a proof step and adds it to [steps] *) + let tr_node_to_step () (n_init:SP.proof_node) : unit = + let {SP.conclusion=c; step} = n_init in if SC.Tbl.mem n_tbl_ c then () else ( - let idx = !n_step in + let name = Printf.sprintf "c%d" !n_step in incr n_step; - SC.Tbl.add n_tbl_ c idx; + SC.Tbl.add n_tbl_ c name; - let atoms = Sat_solver.Clause.atoms_l c in - let pp_atom out a = - let lit = Sat_solver.Atom.formula a in - let sign = if Sat_solver.Atom.sign a then "+" else "-" in - Fmt.fprintf out "(@[%s %a@])" sign T.Term.pp (Lit.term lit) + (* build conclusion of proof step *) + let tr_atom a : P.lit = + let sign = Sat_solver.Atom.sign a in + let t = Lit.term (Sat_solver.Atom.formula a) in + P.lit_st (t,sign) in + let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l c in + + (* proof for the node *) + let pr_step : P.t = + match step with + | SP.Hypothesis pr -> pr (* FIXME: should this have a special rule? *) + + | SP.Assumption -> + (* push into assumptions and introduce a name for it *) + let name = Printf.sprintf "a%d" !n_step in + let lit = match concl with + | [l] -> l + | _ -> Error.errorf "assumption with non-unit clause %a" SC.pp c + in + incr n_step; + assms := (name, lit) :: !assms; + P.ref_by_name name + + | Lemma pr -> pr - let pp_step out (s:step) : unit = - match s with - | Hypothesis l -> - Fmt.fprintf out "(@[hyp@ %a@])" P.pp l - | Assumption -> Fmt.string out "assumption" - | Lemma l -> Fmt.fprintf out "(@[lemma@ %a@])" P.pp l | Duplicate (c, _) -> - let n = find_idx_of_proof_ c in - Fmt.fprintf out "(@[dedup@ c%d@])" n + let n = find_proof_name c in + let p = P.ref_by_name n in + (* NOTE: we do not represent this form of transformation for now. + Quip should be able to process clauses as sets. *) + p + | Hyper_res { hr_init=init; hr_steps=steps } -> - let n_init = find_idx_of_proof_ init in - let pp_step out (pivot,p') = - let unit_res = - Array.length (SC.atoms (conclusion p')) = 1 in - let n_p' = find_idx_of_proof_ p' in - if unit_res then ( - Fmt.fprintf out "(@[r1 c%d@])" n_p' + let proof_init = P.ref_by_name @@ find_proof_name init in + let tr_step (pivot,p') : P.hres_step = + (* unit resolution? *) + let is_r1_step = Array.length (SC.atoms (SP.conclusion p')) = 1 in + let proof_p' = P.ref_by_name @@ find_proof_name p' in + if is_r1_step then ( + P.r1 proof_p' ) else ( - Fmt.fprintf out "(@[r c%d@ :pivot %a@])" n_p' pp_atom pivot + let pivot = Lit.term (Sat_solver.Atom.formula pivot) in + P.r proof_p' ~pivot ) in - Fmt.fprintf out "(@[hres@ c%d@ (@[%a@])@])" - n_init Fmt.(list ~sep:(return "@ ") pp_step) steps + P.hres_iter proof_init + (Iter.of_list steps |> Iter.map tr_step) in - Fmt.fprintf out "@ (@[defc c%d@ (@[cl %a@])@ (@[<1>src@ %a@])@])" - idx Fmt.(list ~sep:(return "@ ") pp_atom) atoms - pp_step step; + let step = P.defc ~name concl pr_step in + add_step step; ) in - Fmt.fprintf out "(@[quip 1"; - Sat_solver.Proof.fold pp_node () self; - Fmt.fprintf out "@])"; - () - end - type proof = Proof.t + (* this should traverse from the leaves, so that order of [steps] is correct *) + Sat_solver.Proof.fold tr_node_to_step () msat; + let assms = !assms in + P.composite_l ~assms (List.rev !steps) + + let make (msat: Sat_solver.proof) : t = + { msat; p=lazy (conv_proof msat) } + + let check self = SP.check self.msat + let pp out (self:t) = P.Quip.pp out (to_proof self) + end (* main solver state *) type t = { @@ -747,7 +783,7 @@ module Make(A : ARG) type res = | Sat of Model.t | Unsat of { - proof: proof option lazy_t; + proof: Pre_proof.t option lazy_t; unsat_core: Atom.t list lazy_t; } | Unknown of Unknown.t @@ -761,7 +797,7 @@ module Make(A : ARG) let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit = Stat.incr self.count_clause; Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])" - (Util.pp_iarray Atom.pp) c P.pp proof); + (Util.pp_iarray Atom.pp) c P.pp_debug proof); let pb = Profile.begin_ "add-clause" in Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof; Profile.exit pb @@ -860,7 +896,7 @@ module Make(A : ARG) try let pr = us.get_proof () in if check then Sat_solver.Proof.check pr; - Some pr + Some (Pre_proof.make pr) with Msat.Solver_intf.No_proof -> None ) in let unsat_core = lazy (us.Msat.unsat_assumptions ()) in diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 85b56925..485266b2 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -185,19 +185,18 @@ let solve if check then ( match proof_opt with | Some p -> - Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p); + Profile.with_ "unsat.check" (fun () -> Solver.Pre_proof.check p); | _ -> () ); - begin match dot_proof, proof with - | None, _ -> () - | Some file, lazy (Some p) -> + begin match dot_proof, proof, Solver.Pre_proof.pp_dot with + | Some file, lazy (Some p), Some pp_dot -> Profile.with_ "dot.proof" @@ fun () -> 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 - Solver.Proof.pp_dot fmt p; + pp_dot fmt p; Format.pp_print_flush fmt (); flush oc) | _ -> () end; @@ -210,7 +209,8 @@ let solve match proof_opt with | None -> Error.errorf "cannot print proof, none was generated" | Some p -> - Fmt.printf "(@[proof@ %a@])@." Solver.Proof.pp p; + let p = Solver.Pre_proof.to_proof p in + Fmt.printf "(@[proof@ %a@])@." Solver.P.Quip.pp p; ); | Solver.Unknown reas -> diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 4c36b3bf..7bf0b6a3 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -317,7 +317,7 @@ module Make(A : ARG) : S with module A = A = struct | Some (u, pr_t_u) -> Log.debugf 5 (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])" - T.pp t T.pp u SI.P.pp pr_t_u); + T.pp t T.pp u SI.P.Quip.pp pr_t_u); SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); ()); end;