wip: use real proofs

src/base-solver/sidekick_base_solver.ml

@@ -14,7 +14,7 @@ module Solver_arg = struct
 
   let cc_view = Term.cc_view
   let is_valid_literal _ = true
-  module P = Proof_dummy
+  module P = Sidekick_base.Proof
   type proof = P.t
   type proof_step = P.proof_step
 end
@@ -27,7 +27,7 @@ module Th_data = Sidekick_th_data.Make(struct
     module S = Solver
     open! Base_types
     open! Sidekick_th_data
-    module Proof = Proof_dummy
+    module Proof = Proof
     module Cstor = Cstor
 
     let as_datatype ty = match Ty.view ty with
@@ -75,11 +75,11 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   module S = Solver
   type term = S.T.Term.t
   include Form
-  let lemma_bool_tauto = Proof_dummy.lemma_bool_tauto
-  let lemma_bool_c = Proof_dummy.lemma_bool_c
-  let lemma_bool_equiv = Proof_dummy.lemma_bool_equiv
-  let lemma_ite_true = Proof_dummy.lemma_ite_true
-  let lemma_ite_false = Proof_dummy.lemma_ite_false
+  let lemma_bool_tauto = Proof.lemma_bool_tauto
+  let lemma_bool_c = Proof.lemma_bool_c
+  let lemma_bool_equiv = Proof.lemma_bool_equiv
+  let lemma_ite_true = Proof.lemma_ite_true
+  let lemma_ite_false = Proof.lemma_ite_false
 end)
 
 (** Theory of Linear Rational Arithmetic *)
@@ -102,7 +102,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   let ty_lra _st = Ty.real()
   let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
 
-  let lemma_lra = Proof_dummy.lemma_lra
+  let lemma_lra = Proof.lemma_lra
 
   module Gensym = struct
     type t = {

src/base/Proof.ml

@@ -32,6 +32,7 @@ module Config = struct
   let enable b self = {self with enabled=b}
   let store_in_memory self = {self with storage=In_memory}
   let store_on_disk_at file self = {self with storage=On_disk_at file}
+  let no_store self = {self with storage=No_store}
 end
 
 (* where we store steps *)

src/base/Proof.mli

@@ -23,6 +23,8 @@ module Config : sig
 
   val store_on_disk_at : string -> t -> t
   (** [store_on_disk_at file] stores temporary proof in file [file] *)
+
+  val no_store : t -> t
 end
 
 (** {2 Main Proof API} *)

src/base/Proof_quip.ml

@@ -533,4 +533,6 @@ let pp_debug ~sharing out p =
   M.pp_debug ~sharing p out
 
 
-let of_proof _ : t = assert false
+let of_proof _ _ : t = assert false
+
+let output = Quip.output

src/base/Proof_quip.mli

@@ -17,4 +17,6 @@ type t
 
 val pp_debug : sharing:bool -> t Fmt.printer
 
-val of_proof : Proof.t -> t
+val of_proof : Proof.t -> Proof.proof_step -> t
+
+val output : out_channel -> t -> unit

src/core/Sidekick_core.ml

@@ -1144,7 +1144,11 @@ module type SOLVER = sig
   type res =
     | Sat of Model.t (** Satisfiable *)
     | Unsat of {
-        unsat_core: unit -> lit Iter.t; (** subset of assumptions responsible for unsat *)
+        unsat_core: unit -> lit Iter.t;
+        (** Unsat core (subset of assumptions), or empty *)
+
+        unsat_proof_step : unit -> proof_step option;
+        (** Proof step for the empty clause *)
       } (** Unsatisfiable *)
     | Unknown of Unknown.t
     (** Unknown, obtained after a timeout, memory limit, etc. *)

src/main/main.ml

@@ -30,6 +30,7 @@ let p_stat = ref false
 let p_gc_stat = ref false
 let p_progress = ref false
 let proof_file = ref ""
+let proof_store_memory = ref false
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -69,6 +70,7 @@ let argspec = Arg.align [
     "--stat", Arg.Set p_stat, " print statistics";
     "--proof", Arg.Set p_proof, " print proof";
     "--no-proof", Arg.Clear p_proof, " do not print proof";
+    "--proof-in-memory", Arg.Set proof_store_memory, " store temporary proof in memory";
     "-o", Arg.Set_string proof_file, " file into which to output a proof";
     "--model", Arg.Set p_model, " print model";
     "--no-model", Arg.Clear p_model, " do not print model";
@@ -96,10 +98,36 @@ let check_limits () =
 let main_smt () : _ result =
   let module Proof = Sidekick_smtlib.Proof in
   let tst = Term.create ~size:4_096 () in
-  (* FIXME: use this to enable/disable actual proof
-    let store_proof = !check || !p_proof || !proof_file <> "" in
-     *)
-  let proof = Proof.create() in
+
+  let enable_proof_ = !check || !p_proof || !proof_file <> "" in
+  Log.debugf 1 (fun k->k"(@[proof-enable@ %B@])" enable_proof_);
+
+  (* call [k] with the name of a temporary proof file, and cleanup if necessary *)
+  let run_with_tmp_file k =
+    if enable_proof_ then (
+      CCIO.File.with_temp
+        ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat" k
+    ) else (
+      k "/dev/null"
+    )
+  in
+
+  run_with_tmp_file @@ fun temp_proof_file ->
+  Log.debugf 1 (fun k->k"(@[temp-proof-file@ %S@])" temp_proof_file);
+
+  let config =
+    if enable_proof_ then (
+      Proof.Config.default
+      |> Proof.Config.enable true
+      |> Proof.Config.store_on_disk_at temp_proof_file
+    ) else (
+      Proof.Config.empty
+    )
+  in
+
+  (* main proof object *)
+  let proof = Proof.create ~config () in
+
   let solver =
     let theories =
       (* TODO: probes, to load only required theories *)
@@ -111,6 +139,7 @@ let main_smt () : _ result =
     in
     Process.Solver.create ~proof ~theories tst () ()
   in
+
   (* FIXME: emit an actual proof *)
   let proof_file = if !proof_file ="" then None else Some !proof_file in
   if !check then (
@@ -129,7 +158,7 @@ let main_smt () : _ result =
            Process.process_stmt
              ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
              ~time:!time_limit ~memory:!size_limit
-             ~pp_model:!p_model
+             ~pp_model:!p_model ?proof_file
              ~check:!check ~progress:!p_progress
              solver)
         () input

src/smt-solver/Sidekick_smt_solver.ml

@@ -752,6 +752,10 @@ module Make(A : ARG)
     | Sat of Model.t
     | Unsat of {
         unsat_core: unit -> lit Iter.t;
+        (** Unsat core (subset of assumptions), or empty *)
+
+        unsat_proof_step: unit -> proof_step option;
+        (** Proof step for the empty clause *)
       }
     | Unknown of Unknown.t
     (** Result of solving for the current set of clauses *)
@@ -858,8 +862,9 @@ module Make(A : ARG)
 
     | Sat_solver.Unsat (module UNSAT) ->
       let unsat_core () = UNSAT.unsat_assumptions () in
+      let unsat_proof_step () = Some (UNSAT.unsat_proof()) in
       do_on_exit ();
-      Unsat {unsat_core}
+      Unsat {unsat_core; unsat_proof_step}
 
   let mk_theory (type st)
       ~name ~create_and_setup

src/smtlib/Process.ml

@@ -133,6 +133,7 @@ let mk_progress (_s:Solver.t) : _ -> unit =
 let solve
     ?gc:_
     ?restarts:_
+    ?proof_file
     ?(pp_model=false)
     ?(check=false)
     ?time:_ ?memory:_ ?(progress=false)
@@ -163,7 +164,7 @@ let solve
          *)
       let t3 = Sys.time () -. t2 in
       Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
-    | Solver.Unsat _ ->
+    | Solver.Unsat { unsat_proof_step; unsat_core=_ } ->
 
       if check then (
         ()
@@ -175,16 +176,24 @@ let solve
            *)
       );
 
-      (* FIXME: instead, create a proof if proof file or --check is given
-      begin match proof_file, proof with
-        | Some file, lazy (Some p) ->
-          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 -> Proof.Quip.output oc p; flush oc)
+      begin match proof_file with
+        | Some file ->
+          begin match unsat_proof_step() with
+            | None -> ()
+            | Some step ->
+              let proof = Solver.proof s in
+              let proof_quip =
+                Profile.with_ "proof.to-quip" @@ fun () ->
+                Proof_quip.of_proof proof step
+              in
+              Profile.with_ "proof.write-file"
+                (fun () ->
+                   CCIO.with_out file @@ fun oc ->
+                   Proof_quip.output oc proof_quip;
+                   flush oc);
+          end
         | _ -> ()
       end;
-         *)
 
       let t3 = Sys.time () -. t2 in
       Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
@@ -196,7 +205,7 @@ let solve
 (* process a single statement *)
 let process_stmt
     ?gc ?restarts ?(pp_cnf=false)
-    ?pp_model ?(check=false)
+    ?proof_file ?pp_model ?(check=false)
     ?time ?memory ?progress
     (solver:Solver.t)
     (stmt:Statement.t) : unit or_error =
@@ -234,7 +243,7 @@ let process_stmt
           l
       in
       solve
-        ?gc ?restarts ~check ?pp_model
+        ?gc ?restarts ~check ?pp_model ?proof_file
         ?time ?memory ?progress
         ~assumptions
         solver;

src/smtlib/Process.mli

@@ -7,7 +7,7 @@ module Solver
                             and type T.Term.store = Term.store
                             and type T.Ty.t = Ty.t
                             and type T.Ty.store = Ty.store
-                            and type proof = Proof_dummy.t
+                            and type proof = Proof.t
 
 val th_bool : Solver.theory
 val th_data : Solver.theory
@@ -24,6 +24,7 @@ val process_stmt :
   ?gc:bool ->
   ?restarts:bool ->
   ?pp_cnf:bool ->
+  ?proof_file:string ->
   ?pp_model:bool ->
   ?check:bool ->
   ?time:float ->

src/smtlib/Sidekick_smtlib.ml

@@ -6,7 +6,7 @@ module Process = Process
 module Solver = Process.Solver
 module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
-module Proof = Sidekick_base.Proof_dummy
+module Proof = Sidekick_base.Proof
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Sidekick_smtlib.mli

@@ -10,7 +10,7 @@ module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
 module Process = Process
 module Solver = Process.Solver
-module Proof = Sidekick_base.Proof_dummy (* FIXME: actual DRUP(T) proof *)
+module Proof = Sidekick_base.Proof
 
 val parse : Term.store -> string -> Stmt.t list or_error