wip: decode more proof steps to quip

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

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 _ _ = ()

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_unsat { c=uclause } ->
-        | PS.Step_view.Step_rup rup -> () (* TODO *)
+          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
     )

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
+  val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
-  (** [lemma_rw_clause prc ~using], where [prc] is the proof of [|- c],
+  (** [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
 

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 *)

src/proof-trace/proof_ser.bare

@@ -38,6 +38,7 @@ type Step_preprocess {
 
 type Step_clause_rw {
   c: ID
+  res: Clause
   using: []ID
 }
 

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

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 =

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) ->

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);

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]

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)
+          add_step_eq t b ~using:(Iter.of_opt prf_a)
-            (A.lemma_ite_true ~ite:t proof) proof;
+            ~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)
+          add_step_eq t c ~using:(Iter.of_opt prf_a)
-            (A.lemma_ite_false ~ite:t proof) proof;
+            ~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)
+          add_step_
-            (A.lemma_ite_true ~ite:t PA.proof) PA.proof;
+            (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)
+          add_step_
-            (A.lemma_ite_false ~ite:t PA.proof) PA.proof;
+            (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)]
+          add_clause_rw [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))
+            ~using:Iter.(append (return pr_def) (of_opt pr_a))
-               (A.lemma_ite_true ~ite:t PA.proof) PA.proof);
+            ~c0:(A.lemma_ite_true ~ite:t PA.proof);
-          PA.add_clause [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)]
+          add_clause_rw [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))
+            ~using:Iter.(append (return pr_def) (of_opt pr_a))
-               (A.lemma_ite_false ~ite:t PA.proof) PA.proof);
+            ~c0:(A.lemma_ite_false ~ite:t PA.proof);
           ret t_ite
       end
     | _ -> None

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)