feat: basic proof production for QF_UF (wip)

src/cc/Sidekick_cc.ml

@@ -373,14 +373,14 @@ module Make (A: CC_ARG)
         n.n_expl <- FL_none;
     end
 
-  let raise_conflict (cc:t) ~th (acts:actions) (e:lit list) : _ =
+  let raise_conflict_ (cc:t) ~th (acts:actions) (e:lit list) p : _ =
     Profile.instant "cc.conflict";
     (* clear tasks queue *)
     Vec.clear cc.pending;
     Vec.clear cc.combine;
     List.iter (fun f -> f cc ~th e) cc.on_conflict;
     Stat.incr cc.count_conflict;
-    Actions.raise_conflict acts e P.default
+    Actions.raise_conflict acts e p
 
   let[@inline] all_classes cc : repr Iter.t =
     T_tbl.values cc.tbl
@@ -652,7 +652,14 @@ module Make (A: CC_ARG)
         let lits = explain_decompose cc ~th [] e_ab in
         let lits = explain_pair cc ~th lits a ra in
         let lits = explain_pair cc ~th lits b rb in
-        raise_conflict cc ~th:!th acts (List.rev_map Lit.neg lits)
+        let proof =
+          let lits =
+            Iter.of_list lits
+            |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit)
+          in
+          P.make_cc lits
+        in
+        raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof
       );
       (* We will merge [r_from] into [r_into].
          we try to ensure that [size ra <= size rb] in general, but always
@@ -833,7 +840,14 @@ module Make (A: CC_ARG)
     let th = ref true in
     let lits = explain_decompose cc ~th [] expl in
     let lits = List.rev_map Lit.neg lits in
-    raise_conflict cc ~th:!th acts lits
+    let proof =
+      let lits =
+        Iter.of_list lits
+        |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit)
+      in
+      P.make_cc lits
+    in
+    raise_conflict_ cc ~th:!th acts lits proof
 
   let merge cc n1 n2 expl =
     Log.debugf 5

src/core/Sidekick_core.ml

@@ -146,10 +146,11 @@ module type TERM = sig
 end
 
 module type PROOF = sig
+  type term
   type t
   val pp : t Fmt.printer
-
   val default : t
+  val make_cc : (term*bool) Iter.t -> t
 end
 
 (** Literals
@@ -192,9 +193,10 @@ end
     is inconsistent *)
 module type CC_ACTIONS = sig
   module T : TERM
-  module P : PROOF
   module Lit : LIT with module T = T
 
+  module P : PROOF with type term = T.Term.t
+
   type t
   (** An action handle. It is used by the congruence closure
       to perform the actions below. How it performs the actions
@@ -220,7 +222,7 @@ end
 (** Arguments to a congruence closure's implementation *)
 module type CC_ARG = sig
   module T : TERM
-  module P : PROOF
+  module P : PROOF with type term = T.Term.t
   module Lit : LIT with module T = T
   module Actions : CC_ACTIONS with module T=T and module P = P and module Lit = Lit
 
@@ -231,7 +233,7 @@ end
 (** Signature of the congruence closure *)
 module type CC_S = sig
   module T : TERM
-  module P : PROOF
+  module P : PROOF with type term = T.Term.t
   module Lit : LIT with module T = T
   module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P
   type term_state = T.Term.state
@@ -491,7 +493,7 @@ end
     new lemmas, propagate literals, access the congruence closure, etc. *)
 module type SOLVER_INTERNAL = sig
   module T : TERM
-  module P : PROOF
+  module P : PROOF with type term = T.Term.t
 
   type ty = T.Ty.t
   type term = T.Term.t
@@ -728,7 +730,8 @@ end
     Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *)
 module type SOLVER = sig
   module T : TERM
-  module P : PROOF
+  module P : PROOF with type term = T.Term.t
+
   module Lit : LIT with module T = T
 
   module Solver_internal
@@ -854,6 +857,7 @@ module type SOLVER = sig
     type t
     val check : t -> unit
     val pp_dot : t Fmt.printer
+    val pp : t Fmt.printer
   end
   type proof = Proof.t
 

src/main/main.ml

@@ -21,7 +21,7 @@ exception Out_of_space
 let file = ref ""
 let p_cnf = ref false
 let p_dot_proof = ref ""
-let p_proof_print = ref false
+let p_proof = ref false
 let p_model = ref false
 let check = ref false
 let time_limit = ref 300.
@@ -71,6 +71,8 @@ let argspec = Arg.align [
     "--no-restarts", Arg.Clear restarts, " disable restarts";
     "--dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file";
     "--stat", Arg.Set p_stat, " print statistics";
+    "--proof", Arg.Set p_proof, " print proof";
+    "--no-proof", Arg.Clear p_proof, " do not print proof";
     "--model", Arg.Set p_model, " print model";
     "--no-model", Arg.Clear p_model, " do not print model";
     "--gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC";
@@ -151,7 +153,8 @@ let main () =
         Process.th_lra;
       ]
     in
-    Process.Solver.create ~store_proof:!check ~theories tst () ()
+    let store_proof = !check || !p_proof in
+    Process.Solver.create ~store_proof ~theories tst () ()
   in
   if !check then (
     (* might have to check conflicts *)
@@ -171,7 +174,8 @@ let main () =
            Process.process_stmt
              ~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
              ~time:!time_limit ~memory:!size_limit
-             ?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress
+             ?dot_proof ~pp_proof:!p_proof ~pp_model:!p_model
+             ~check:!check ~progress:!p_progress
              solver)
         () input
     with Exit ->

src/msat-solver/Sidekick_msat_solver.ml

@@ -13,7 +13,7 @@ module Log = Msat.Log
 module type ARG = sig
   open Sidekick_core
   module T : TERM
-  module P : PROOF
+  module P : PROOF with type term = T.Term.t
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
 
@@ -435,6 +435,7 @@ module Make(A : ARG)
     include Sat_solver.Proof
     module Dot = Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver))
     let pp_dot = Dot.pp
+    let pp out (_self:t) = Fmt.string out "<Proof>" (* TODO *)
   end
 
   type proof = Proof.t

src/smtlib/Process.ml

@@ -17,11 +17,7 @@ module Solver_arg = struct
 
   let cc_view = Term.cc_view
   let is_valid_literal _ = true
-  module P = struct
-    type t = Default
-    let default=Default
-    let pp out _ = Fmt.string out "default"
-  end
+  module P = Proof
 end
 module Solver = Sidekick_msat_solver.Make(Solver_arg)
 
@@ -147,6 +143,7 @@ let solve
     ?gc:_
     ?restarts:_
     ?dot_proof
+    ?(pp_proof=false)
     ?(pp_model=false)
     ?(check=false)
     ?time:_ ?memory:_ ?(progress=false)
@@ -179,12 +176,19 @@ let solve
       let t3 = Sys.time () -. t2 in
       Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
     | Solver.Unsat {proof;_} ->
+
+      let proof_opt =
+        if check||pp_proof then Lazy.force proof
+        else None
+      in
+
       if check then (
-        match proof with
-        | lazy (Some p) ->
+        match proof_opt with
+        | Some p ->
           Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
         | _ -> ()
       );
+
       begin match dot_proof, proof with
         | None, _ ->  ()
         | Some file, lazy (Some p) ->
@@ -197,8 +201,18 @@ let solve
                Format.pp_print_flush fmt (); 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 ->
+          Fmt.printf "(@[proof@ %a@])@." Solver.Proof.pp p;
+      );
+
     | Solver.Unknown reas ->
       Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
   end
@@ -206,7 +220,7 @@ let solve
 (* process a single statement *)
 let process_stmt
     ?hyps
-    ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?(check=false)
+    ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_proof ?pp_model ?(check=false)
     ?time ?memory ?progress
     (solver:Solver.t)
     (stmt:Statement.t) : unit or_error =
@@ -240,7 +254,8 @@ let process_stmt
         List.map (fun (sign,t) -> Solver.mk_atom_t solver ~sign t) l
       in
       solve
-        ?gc ?restarts ?dot_proof ~check ?pp_model ?time ?memory ?progress
+        ?gc ?restarts ?dot_proof ~check ?pp_proof ?pp_model
+        ?time ?memory ?progress
         ~assumptions ?hyps
         solver;
       E.return()

src/smtlib/Process.mli

@@ -25,6 +25,7 @@ val process_stmt :
   ?restarts:bool ->
   ?pp_cnf:bool ->
   ?dot_proof:string ->
+  ?pp_proof:bool ->
   ?pp_model:bool ->
   ?check:bool ->
   ?time:float ->

src/smtlib/Sidekick_smtlib.ml

@@ -1,7 +1,6 @@
 (** {1 Process Statements} *)
 
 module ID = Sidekick_base_term.ID
-module Fmt = CCFormat
 module E = CCResult
 module Loc = Smtlib_utils.V_2_6.Loc
 module Parse_ast = Smtlib_utils.V_2_6.Ast
@@ -9,11 +8,7 @@ module Process = Process
 module Solver = Process.Solver
 module Term = Sidekick_base_term.Term
 module Stmt = Sidekick_base_term.Statement
-
-module Proof = struct
-  type t = Proof_default
-  let default = Proof_default
-end
+module Proof = Proof
 
 type 'a or_error = ('a, string) CCResult.t