From 06a0089a8c678d598219a67059d04092659a5bf4 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Oct 2022 23:07:53 -0400 Subject: [PATCH] feat: add `Clause_tracer`, works both for SMT and SAT --- src/core/Sidekick_core.ml | 1 + src/core/clause_tracer.ml | 30 ++++++++++++++++++ src/core/clause_tracer.mli | 22 +++++++++++++ src/main/main.ml | 18 ++++++++--- src/main/pure_sat_solver.ml | 40 +++++++++++++++++++++++- src/main/show_trace.ml | 61 ++++++++++++++++++++++++++++++++----- src/sat/solver.ml | 30 ++++++++++++++---- src/sat/solver.mli | 2 ++ 8 files changed, 185 insertions(+), 19 deletions(-) create mode 100644 src/core/clause_tracer.ml create mode 100644 src/core/clause_tracer.mli diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 25545ea5..951d5844 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -46,5 +46,6 @@ module Proof_term = Proof_term module Subst = Sidekick_core_logic.Subst module Var = Sidekick_core_logic.Var module Box = Box +module Clause_tracer = Clause_tracer exception Resource_exhausted diff --git a/src/core/clause_tracer.ml b/src/core/clause_tracer.ml new file mode 100644 index 00000000..297c355e --- /dev/null +++ b/src/core/clause_tracer.ml @@ -0,0 +1,30 @@ +module Tr = Sidekick_trace + +class type t = + object + method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t + method delete_clause : id:int -> Lit.t Iter.t -> unit + method unsat_clause : id:int -> Tr.Entry_id.t + method encode_lit : Lit.t -> Ser_value.t + end + +let dummy : t = + object + method assert_clause ~id:_ _ = Tr.Entry_id.dummy + method delete_clause ~id:_ _ = () + method unsat_clause ~id:_ = Tr.Entry_id.dummy + method encode_lit _ = Ser_value.null + end + +let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c + +let assert_clause' (self : #t) ~id c : unit = + ignore (self#assert_clause ~id c : Tr.Entry_id.t) + +let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id + +let unsat_clause' (self : #t) ~id : unit = + ignore (self#unsat_clause ~id : Tr.Entry_id.t) + +let delete_clause (self : #t) ~id c = self#delete_clause ~id c +let encode_lit (self : #t) lit = self#encode_lit lit diff --git a/src/core/clause_tracer.mli b/src/core/clause_tracer.mli new file mode 100644 index 00000000..4acca1aa --- /dev/null +++ b/src/core/clause_tracer.mli @@ -0,0 +1,22 @@ +(** Tracer for clauses and literals *) + +module Tr = Sidekick_trace + +(** Tracer for clauses. *) +class type t = + object + method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t + method delete_clause : id:int -> Lit.t Iter.t -> unit + method unsat_clause : id:int -> Tr.Entry_id.t + method encode_lit : Lit.t -> Ser_value.t + end + +val dummy : t +(** Dummy tracer, recording nothing. *) + +val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t +val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit +val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit +val unsat_clause : #t -> id:int -> Tr.Entry_id.t +val unsat_clause' : #t -> id:int -> unit +val encode_lit : #t -> Lit.t -> Ser_value.t diff --git a/src/main/main.ml b/src/main/main.ml index 9a897a43..ff942efc 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -4,6 +4,7 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Sidekick_core module E = CCResult module Fmt = CCFormat module Term = Sidekick_base.Term @@ -135,7 +136,7 @@ let check_limits () = else if s > !mem_limit then raise Out_of_space -let mk_tracer () = +let mk_smt_tracer () = if !file_trace = "" then Sidekick_smt_solver.Tracer.dummy else ( @@ -144,6 +145,15 @@ let mk_tracer () = ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc) ) +let mk_sat_tracer () : Clause_tracer.t = + if !file_trace = "" then + Clause_tracer.dummy + else ( + let oc = open_out_bin !file_trace in + let sink = Sidekick_trace.Sink.of_out_channel_using_bencode oc in + Pure_sat_solver.tracer ~sink () + ) + let main_smt ~config () : _ result = let tst = Term.Store.create ~size:4_096 () in @@ -180,7 +190,7 @@ let main_smt ~config () : _ result = let proof = Proof.create ~config () in *) let proof = Proof.dummy in - let tracer = mk_tracer () in + let tracer = mk_smt_tracer () in let solver = (* TODO: probes, to load only required theories *) @@ -250,8 +260,8 @@ let main_cnf () : _ result = in CCFun.protect ~finally @@ fun () -> let tst = Term.Store.create () in - (* FIXME :tracer? *) - let solver = S.SAT.create_pure_sat ~size:`Big ~proof ~stat () in + let tracer = mk_sat_tracer () in + let solver = S.SAT.create_pure_sat ~size:`Big ~tracer ~proof ~stat () in S.Dimacs.parse_file solver tst !file >>= fun () -> let r = S.solve ~check:!check ?in_memory_proof solver in diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 3bee156c..02a6d24a 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -1,11 +1,13 @@ (* pure SAT solver *) open Sidekick_core -module Tracer = Sidekick_smt_solver.Tracer module E = CCResult module SS = Sidekick_sat +module Tr = Sidekick_trace module I_const : sig + type Const.view += I of int + val make : Term.store -> int -> Lit.t val const_decoders : Const.decoders end = struct @@ -77,6 +79,42 @@ module Dimacs = struct with e -> E.of_exn_trace e end +(** Tracer that emit list of integers. *) +let tracer ~(sink : Tr.Sink.t) () : Clause_tracer.t = + object (self) + method encode_lit (lit : Lit.t) = + let sign = Lit.sign lit in + let i = + match Term.view (Lit.term lit) with + | Term.E_const { Const.c_view = I_const.I i; _ } -> abs i + | _ -> assert false + in + Ser_value.int + (if sign then + i + else + -i) + + method assert_clause ~id (lits : Lit.t Iter.t) = + let v = + Ser_value.( + dict_of_list + [ + "id", int id; + "c", list (lits |> Iter.map self#encode_lit |> Iter.to_rev_list); + ]) + in + Tr.Sink.emit sink ~tag:"AssCSat" v + + method 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 = + let v = Ser_value.(dict_of_list [ "id", int id ]) in + ignore (Tr.Sink.emit sink ~tag:"DelCSat" v : Tr.Entry_id.t) + end + (* FIXME let check_proof (proof : Proof.in_memory) : bool = Profile.with_ "pure-sat.check-proof" @@ fun () -> diff --git a/src/main/show_trace.ml b/src/main/show_trace.ml index 46d59efd..9aa71de4 100644 --- a/src/main/show_trace.ml +++ b/src/main/show_trace.ml @@ -2,6 +2,57 @@ open Sidekick_core open Sidekick_trace module Smt = Sidekick_smt_solver +type state = { dump: bool; src: Source.t; t_reader: Smt.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 @@ -16,14 +67,8 @@ let show_file ~dump file : unit = ] in - Source.iter_all src (fun i ~tag v -> - Log.debugf 10 (fun k -> - k "(@[show-trace[%d]@ :tag %S@ :val %a@])" i tag Ser_value.pp v); - if dump then Format.printf "[%d]: %S %a@." i tag Ser_value.pp v; - - match Smt.Trace_reader.decode t_reader ~tag v with - | Some e -> Fmt.printf "[%d]: %a@." i Smt.Trace_reader.pp_entry e - | None -> ()) + let st = { t_reader; src; dump } in + Source.iter_all src (fun i ~tag v -> show_event st i ~tag v) let () = let files = ref [] in diff --git a/src/sat/solver.ml b/src/sat/solver.ml index 5fc1110b..a0a7b1a6 100644 --- a/src/sat/solver.ml +++ b/src/sat/solver.ml @@ -244,6 +244,7 @@ type t = { store: store; (* atom/var/clause store *) plugin: plugin; (* user defined theory *) proof: Proof_trace.t; (* the proof object *) + tracer: Clause_tracer.t; (* Clauses are simplified for efficiency purposes. In the following vectors, the comments actually refer to the original non-simplified clause. *) @@ -306,10 +307,12 @@ let restart_first = 100 let _nop_on_conflict (_ : atom array) = () (* Starting environment. *) -let create_ ~store ~proof ~stat ~max_clauses_learnt (plugin : plugin) : t = +let create_ ~store ~proof ~tracer ~stat ~max_clauses_learnt (plugin : plugin) : + t = { store; plugin; + tracer; unsat_at_0 = None; next_decisions = []; max_clauses_learnt; @@ -677,6 +680,8 @@ let report_unsat self (us : unsat_cause) : _ = Event.emit self.on_learnt c; let p = Clause.proof_step self.store c in Proof_trace.add_unsat self.proof p; + Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int c) Iter.empty; + Clause_tracer.unsat_clause' self.tracer ~id:(Clause.to_int c); US_false c | US_local _ -> us in @@ -1018,6 +1023,8 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit = Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps) in let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in + Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int uclause) + (Clause.lits_iter store uclause); Event.emit self.on_learnt uclause; if Atom.is_false store fuip then @@ -1034,6 +1041,8 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit = Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps) in let lclause = Clause.make_a store ~removable:true cr.cr_learnt p in + Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int lclause) + (Clause.lits_iter store lclause); add_clause_to_vec_ ~pool self lclause; attach_clause self lclause; @@ -1071,6 +1080,8 @@ let add_clause_ (self : t) ~pool (init : clause) : unit = let store = self.store in Log.debugf 30 (fun k -> k "(@[sat.add-clause@ @[%a@]@])" (Clause.debug store) init); + Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int init) + (Clause.lits_iter store init); (* Insertion of new lits is done before simplification. Indeed, else a lit in a trivial clause could end up being not decided on, which is a bug. *) Clause.iter store init ~f:(fun x -> insert_var_order self (Atom.var x)); @@ -1530,6 +1541,8 @@ let reduce_clause_db (self : t) : unit = (* need to remove from watchlists *) mark_dirty_atom (Atom.neg atoms.(1)); Event.emit self.on_gc (Clause.lits_a store c); + Clause_tracer.delete_clause self.tracer ~id:(Clause.to_int c) + (Clause.lits_iter store c); Proof_trace.delete self.proof (Clause.proof_step store c) in @@ -1647,7 +1660,7 @@ let search (self : t) ~on_progress ~(max_conflicts : int) : unit = | Some confl -> (* Conflict *) incr n_conflicts; - (* When the theory has raised Unsat, add_boolean_conflict + (* When the theory has raised Unsat, [add_boolean_conflict] might 'forget' the initial conflict clause, and only add the analyzed backtrack clause. So in those case, we use add_clause to make sure the initial conflict clause is also added. *) @@ -2034,10 +2047,15 @@ let[@inline] eval_lit self (lit : Lit.t) : lbool = | Some a -> eval_atom_ self a | None -> L_undefined -let create ?(stat = Stat.global) ?(size = `Big) ~proof (p : plugin) : t = +let create ?(stat = Stat.global) ?(size = `Big) ?tracer ~proof (p : plugin) : t + = + let tracer = + (tracer : #Clause_tracer.t option :> Clause_tracer.t option) + |> Option.value ~default:Clause_tracer.dummy + in let store = Store.create ~size ~stat () in let max_clauses_learnt = ref 0 in - let self = create_ ~max_clauses_learnt ~store ~proof ~stat p in + let self = create_ ~max_clauses_learnt ~store ~tracer ~proof ~stat p in self let plugin_cdcl_t (module P : THEORY_CDCL_T) : (module PLUGIN) = @@ -2066,5 +2084,5 @@ let plugin_pure_sat : plugin = let has_theory = false end) -let create_pure_sat ?stat ?size ~proof () : t = - create ?stat ?size ~proof plugin_pure_sat +let create_pure_sat ?stat ?size ?tracer ~proof () : t = + create ?stat ?size ?tracer ~proof plugin_pure_sat diff --git a/src/sat/solver.mli b/src/sat/solver.mli index 689bb6ba..120ab2d9 100644 --- a/src/sat/solver.mli +++ b/src/sat/solver.mli @@ -176,6 +176,7 @@ val mk_plugin_cdcl_t : val create : ?stat:Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> + ?tracer:#Clause_tracer.t -> proof:Proof_trace.t -> plugin -> t @@ -190,6 +191,7 @@ val plugin_pure_sat : plugin val create_pure_sat : ?stat:Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> + ?tracer:#Clause_tracer.t -> proof:Proof_trace.t -> unit -> t