From a6d3ed259f404a6b96df384159bf99eebf8ee9ed Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 12 Oct 2022 22:19:41 -0400 Subject: [PATCH] refactor: make it compile again (driver, main) --- src/abstract-solver/asolver.ml | 2 +- src/base/Solver.ml | 4 +- src/main/main.ml | 104 ++++++++++++++------------------- src/main/pure_sat_solver.ml | 27 ++++----- src/smt/tracer.ml | 7 +-- src/smtlib/Driver.ml | 13 +++-- src/smtlib/Sidekick_smtlib.ml | 1 - src/smtlib/Sidekick_smtlib.mli | 1 - 8 files changed, 68 insertions(+), 91 deletions(-) diff --git a/src/abstract-solver/asolver.ml b/src/abstract-solver/asolver.ml index f233fe23..ecf1d7ab 100644 --- a/src/abstract-solver/asolver.ml +++ b/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 diff --git a/src/base/Solver.ml b/src/base/Solver.ml index d2937f60..12438b03 100644 --- a/src/base/Solver.ml +++ b/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 = - create default_arg ?stat ?size ?tracer ~proof ~theories tst () +let create_default ?stat ?size ~tracer ~theories tst : t = + create default_arg ?stat ?size ~tracer ~theories tst () diff --git a/src/main/main.ml b/src/main/main.ml index d469dee0..d1466275 100644 --- a/src/main/main.ml +++ b/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 proof_store_file = ref "" +let trace_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 "; + "--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 () = - if !file_trace = "" then - Sidekick_smt_solver.Tracer.dummy - else ( - let oc = open_out_bin !file_trace in +(* call [k] with the name of a temporary proof file, and cleanup if necessary *) +let run_with_tmp_file ~enable_proof k = + (* TODO: use memory writer if [!proof_store_memory] *) + if enable_proof then + 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 = - if !file_trace = "" then - Clause_tracer.dummy +let mk_sat_tracer () : Sidekick_sat.Tracer.t = + if !trace_file = "" then + 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 - Log.debugf 1 (fun k -> k "(@[proof-enable@ %B@])" enable_proof_); + 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 = - (* 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); + run_with_tmp_file ~enable_proof @@ fun trace_file -> + Log.debugf 1 (fun k -> k "(@[trace_file@ %S@])" trace_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 () in + let tracer = mk_smt_tracer ~trace_file () 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 () = - if !p_stat then Fmt.printf "%a@." Stat.pp stat; - Proof.close proof - in + let finally () = if !p_stat then Fmt.printf "%a@." Stat.pp stat 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 diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 02a6d24a..a1ede58a 100644 --- a/src/main/pure_sat_solver.ml +++ b/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 - | 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" - ); + + (* TODO: extract proof from trace; use check_proof *) let t3 = Sys.time () in Format.printf "Unsat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2)); diff --git a/src/smt/tracer.ml b/src/smt/tracer.ml index 8405d422..00096473 100644 --- a/src/smt/tracer.ml +++ b/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 + inherit Sidekick_proof.Tracer.concrete ~sink as p_tracer 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) = diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml index 82218a4a..b197f0c3 100644 --- a/src/smtlib/Driver.ml +++ b/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 "(@[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; diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 26f43235..cd022f0f 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/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 diff --git a/src/smtlib/Sidekick_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli index c3921b89..563d5f45 100644 --- a/src/smtlib/Sidekick_smtlib.mli +++ b/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