simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: renaming in DRUP traces

Browse source
This commit is contained in:
Simon Cruanes 2021-08-08 00:46:58 -04:00
parent feff94bdbb
commit a8522e66f0
1 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/drup/sidekick_drup.ml
View file

@ -60,9 +60,9 @@ module Trace : sig
val del_clause : t -> clause -> unit val del_clause : t -> clause -> unit
type event = type event =
| I of clause | Input of clause
| A of clause | Redundant of clause
| D of clause | Delete of clause
val iteri : t -> f:(int -> event -> unit) -> unit val iteri : t -> f:(int -> event -> unit) -> unit
val events : t -> event Iter.t val events : t -> event Iter.t
@ -74,9 +74,9 @@ module Trace : sig
val dump : out_channel -> t -> unit val dump : out_channel -> t -> unit
end = struct end = struct
type event = type event =
| I of clause | Input of clause
| A of clause | Redundant of clause
| D of clause | Delete of clause
type t = { type t = {
evs: event Vec.t; evs: event Vec.t;
@ -85,27 +85,27 @@ end = struct
let create() : t = let create() : t =
{ evs=Vec.create() } { evs=Vec.create() }
let add_clause self c = Vec.push self.evs (A c) let add_clause self c = Vec.push self.evs (Redundant c)
let add_input_clause self c = Vec.push self.evs (I c) let add_input_clause self c = Vec.push self.evs (Input c)
let del_clause self c = Vec.push self.evs (D c) let del_clause self c = Vec.push self.evs (Delete c)
let get self i = Vec.get self.evs i let get self i = Vec.get self.evs i
let size self = Vec.size self.evs let size self = Vec.size self.evs
let events self = Vec.to_seq self.evs let events self = Vec.to_seq self.evs
let iteri self ~f = Vec.iteri f self.evs let iteri self ~f = Vec.iteri f self.evs
let pp_event out = function let pp_event out = function
| I c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c | Input c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c
| A c -> Fmt.fprintf out "(@[Add %a@])" Clause.pp c | Redundant c -> Fmt.fprintf out "(@[Redundant %a@])" Clause.pp c
| D c -> Fmt.fprintf out "(@[Del %a@])" Clause.pp c | Delete c -> Fmt.fprintf out "(@[Del %a@])" Clause.pp c
let dump oc self : unit = let dump oc self : unit =
let fpf = Printf.fprintf in let fpf = Printf.fprintf in
let pp_c out c = Clause.iter c ~f:(fun a -> fpf oc "%d " (Atom.to_int a)); in let pp_c out c = Clause.iter c ~f:(fun a -> fpf oc "%d " (Atom.to_int a)); in
Vec.iter Vec.iter
(function (function
| I c -> fpf oc "i %a0\n" pp_c c; | Input c -> fpf oc "i %a0\n" pp_c c;
| A c -> fpf oc "%a0\n" pp_c c; | Redundant c -> fpf oc "%a0\n" pp_c c;
| D c -> fpf oc "d %a0\n" pp_c c; | Delete c -> fpf oc "d %a0\n" pp_c c;
) )
self.evs self.evs
end end
@ -261,11 +261,11 @@ end = struct
in in
match ev with match ev with
| Trace.I c -> | Trace.Input c ->
add_c_ c; add_c_ c;
true true
| Trace.A c -> | Trace.Redundant c ->
(* negate [c], pushing each atom on trail, and see if we get [Conflict] (* negate [c], pushing each atom on trail, and see if we get [Conflict]
by pure propagation *) by pure propagation *)
@ -288,7 +288,7 @@ end = struct
add_c_ c; add_c_ c;
ok ok
| Trace.D _c -> | Trace.Delete _c ->
true (* TODO*) true (* TODO*)
let check trace : _ result = let check trace : _ result =
@ -300,7 +300,7 @@ end = struct
let ok = check_ev self i ev in let ok = check_ev self i ev in
if not ok then ( if not ok then (
Log.debugf 10 Log.debugf 10
(fun k->k"(@[check.step.fail@ event[%d]@ :def %a@])" i Trace.pp_event ev); (fun k->k"(@[check.step.fail@ :on event[%d]@ :def %a@])" i Trace.pp_event ev);
VecI32.push self.errors i VecI32.push self.errors i
)); ));