real proof production for CC

src/algos/simplex/tests/test_simplex.real.ml

@@ -116,7 +116,7 @@ module Step = struct
         return (List.rev acc)
       else
         let* vars, proof_rule =
-          frequency
+          oneof_weighted
           @@ List.flatten
                [
                  (* add a bound *)

src/cc/CC.ml

@@ -302,41 +302,48 @@ module Expl_state = struct
     let { lits = o_lits; th_lemmas = o_lemmas } = other in
     self.lits <- List.rev_append o_lits self.lits;
     self.th_lemmas <- List.rev_append o_lemmas self.th_lemmas;
-
     ()
 
+  let emit_cc_eq_proof (self : t) (_tracer : Proof.Tracer.t) : Proof.Pterm.t =
+    let neg_lits = List.rev_map Lit.neg self.lits in
+    Proof.Pterm.apply_rule ~lits:neg_lits "core.cc-eq-proof"
+
   (* proof of [\/_i ¬lits[i]] *)
   let proof_of_th_lemmas (self : t) (tracer : Proof.Tracer.t) :
       Proof.Pterm.delayed =
     Proof.Pterm.delay @@ fun () ->
-    (* Emit each sub-proof immediately; use its offset (Step.id) as a P_ref. *)
-    let bind (t : Proof.Pterm.t) : Proof.Step.id =
-      Proof.Tracer.add_step tracer (Proof.Pterm.delay (fun () -> t))
-    in
-
-    let p_lits1 = List.rev_map Lit.neg self.lits in
-    let p_lits2 =
-      self.th_lemmas |> List.rev_map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u)
-    in
-    let p_cc = Proof.Core_rules.lemma_cc (List.rev_append p_lits1 p_lits2) in
-    let resolve_with_th_proof pr (lit_t_u, sub_proofs, pr_th) =
-      let pr_th = pr_th () in
-      let pr_th =
-        List.fold_left
-          (fun pr_th (lit_i, hyps_i) ->
-            let lemma_i =
-              bind
-              @@ Proof.Core_rules.lemma_cc (lit_i :: List.rev_map Lit.neg hyps_i)
-            in
-            Proof.Core_rules.proof_res ~pivot:(Lit.term lit_i) lemma_i
-              (bind pr_th))
-          pr_th sub_proofs
+    if self.th_lemmas = [] then
+      emit_cc_eq_proof self tracer
+    else (
+      let bind (t : Proof.Pterm.t) : Proof.Step.id =
+        Proof.Tracer.add_step tracer (Proof.Pterm.delay (fun () -> t))
       in
-      Proof.Core_rules.proof_res ~pivot:(Lit.term lit_t_u) (bind pr_th)
-        (bind pr)
-    in
-    let body = List.fold_left resolve_with_th_proof p_cc self.th_lemmas in
-    body
+
+      let p_lits1 = List.rev_map Lit.neg self.lits in
+      let p_lits2 =
+        self.th_lemmas |> List.rev_map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u)
+      in
+      let p_cc = Proof.Core_rules.lemma_cc (List.rev_append p_lits1 p_lits2) in
+      let resolve_with_th_proof pr (lit_t_u, sub_proofs, pr_th) =
+        let pr_th = pr_th () in
+        let pr_th =
+          List.fold_left
+            (fun pr_th (lit_i, hyps_i) ->
+              let lemma_i =
+                bind
+                @@ Proof.Core_rules.lemma_cc
+                     (lit_i :: List.rev_map Lit.neg hyps_i)
+              in
+              Proof.Core_rules.proof_res ~pivot:(Lit.term lit_i) lemma_i
+                (bind pr_th))
+            pr_th sub_proofs
+        in
+        Proof.Core_rules.proof_res ~pivot:(Lit.term lit_t_u) (bind pr_th)
+          (bind pr)
+      in
+      let body = List.fold_left resolve_with_th_proof p_cc self.th_lemmas in
+      body
+    )
 
   let to_resolved_expl (self : t) (tracer : Proof.Tracer.t) : Resolved_expl.t =
     let { lits; th_lemmas = _ } = self in

src/main/dune

@@ -10,11 +10,3 @@
    sidekick.smt-solver sidekick-base.smtlib sidekick.drup sidekick.memtrace
    sidekick-bin.lib sidekick.proof_twp sidekick.proof-minidag)
  (flags :standard -safe-string -color always -open Sidekick_util))
-
-(executable
- (name show_trace)
- (modules show_trace)
- (modes native)
- (libraries containers sidekick.util sidekick.core sidekick.trace
-   sidekick.smt-solver sidekick.proof sidekick-base)
- (flags :standard -safe-string -color always -open Sidekick_util))

src/main/show_trace.ml

@@ -1,95 +0,0 @@
-open Sidekick_core
-open Sidekick_trace
-module Proof = Sidekick_proof
-module Smt = Sidekick_smt_solver
-
-type state = {
-  dump: bool;
-  src: Source.t;
-  t_reader: Smt.Trace_reader.t;
-  p_reader: Proof.Trace_reader.t;
-}
-
-let show_sat (_self : state) ~tag v : unit =
-  match tag with
-  | "AssCSat" ->
-    (match
-       Ser_decode.(
-         let d =
-           let+ id = dict_field "id" int and+ c = dict_field "c" (list int) in
-           id, c
-         in
-         run d v)
-     with
-    | Ok (id, c) -> Fmt.printf "[%d]: %a@." id Fmt.Dump.(list int) c
-    | Error _ -> ())
-  | "DelCSat" ->
-    (match
-       Ser_decode.(
-         let d =
-           let+ id = dict_field "id" int in
-           id
-         in
-         run d v)
-     with
-    | Ok id -> Fmt.printf "del [%d]@." id
-    | Error _ -> ())
-  | "UnsatC" ->
-    (match
-       Ser_decode.(
-         let d =
-           let+ id = dict_field "id" int in
-           id
-         in
-         run d v)
-     with
-    | Ok id -> Fmt.printf "unsat [%d]@." id
-    | Error _ -> ())
-  | _ -> ()
-
-let show_event (self : state) i ~tag v : unit =
-  Log.debugf 10 (fun k ->
-      k "(@[show-trace[%d]@ :tag %S@ :val %a@])" i tag Ser_value.pp v);
-  if self.dump then Format.printf "[%d]: %S %a@." i tag Ser_value.pp v;
-
-  (match Smt.Trace_reader.decode self.t_reader ~tag v with
-  | Some e -> Fmt.printf "[%d]: %a@." i Smt.Trace_reader.pp_entry e
-  | None -> ());
-
-  show_sat self ~tag v;
-  ()
-
-let show_file ~dump file : unit =
-  Log.debugf 1 (fun k -> k "(@[show-file %S@])" file);
-  let src = Source.of_string_using_bencode @@ CCIO.File.read_exn file in
-  let tst = Term.Store.create () in
-
-  (* trace reader *)
-  let t_reader =
-    Smt.Trace_reader.create tst src
-      ~const_decoders:
-        [ Sidekick_core.const_decoders; Sidekick_base.const_decoders ]
-  in
-  let p_reader =
-    Proof.Trace_reader.create ~src (Smt.Trace_reader.term_trace_reader t_reader)
-  in
-
-  let st = { t_reader; src; dump; p_reader } in
-  Source.iter_all src (fun i ~tag v -> show_event st i ~tag v)
-
-let () =
-  let files = ref [] in
-  let dump = ref false in
-  let opts =
-    [
-      "--dump", Arg.Set dump, " dump each raw entry";
-      ( "--bt",
-        Arg.Unit (fun () -> Printexc.record_backtrace true),
-        " enable backtraces" );
-      "-d", Arg.Int Log.set_debug, " debug level";
-    ]
-    |> Arg.align
-  in
-  Arg.parse opts (fun f -> files := f :: !files) "show_trace [file]+";
-  let files = List.rev !files in
-  List.iter (show_file ~dump:!dump) files

src/proof_minidag/proof_encoder.ml

@@ -34,7 +34,7 @@ let emit_seq self ~hyps ~concls =
 (** Emit [p.hyp] with the given conclusion offsets and no hypotheses. *)
 let emit_hyp self concls =
   let seq = emit_seq self ~hyps:[] ~concls in
-  nd self "p.hyp" (fun e -> E.ref e seq)
+  nd self "hol.hypothesis" (fun e -> E.ref e seq)
 
 (** Emit [sk.sorry] with a descriptive message. *)
 let emit_sorry self msg = nd self "sk.sorry" (fun e -> E.string e msg)
@@ -60,10 +60,158 @@ let emit_sat_rup self hyp_sids =
   let dag_offs = List.map (step_off self) hyp_sids in
   nd self "sk.sat_rup" (fun e -> List.iter (E.ref e) dag_offs)
 
-(** CC conflict: oracle step referencing all conflicting lits. *)
-let emit_cc_conflict self lits =
-  let lit_offs = List.map (encode_lit' self) lits in
-  nd self "sk.cc_conflict" (fun e -> List.iter (E.ref e) lit_offs)
+(** Extract equality pairs [(a, b)] from positive equality literals. A positive
+    literal [a = b] (encoded as [(= a b)]) yields [(a, b)]. A negative literal
+    [not(a = b)] is skipped. *)
+let eq_pairs_of_lits (_tst : Term.store) lits =
+  List.filter_map
+    (fun lit ->
+      if Lit.sign lit then (
+        let t = Lit.term lit in
+        match Term.view t with
+        | Term.E_app (eq, a) ->
+          (match Term.view eq with
+          | Term.E_app (_, b) -> Some (a, b)
+          | _ -> None)
+        | _ -> None
+      ) else
+        None)
+    lits
+
+(** Compute congruence closure steps from a set of equalities. Uses a union-find
+    over [Term.t] (by identity/physical equality). Returns a list of [(t, u)]
+    pairs for [eq.c] steps in an order that respects dependencies (congruence
+    steps use terms whose sub-terms are already equal via prior unions or
+    congruences). *)
+let compute_cc_steps eq_pairs =
+  let uf = Term.Tbl.create 16 in
+  let rec find t =
+    match Term.Tbl.find_opt uf t with
+    | None -> t
+    | Some r ->
+      if Term.equal r t then
+        t
+      else (
+        let r = find r in
+        Term.Tbl.replace uf t r;
+        r
+      )
+  in
+  let union a b =
+    let a = find a and b = find b in
+    if not (Term.equal a b) then Term.Tbl.replace uf a b
+  in
+  (* Collect all application terms reachable from both sides of equalities *)
+  let all_terms =
+    let seen = Term.Tbl.create 16 in
+    let acc = ref [] in
+    let rec collect t =
+      if Term.Tbl.mem seen t then
+        ()
+      else (
+        Term.Tbl.add seen t ();
+        acc := t :: !acc;
+        match Term.view t with
+        | Term.E_app (f, x) ->
+          collect f;
+          collect x
+        | _ -> ()
+      )
+    in
+    List.iter
+      (fun (a, b) ->
+        collect a;
+        collect b)
+      eq_pairs;
+    !acc
+  in
+  let app_terms =
+    List.filter_map
+      (fun t ->
+        match Term.view t with
+        | Term.E_app (f, x) -> Some (t, f, x)
+        | _ -> None)
+      all_terms
+  in
+  (* Step 1: do all initial unions *)
+  List.iter (fun (a, b) -> union a b) eq_pairs;
+  (* Step 2: fixed-point congruence detection *)
+  let module PairKey = struct
+    type t = Term.t * Term.t
+
+    let equal (a1, b1) (a2, b2) = Term.equal a1 a2 && Term.equal b1 b2
+    let hash (a, b) = Hash.combine2 (Term.hash a) (Term.hash b)
+  end in
+  let module PairTbl = CCHashtbl.Make (PairKey) in
+  let congr_pairs = ref [] in
+  let changed = ref true in
+  while !changed do
+    changed := false;
+    let app_sig = PairTbl.create 16 in
+    List.iter
+      (fun (t, f, x) ->
+        let key = find f, find x in
+        match PairTbl.get app_sig key with
+        | None -> PairTbl.add app_sig key t
+        | Some other ->
+          if not (Term.equal (find other) (find t)) then (
+            congr_pairs := (other, t) :: !congr_pairs;
+            union other t;
+            changed := true
+          ))
+      app_terms
+  done;
+  eq_pairs, List.rev !congr_pairs
+
+(** Emit a [p.eq] proof from negated conflict literals. Extracts equalities,
+    computes congruence closure, emits [eq.u]/[eq.c] steps. *)
+let emit_cc_eq_proof self neg_lits =
+  let true_off = encode_term' self (Term.true_ self.tst) in
+  let false_off = encode_term' self (Term.false_ self.tst) in
+  let lit_offs = List.map (encode_lit' self) neg_lits in
+  (* Build dag: one hypothesis per negated literal *)
+  let dag_offs =
+    Array.of_list
+      (List.map
+         (fun lit_off ->
+           let seq = emit_seq self ~hyps:[] ~concls:[ lit_off ] in
+           nd self "hol.hypothesis" (fun e -> E.ref e seq))
+         lit_offs)
+  in
+  (* Extract equalities and compute congruences *)
+  let eq_pairs, congr_pairs =
+    compute_cc_steps (eq_pairs_of_lits self.tst neg_lits)
+  in
+  (* Emit eq.u for each equality, using dag[i] for the i-th equality literal *)
+  let eq_step_offs = ref [] in
+  List.iteri
+    (fun i (a, b) ->
+      let eq_lit = encode_term' self (Term.eq self.tst a b) in
+      let step =
+        nd self "eq.u" (fun e ->
+            E.ref e dag_offs.(i);
+            E.ref e eq_lit)
+      in
+      eq_step_offs := !eq_step_offs @ [ step ])
+    eq_pairs;
+  (* Emit eq.c for each congruence pair *)
+  List.iter
+    (fun (t, u) ->
+      let t_off = encode_term' self t in
+      let u_off = encode_term' self u in
+      let step =
+        nd self "eq.c" (fun e ->
+            E.ref e t_off;
+            E.ref e u_off)
+      in
+      eq_step_offs := !eq_step_offs @ [ step ])
+    congr_pairs;
+  nd self "p.eq" (fun e ->
+      E.ref e true_off;
+      E.ref e false_off;
+      List.iter (E.ref e) !eq_step_offs;
+      E.null e;
+      Array.iter (E.ref e) dag_offs)
 
 (** Boolean axiom: any [bool.*] rule name. *)
 let emit_bool_ax self name term_args =
@@ -111,7 +259,10 @@ let rec encode_rule self (r : Pterm.rule_apply) : E.offset =
           E.ref e o1;
           E.ref e o2)
     | _ -> emit_sorry self "core.p1: bad args")
-  | "core.lemma-cc" -> emit_cc_conflict self lit_args
+  | "core.lemma-cc" ->
+    let lit_offs = List.map (encode_lit' self) lit_args in
+    nd self "sk.cc_conflict" (fun e -> List.iter (E.ref e) lit_offs)
+  | "core.cc-eq-proof" -> emit_cc_eq_proof self lit_args
   | "core.define-term" ->
     (match term_args with
     | [ c; rhs ] -> emit_hyp self [ encode_term' self (Term.eq self.tst c rhs) ]