refactor: make it compile again (driver, main)

src/abstract-solver/asolver.ml

@@ -63,4 +63,4 @@ let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () :
   self#solve ?on_exit ?on_progress ?should_stop ~assumptions ()
 
 let last_res (self : #t) = self#last_res
-let proof (self : #t) : #Proof.Tracer.t = self#proof
+let proof (self : #t) : Proof.Tracer.t = self#proof_tracer

src/base/Solver.ml

@@ -5,5 +5,5 @@ let default_arg =
     let view_as_cc = Term.view_as_cc
   end : Sidekick_smt_solver.Sigs.ARG)
 
-let create_default ?stat ?size ?tracer ~proof ~theories tst : t =
+let create_default ?stat ?size ~tracer ~theories tst : t =
-  create default_arg ?stat ?size ?tracer ~proof ~theories tst ()
+  create default_arg ?stat ?size ~tracer ~theories tst ()

src/main/main.ml

@@ -4,14 +4,13 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-open Sidekick_core
 module E = CCResult
 module Fmt = CCFormat
 module Term = Sidekick_base.Term
 module Config = Sidekick_base.Config
 module Solver = Sidekick_smtlib.Solver
 module Driver = Sidekick_smtlib.Driver
-module Proof = Sidekick_smtlib.Proof_trace
+module Proof = Sidekick_proof
 open E.Infix
 
 type 'a or_error = ('a, string) E.t
@@ -23,7 +22,6 @@ let file = ref ""
 let p_cnf = ref false
 let p_proof = ref false
 let p_model = ref false
-let file_trace = ref ""
 let check = ref false
 let time_limit = ref 300.
 let mem_limit = ref 1_000_000_000.
@@ -31,9 +29,9 @@ let restarts = ref true
 let p_stat = ref false
 let p_gc_stat = ref false
 let p_progress = ref false
+let enable_trace = ref false
 let proof_file = ref ""
-let proof_store_memory = ref false
+let trace_file = ref ""
-let proof_store_file = ref ""
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -81,15 +79,12 @@ let argspec =
       "--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" );
-      ( "--proof-trace-file",
-        Arg.Set_string proof_store_file,
-        " store temporary proof in given file (no cleanup)" );
       "-o", Arg.Set_string proof_file, " file into which to output a proof";
       "--model", Arg.Set p_model, " print model";
-      "--trace", Arg.Set_string file_trace, " emit trace into <file>";
+      "--trace", Arg.Set enable_trace, " enable/disable tracing";
+      ( "--trace-file",
+        Arg.Set_string trace_file,
+        " store trace in given file (no cleanup)" );
       "--no-model", Arg.Clear p_model, " do not print model";
       ( "--bool",
         Arg.Symbol
@@ -133,21 +128,34 @@ let check_limits () =
   else if s > !mem_limit then
     raise Out_of_space
 
-let mk_smt_tracer () =
+(* call [k] with the name of a temporary proof file, and cleanup if necessary *)
-  if !file_trace = "" then
+let run_with_tmp_file ~enable_proof k =
-    Sidekick_smt_solver.Tracer.dummy
+  (* TODO: use memory writer if [!proof_store_memory] *)
-  else (
+  if enable_proof then
-    let oc = open_out_bin !file_trace in
+    if !trace_file <> "" then (
+      let file = !trace_file in
+      k file
+    ) else
+      CCIO.File.with_temp ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat"
+        k
+  else
+    k "/dev/null"
+
+let mk_smt_tracer ~trace_file () =
+  if !enable_trace || trace_file <> "" then (
+    Log.debugf 1 (fun k -> k "(@[emit-trace-into@ %S@])" trace_file);
+    let oc = open_out_bin trace_file in
     Sidekick_smt_solver.Tracer.make
       ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc)
       ()
-  )
+  ) else
+    Sidekick_smt_solver.Tracer.dummy
 
-let mk_sat_tracer () : Clause_tracer.t =
+let mk_sat_tracer () : Sidekick_sat.Tracer.t =
-  if !file_trace = "" then
+  if !trace_file = "" then
-    Clause_tracer.dummy
+    Sidekick_sat.Tracer.dummy
   else (
-    let oc = open_out_bin !file_trace in
+    let oc = open_out_bin !trace_file in
     let sink = Sidekick_trace.Sink.of_out_channel_using_bencode oc in
     Pure_sat_solver.tracer ~sink ()
   )
@@ -155,25 +163,11 @@ let mk_sat_tracer () : Clause_tracer.t =
 let main_smt ~config () : _ result =
   let tst = Term.Store.create ~size:4_096 () in
 
-  let enable_proof_ = !check || !p_proof || !proof_file <> "" in
+  let enable_proof = !check || !p_proof || !proof_file <> "" in
-  Log.debugf 1 (fun k -> k "(@[proof-enable@ %B@])" enable_proof_);
+  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 *)
+  run_with_tmp_file ~enable_proof @@ fun trace_file ->
-  let run_with_tmp_file k =
+  Log.debugf 1 (fun k -> k "(@[trace_file@ %S@])" trace_file);
-    (* TODO: use memory writer if [!proof_store_memory] *)
-    if enable_proof_ then
-      if !proof_store_file <> "" then (
-        let file = !proof_store_file in
-        k file
-      ) else
-        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);
 
   (* FIXME
      let config =
@@ -187,8 +181,8 @@ let main_smt ~config () : _ result =
      (* main proof object *)
      let proof = Proof.create ~config () in
   *)
-  let proof = Proof.dummy in
+  let tracer = mk_smt_tracer ~trace_file () in
-  let tracer = mk_smt_tracer () in
+  Proof.Tracer.enable tracer enable_proof;
 
   let solver =
     (* TODO: probes, to load only required theories *)
@@ -199,7 +193,7 @@ let main_smt ~config () : _ result =
             (Sidekick_smt_solver.Theory.name th_bool));
       [ th_bool; Driver.th_ty_unin; Driver.th_data; Driver.th_lra ]
     in
-    Solver.Smt_solver.Solver.create_default ~tracer ~proof ~theories tst ()
+    Solver.Smt_solver.Solver.create_default ~tracer ~theories tst ()
   in
 
   let finally () =
@@ -240,31 +234,19 @@ let main_smt ~config () : _ result =
 
 let main_cnf () : _ result =
   let module S = Pure_sat_solver in
-  let proof, in_memory_proof =
-    (* FIXME
-       if !check then (
-         let pr, inmp = Proof.create_in_memory () in
-         pr, Some inmp
-       ) else if !proof_file <> "" then
-         Proof.create_to_file !proof_file, None
-       else
-    *)
-    Proof.dummy, None
-  in
-
   let stat = Stat.create () in
 
-  let finally () =
+  let finally () = if !p_stat then Fmt.printf "%a@." Stat.pp stat in
-    if !p_stat then Fmt.printf "%a@." Stat.pp stat;
-    Proof.close proof
-  in
   CCFun.protect ~finally @@ fun () ->
+  let enable_proof_ = !check || !p_proof || !proof_file <> "" in
+
   let tst = Term.Store.create () in
   let tracer = mk_sat_tracer () in
-  let solver = S.SAT.create_pure_sat ~size:`Big ~tracer ~proof ~stat () in
+  Proof.Tracer.enable tracer enable_proof_;
+  let solver = S.SAT.create_pure_sat ~size:`Big ~tracer ~stat () in
 
   S.Dimacs.parse_file solver tst !file >>= fun () ->
-  let r = S.solve ~check:!check ?in_memory_proof solver in
+  let r = S.solve ~check:!check solver in
   (* FIXME: if in memory proof and !proof_file<>"",
      then dump proof into file now *)
   r

src/main/pure_sat_solver.ml

@@ -80,9 +80,12 @@ module Dimacs = struct
 end
 
 (** Tracer that emit list of integers. *)
-let tracer ~(sink : Tr.Sink.t) () : Clause_tracer.t =
+let tracer ~(sink : Tr.Sink.t) () : SAT.Tracer.t =
   object (self)
-    method encode_lit (lit : Lit.t) =
+    (* we don't use the proofs, actually. *)
+    inherit Sidekick_proof.Tracer.dummy
+
+    method sat_encode_lit (lit : Lit.t) =
       let sign = Lit.sign lit in
       let i =
         match Term.view (Lit.term lit) with
@@ -95,22 +98,22 @@ let tracer ~(sink : Tr.Sink.t) () : Clause_tracer.t =
         else
           -i)
 
-    method assert_clause ~id (lits : Lit.t Iter.t) =
+    method sat_assert_clause ~id (lits : Lit.t Iter.t) _p =
       let v =
         Ser_value.(
           dict_of_list
             [
               "id", int id;
-              "c", list (lits |> Iter.map self#encode_lit |> Iter.to_rev_list);
+              "c", list (lits |> Iter.map self#sat_encode_lit |> Iter.to_rev_list);
             ])
       in
       Tr.Sink.emit sink ~tag:"AssCSat" v
 
-    method unsat_clause ~id =
+    method sat_unsat_clause ~id =
       let v = Ser_value.(dict_of_list [ "id", int id ]) in
       Tr.Sink.emit sink ~tag:"UnsatC" v
 
-    method delete_clause ~id _lits : unit =
+    method sat_delete_clause ~id _lits : unit =
       let v = Ser_value.(dict_of_list [ "id", int id ]) in
       ignore (Tr.Sink.emit sink ~tag:"DelCSat" v : Tr.Entry_id.t)
   end
@@ -144,7 +147,7 @@ let tracer ~(sink : Tr.Sink.t) () : Clause_tracer.t =
 
 let start = Sys.time ()
 
-let solve ?(check = false) ?in_memory_proof (solver : SAT.t) :
+let solve ?(check = false) (solver : SAT.t) :
     (unit, string) result =
   let res = Profile.with_ "solve" (fun () -> SAT.solve solver) in
   let t2 = Sys.time () in
@@ -155,14 +158,8 @@ let solve ?(check = false) ?in_memory_proof (solver : SAT.t) :
     let t3 = Sys.time () in
     Format.printf "Sat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2)
   | SAT.Unsat _ ->
-    if check then (
+
-      match in_memory_proof with
+      (* TODO: extract proof from trace; use check_proof *)
-      | None ->
-        Error.errorf "Cannot validate proof, no in-memory proof provided"
-      | Some _proof ->
-        let ok = true (* FIXME check_proof proof *) in
-        if not ok then Error.errorf "Proof validation failed"
-    );
 
     let t3 = Sys.time () in
     Format.printf "Unsat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2));

src/smt/tracer.ml

@@ -13,18 +13,17 @@ class type t =
 
 class concrete (sink : Tr.Sink.t) : t =
   object (self)
-    inherit Term.Tracer.concrete ~sink as emit_t
+    inherit Sidekick_proof.Tracer.concrete ~sink as p_tracer
-    inherit Sidekick_proof.Tracer.concrete ~sink
 
     method emit_assert_term t =
-      let id_t = emit_t#emit_term t in
+      let id_t = p_tracer#emit_term t in
       let v = V.int id_t in
       let id = Tr.Sink.emit sink ~tag:"AssT" v in
       id
 
     method sat_encode_lit (lit : Lit.t) : V.t =
       let sign = Lit.sign lit in
-      let id_t = emit_t#emit_term @@ Lit.term lit in
+      let id_t = p_tracer#emit_term @@ Lit.term lit in
       V.(list [ bool sign; int id_t ])
 
     method sat_assert_clause ~id (c : Lit.t Iter.t) (pr : Proof.Step.id) =

src/smtlib/Driver.ml

@@ -1,5 +1,6 @@
 open Sidekick_core
 module Profile = Sidekick_util.Profile
+module Proof = Sidekick_proof
 module Asolver = Solver.Asolver
 open! Sidekick_base
 open Common_
@@ -145,7 +146,7 @@ let solve (self : t) ~assumptions () : Solver.res =
     let t3 = now () in
     Fmt.printf "sat@.";
     Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. time_start) (t2 -. t1) (t3 -. t2)
-  | Asolver.Check_res.Unsat { unsat_step_id; unsat_core = _ } ->
+  | Asolver.Check_res.Unsat { unsat_proof; unsat_core = _ } ->
     if self.check then
       ()
     (* FIXME: check trace?
@@ -157,7 +158,7 @@ let solve (self : t) ~assumptions () : Solver.res =
 
     (match self.proof_file with
     | Some file ->
-      (match unsat_step_id () with
+      (match unsat_proof () with
       | None -> ()
       | Some step_id ->
         (* TODO: read trace; emit proof
@@ -193,7 +194,7 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
   Log.debugf 5 (fun k ->
       k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt);
 
-  let add_step r = Proof_trace.add_step (Asolver.proof self.solver) r in
+  let add_step r = Proof.Tracer.add_step (Asolver.proof self.solver) r in
 
   match stmt with
   | Statement.Stmt_set_logic logic ->
@@ -225,7 +226,7 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
     if self.pp_cnf then Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t;
     let lit = Asolver.lit_of_term self.solver t in
     Asolver.assert_clause self.solver [| lit |]
-      (add_step @@ fun () -> Proof_sat.sat_input_clause [ lit ]);
+      (fun () -> Proof.Sat_rules.sat_input_clause [ lit ]);
     E.return ()
   | Statement.Stmt_assert_clause c_ts ->
     if self.pp_cnf then
@@ -235,9 +236,9 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error =
 
     (* proof of assert-input + preprocessing *)
     let pr =
-      add_step @@ fun () ->
+      fun () ->
       let lits = List.map (Asolver.lit_of_term self.solver) c_ts in
-      Proof_sat.sat_input_clause lits
+      Proof.Sat_rules.sat_input_clause lits
     in
 
     Asolver.assert_clause self.solver (CCArray.of_list c) pr;

src/smtlib/Sidekick_smtlib.ml

@@ -4,7 +4,6 @@ module Driver = Driver
 module Solver = Solver
 module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
-module Proof_trace = Sidekick_core.Proof_trace
 module Check_cc = Check_cc
 
 type 'a or_error = ('a, string) CCResult.t

src/smtlib/Sidekick_smtlib.mli

@@ -10,7 +10,6 @@ module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
 module Driver = Driver
 module Solver = Solver
-module Proof_trace = Sidekick_core.Proof_trace
 module Check_cc = Check_cc
 
 val parse : Term.store -> string -> Stmt.t list or_error