From 2eee760e292ab18435a96616e38415bda7784465 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 10 Jun 2021 22:20:54 -0400 Subject: [PATCH] refactor(proof): new serialization; faster implem --- src/base-term/Base_types.ml | 6 + src/base-term/Proof.ml | 279 ++++++++++++------ src/cc/Sidekick_cc.ml | 2 +- src/core/Sidekick_core.ml | 9 +- src/main/main.ml | 2 +- src/msat-solver/Sidekick_msat_solver.ml | 7 +- src/smtlib/Process.ml | 20 +- src/smtlib/Process.mli | 1 - src/th-bool-static/Sidekick_th_bool_static.ml | 2 +- 9 files changed, 207 insertions(+), 121 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 04b911aa..15fc467c 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -287,6 +287,7 @@ module Ty : sig val bool : state -> t val real : state -> t val atomic : def -> t list -> t + val id_of_def : def -> ID.t val atomic_uninterpreted : ID.t -> t @@ -399,6 +400,10 @@ end = struct make_ (Ty_atomic {def; args; finite=true;}) let atomic_uninterpreted id = atomic (Ty_uninterpreted id) [] + let id_of_def = function + | Ty_uninterpreted id -> id + | Ty_def {id;_} -> id + | Ty_data {data} -> data.data_id let is_bool t = match t.ty_view with | Ty_bool -> true | _ -> false @@ -1095,6 +1100,7 @@ module Cstor = struct cstor_ty_as_data: data; cstor_ty: ty lazy_t; } + let id c = c.cstor_id let ty_args c = Lazy.force c.cstor_args |> Iter.of_list |> Iter.map Select.ty let equal = eq_cstor diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index 12b50946..4d8262aa 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -292,113 +292,202 @@ end 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 + (* TODO: make sure we print terms properly *) - (* TODO: print into a buffer, without Format (should be faster) *) - (* TODO: print as C-sexp *) + module Make(Out : OUT) = struct + open Out - let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l - let pp_a ppx out l = Fmt.(array ~sep:(return "@ ") ppx) out l - let pp_cl ~pp_t out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l (pp_lit_with ~pp_t)) c + let rec pp_t sharing (t:Term.t) : printer = + match T.Tbl.find_opt 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 - let rec pp_rec (sharing:Compress.sharing_info) out (self:t) : unit = - 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 -> 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 pp_t t pp_t u - | Refl t -> Fmt.fprintf out "(@[refl@ %a@])" pp_t 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@])" - pp_t a pp_t b - | Bool_c (name,ts) -> - Fmt.fprintf out "(@[bool-c %s@ %a@])" name (pp_l pp_t) ts - | Nn p -> Fmt.fprintf out "(@[nn@ %a@])" pp_rec p - | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t 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 sharing)) l - | DT_isa_split (ty,l) -> - Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])" - Ty.pp ty (pp_l pp_t) l - | DT_isa_disj (ty,t,u) -> - Fmt.fprintf out "(@[dt.isa.disj@ (@[ty %a@])@ %a@ %a@])" - Ty.pp ty pp_t t pp_t 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 pp_t) ts Cstor.pp c (pp_l pp_t) us - | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" pp_t t - | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" pp_t 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_with ~pp_t) a in - Fmt.fprintf out "(@[steps@ (@[%a@])@ (@[%a@])@])" - (pp_l pp_ass) assumptions (pp_a (pp_composite_step sharing)) steps + 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 - and pp_t sharing out (t:T.t) = - match T.Tbl.find_opt sharing.Compress.terms t with - | Some (Named (N_s s)) -> - Fmt.string out s (* use the newly introduced name *) - | Some (Named (N_t t)) -> pp_t sharing out t (* use name *) - | _ -> pp_t_noshare_root sharing out t + 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) - and pp_t_noshare_root sharing out t = - Base_types.pp_term_view_gen ~pp_id:ID.pp_name - ~pp_t:(pp_t sharing) out (T.view t) + 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) - and pp_composite_step sharing out step = - let pp_t = pp_t sharing in - let pp_cl = pp_cl ~pp_t in - match step with - | S_step_c {name;res;proof} -> - Fmt.fprintf out "(@[stepc %s@ %a@ %a@])" name pp_cl res (pp_rec sharing) proof - | S_define_t (c,rhs) -> - Fmt.fprintf out "(@[deft@ %a@ %a@])" - Term.pp c (pp_t_noshare_root sharing) rhs - | S_define_t_name (c,rhs) -> - Fmt.fprintf out "(@[deft@ %s@ %a@])" - c (pp_t_noshare_root sharing) rhs + 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"true-is-true" + | Bool_true_neq_false -> a"true-neq-false" + | 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] + | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)] + | 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)] - (* - | S_define_t (name, t) -> - Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t - *) + and pp_composite_step sharing step : printer = + let pp_t = pp_t sharing in + let pp_cl = pp_cl ~pp_t in + match step 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] - and pp_hres_step sharing out = function - | R {pivot; p} -> - Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" (pp_t sharing) pivot (pp_rec sharing) p - | R1 p -> Fmt.fprintf out "(@[r1@ %a@])" (pp_rec sharing) p - | P {p; lhs; rhs} -> - Fmt.fprintf out "(@[r@ (@[lhs@ %a@])@ (@[rhs@ %a@])@ %a@])" - (pp_t sharing) lhs (pp_t sharing) rhs (pp_rec sharing) p - | P1 p -> Fmt.fprintf out "(@[p1@ %a@])" (pp_rec sharing) p + (* + | S_define_t (name, t) -> + Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t + *) - (* toplevel wrapper *) - let pp out self = - (* 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 *) - Fmt.fprintf out "(@[quip 1@ %a@])" (pp_rec sharing) self + 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] - let pp_debug out self : unit = - pp_rec Compress.no_sharing out self + (* 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 + + let output oc (self:t) : unit = + (* canonical sexp *) + if true then ( + let module M = Make(Out_sexp) in M.pp self oc + ) else ( + let module M = Make(Out_csexp) in M.pp self oc + ) end -let pp_debug = Quip.pp_debug +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 diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 2135192d..093aaacf 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_debug p + | E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" (P.pp_debug ~sharing:false) 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 6363162f..2d84a8a5 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -209,10 +209,10 @@ module type PROOF = sig val default : t [@@alert cstor "do not use default constructor"] - val pp_debug : t Fmt.printer + val pp_debug : sharing:bool -> t Fmt.printer module Quip : sig - val pp : t Fmt.printer + val output : out_channel -> t -> unit (** Printer in Quip format (experimental) *) end end @@ -1004,7 +1004,10 @@ module type SOLVER = sig module Pre_proof : sig type t - val pp : t Fmt.printer + val output : out_channel -> t -> unit + (** Output onto a channel, efficiently *) + + val pp_debug : t Fmt.printer val pp_dot : t Fmt.printer option (** Optional printer into DOT/graphviz *) diff --git a/src/main/main.ml b/src/main/main.ml index e37c228f..ec72a84d 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -177,7 +177,7 @@ let main () = Process.process_stmt ~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file ~time:!time_limit ~memory:!size_limit - ?dot_proof ~pp_proof:!p_proof ~pp_model:!p_model + ?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress solver) () input diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 16836cdc..b7333b82 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -352,7 +352,7 @@ module Make(A : ARG) if not (Lit.equal lit lit') then ( Log.debugf 10 (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])" - Lit.pp lit Lit.pp lit' P.pp_debug p); + Lit.pp lit Lit.pp lit' (P.pp_debug ~sharing:false) p); ); lit', p @@ -639,7 +639,8 @@ module Make(A : ARG) { msat; tdefs; p=lazy (conv_proof msat tdefs) } let check self = SP.check self.msat - let pp out (self:t) = P.Quip.pp out (to_proof self) + let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self) + let output oc (self:t) = P.Quip.output oc (to_proof self) end (* main solver state *) @@ -828,7 +829,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_debug proof); + (Util.pp_iarray Atom.pp) c (P.pp_debug ~sharing:false) proof); let pb = Profile.begin_ "add-clause" in Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof; Profile.exit pb diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index bd83fbbb..5dba5e27 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -143,7 +143,6 @@ let solve ?gc:_ ?restarts:_ ?dot_proof - ?(pp_proof=false) ?(pp_model=false) ?proof_file ?(check=false) @@ -179,7 +178,7 @@ let solve | Solver.Unsat {proof;_} -> let proof_opt = - if check||pp_proof then Lazy.force proof + if check||CCOpt.is_some proof_file then Lazy.force proof else None in @@ -207,24 +206,13 @@ let solve Profile.with_ "proof.write-file" @@ fun () -> let p = Profile.with1 "proof.mk-proof" Solver.Pre_proof.to_proof p in CCIO.with_out file - (fun oc -> - let fmt = Format.formatter_of_out_channel oc in - Fmt.fprintf fmt "%a@." Proof.Quip.pp p); + (fun oc -> Proof.Quip.output oc p; flush oc) | _ -> () end; let t3 = Sys.time () -. t2 in Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; - (* TODO: allow to print proof into a file, more realistic for checking *) - if pp_proof then ( - match proof_opt with - | None -> Error.errorf "cannot print proof, none was generated" - | Some p -> - let p = Solver.Pre_proof.to_proof p in - Fmt.printf "(@[proof@ %a@])@." Solver.P.Quip.pp p; - ); - | Solver.Unknown reas -> Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas end @@ -233,7 +221,7 @@ let solve let process_stmt ?hyps ?gc ?restarts ?(pp_cnf=false) - ?dot_proof ?pp_proof ?proof_file ?pp_model ?(check=false) + ?dot_proof ?proof_file ?pp_model ?(check=false) ?time ?memory ?progress (solver:Solver.t) (stmt:Statement.t) : unit or_error = @@ -272,7 +260,7 @@ let process_stmt l in solve - ?gc ?restarts ?dot_proof ~check ?pp_proof ?proof_file ?pp_model + ?gc ?restarts ?dot_proof ~check ?proof_file ?pp_model ?time ?memory ?progress ~assumptions ?hyps solver; diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 7277edaa..abe20f0b 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -25,7 +25,6 @@ val process_stmt : ?restarts:bool -> ?pp_cnf:bool -> ?dot_proof:string -> - ?pp_proof:bool -> ?proof_file:string -> ?pp_model:bool -> ?check:bool -> diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 300cb827..e47d3899 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -360,7 +360,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.Quip.pp pr_t_u); + T.pp t T.pp u (SI.P.pp_debug ~sharing:false) pr_t_u); SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); ()); end;