From 4a30a06f87f66f998b27e066486429f5d7236c16 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 26 Oct 2021 21:57:17 -0400 Subject: [PATCH] wip: reconstruct quip proof from binary proof-trace --- src/base/Proof.ml | 16 +- src/base/Proof.mli | 4 + src/base/Proof_quip.ml | 653 ++++++++----------------------------- src/base/Proof_quip.mli | 23 +- src/base/dune | 2 +- src/quip/Sidekick_quip.ml | 595 ++++++++++----------------------- src/quip/Sidekick_quip.mli | 18 +- src/smtlib/Process.ml | 4 +- src/util/Util.ml | 3 + src/util/Util.mli | 3 + 10 files changed, 352 insertions(+), 969 deletions(-) diff --git a/src/base/Proof.ml b/src/base/Proof.ml index d4632f77..a4d6c2e9 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -128,7 +128,6 @@ let emit_fun_ (self:t) (f:Fun.t) : term_id = let id = alloc_id self in Fun.Tbl.add self.map_fun f id; let f_name = ID.to_string (Fun.id f) in - Format.printf "encode fun with name %S@." f_name; emit_step_ self Proof_ser.({ Step.id; view=Fun_decl {Fun_decl.f=f_name}}); id @@ -222,18 +221,19 @@ let lemma_rw_clause c ~using (self:t) = let using = Iter.to_array using in PS.(Step_view.Step_clause_rw {Step_clause_rw.c; using}) +(* TODO *) let with_defs _ _ (_pr:t) = dummy_step +(* not useful *) let del_clause _ _ (_pr:t) = () -let emit_unsat_core _ (_pr:t) = dummy_step (* TODO *) +(* TODO *) +let emit_unsat_core _ (_pr:t) = dummy_step let emit_unsat c (self:t) : unit = emit_no_return_ self @@ fun() -> PS.(Step_view.Step_unsat {Step_unsat.c}) -let lemma_lra _ _ = dummy_step - let lemma_bool_tauto lits (self:t) = emit_ self @@ fun() -> let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in @@ -244,6 +244,10 @@ let lemma_bool_c rule (ts:Term.t list) (self:t) = let exprs = ts |> Util.array_of_list_map (emit_term_ self) in PS.(Step_view.Step_bool_c {Step_bool_c.exprs; rule}) +(* TODO *) + +let lemma_lra _ _ = dummy_step + let lemma_bool_equiv _ _ _ = dummy_step let lemma_ite_true ~ite:_ _ = dummy_step @@ -257,3 +261,7 @@ let lemma_isa_disj _ _ (_pr:t) = dummy_step let lemma_cstor_inj _ _ _ (_pr:t) = dummy_step let lemma_cstor_distinct _ _ (_pr:t) = dummy_step let lemma_acyclicity _ (_pr:t) = dummy_step + +module Unsafe_ = struct + let[@inline] id_of_proof_step_ (p:proof_step) : proof_step = p +end diff --git a/src/base/Proof.mli b/src/base/Proof.mli index 02df8338..0d585c7e 100644 --- a/src/base/Proof.mli +++ b/src/base/Proof.mli @@ -78,3 +78,7 @@ val iter_steps_backward : t -> Proof_ser.Step.t Iter.t This will yield nothing if the proof was disabled or used a dummy backend. *) + +module Unsafe_ : sig + val id_of_proof_step_ : proof_step -> Proof_ser.ID.t +end diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index a688eaa1..8729bddf 100644 --- a/src/base/Proof_quip.ml +++ b/src/base/Proof_quip.ml @@ -1,538 +1,141 @@ -open Base_types +(* output proof *) +module P = Sidekick_quip.Proof -module T = Term -module Ty = Ty -type term = T.t -type ty = Ty.t +(* serialized proof trace *) +module PS = Sidekick_base_proof_trace.Proof_ser -type lit = - | L_eq of bool * term * term - | L_a of bool * term +type t = P.t -let lit_not = function - | L_eq (sign,a,b) -> L_eq(not sign,a,b) - | L_a (sign,t) -> L_a (not sign,t) - -let pp_lit_with ~pp_t out = - let strsign = function true -> "+" | false -> "-" in - function - | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u - | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t -let pp_lit = pp_lit_with ~pp_t:Term.pp - -let lit_a t = L_a (true,t) -let lit_na t = L_a (false,t) -let lit_eq t u = L_eq (true,t,u) -let lit_neq t u = L_eq (false,t,u) -let lit_mk b t = L_a (b,t) -let lit_sign = function L_a (b,_) | L_eq (b,_,_) -> b - -type clause = lit list - -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 - | Assertion of term - | Assertion_c of clause - | Drup_res of clause - | Hres of t * hres_step list - | Res of term * t * t - | Res1 of t * t - | DT_isa_split of ty * term list - | DT_isa_disj of ty * term * term - | DT_cstor_inj of Cstor.t * int * term list * term list (* [c t…=c u… |- t_i=u_i] *) - | Bool_true_is_true - | Bool_true_neq_false - | Bool_eq of term * term (* equal by pure boolean reasoning *) - | Bool_c of bool_c_name * term list (* boolean tautology *) - | Nn of t (* negation normalization *) - | 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 array; (* last proof_rule is the proof *) - } - -and bool_c_name = string - -and composite_step = - | S_step_c of { - name: string; (* name *) - res: clause; (* result of [proof] *) - proof: t; (* sub-proof *) - } - | S_define_t of term * term (* [const := t] *) - | S_define_t_name of string * term (* [const := t] *) - - (* TODO: be able to name clauses, to be expanded at parsing. - note that this is not the same as [S_step_c] which defines an - explicit proof_rule with a conclusion and proofs that can be exploited - separately. - - We could introduce that in Compress.rename… - - | S_define_c of string * clause (* [name := c] *) - *) - -and hres_step = - | R of { pivot: term; p: t} - | R1 of t - | P of { lhs: term; rhs: term; p: t} - | P1 of t - -let r p ~pivot : hres_step = R { pivot; p } -let r1 p = R1 p -let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs } -let p1 p = P1 p - -let stepc ~name res proof : composite_step = S_step_c {proof;name;res} -let deft c rhs : composite_step = S_define_t (c,rhs) -let deft_name c rhs : composite_step = S_define_t_name (c,rhs) - -let is_trivial_refl = function - | Refl _ -> true - | _ -> false - -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 cc_lemma c : t = CC_lemma c -let cc_imply_l l t u : t = - let l = List.filter (fun p -> not (is_trivial_refl p)) l in - match l with - | [] -> refl t (* only possible way [t=u] *) - | l -> CC_lemma_imply (l, t, u) -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_a ?(assms=[]) steps : t = - Composite {assumptions=assms; steps} -let composite_l ?(assms=[]) steps : t = - Composite {assumptions=assms; steps=Array.of_list steps} -let composite_iter ?(assms=[]) steps : t = - let steps = Iter.to_array 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) -let cstor_inj c i t u = DT_cstor_inj (c, i, t, u) - -let ite_true t = Ite_true t -let ite_false t = Ite_false t -let true_is_true : t = Bool_true_is_true -let true_neq_false : t = Bool_true_neq_false -let bool_eq a b : t = Bool_eq (a,b) -let bool_c name c : t = Bool_c (name, c) -let nn c : t = Nn c - -let drup_res c : t = Drup_res c -let hres_l p l : t = - let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in - if l=[] then p else Hres (p,l) -let hres_iter c i : t = hres_l c (Iter.to_list i) -let res ~pivot p1 p2 : t = Res (pivot,p1,p2) -let res1 p1 p2 : t = Res1 (p1,p2) - -let lra_l c : t = LRA c -let lra c = LRA (Iter.to_rev_list c) - -let iter_lit ~f_t = function - | L_eq (_,a,b) -> f_t a; f_t b - | L_a (_,t) -> f_t t - -let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = - match p with - | Unspecified | Sorry -> () - | Sorry_c c -> f_clause c - | Named _ -> () - | Refl t -> f_t t - | CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u - | CC_lemma c | Assertion_c c -> f_clause c - | Assertion t -> f_t t - | Drup_res c -> f_clause c - | Hres (i, l) -> - f_p i; - List.iter - (function - | R1 p -> f_p p - | P1 p -> f_p p - | R {pivot;p} -> f_p p; f_t pivot - | P {lhs;rhs;p} -> f_p p; f_t lhs; f_t rhs) - l - | Res (t,p1,p2) -> f_t t; f_p p1; f_p p2 - | Res1 (p1,p2) -> f_p p1; f_p p2 - | DT_isa_split (_, l) -> List.iter f_t l - | DT_isa_disj (_, t, u) -> f_t t; f_t u - | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us - | Bool_true_is_true | Bool_true_neq_false -> () - | Bool_eq (t, u) -> f_t t; f_t u - | Bool_c (_, ts) -> List.iter f_t ts - | Nn p -> f_p p - | Ite_true t | Ite_false t -> f_t t - | LRA c -> f_clause c - | Composite { assumptions; steps } -> - List.iter (fun (_,lit) -> iter_lit ~f_t lit) assumptions; - Array.iter f_step steps; - -(** {2 Compress by making more sharing explicit} *) -module Compress = struct - type 'a shared_status = - | First (* first occurrence of t *) - | Shared (* multiple occurrences observed *) - | Pre_named of 'a (* another proof_rule names it *) - | Named of 'a (* already named it *) - - (* is [t] too small to be shared? *) - let rec is_small_ t = - match T.view t with - | T.Bool _ -> true - | T.App_fun (_, a) -> IArray.is_empty a (* only constants are small *) - | T.Not u -> is_small_ u - | T.Eq (_, _) | T.Ite (_, _, _) -> false - | T.LRA _ -> false - - type name = N_s of string | N_t of T.t - type sharing_info = { - terms: name shared_status T.Tbl.t; (* sharing for non-small terms *) - } - - let no_sharing : sharing_info = - { terms = T.Tbl.create 8 } - - (* traverse [p] and apply [f_t] to subterms (except to [c] in [c := rhs]) *) - let rec traverse_proof_ ?on_step ~f_t (p:t) : unit = - let recurse = traverse_proof_ ?on_step ~f_t in - let f_step s = - CCOpt.iter (fun f->f s) on_step; - traverse_step_ ~f_t s - in - iter_p p - ~f_t - ~f_clause:(traverse_clause_ ~f_t) - ~f_step - ~f_p:recurse - and traverse_step_ ~f_t = function - | S_define_t_name (_, rhs) - | S_define_t (_, rhs) -> f_t rhs - | S_step_c {name=_; res; proof} -> - traverse_clause_ ~f_t res; traverse_proof_ ~f_t proof - and traverse_clause_ ~f_t c : unit = - List.iter (iter_lit ~f_t) c - - (** [find_sharing p] returns a {!sharing_info} which contains sharing information. - This information can be used during printing to reduce the - number of duplicated sub-terms that are printed. *) - let find_sharing p : sharing_info = - let self = {terms=T.Tbl.create 32} in - - let traverse_t t = - T.iter_dag t - (fun u -> - if not (is_small_ u) then ( - match T.Tbl.get self.terms u with - | None -> T.Tbl.add self.terms u First - | Some First -> T.Tbl.replace self.terms u Shared - | Some (Shared | Named _ | Pre_named _) -> () - )) - in - - (* if a term is already name, remember that, do not rename it *) - let on_step = function - | S_define_t_name (n,rhs) -> - T.Tbl.replace self.terms rhs (Pre_named (N_s n)); - | S_define_t (c,rhs) -> - T.Tbl.replace self.terms rhs (Pre_named (N_t c)); - | S_step_c _ -> () - in - - traverse_proof_ p ~on_step ~f_t:traverse_t; - self - - (** [renaming sharing p] returns a new proof [p'] with more definitions. - It also modifies [sharing] so that the newly defined objects are - mapped to {!Named}, which we can use during printing. *) - let rename sharing (p:t) : t = - let n = ref 0 in - let new_name () = incr n; Printf.sprintf "$t%d" !n in - - match p with - | Composite {assumptions; steps} -> - (* now traverse again, renaming some things on the fly *) - let new_steps = Vec.create() in - - (* definitions we can skip *) - let skip_name_s = Hashtbl.create 8 in - let skip_name_t = T.Tbl.create 8 in - - (* traverse [t], and if there's a subterm that is shared but - not named yet, name it now. - *) - let traverse_t t : unit = - T.iter_dag_with ~order:T.Iter_dag.Post t - (fun u -> - match T.Tbl.get sharing.terms u with - | Some Shared -> - (* shared, but not named yet *) - let name = new_name() in - Vec.push new_steps (deft_name name u); - T.Tbl.replace sharing.terms u (Named (N_s name)) - | Some (Pre_named name) -> - (* named later in the file, declare it earlier to preserve - a well ordering on definitions since we need it right now *) - Vec.push new_steps - (match name with - | N_s n -> Hashtbl.add skip_name_s n (); deft_name n u - | N_t t -> T.Tbl.add skip_name_t t (); deft t u); - T.Tbl.replace sharing.terms u (Named name) - | _ -> ()) - in - - (* introduce naming in [proof_rule], then push it into {!new_steps} *) - let process_step_ proof_rule = - traverse_step_ proof_rule ~f_t:traverse_t; - (* see if we print the proof_rule or skip it *) - begin match proof_rule with - | S_define_t (t,_) when T.Tbl.mem skip_name_t t -> () - | S_define_t_name (s,_) when Hashtbl.mem skip_name_s s -> () - | _ -> - Vec.push new_steps proof_rule; - end - in - - Array.iter process_step_ steps; - composite_a ~assms:assumptions (Vec.to_array new_steps) - - | p -> p (* TODO: warning? *) +module type CONV_ARG = sig + val proof : Proof.t + val unsat : Proof.proof_step end -(** {2 Print to Quip} +module Make_lazy_tbl(T:sig type t end)() = struct + let lazy_tbl_ : T.t lazy_t Util.Int_tbl.t = Util.Int_tbl.create 32 - Print to a format for checking by an external tool *) -module Quip = struct - module type OUT = sig - type out - type printer = out -> unit - val l : printer list -> printer - val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer - (* list of steps, should be printed vertically if possible *) - val a : string -> printer - end + (** FInd step by its ID *) + let find (id:PS.ID.t) : T.t = + match Util.Int_tbl.get lazy_tbl_ (Int32.to_int id) with + | Some (lazy p) -> p + | None -> + Error.errorf "proof-quip: step `%a` was not reconstructed" PS.ID.pp id - (* - TODO: make sure we print terms properly - *) - - module Make(Out : OUT) = struct - open Out - - let rec pp_t sharing (t:Term.t) : printer = - match T.Tbl.get sharing.Compress.terms t with - | Some (Named (N_s s)) -> a s(* use the newly introduced name *) - | Some (Named (N_t t)) -> pp_t sharing t (* use name *) - | _ -> pp_t_nonshare_root sharing t - - and pp_t_nonshare_root sharing t = - let pp_t = pp_t sharing in - match Term.view t with - | Bool true -> a"true" - | Bool false -> a"false" - | App_fun (c, args) when IArray.is_empty args -> a (ID.to_string (id_of_fun c)) - | App_fun (c, args) -> - l(a (ID.to_string (id_of_fun c)) :: IArray.to_list_map pp_t args) - | Eq (t,u) -> l[a"=";pp_t t;pp_t u] - | Not u -> l[a"not";pp_t u] - | Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3] - | LRA lra -> - begin match lra with - | LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2] - | LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2] - | LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x] - | LRA_const q -> a(Q.to_string q) - | LRA_simplex_var v -> pp_t v - | LRA_simplex_pred (v, op, q) -> - l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)] - | LRA_other x -> pp_t x - end - - let rec pp_ty ty : printer = - match Ty.view ty with - | Ty_bool -> a"Bool" - | Ty_real -> a"Real" - | Ty_atomic {def;args=[];finite=_} -> - let id = Ty.id_of_def def in - a(ID.to_string id) - | Ty_atomic {def;args;finite=_} -> - let id = Ty.id_of_def def in - l(a(ID.to_string id)::List.map pp_ty args) - - let pp_l ppx xs = l (List.map ppx xs) - let pp_lit ~pp_t lit = match lit with - | L_a(b,t) -> l[a(if b then"+" else"-");pp_t t] - | L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]] - let pp_cl ~pp_t c = - l (a "cl" :: List.map (pp_lit ~pp_t) c) - - let rec pp_rec (sharing:Compress.sharing_info) (self:t) : printer = - let pp_rec = pp_rec sharing in - let pp_t = pp_t sharing in - let pp_cl = pp_cl ~pp_t in - match self with - | Unspecified -> a "" - | Named s -> l[a "@"; a s] - | CC_lemma c -> l[a"ccl"; pp_cl c] - | CC_lemma_imply (hyps,t,u) -> - l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u] - | Refl t -> l[a"refl"; pp_t t] - | Sorry -> a"sorry" - | Sorry_c c -> l[a"sorry-c"; pp_cl c] - | Bool_true_is_true -> a"t-is-t" - | Bool_true_neq_false -> a"t-ne-f" - | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2] - | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts) - | Nn p -> l[a"nn";pp_rec p] - | Assertion t -> l[a"assert";pp_t t] - | Assertion_c c -> l[a"assert-c";pp_cl c] - | Drup_res c -> l[a"drup";pp_cl c] - | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)] - | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2] - | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2] - | DT_isa_split (ty,cs) -> - l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)] - | DT_isa_disj (ty,t,u) -> - l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u] - | DT_cstor_inj (c,i,ts,us) -> - l[a"dt.cstor.inj";a(ID.to_string(Cstor.id c)); - a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)] - | Ite_true t -> l[a"ite-true"; pp_t t] - | Ite_false t -> l[a"ite-false"; pp_t t] - | LRA c -> l[a"lra";pp_cl c] - | Composite {steps; assumptions} -> - let pp_ass (n,ass) : printer = - l[a"assuming";a n;pp_lit ~pp_t ass] in - l[a"steps";l(List.map pp_ass assumptions); - iter_toplist (pp_composite_step sharing) (Iter.of_array steps)] - - and pp_composite_step sharing proof_rule : printer = - let pp_t = pp_t sharing in - let pp_cl = pp_cl ~pp_t in - match proof_rule with - | S_step_c {name;res;proof} -> - l[a"stepc";a name;pp_cl res;pp_rec sharing proof] - | S_define_t (c,rhs) -> - (* disable sharing for [rhs], otherwise it'd print [c] *) - l[a"deft";pp_t c; pp_t_nonshare_root sharing rhs] - | S_define_t_name (c,rhs) -> - l[a"deft";a c; pp_t_nonshare_root sharing rhs] - - (* - | S_define_t (name, t) -> - Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t - *) - - and pp_hres_step sharing = function - | R {pivot; p} -> l[a"r";pp_t sharing pivot; pp_rec sharing p] - | R1 p -> l[a"r1";pp_rec sharing p] - | P {p; lhs; rhs} -> - l[a"r"; pp_t sharing lhs; pp_t sharing rhs; pp_rec sharing p] - | P1 p -> l[a"p1"; pp_rec sharing p] - - (* toplevel wrapper *) - let pp self : printer = - (* find sharing *) - let sharing = Profile.with1 "proof.find-sharing" Compress.find_sharing self in - (* introduce names *) - let self = Profile.with2 "proof.rename" Compress.rename sharing self in - (* now print *) - l[a"quip"; a"1"; pp_rec sharing self] - - let pp_debug ~sharing self : printer = - if sharing then pp self - else pp_rec Compress.no_sharing self - end - - module Out_csexp = struct - type out = out_channel - type printer = out -> unit - let l prs out = - output_char out '('; - List.iter (fun x->x out) prs; - output_char out ')' - let a s out = Printf.fprintf out "%d:%s" (String.length s) s - let iter_toplist f it out = - output_char out '('; - it (fun x -> f x out); - output_char out ')' - end - - module Out_sexp = struct - type out = out_channel - type printer = out -> unit - let l prs out = - output_char out '('; - List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs; - output_char out ')' - let a = - let buf = Buffer.create 128 in - fun s out -> - Buffer.clear buf; - CCSexp.to_buf buf (`Atom s); - Buffer.output_buffer out buf - let iter_toplist f it out = - output_char out '('; - let first=ref true in - it (fun x -> if !first then first := false else output_char out '\n'; f x out); - output_char out ')' - end - - type out_format = Sexp | CSexp - let default_out_format = Sexp - - let out_format_ = match Sys.getenv "PROOF_FMT" with - | "csexp" -> CSexp - | "sexp" -> Sexp - | s -> failwith (Printf.sprintf "unknown proof format %S" s) - | exception _ -> default_out_format - - let output oc (self:t) : unit = - match out_format_ with - | Sexp -> let module M = Make(Out_sexp) in M.pp self oc - | CSexp -> - (* canonical sexp *) - let module M = Make(Out_csexp) in M.pp self oc + (** Add entry *) + let add id (e:T.t lazy_t) = + assert (not (Util.Int_tbl.mem lazy_tbl_ (Int32.to_int id))); + Util.Int_tbl.add lazy_tbl_ (Int32.to_int id) e end -let pp_debug ~sharing out p = - let module Out = struct - type out = Format.formatter - type printer = out -> unit - let l prs out = - Fmt.fprintf out "(@["; - List.iteri(fun i x -> if i>0 then Fmt.fprintf out "@ "; x out) prs; - Fmt.fprintf out "@])" - let a s out = Fmt.string out s - let iter_toplist f it out = - Fmt.fprintf out "(@["; - let first=ref true in - it (fun x -> if !first then first := false else Fmt.fprintf out "@ "; f x out); - Fmt.fprintf out "@])" - end - in - let module M = Quip.Make(Out) in - M.pp_debug ~sharing p out +module Conv(X : CONV_ARG) : sig + val reconstruct : unit -> t +end = struct + (* Steps we need to decode. + Invariant: the IDs of these steps must be lower than the current processed + ID (we start from the end) *) + let needed_steps_ = Util.Int_tbl.create 128 -let of_proof _ _ : t = Sorry + let add_needed_step (id:PS.ID.t) : unit = + Util.Int_tbl.replace needed_steps_ (Int32.to_int id) () -let output = Quip.output + let unsat_id = Proof.Unsafe_.id_of_proof_step_ X.unsat + + (* start with the unsat step *) + let () = add_needed_step unsat_id + + (* store reconstructed proofs, but lazily because their dependencies + (sub-steps, terms, etc.) might not have come up in the reverse stream yet. *) + module L_proofs = Make_lazy_tbl(struct type t = P.t end)() + + (* store reconstructed terms *) + module L_terms = Make_lazy_tbl(struct type t = P.term end)() + + (* list of toplevel steps, in the final proof order *) + let top_steps_ : P.composite_step lazy_t list ref = ref [] + let add_top_step s = top_steps_ := s :: !top_steps_ + + let conv_lit (lit:PS.Lit.t) : P.Lit.t lazy_t = + let v = Int32.abs lit in + add_needed_step v; + lazy ( + let t = L_terms.find v in + let sign = lit > Int32.zero in + (* reconstruct literal *) + P.Lit.mk sign t + ) + + let conv_clause (c:PS.Clause.t) : P.clause lazy_t = + let lits = + c.lits + |> Util.array_to_list_map conv_lit + in + lazy (List.map Lazy.force lits) + + (* process a step of the trace *) + let process_step_ (step: PS.Step.t) : unit = + let lid = step.id in + let id = Int32.to_int lid in + if Util.Int_tbl.mem needed_steps_ id then ( + Log.debugf 1 (fun k->k"(@[proof-quip.process-needed-step@ %a@])" PS.Step.pp step); + Util.Int_tbl.remove needed_steps_ id; + + (* now process the step *) + begin match step.view with + | PS.Step_view.Step_input i -> + let c = conv_clause i.PS.Step_input.c in + let name = Printf.sprintf "c%d" id in + let step = lazy ( + let lazy c = c in + P.S_step_c {name; res=c; proof=P.assertion_c_l c} + ) in + add_top_step step; + (* refer to the step by name now *) + L_proofs.add lid (lazy (P.ref_by_name name)); + + | PS.Step_view.Step_unsat us -> () (* TODO *) + | PS.Step_view.Step_rup rup -> () (* TODO *) + | PS.Step_view.Step_bridge_lit_expr _ -> assert false + | PS.Step_view.Step_cc cc -> () (* TODO *) + | PS.Step_view.Step_preprocess _ -> () (* TODO *) + | PS.Step_view.Step_clause_rw _ -> () (* TODO *) + | PS.Step_view.Step_bool_tauto _ -> () (* TODO *) + | PS.Step_view.Step_bool_c _ -> () (* TODO *) + | PS.Step_view.Step_proof_p1 _ -> () (* TODO *) + | PS.Step_view.Step_true _ -> () (* TODO *) + | PS.Step_view.Fun_decl _ -> () (* TODO *) + | PS.Step_view.Expr_def _ -> () (* TODO *) + | PS.Step_view.Expr_bool _ -> () (* TODO *) + | PS.Step_view.Expr_if _ -> () (* TODO *) + | PS.Step_view.Expr_not _ -> () (* TODO *) + | PS.Step_view.Expr_eq _ -> () (* TODO *) + | PS.Step_view.Expr_app _ -> () (* TODO *) + + end + ) + + let reconstruct_once_ = lazy ( + Profile.with_ "proof-quip.reconstruct" @@ fun () -> + Proof.iter_steps_backward X.proof process_step_; + () + ) + + let reconstruct () : t = + Lazy.force reconstruct_once_; + let steps = Util.array_of_list_map Lazy.force !top_steps_ in + P.composite_a steps +end + +let of_proof (self:Proof.t) ~(unsat:Proof.proof_step) : P.t = + let module C = Conv(struct + let proof = self + let unsat = unsat + end) in + C.reconstruct() + +type out_format = Sidekick_quip.out_format = + | Sexp + | CSexp + +let output = Sidekick_quip.output diff --git a/src/base/Proof_quip.mli b/src/base/Proof_quip.mli index 85876f56..3b83b7a2 100644 --- a/src/base/Proof_quip.mli +++ b/src/base/Proof_quip.mli @@ -1,22 +1,13 @@ +(** Export to Quip from {!module:Proof}. -(** Proofs of unsatisfiability exported in Quip - - Proofs are used in sidekick when the problem is found {b unsatisfiable}. - A proof collects inferences made by the solver into a list of steps, - each with its own kind of justification (e.g. "by congruence"), - and outputs it in some kind of format. - - Currently we target {{: https://c-cube.github.io/quip-book/ } Quip} - as an {b experimental} proof backend. -*) - -open Base_types + We use {!Sidekick_quip} but do not export anything from it. *) type t -(** The state holding the whole proof. *) -val pp_debug : sharing:bool -> t Fmt.printer +val of_proof : Proof.t -> unsat:Proof.proof_step -> t -val of_proof : Proof.t -> Proof.proof_step -> t +type out_format = Sidekick_quip.out_format = + | Sexp + | CSexp -val output : out_channel -> t -> unit +val output : ?fmt:out_format -> out_channel -> t -> unit diff --git a/src/base/dune b/src/base/dune index 90751913..a7b3ddd7 100644 --- a/src/base/dune +++ b/src/base/dune @@ -3,7 +3,7 @@ (public_name sidekick-base) (synopsis "Base term definitions for the standalone SMT solver and library") (libraries containers iter sidekick.core sidekick.util sidekick.lit - sidekick-base.proof-trace + sidekick-base.proof-trace sidekick.quip sidekick.arith-lra sidekick.th-bool-static sidekick.th-data sidekick.zarith zarith) diff --git a/src/quip/Sidekick_quip.ml b/src/quip/Sidekick_quip.ml index d0f010f9..b38c34f8 100644 --- a/src/quip/Sidekick_quip.ml +++ b/src/quip/Sidekick_quip.ml @@ -1,430 +1,193 @@ -(** A reference to a previously defined object in the proof *) -type id = int +module Proof = Proof +open Proof -module Ty = struct - type t = - | Bool - | Arrow of t array * t - | App of string * t array - | Ref of id - - let equal : t -> t -> bool = (=) - let hash : t -> int = CCHash.poly - let[@inline] view (self:t) : t = self - - let rec pp out (self:t) = - match self with - | Bool -> Fmt.string out "Bool" - | Arrow (args, ret) -> - Fmt.fprintf out "(@[->@ %a@ %a@])" (Util.pp_array pp) args pp ret - | App (c, [||]) -> Fmt.string out c - | App (c, args) -> - Fmt.fprintf out "(@[%s@ %a@])" c (Util.pp_array pp) args - | Ref id -> Fmt.fprintf out "@@%d" id -end - -module Fun = struct - type t = string - let pp out (self:t) = Fmt.string out self - let equal : t -> t -> bool = (=) - let hash : t -> int = CCHash.poly -end - -module Cstor = Fun - -module T = struct - type t = - | Bool of bool - | App_fun of Fun.t * t array - | App_ho of t * t - | Ite of t * t * t - | Not of t - | Eq of t * t - | Ref of id - let[@inline] view (self:t) : t = self - - let equal : t -> t -> bool = (=) - let hash : t -> int = CCHash.poly - - let rec pp out = function - | Bool b -> Fmt.bool out b - | Ite (a,b,c) -> Fmt.fprintf out "(@[if@ %a@ %a@ %a@])" pp a pp b pp c - | App_fun (f,[||]) -> Fmt.string out f - | App_fun (f,args) -> - Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_array pp) args - | App_ho (f,a) -> Fmt.fprintf out "(@[%a@ %a@])" pp f pp a - | Not a -> Fmt.fprintf out "(@[not@ %a@])" pp a - | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b - | Ref id -> Fmt.fprintf out "@@%d" id - - module As_key = struct - type nonrec t = t - let hash = hash - let equal = equal - end - module Tbl = CCHashtbl.Make(As_key) -end - -type term = T.t -type ty = Ty.t - -type lit = - | L_eq of bool * term * term - | L_a of bool * term - -let lit_not = function - | L_eq (sign,a,b) -> L_eq(not sign,a,b) - | L_a (sign,t) -> L_a (not sign,t) - -let pp_lit_with ~pp_t out = - let strsign = function true -> "+" | false -> "-" in - function - | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u - | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t - -let pp_lit = pp_lit_with ~pp_t:T.pp - -let lit_a t = L_a (true,t) -let lit_na t = L_a (false,t) -let lit_eq t u = L_eq (true,t,u) -let lit_neq t u = L_eq (false,t,u) -let lit_mk b t = L_a (b,t) -let lit_sign = function L_a (b,_) | L_eq (b,_,_) -> b - -type clause = lit list - -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 - | Assertion of term - | Assertion_c of clause - | Drup_res of clause - | Hres of t * hres_step list - | Res of term * t * t - | Res1 of t * t - | DT_isa_split of ty * term list - | DT_isa_disj of ty * term * term - | DT_cstor_inj of Cstor.t * int * term list * term list (* [c t…=c u… |- t_i=u_i] *) - | Bool_true_is_true - | Bool_true_neq_false - | Bool_eq of term * term (* equal by pure boolean reasoning *) - | Bool_c of bool_c_name * term list (* boolean tautology *) - | Nn of t (* negation normalization *) - | 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 array; (* last proof_rule is the proof *) - } - -and bool_c_name = string - -and composite_step = - | S_step_c of { - name: string; (* name *) - res: clause; (* result of [proof] *) - proof: t; (* sub-proof *) - } - | S_define_t of term * term (* [const := t] *) - | S_define_t_name of string * term (* [const := t] *) - -and hres_step = - | R of { pivot: term; p: t} - | R1 of t - | P of { lhs: term; rhs: term; p: t} - | P1 of t - -let r p ~pivot : hres_step = R { pivot; p } -let r1 p = R1 p -let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs } -let p1 p = P1 p - -let stepc ~name res proof : composite_step = S_step_c {proof;name;res} -let deft c rhs : composite_step = S_define_t (c,rhs) -let deft_name c rhs : composite_step = S_define_t_name (c,rhs) - -let is_trivial_refl = function - | Refl _ -> true - | _ -> false - -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 cc_lemma c : t = CC_lemma c -let cc_imply_l l t u : t = - let l = List.filter (fun p -> not (is_trivial_refl p)) l in - match l with - | [] -> refl t (* only possible way [t=u] *) - | l -> CC_lemma_imply (l, t, u) -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_a ?(assms=[]) steps : t = - Composite {assumptions=assms; steps} -let composite_l ?(assms=[]) steps : t = - Composite {assumptions=assms; steps=Array.of_list steps} -let composite_iter ?(assms=[]) steps : t = - let steps = Iter.to_array 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) -let cstor_inj c i t u = DT_cstor_inj (c, i, t, u) - -let ite_true t = Ite_true t -let ite_false t = Ite_false t -let true_is_true : t = Bool_true_is_true -let true_neq_false : t = Bool_true_neq_false -let bool_eq a b : t = Bool_eq (a,b) -let bool_c name c : t = Bool_c (name, c) -let nn c : t = Nn c - -let drup_res c : t = Drup_res c -let hres_l p l : t = - let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in - if l=[] then p else Hres (p,l) -let hres_iter c i : t = hres_l c (Iter.to_list i) -let res ~pivot p1 p2 : t = Res (pivot,p1,p2) -let res1 p1 p2 : t = Res1 (p1,p2) - -let lra_l c : t = LRA c -let lra c = LRA (Iter.to_rev_list c) - -let iter_lit ~f_t = function - | L_eq (_,a,b) -> f_t a; f_t b - | L_a (_,t) -> f_t t - -let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = - match p with - | Unspecified | Sorry -> () - | Sorry_c c -> f_clause c - | Named _ -> () - | Refl t -> f_t t - | CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u - | CC_lemma c | Assertion_c c -> f_clause c - | Assertion t -> f_t t - | Drup_res c -> f_clause c - | Hres (i, l) -> - f_p i; - List.iter - (function - | R1 p -> f_p p - | P1 p -> f_p p - | R {pivot;p} -> f_p p; f_t pivot - | P {lhs;rhs;p} -> f_p p; f_t lhs; f_t rhs) - l - | Res (t,p1,p2) -> f_t t; f_p p1; f_p p2 - | Res1 (p1,p2) -> f_p p1; f_p p2 - | DT_isa_split (_, l) -> List.iter f_t l - | DT_isa_disj (_, t, u) -> f_t t; f_t u - | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us - | Bool_true_is_true | Bool_true_neq_false -> () - | Bool_eq (t, u) -> f_t t; f_t u - | Bool_c (_, ts) -> List.iter f_t ts - | Nn p -> f_p p - | Ite_true t | Ite_false t -> f_t t - | LRA c -> f_clause c - | Composite { assumptions; steps } -> - List.iter (fun (_,lit) -> iter_lit ~f_t lit) assumptions; - Array.iter f_step steps; +type t = Proof.t (** {2 Print to Quip} Print to a format for checking by an external tool *) -module Quip = struct - module type OUT = sig - type out - type printer = out -> unit - val l : printer list -> printer - val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer - (* list of steps, should be printed vertically if possible *) - val a : string -> printer - end + +module type OUT = sig + type out + type printer = out -> unit + val l : printer list -> printer + val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer + (* list of steps, should be printed vertically if possible *) + val a : string -> printer +end + +(** Build a printer that uses {!Out} *) +module Make_printer(Out : OUT) = struct + open Out + + let rec pp_t t = + match T.view t with + | T.Bool true -> a"true" + | T.Bool false -> a"false" + | T.App_fun (c, [||]) -> a c + | T.App_fun (c, args) -> + l(a c :: Util.array_to_list_map pp_t args) + | T.Ref i -> l[a"@"; a(string_of_int i)] + | T.App_ho(f,a) -> l[pp_t f;pp_t a] + | T.Eq (t,u) -> l[a"=";pp_t t;pp_t u] + | T.Not u -> l[a"not";pp_t u] + | T.Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3] + (* + | T.LRA lra -> + begin match lra with + | LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2] + | LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2] + | LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x] + | LRA_const q -> a(Q.to_string q) + | LRA_simplex_var v -> pp_t v + | LRA_simplex_pred (v, op, q) -> + l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)] + | LRA_other x -> pp_t x + end + *) + + let rec pp_ty ty : printer = + match Ty.view ty with + | Ty.Bool -> a"Bool" + | Ty.App (c,[||]) -> + a c + | Ty.App (c,args) -> + l(a c::Util.array_to_list_map pp_ty args) + | Ty.Ref i -> l[a "@"; a (string_of_int i)] + | Ty.Arrow (args,b) -> + l (a "->" :: Util.array_to_list_map pp_ty args @ [pp_ty b]) + + let pp_l ppx xs = l (List.map ppx xs) + let pp_lit ~pp_t lit = match lit with + | Lit.L_a(b,t) -> l[a(if b then"+" else"-");pp_t t] + | Lit.L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]] + let pp_cl ~pp_t c = + l (a "cl" :: List.map (pp_lit ~pp_t) c) + + let rec pp_rec (self:t) : printer = + let pp_cl = pp_cl ~pp_t in + match self with + | Unspecified -> a "" + | Named s -> l[a "@"; a s] + | CC_lemma c -> l[a"ccl"; pp_cl c] + | CC_lemma_imply (hyps,t,u) -> + l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u] + | Refl t -> l[a"refl"; pp_t t] + | Sorry -> a"sorry" + | Sorry_c c -> l[a"sorry-c"; pp_cl c] + | Bool_true_is_true -> a"t-is-t" + | Bool_true_neq_false -> a"t-ne-f" + | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2] + | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts) + | Nn p -> l[a"nn";pp_rec p] + | Assertion t -> l[a"assert";pp_t t] + | Assertion_c c -> l[a"assert-c";pp_cl c] + | Drup_res c -> l[a"drup";pp_cl c] + | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map pp_hres_step steps)] + | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2] + | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2] + | DT_isa_split (ty,cs) -> + l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)] + | DT_isa_disj (ty,t,u) -> + l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u] + | DT_cstor_inj (c,i,ts,us) -> + l[a"dt.cstor.inj";a c; + a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)] + | Ite_true t -> l[a"ite-true"; pp_t t] + | Ite_false t -> l[a"ite-false"; pp_t t] + | LRA c -> l[a"lra";pp_cl c] + | Composite {steps; assumptions} -> + let pp_ass (n,ass) : printer = + l[a"assuming";a n;pp_lit ~pp_t ass] in + l[a"steps";l(List.map pp_ass assumptions); + iter_toplist pp_composite_step (Iter.of_array steps)] + + and pp_composite_step proof_rule : printer = + let pp_cl = pp_cl ~pp_t in + match proof_rule with + | S_step_c {name;res;proof} -> + l[a"stepc";a name;pp_cl res;pp_rec proof] + | S_define_t (c,rhs) -> + (* disable sharing for [rhs], otherwise it'd print [c] *) + l[a"deft";pp_t c; pp_t rhs] + | S_define_t_name (c,rhs) -> + l[a"deft";a c; pp_t rhs] (* - TODO: make sure we print terms properly + | S_define_t (name, t) -> + Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t *) - module Make(Out : OUT) = struct - open Out + and pp_hres_step = function + | R {pivot; p} -> l[a"r";pp_t pivot; pp_rec p] + | R1 p -> l[a"r1";pp_rec p] + | P {p; lhs; rhs} -> + l[a"r"; pp_t lhs; pp_t rhs; pp_rec p] + | P1 p -> l[a"p1"; pp_rec p] - let rec pp_t t = - match T.view t with - | T.Bool true -> a"true" - | T.Bool false -> a"false" - | T.App_fun (c, [||]) -> a c - | T.App_fun (c, args) -> - l(a c :: Util.array_to_list_map pp_t args) - | T.Ref i -> l[a"@"; a(string_of_int i)] - | T.App_ho(f,a) -> l[pp_t f;pp_t a] - | T.Eq (t,u) -> l[a"=";pp_t t;pp_t u] - | T.Not u -> l[a"not";pp_t u] - | T.Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3] - (* - | T.LRA lra -> - begin match lra with - | LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2] - | LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2] - | LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x] - | LRA_const q -> a(Q.to_string q) - | LRA_simplex_var v -> pp_t v - | LRA_simplex_pred (v, op, q) -> - l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)] - | LRA_other x -> pp_t x - end - *) + (* toplevel wrapper *) + let pp self : printer = + fun out -> + Profile.with_ "quip.print" @@ fun () -> + l[a"quip"; a"1"; pp_rec self] out - let rec pp_ty ty : printer = - match Ty.view ty with - | Ty.Bool -> a"Bool" - | Ty.App (c,[||]) -> - a c - | Ty.App (c,args) -> - l(a c::Util.array_to_list_map pp_ty args) - | Ty.Ref i -> l[a "@"; a (string_of_int i)] - | Ty.Arrow (args,b) -> - l (a "->" :: Util.array_to_list_map pp_ty args @ [pp_ty b]) - - let pp_l ppx xs = l (List.map ppx xs) - let pp_lit ~pp_t lit = match lit with - | L_a(b,t) -> l[a(if b then"+" else"-");pp_t t] - | L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]] - let pp_cl ~pp_t c = - l (a "cl" :: List.map (pp_lit ~pp_t) c) - - let rec pp_rec (self:t) : printer = - let pp_cl = pp_cl ~pp_t in - match self with - | Unspecified -> a "" - | Named s -> l[a "@"; a s] - | CC_lemma c -> l[a"ccl"; pp_cl c] - | CC_lemma_imply (hyps,t,u) -> - l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u] - | Refl t -> l[a"refl"; pp_t t] - | Sorry -> a"sorry" - | Sorry_c c -> l[a"sorry-c"; pp_cl c] - | Bool_true_is_true -> a"t-is-t" - | Bool_true_neq_false -> a"t-ne-f" - | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2] - | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts) - | Nn p -> l[a"nn";pp_rec p] - | Assertion t -> l[a"assert";pp_t t] - | Assertion_c c -> l[a"assert-c";pp_cl c] - | Drup_res c -> l[a"drup";pp_cl c] - | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map pp_hres_step steps)] - | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2] - | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2] - | DT_isa_split (ty,cs) -> - l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)] - | DT_isa_disj (ty,t,u) -> - l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u] - | DT_cstor_inj (c,i,ts,us) -> - l[a"dt.cstor.inj";a c; - a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)] - | Ite_true t -> l[a"ite-true"; pp_t t] - | Ite_false t -> l[a"ite-false"; pp_t t] - | LRA c -> l[a"lra";pp_cl c] - | Composite {steps; assumptions} -> - let pp_ass (n,ass) : printer = - l[a"assuming";a n;pp_lit ~pp_t ass] in - l[a"steps";l(List.map pp_ass assumptions); - iter_toplist pp_composite_step (Iter.of_array steps)] - - and pp_composite_step proof_rule : printer = - let pp_cl = pp_cl ~pp_t in - match proof_rule with - | S_step_c {name;res;proof} -> - l[a"stepc";a name;pp_cl res;pp_rec proof] - | S_define_t (c,rhs) -> - (* disable sharing for [rhs], otherwise it'd print [c] *) - l[a"deft";pp_t c; pp_t rhs] - | S_define_t_name (c,rhs) -> - l[a"deft";a c; pp_t rhs] - - (* - | S_define_t (name, t) -> - Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t - *) - - and pp_hres_step = function - | R {pivot; p} -> l[a"r";pp_t pivot; pp_rec p] - | R1 p -> l[a"r1";pp_rec p] - | P {p; lhs; rhs} -> - l[a"r"; pp_t lhs; pp_t rhs; pp_rec p] - | P1 p -> l[a"p1"; pp_rec p] - - (* toplevel wrapper *) - let pp self : printer = - fun out -> - Profile.with_ "quip.print" @@ fun () -> - l[a"quip"; a"1"; pp_rec self] out - - let pp_debug self : printer = pp self - end - - module Out_csexp = struct - type out = out_channel - type printer = out -> unit - let l prs out = - output_char out '('; - List.iter (fun x->x out) prs; - output_char out ')' - let a s out = Printf.fprintf out "%d:%s" (String.length s) s - let iter_toplist f it out = - output_char out '('; - it (fun x -> f x out); - output_char out ')' - end - - module Out_sexp = struct - type out = out_channel - type printer = out -> unit - let l prs out = - output_char out '('; - List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs; - output_char out ')' - let a = - let buf = Buffer.create 128 in - fun s out -> - Buffer.clear buf; - CCSexp.to_buf buf (`Atom s); - Buffer.output_buffer out buf - let iter_toplist f it out = - output_char out '('; - let first=ref true in - it (fun x -> if !first then first := false else output_char out '\n'; f x out); - output_char out ')' - end - - type out_format = Sexp | CSexp - let default_out_format = Sexp - - let out_format_ = match Sys.getenv "PROOF_FMT" with - | "csexp" -> CSexp - | "sexp" -> Sexp - | s -> failwith (Printf.sprintf "unknown proof format %S" s) - | exception _ -> default_out_format - - let output oc (self:t) : unit = - match out_format_ with - | Sexp -> let module M = Make(Out_sexp) in M.pp self oc - | CSexp -> - (* canonical sexp *) - let module M = Make(Out_csexp) in M.pp self oc + let pp_debug self : printer = pp self end +(** Output to canonical S-expressions *) +module Out_csexp = struct + type out = out_channel + type printer = out -> unit + let l prs out = + output_char out '('; + List.iter (fun x->x out) prs; + output_char out ')' + let a s out = Printf.fprintf out "%d:%s" (String.length s) s + let iter_toplist f it out = + output_char out '('; + it (fun x -> f x out); + output_char out ')' +end + +(** Output to classic S-expressions *) +module Out_sexp = struct + type out = out_channel + type printer = out -> unit + let l prs out = + output_char out '('; + List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs; + output_char out ')' + let a = + let buf = Buffer.create 128 in + fun s out -> + Buffer.clear buf; + CCSexp.to_buf buf (`Atom s); + Buffer.output_buffer out buf + let iter_toplist f it out = + output_char out '('; + let first=ref true in + it (fun x -> if !first then first := false else output_char out '\n'; f x out); + output_char out ')' +end + +type out_format = Sexp | CSexp +let string_of_out_format = function + | Sexp -> "sexp" + | CSexp -> "csexp" +let pp_out_format out f = Fmt.string out (string_of_out_format f) + +let default_out_format = Sexp + +let output ?(fmt=Sexp) oc (self:t) : unit = + match fmt with + | Sexp -> + let module M = Make_printer(Out_sexp) in + M.pp self oc + | CSexp -> + let module M = Make_printer(Out_csexp) in + M.pp self oc + let pp_debug out p = let module Out = struct type out = Format.formatter @@ -441,10 +204,6 @@ let pp_debug out p = Fmt.fprintf out "@])" end in - let module M = Quip.Make(Out) in + let module M = Make_printer(Out) in M.pp_debug p out - -let of_proof _ _ : t = Sorry - -let output = Quip.output diff --git a/src/quip/Sidekick_quip.mli b/src/quip/Sidekick_quip.mli index f2d9082e..8aec8774 100644 --- a/src/quip/Sidekick_quip.mli +++ b/src/quip/Sidekick_quip.mli @@ -5,9 +5,21 @@ as an {b experimental} proof backend. *) -type t +module Proof = Proof + +type t = Proof.t (** The state holding the whole proof. *) -val pp_debug : t Fmt.printer +(** What format to use to serialize the proof? *) +type out_format = + | Sexp + (** S-expressions *) -val output : out_channel -> t -> unit + | CSexp + (** Canonical S-expressions *) + +val pp_out_format : out_format Fmt.printer + +val output : ?fmt:out_format -> out_channel -> t -> unit + +val pp_debug : t Fmt.printer diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 36dc2018..1ae6b3fc 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -180,11 +180,11 @@ let solve | Some file -> begin match unsat_proof_step() with | None -> () - | Some step -> + | Some unsat_step -> let proof = Solver.proof s in let proof_quip = Profile.with_ "proof.to-quip" @@ fun () -> - Proof_quip.of_proof proof step + Proof_quip.of_proof proof ~unsat:unsat_step in Profile.with_ "proof.write-file" (fun () -> diff --git a/src/util/Util.ml b/src/util/Util.ml index f0a2357c..c45c7093 100644 --- a/src/util/Util.ml +++ b/src/util/Util.ml @@ -37,6 +37,9 @@ let array_of_list_map f l = let array_to_list_map f arr = CCList.init (Array.length arr) (fun i -> f arr.(i)) +let lazy_map f x = lazy (let (lazy x) = x in f x) +let lazy_map2 f x y = lazy (let (lazy x) = x and (lazy y) = y in f x y) + let setup_gc () = let g = Gc.get () in Gc.set { diff --git a/src/util/Util.mli b/src/util/Util.mli index 91c57501..fc3a58aa 100644 --- a/src/util/Util.mli +++ b/src/util/Util.mli @@ -21,6 +21,9 @@ val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list +val lazy_map : ('a -> 'b) -> 'a lazy_t -> 'b lazy_t +val lazy_map2 : ('a -> 'b -> 'c) -> 'a lazy_t -> 'b lazy_t -> 'c lazy_t + val setup_gc : unit -> unit (** Change parameters of the GC *)