From 0abe4b7020a0b9b02e61dfe151e87218e0a79031 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 27 Oct 2021 21:50:28 -0400 Subject: [PATCH] wip: decode more proof steps to quip --- src/base/Proof.ml | 6 +- src/base/Proof_dummy.ml | 2 +- src/base/Proof_quip.ml | 108 +++++++++++++++--- src/core/Sidekick_core.ml | 6 +- src/lra/sidekick_arith_lra.ml | 2 +- src/proof-trace/proof_ser.bare | 1 + src/proof-trace/proof_ser.ml | 6 +- src/quip/Proof.ml | 9 ++ src/quip/Sidekick_quip.ml | 4 + src/sat/Solver.ml | 5 +- src/smt-solver/Sidekick_smt_solver.ml | 10 +- src/th-bool-static/Sidekick_th_bool_static.ml | 42 ++++--- src/util/Util.ml | 1 + 13 files changed, 159 insertions(+), 43 deletions(-) diff --git a/src/base/Proof.ml b/src/base/Proof.ml index a4d6c2e9..6e43f353 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -216,10 +216,12 @@ let lemma_cc lits (self:t) = let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in PS.(Step_view.Step_cc {Step_cc.eqns=lits}) -let lemma_rw_clause c ~using (self:t) = +let lemma_rw_clause c ~res ~using (self:t) = emit_ self @@ fun() -> + let lits = Iter.map (emit_lit_ self) res |> Iter.to_array in + let res = Proof_ser.{Clause.lits} in let using = Iter.to_array using in - PS.(Step_view.Step_clause_rw {Step_clause_rw.c; using}) + PS.(Step_view.Step_clause_rw {Step_clause_rw.c; res; using}) (* TODO *) let with_defs _ _ (_pr:t) = dummy_step diff --git a/src/base/Proof_dummy.ml b/src/base/Proof_dummy.ml index c44d5f72..14cea03b 100644 --- a/src/base/Proof_dummy.ml +++ b/src/base/Proof_dummy.ml @@ -24,7 +24,7 @@ let emit_unsat_core _ (_pr:t) = () let lemma_preprocess _ _ ~using:_ (_pr:t) = () let lemma_true _ _ = () let lemma_cc _ _ = () -let lemma_rw_clause _ ~using:_ (_pr:t) = () +let lemma_rw_clause _ ~res:_ ~using:_ (_pr:t) = () let with_defs _ _ (_pr:t) = () let lemma_lra _ _ = () diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index 8729bddf..5846e6c7 100644 --- a/src/base/Proof_quip.ml +++ b/src/base/Proof_quip.ml @@ -52,6 +52,9 @@ end = struct (* store reconstructed terms *) module L_terms = Make_lazy_tbl(struct type t = P.term end)() + (* id -> function symbol *) + let funs: P.Fun.t Util.Int_tbl.t = Util.Int_tbl.create 32 + (* 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_ @@ -66,13 +69,23 @@ end = struct P.Lit.mk sign t ) - let conv_clause (c:PS.Clause.t) : P.clause lazy_t = + let conv_lits (lits:PS.Lit.t array) : P.Lit.t list lazy_t = let lits = - c.lits + lits |> Util.array_to_list_map conv_lit in lazy (List.map Lazy.force lits) + let conv_clause (c:PS.Clause.t) : P.clause lazy_t = conv_lits c.lits + + let name_clause (id: PS.ID.t) : string = Printf.sprintf "c%ld" id + + (* TODO: see if we can allow `(stepc c5 (cl …) (… (@ c5) …))`. + Namely, the alias `c5 := (cl …)` could be available within its own proof + so we don't have to print it twice, which is useful for rules like `ccl` + where it's typically `(stepc c5 (cl …) (ccl (cl …)))` for twice the space. + *) + (* process a step of the trace *) let process_step_ (step: PS.Step.t) : unit = let lid = step.id in @@ -85,7 +98,7 @@ end = struct 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 name = name_clause lid in let step = lazy ( let lazy c = c in P.S_step_c {name; res=c; proof=P.assertion_c_l c} @@ -94,23 +107,90 @@ end = struct (* 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_unsat { c=uclause } -> + let c = [] in + let name = "unsat" in + add_needed_step uclause; + let name_c = name_clause uclause in + add_top_step (lazy (P.S_step_c{name; res=c; proof=P.ref_by_name name_c})); + + | PS.Step_view.Step_cc { eqns } -> + let c = conv_lits eqns in + let name = name_clause lid in + let step = lazy ( + let lazy c = c in + P.S_step_c {name; res=c; proof=P.cc_lemma c} + ) in + add_top_step step; + L_proofs.add lid (lazy (P.ref_by_name name)) + + | PS.Step_view.Fun_decl { f } -> + Util.Int_tbl.add funs id f; + + | PS.Step_view.Expr_eq { lhs; rhs } -> + add_needed_step lhs; + add_needed_step rhs; + let t = lazy ( + let lhs = L_terms.find lhs + and rhs = L_terms.find rhs in + P.T.eq lhs rhs + ) in + L_terms.add lid t + + | PS.Step_view.Expr_bool {b} -> + let t = Lazy.from_val (P.T.bool b) in + L_terms.add lid t + + | PS.Step_view.Expr_app { f; args } -> + add_needed_step f; + Array.iter add_needed_step args; + let t = lazy ( + let f = + try Util.Int_tbl.find funs (Int32.to_int f) + with Not_found -> Error.errorf "unknown function '%ld'" f + in + let args = Array.map L_terms.find args in + P.T.app_fun f args + ) in + L_terms.add lid t + + | PS.Step_view.Expr_def _ -> () (* TODO *) + | PS.Step_view.Expr_if _ -> () (* TODO *) + | PS.Step_view.Expr_not _ -> () (* TODO *) + + | PS.Step_view.Step_rup { res; hyps } -> + let res = conv_clause res in + Array.iter add_needed_step hyps; + let name = name_clause lid in + let step = lazy ( + let lazy res = res in + let hyps = Util.array_to_list_map L_proofs.find hyps in + P.S_step_c {name; res; proof=P.rup res hyps} + ) in + add_top_step step; + L_proofs.add lid (lazy (P.ref_by_name name)); + + | PS.Step_view.Step_clause_rw { c; res; using } -> + let res = conv_clause res in + add_needed_step c; + Array.iter add_needed_step using; + let name = name_clause lid in + + let step = lazy ( + let lazy res = res in + let c = L_proofs.find c in + let using = Util.array_to_list_map L_proofs.find using in + P.S_step_c {name; res; proof=P.Clause_rw {res; c0=c; using}} + ) in + add_top_step step; + L_proofs.add lid (lazy (P.ref_by_name name)) + | 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 ) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index cdb083bd..95a0ca70 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -248,10 +248,10 @@ module type PROOF = sig From now on, [t] and [u] will be used interchangeably. @return a proof_rule ID for the clause [(t=u)]. *) - val lemma_rw_clause : proof_step -> using:proof_step Iter.t -> proof_rule - (** [lemma_rw_clause prc ~using], where [prc] is the proof of [|- c], + val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule + (** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c], uses the equations [|- p_i = q_i] from [using] - to rewrite some literals of [c] into [c']. This is used to preprocess + to rewrite some literals of [c] into [res]. This is used to preprocess literals of a clause (using {!lemma_preprocess} individually). *) end diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index aab666da..dcab4b4d 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -239,7 +239,7 @@ module Make(A : ARG) : S with module A = A = struct let pr = A.lemma_lra (Iter.of_list lits) PA.proof in let pr = match using with | None -> pr - | Some using -> SI.P.lemma_rw_clause pr ~using PA.proof in + | Some using -> SI.P.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using PA.proof in PA.add_clause lits pr (* preprocess linear expressions away *) diff --git a/src/proof-trace/proof_ser.bare b/src/proof-trace/proof_ser.bare index ad674107..534afd1e 100644 --- a/src/proof-trace/proof_ser.bare +++ b/src/proof-trace/proof_ser.bare @@ -38,6 +38,7 @@ type Step_preprocess { type Step_clause_rw { c: ID + res: Clause using: []ID } diff --git a/src/proof-trace/proof_ser.ml b/src/proof-trace/proof_ser.ml index 588a7117..e16c628c 100644 --- a/src/proof-trace/proof_ser.ml +++ b/src/proof-trace/proof_ser.ml @@ -483,21 +483,24 @@ end module Step_clause_rw = struct type t = { c: ID.t; + res: Clause.t; using: ID.t array; } (** @raise Bare.Decode.Error in case of error. *) let decode (dec: Bare.Decode.t) : t = let c = ID.decode dec in + let res = Clause.decode dec in let using = (let len = Bare.Decode.uint dec in if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big"); Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in - {c; using; } + {c; res; using; } let encode (enc: Bare.Encode.t) (self: t) : unit = begin ID.encode enc self.c; + Clause.encode enc self.res; (let arr = self.using in Bare.Encode.uint enc (Int64.of_int (Array.length arr)); Array.iter (fun xi -> ID.encode enc xi) arr); @@ -508,6 +511,7 @@ module Step_clause_rw = struct begin Format.fprintf out "{ @["; Format.fprintf out "c=%a;@ " ID.pp x.c; + Format.fprintf out "res=%a;@ " Clause.pp x.res; Format.fprintf out "using=%a;@ " (Bare.Pp.array ID.pp) x.using; Format.fprintf out "@]}"; end) out self diff --git a/src/quip/Proof.ml b/src/quip/Proof.ml index 9bb7b9fc..fb7f6b49 100644 --- a/src/quip/Proof.ml +++ b/src/quip/Proof.ml @@ -51,6 +51,7 @@ module T = struct let true_ : t = Bool true let false_ : t = Bool false + let bool b = Bool b let not_ = function Not x -> x | x -> Not x let eq a b : t = Eq (a,b) let ref id : t = Ref id @@ -115,6 +116,12 @@ type t = | Hres of t * hres_step list | Res of term * t * t | Res1 of t * t + | Rup of clause * t list + | Clause_rw of { + res: clause; + c0: t; + using: t list; (** the rewriting equations/atoms *) + } | 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] *) @@ -178,6 +185,8 @@ 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 rup c hyps : t = Rup (c,hyps) +let clause_rw c0 ~res ~using : t = Clause_rw{res;c0;using} let composite_a ?(assms=[]) steps : t = Composite {assumptions=assms; steps} let composite_l ?(assms=[]) steps : t = diff --git a/src/quip/Sidekick_quip.ml b/src/quip/Sidekick_quip.ml index b38c34f8..47f036dd 100644 --- a/src/quip/Sidekick_quip.ml +++ b/src/quip/Sidekick_quip.ml @@ -87,6 +87,10 @@ module Make_printer(Out : OUT) = struct | 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] + | Rup (c, hyps) -> + l[a"rup";pp_cl c;l(List.map pp_rec hyps)] + | Clause_rw{res; c0; using} -> + l[a"clause-rw";pp_cl res;pp_rec c0;l(List.map pp_rec using)] | 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) -> diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index ecfa7461..0aff55d8 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -2168,12 +2168,13 @@ module Make(Plugin : PLUGIN) in let unsat_conflict = match us with | US_false c0 -> - Log.debugf 1 (fun k->k"unsat conflict clause %a" (Clause.debug store) c0); + Log.debugf 10 (fun k->k"unsat conflict clause %a" (Clause.debug store) c0); let c = resolve_with_lvl0 self c0 in - Log.debugf 1 (fun k->k"proper conflict clause %a" (Clause.debug store) c); + Log.debugf 10 (fun k->k"proper conflict clause %a" (Clause.debug store) c); (fun() -> c) | US_local {core=[]; _} -> assert false | US_local {first; core} -> + (* TODO: do we need to filter out literals? *) let c = lazy ( let core = List.rev core in (* increasing trail order *) assert (Atom.equal first @@ List.hd core); diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 992dcf52..f7da414d 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -394,7 +394,9 @@ module Make(A : ARG) let steps = ref [] in let c' = CCList.map (preprocess_lit ~steps) c in let pr_c' = - A.P.lemma_rw_clause pr_c ~using:(Iter.of_list !steps) proof + A.P.lemma_rw_clause pr_c + ~res:(Iter.of_list c') + ~using:(Iter.of_list !steps) proof in A0.add_clause c' pr_c' @@ -455,7 +457,8 @@ module Make(A : ARG) let pacts = preprocess_acts_of_acts self acts in let c = CCList.map (preprocess_lit_ ~steps self pacts) c in let pr = - P.lemma_rw_clause proof ~using:(Iter.of_list !steps) self.proof + P.lemma_rw_clause proof + ~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof in c, pr @@ -783,7 +786,8 @@ module Make(A : ARG) (* TODO: if c != c0 then P.emit_redundant_clause c because we jsut preprocessed it away? *) let pr = P.emit_input_clause (Iter.of_list c) self.proof in - let pr = P.lemma_rw_clause pr ~using:(Iter.of_list !steps) self.proof in + let pr = P.lemma_rw_clause pr + ~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof in add_clause_l self c pr let assert_term self t = assert_terms self [t] diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index a512afc0..7d401aae 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -136,6 +136,12 @@ module Make(A : ARG) : S with module A = A = struct let steps = ref [] in let add_step_ s = steps := s :: !steps in + let add_step_eq a b ~using ~c0 :unit = + add_step_ @@ SI.P.lemma_rw_clause c0 (SI.Simplify.proof simp) + ~using + ~res:(Iter.return (Lit.atom tst (A.mk_bool tst (B_eq (a,b))))) + in + let[@inline] ret u = Some (u, Iter.of_list !steps) in @@ -170,13 +176,13 @@ module Make(A : ARG) : S with module A = A = struct CCOpt.iter add_step_ prf_a; begin match A.view_as_bool a with | B_bool true -> - add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt prf_a) - (A.lemma_ite_true ~ite:t proof) proof; + add_step_eq t b ~using:(Iter.of_opt prf_a) + ~c0:(A.lemma_ite_true ~ite:t proof); ret b | B_bool false -> - add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt prf_a) - (A.lemma_ite_false ~ite:t proof) proof; + add_step_eq t c ~using:(Iter.of_opt prf_a) + ~c0:(A.lemma_ite_false ~ite:t proof); ret c | _ -> @@ -208,11 +214,10 @@ module Make(A : ARG) : S with module A = A = struct let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in proxy, mk_lit proxy + let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p let pr_p1_opt p s1 s2 : SI.proof_step = CCOpt.map_or ~default:s2 (fun s1 -> SI.P.proof_p1 s1 s2 p) s1 - let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p - (* preprocess "ite" away *) let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option = @@ -221,6 +226,11 @@ module Make(A : ARG) : S with module A = A = struct let ret t = Some (t, Iter.of_list !steps) in + let add_clause_rw lits ~using ~c0 : unit = + PA.add_clause lits @@ + SI.P.lemma_rw_clause c0 ~res:(Iter.of_list lits) ~using PA.proof + in + match A.view_as_bool t with | B_ite (a,b,c) -> let a', pr_a = SI.simp_t si a in @@ -228,26 +238,26 @@ module Make(A : ARG) : S with module A = A = struct begin match A.view_as_bool a' with | B_bool true -> (* [a |- ite a b c=b], [a=true] implies [ite a b c=b] *) - add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt pr_a) - (A.lemma_ite_true ~ite:t PA.proof) PA.proof; + add_step_ + (pr_p1_opt PA.proof pr_a @@ A.lemma_ite_true ~ite:t PA.proof); ret b | B_bool false -> (* [¬a |- ite a b c=c], [a=false] implies [ite a b c=c] *) - add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt pr_a) - (A.lemma_ite_false ~ite:t PA.proof) PA.proof; + add_step_ + (pr_p1_opt PA.proof pr_a @@ A.lemma_ite_false ~ite:t PA.proof); ret c | _ -> let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in let pr_def = SI.P.define_term t_ite t PA.proof in let lit_a = PA.mk_lit_nopreproc a' in - PA.add_clause [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)] - (SI.P.lemma_rw_clause ~using:Iter.(append (return pr_def) (of_opt pr_a)) - (A.lemma_ite_true ~ite:t PA.proof) PA.proof); - PA.add_clause [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)] - (SI.P.lemma_rw_clause ~using:Iter.(append (return pr_def) (of_opt pr_a)) - (A.lemma_ite_false ~ite:t PA.proof) PA.proof); + add_clause_rw [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)] + ~using:Iter.(append (return pr_def) (of_opt pr_a)) + ~c0:(A.lemma_ite_true ~ite:t PA.proof); + add_clause_rw [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)] + ~using:Iter.(append (return pr_def) (of_opt pr_a)) + ~c0:(A.lemma_ite_false ~ite:t PA.proof); ret t_ite end | _ -> None diff --git a/src/util/Util.ml b/src/util/Util.ml index c45c7093..955469f6 100644 --- a/src/util/Util.ml +++ b/src/util/Util.ml @@ -53,3 +53,4 @@ module Int_set = CCSet.Make(CCInt) module Int_map = CCMap.Make(CCInt) module Int_tbl = CCHashtbl.Make(CCInt) +module Str_tbl = CCHashtbl.Make(CCString)