simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 20:34:53 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix sat for new event

Browse source
This commit is contained in:
Simon Cruanes 2022-07-21 23:21:01 -04:00
parent 7a6d94e622
commit 6694ce856b
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/Solver.ml
View file

@ -881,10 +881,10 @@ module Make (Plugin : PLUGIN) = struct
mutable var_incr: float; (* increment for variables' activity *) mutable var_incr: float; (* increment for variables' activity *)
mutable clause_incr: float; (* increment for clauses' activity *) mutable clause_incr: float; (* increment for clauses' activity *)
(* FIXME: use event *) (* FIXME: use event *)
on_conflict: Clause.t Event.Emitter.t; on_conflict: (Clause.t, unit) Event.Emitter.t;
on_decision: lit Event.Emitter.t; on_decision: (lit, unit) Event.Emitter.t;
on_learnt: Clause.t Event.Emitter.t; on_learnt: (Clause.t, unit) Event.Emitter.t;
on_gc: lit array Event.Emitter.t; on_gc: (lit array, unit) Event.Emitter.t;
stat: Stat.t; stat: Stat.t;
n_conflicts: int Stat.counter; n_conflicts: int Stat.counter;
n_propagations: int Stat.counter; n_propagations: int Stat.counter;

8
src/sat/Solver_intf.ml
View file

@ -308,10 +308,10 @@ module type S = sig
val proof : t -> proof_trace val proof : t -> proof_trace
(** Access the inner proof *) (** Access the inner proof *)
val on_conflict : t -> Clause.t Event.t val on_conflict : t -> (Clause.t, unit) Event.t
val on_decision : t -> lit Event.t val on_decision : t -> (lit, unit) Event.t
val on_learnt : t -> Clause.t Event.t val on_learnt : t -> (Clause.t, unit) Event.t
val on_gc : t -> lit array Event.t val on_gc : t -> (lit array, unit) Event.t
(** {2 Types} *) (** {2 Types} *)