From 6694ce856be14f5d6d6ce4aa71af268ad0c58017 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 21 Jul 2022 23:21:01 -0400 Subject: [PATCH] fix sat for new event --- src/sat/Solver.ml | 8 ++++---- src/sat/Solver_intf.ml | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 08d7d7f0..1d33c63c 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -881,10 +881,10 @@ module Make (Plugin : PLUGIN) = struct mutable var_incr: float; (* increment for variables' activity *) mutable clause_incr: float; (* increment for clauses' activity *) (* FIXME: use event *) - on_conflict: Clause.t Event.Emitter.t; - on_decision: lit Event.Emitter.t; - on_learnt: Clause.t Event.Emitter.t; - on_gc: lit array Event.Emitter.t; + on_conflict: (Clause.t, unit) Event.Emitter.t; + on_decision: (lit, unit) Event.Emitter.t; + on_learnt: (Clause.t, unit) Event.Emitter.t; + on_gc: (lit array, unit) Event.Emitter.t; stat: Stat.t; n_conflicts: int Stat.counter; n_propagations: int Stat.counter; diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index e38954a6..a0797607 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -308,10 +308,10 @@ module type S = sig val proof : t -> proof_trace (** Access the inner proof *) - val on_conflict : t -> Clause.t Event.t - val on_decision : t -> lit Event.t - val on_learnt : t -> Clause.t Event.t - val on_gc : t -> lit array Event.t + val on_conflict : t -> (Clause.t, unit) Event.t + val on_decision : t -> (lit, unit) Event.t + val on_learnt : t -> (Clause.t, unit) Event.t + val on_gc : t -> (lit array, unit) Event.t (** {2 Types} *)