From 656d93d5fbd6927024fdd60fb7869b25c725b789 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Oct 2022 23:23:34 -0400 Subject: [PATCH] smt tracer is now a clause tracer --- src/core/clause_tracer.ml | 3 ++- src/core/clause_tracer.mli | 2 ++ src/main/main.ml | 3 ++- src/smt/solver.ml | 5 ++-- src/smt/trace_reader.ml | 14 +++++----- src/smt/trace_reader.mli | 2 +- src/smt/tracer.ml | 54 ++++++++++++++++++++++++-------------- src/smt/tracer.mli | 15 ++++++----- 8 files changed, 61 insertions(+), 37 deletions(-) diff --git a/src/core/clause_tracer.ml b/src/core/clause_tracer.ml index 297c355e..dc846105 100644 --- a/src/core/clause_tracer.ml +++ b/src/core/clause_tracer.ml @@ -8,7 +8,7 @@ class type t = method encode_lit : Lit.t -> Ser_value.t end -let dummy : t = +class dummy : t = object method assert_clause ~id:_ _ = Tr.Entry_id.dummy method delete_clause ~id:_ _ = () @@ -16,6 +16,7 @@ let dummy : t = method encode_lit _ = Ser_value.null end +let dummy : t = new dummy let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c let assert_clause' (self : #t) ~id c : unit = diff --git a/src/core/clause_tracer.mli b/src/core/clause_tracer.mli index 4acca1aa..e9f30ebf 100644 --- a/src/core/clause_tracer.mli +++ b/src/core/clause_tracer.mli @@ -11,6 +11,8 @@ class type t = method encode_lit : Lit.t -> Ser_value.t end +class dummy : t + val dummy : t (** Dummy tracer, recording nothing. *) diff --git a/src/main/main.ml b/src/main/main.ml index ff942efc..4312ea90 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -141,8 +141,9 @@ let mk_smt_tracer () = Sidekick_smt_solver.Tracer.dummy else ( let oc = open_out_bin !file_trace in - Sidekick_smt_solver.Tracer.concrete + Sidekick_smt_solver.Tracer.make ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc) + () ) let mk_sat_tracer () : Clause_tracer.t = diff --git a/src/smt/solver.ml b/src/smt/solver.ml index bc38b854..f0b765f1 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -82,7 +82,8 @@ let create arg ?(stat = Stat.global) ?size ?(tracer = Tracer.dummy) ~proof proof; tracer; last_res = None; - solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si); + solver = + Sat_solver.create ~proof ?size ~tracer ~stat (SI.to_sat_plugin si); stat; theory_id_gen = Theory_id.create (); n_clause_input = Stat.mk_int stat "smt.solver.add-clause.input"; @@ -158,7 +159,7 @@ end) let add_clause (self : t) (c : lit array) (proof : step_id) : unit = let c, proof = preprocess_clause_ self c proof in - Tracer.assert_clause_arr' self.tracer c; + Tracer.assert_clause' self.tracer ~id:0 (Iter.of_array c); add_clause_nopreproc_ ~internal:false self c proof; Perform_delayed_.top self.si self; (* finish preproc *) diff --git a/src/smt/trace_reader.ml b/src/smt/trace_reader.ml index 85ccf19c..42e20638 100644 --- a/src/smt/trace_reader.ml +++ b/src/smt/trace_reader.ml @@ -1,12 +1,12 @@ open Sidekick_core module Tr = Sidekick_trace -type entry = Assert of Term.t | Assert_clause of Lit.t list +type entry = Assert of Term.t | Assert_clause of { id: int; c: Lit.t list } let pp_entry out = function | Assert t -> Fmt.fprintf out "(@[assert@ %a@])" Term.pp t - | Assert_clause c -> - Fmt.fprintf out "(@[assert-c@ %a@])" (Fmt.Dump.list Lit.pp) c + | Assert_clause { id; c } -> + Fmt.fprintf out "(@[assert-c[%d]@ %a@])" id (Fmt.Dump.list Lit.pp) c type t = { tst: Term.store; src: Tr.Source.t; t_dec: Term.Trace_reader.t } @@ -14,7 +14,8 @@ let create ?const_decoders tst src : t = let t_dec = Term.Trace_reader.create ?const_decoders tst ~source:src in { tst; src; t_dec } -let add_const_decoders self c = Term.Trace_reader.add_const_decoders self.t_dec c +let add_const_decoders self c = + Term.Trace_reader.add_const_decoders self.t_dec c let dec_t (self : t) = Ser_decode.( @@ -27,7 +28,8 @@ let dec_c (self : t) = let+ b, t = tup2 bool @@ dec_t self in Lit.atom self.tst ~sign:b t in - list dec_lit) + let+ id = dict_field "id" int and+ c = dict_field "c" (list dec_lit) in + id, c) let decode (self : t) ~tag v = Log.debugf 30 (fun k -> @@ -43,7 +45,7 @@ let decode (self : t) ~tag v = | "AssC" -> Ser_decode.( (match run (dec_c self) v with - | Ok c -> Some (Assert_clause c) + | Ok (id, c) -> Some (Assert_clause { id; c }) | Error err -> Fmt.eprintf "cannot decode entry with tag %S:@ %a@." tag Ser_decode.Error.pp err; diff --git a/src/smt/trace_reader.mli b/src/smt/trace_reader.mli index e26c9a2f..77580e75 100644 --- a/src/smt/trace_reader.mli +++ b/src/smt/trace_reader.mli @@ -3,7 +3,7 @@ open Sidekick_core module Tr = Sidekick_trace -type entry = Assert of Term.t | Assert_clause of Lit.t list +type entry = Assert of Term.t | Assert_clause of { id: int; c: Lit.t list } val pp_entry : entry Fmt.printer diff --git a/src/smt/tracer.ml b/src/smt/tracer.ml index 678e36f2..92967187 100644 --- a/src/smt/tracer.ml +++ b/src/smt/tracer.ml @@ -6,11 +6,12 @@ class type t = object inherit Term.Tracer.t method emit_assert_term : Term.t -> Tr.Entry_id.t - method emit_assert_clause : Lit.t list -> Tr.Entry_id.t + inherit Clause_tracer.t + method emit_assert_term : Term.t -> Tr.Entry_id.t end class concrete (sink : Tr.Sink.t) : t = - object + object (self) inherit Term.Tracer.concrete ~sink as emit_t method emit_assert_term t = @@ -19,32 +20,47 @@ class concrete (sink : Tr.Sink.t) : t = let id = Tr.Sink.emit sink ~tag:"AssT" v in id - method emit_assert_clause (c : Lit.t list) = + method encode_lit (lit : Lit.t) : V.t = + let sign = Lit.sign lit in + let id_t = emit_t#emit_term @@ Lit.term lit in + V.(list [ bool sign; int id_t ]) + + method assert_clause ~id (c : Lit.t Iter.t) = (* get a list of pairs *) - let l = - List.map - (fun lit -> - let sign = Lit.sign lit in - let id_t = emit_t#emit_term @@ Lit.term lit in - V.(list [ bool sign; int id_t ])) - c - |> V.list - in - let id = Tr.Sink.emit sink ~tag:"AssC" l in + let l = Iter.map self#encode_lit c |> Iter.to_rev_list |> V.list in + let v = V.(dict_of_list [ "id", int id; "c", l ]) in + let id = Tr.Sink.emit sink ~tag:"AssC" v in id + + 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 class dummy : t = object inherit Term.Tracer.dummy + inherit Clause_tracer.dummy method emit_assert_term _ = Tr.Entry_id.dummy - method emit_assert_clause _ = Tr.Entry_id.dummy end +let dummy : #t = new dummy +let make ~sink () = new concrete sink +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 let assert_term (self : #t) t = self#emit_assert_term t let assert_term' (self : #t) t = ignore (assert_term self t : Tr.Entry_id.t) -let assert_clause (self : #t) c = self#emit_assert_clause c -let assert_clause' (self : #t) c = ignore (assert_clause self c : Tr.Entry_id.t) -let assert_clause_arr' (self : #t) c = assert_clause' self (Array.to_list c) -let dummy : #t = new dummy -let concrete ~sink = new concrete sink diff --git a/src/smt/tracer.mli b/src/smt/tracer.mli index ef8588a0..1cd55a64 100644 --- a/src/smt/tracer.mli +++ b/src/smt/tracer.mli @@ -4,12 +4,10 @@ module Tr = Sidekick_trace class type t = object inherit Term.Tracer.t + inherit Clause_tracer.t method emit_assert_term : Term.t -> Tr.Entry_id.t (** Emit an assertion *) - - method emit_assert_clause : Lit.t list -> Tr.Entry_id.t - (** Emit an assertion *) end class dummy : t @@ -19,9 +17,12 @@ class concrete : Tr.Sink.t -> t (** Tracer emitting to a sink *) val dummy : t -val concrete : sink:Tr.Sink.t -> t +val make : sink:Tr.Sink.t -> unit -> t val assert_term : #t -> Term.t -> Tr.Entry_id.t val assert_term' : #t -> Term.t -> unit -val assert_clause : #t -> Lit.t list -> Tr.Entry_id.t -val assert_clause' : #t -> Lit.t list -> unit -val assert_clause_arr' : #t -> Lit.t array -> unit +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