From a02515827a0ef2242acf0adc8928994989e173fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 4 Jan 2021 14:18:51 +0100
Subject: [PATCH] [TimeWheel] use a time wheel
in order to more easily prioritize without creating famine
---
src_colibri2/core/demon.ml | 34 ++--
src_colibri2/core/demon.mli | 16 +-
src_colibri2/core/events.ml | 14 +-
src_colibri2/core/events.mli | 4 +-
src_colibri2/popop_lib/TimeWheel.ml | 176 ++++++++++++++++++
src_colibri2/popop_lib/TimeWheel.mli | 46 +++++
src_colibri2/popop_lib/intmap.mli | 3 +
src_colibri2/solver/scheduler.ml | 63 +++----
src_colibri2/stdlib/context.ml | 11 ++
src_colibri2/stdlib/context.mli | 24 +++
src_colibri2/theories/bool/boolean.ml | 6 +-
src_colibri2/theories/bool/equality.ml | 10 +-
src_colibri2/theories/bool/uninterp.ml | 4 +-
.../theories/quantifier/quantifier.ml | 10 +-
14 files changed, 345 insertions(+), 76 deletions(-)
create mode 100644 src_colibri2/popop_lib/TimeWheel.ml
create mode 100644 src_colibri2/popop_lib/TimeWheel.mli
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 985218ad6..110ade1ed 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -115,7 +115,7 @@ module Key = struct
val key: (Key.t, Data.t, info) t
- val immediate: bool
+ val delayed: int option
val wakeup:
Egraph.t -> Key.t -> Data.t Events.Fired.t ->
info -> Key.t alive
@@ -257,7 +257,7 @@ module Key = struct
let enqueue = enqueue
let key = D.key.dk_id
- let immediate = D.immediate
+ let delayed = D.delayed
end in
Egraph.Wait.register_dem (module Dem)
@@ -384,7 +384,7 @@ module Fast = struct
val key: Data.t t
(** never killed *)
- val immediate: bool
+ val delayed: int option
val throttle: int (** todo int ref? *)
(** number of time run in a row *)
val wakeup: Egraph.t -> Data.t Events.Fired.event -> unit
@@ -421,7 +421,7 @@ module Fast = struct
D.Data.pp (Events.Fired.get_data event);
D.wakeup d event;
Debug.dprintf0 debug "[Demon] @[Done@]";
- if not D.immediate then Egraph.flush_internal d;
+ if Option.is_some D.delayed then Egraph.flush_internal d;
run_one () in
try
run_one ();
@@ -469,7 +469,7 @@ module Fast = struct
let enqueue = enqueue
let key = D.key.dk_id
- let immediate = D.immediate
+ let delayed = D.delayed
end in
Egraph.Wait.register_dem (module Dem)
@@ -505,7 +505,7 @@ module Fast = struct
let register_init_daemon
(type a)
~name
- ?(immediate=false)
+ ?(delayed=Some 1)
?(throttle=100)
(thterm: (module Nodes.RegisteredThTerm with type t = a) )
(f:Egraph.t -> a -> unit)
@@ -515,7 +515,7 @@ module Fast = struct
let module DaemonInit = struct
let key = create name
module Data = Popop_stdlib.DUnit
- let immediate = immediate
+ let delayed = delayed
let throttle = throttle
let wakeup d = function
| Events.Fired.EventRegSem(thterm,()) ->
@@ -530,7 +530,7 @@ module Fast = struct
let register_init_daemon_value
(type a)
~name
- ?(immediate=false)
+ ?(delayed=Some 1)
?(throttle=100)
(value: (module Nodes.RegisteredValue with type t = a) )
(f:Egraph.t -> a -> unit)
@@ -540,7 +540,7 @@ module Fast = struct
let module DaemonInit = struct
let key = create name
module Data = Popop_stdlib.DUnit
- let immediate = immediate
+ let delayed = delayed
let throttle = throttle
let wakeup d = function
| Events.Fired.EventRegValue(value,()) ->
@@ -554,7 +554,7 @@ module Fast = struct
let register_change_repr_daemon
~name
- ?(immediate=false)
+ ?(delayed=Some 1)
?(throttle=100)
(f:Egraph.t -> Node.t -> unit)
(init_d:Egraph.t)
@@ -562,7 +562,7 @@ module Fast = struct
let module DaemonInit = struct
let key = create name
module Data = Popop_stdlib.DUnit
- let immediate = immediate
+ let delayed = delayed
let throttle = throttle
let wakeup d = function
| Events.Fired.EventChange(node,()) ->
@@ -576,7 +576,7 @@ module Fast = struct
let register_change_domain_daemon
(type a) (type b)
~name
- ?(immediate=false)
+ ?(delayed=Some 1)
?(throttle=100)
?(pp=Fmt.nop)
(dom:a DomKind.t)
@@ -588,7 +588,7 @@ module Fast = struct
type t = b
let pp = pp
end
- let immediate = immediate
+ let delayed = delayed
let throttle = throttle
let wakeup d = function
| Events.Fired.EventDom(node,dom',data) ->
@@ -608,7 +608,7 @@ module Fast = struct
let register_get_value_daemon
(type a) (type b)
~name
- ?(immediate=false)
+ ?(delayed=Some 1)
?(throttle=100)
?(pp=Fmt.nop)
(value: (module Nodes.RegisteredValue with type s = a) )
@@ -621,7 +621,7 @@ module Fast = struct
type t = b
let pp = pp
end
- let immediate = immediate
+ let delayed = delayed
let throttle = throttle
let wakeup d = function
| Events.Fired.EventValue(node,value,v,data) ->
@@ -643,7 +643,7 @@ module Fast = struct
}
let register_simply
- ?(immediate=false)
+ ?(delayed=Some 1)
?(throttle=100)
name
=
@@ -653,7 +653,7 @@ module Fast = struct
type t = Egraph.t -> Node.t -> unit
let pp = Fmt.nop
end
- let immediate = immediate
+ let delayed = delayed
let throttle = throttle
let wakeup d = function
| Events.Fired.EventDom(node,_,f) ->
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index 771f662fe..e04f49348 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -66,7 +66,7 @@ module Key: sig
val key: (Key.t, Data.t, info) t
- val immediate: bool
+ val delayed: int option
val wakeup:
Egraph.t -> Key.t -> Data.t Events.Fired.t ->
info -> Key.t alive
@@ -113,7 +113,7 @@ module Fast: sig
val key: Data.t t
(** never killed *)
- val immediate: bool
+ val delayed: int option
val throttle: int (** todo int ref? *)
(** number of time run in a row *)
val wakeup: Egraph.t -> Data.t Events.Fired.event -> unit
@@ -130,7 +130,7 @@ module Fast: sig
(** helper *)
val register_init_daemon:
name:string ->
- ?immediate:bool ->
+ ?delayed:int option ->
?throttle:int ->
(module RegisteredThTerm with type t = 'a) ->
(Egraph.t -> 'a -> unit) ->
@@ -141,7 +141,7 @@ module Fast: sig
(** helper *)
val register_init_daemon_value:
name:string ->
- ?immediate:bool ->
+ ?delayed:int option ->
?throttle:int ->
(module RegisteredValue with type t = 'a) ->
(Egraph.t -> 'a -> unit) ->
@@ -152,7 +152,7 @@ module Fast: sig
(** helper *)
val register_change_repr_daemon:
name:string ->
- ?immediate:bool ->
+ ?delayed:int option ->
?throttle:int ->
(Egraph.t -> Node.t -> unit) ->
Egraph.t ->
@@ -162,7 +162,7 @@ module Fast: sig
(** helper *)
val register_change_domain_daemon:
name:string ->
- ?immediate:bool ->
+ ?delayed:int option ->
?throttle:int ->
?pp:('b Fmt.t) ->
'a DomKind.t ->
@@ -173,7 +173,7 @@ module Fast: sig
(** helper *)
val register_get_value_daemon:
name:string ->
- ?immediate:bool ->
+ ?delayed:int option ->
?throttle:int ->
?pp:('b Fmt.t) ->
(module RegisteredValue with type s = 'a) ->
@@ -188,7 +188,7 @@ module Fast: sig
(** helper *)
val register_simply:
- ?immediate:bool ->
+ ?delayed:int option ->
?throttle:int ->
string ->
(Egraph.t -> unit) * waiter
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 4bf8c04b3..7f4bc3718 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -163,13 +163,15 @@ module Wait = struct
val print_event : event Format.printer
val enqueue : delayed_ro -> event Fired.event -> runable enqueue
val key : (event, runable) Dem.t
- val immediate : bool
+ val delayed : int option
end
val register_dem : (module Dem with type event = 'k and type runable = 'd) -> unit
val get_dem : ('k, 'd) Dem.t -> (module Dem with type event = 'k and type runable = 'd)
+ val get_priority: daemon_key -> int
+
val print_dem_event : ('a, 'b) Dem.t -> 'a Format.printer
val print_dem_runable : ('a, 'b) Dem.t -> 'b Format.printer
@@ -210,8 +212,7 @@ module Wait = struct
val enqueue: delayed_ro -> event Fired.event -> runable enqueue
val key: (event,runable) Dem.t
- val immediate: bool
-
+ val delayed: int option
end
module Registry = Dem.Make_Registry(struct
@@ -231,6 +232,11 @@ module Wait = struct
let register_dem = Registry.register
let get_dem = Registry.get
+ let get_priority = function
+ | DaemonKey(dem,_) ->
+ let module Dem = (val get_dem dem) in
+ Option.value ~default:1 Dem.delayed
+
let print_dem_event = Registry.printk
let () = Print.pdem_event.Print.pdem_event <- print_dem_event
@@ -242,7 +248,7 @@ module Wait = struct
let new_pending_daemon (type k) (type d) t (dem:(k,d) Dem.t) runable =
let module Dem = (val get_dem dem) in
let daemonkey = DaemonKey(dem, runable) in
- if Dem.immediate
+ if Option.is_none Dem.delayed
then S.schedule_immediate t daemonkey
else S.schedule t daemonkey
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index 94fac946f..22567d837 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -88,13 +88,15 @@ module Wait : sig
val print_event : event Format.printer
val enqueue : delayed_ro -> event Fired.event -> runable enqueue
val key : (event, runable) Dem.t
- val immediate : bool
+ val delayed : int option
end
val register_dem : (module Dem with type event = 'k and type runable = 'd) -> unit
val get_dem : ('k, 'd) Dem.t -> (module Dem with type event = 'k and type runable = 'd)
+ val get_priority: daemon_key -> int
+
val print_dem_event : ('a, 'b) Dem.t -> 'a Format.printer
val print_dem_runable : ('a, 'b) Dem.t -> 'b Format.printer
diff --git a/src_colibri2/popop_lib/TimeWheel.ml b/src_colibri2/popop_lib/TimeWheel.ml
new file mode 100644
index 000000000..c4c300150
--- /dev/null
+++ b/src_colibri2/popop_lib/TimeWheel.ml
@@ -0,0 +1,176 @@
+open Base
+
+(** TimeWheel *)
+
+module type S = sig
+
+ type 'a t
+ type context
+
+ val create: context -> 'a t
+
+
+ val add: 'a t -> 'a -> int -> unit
+ (** [add t v offset] add the event v at the given offset in the futur *)
+
+ val next: 'a t -> 'a option
+
+
+ val current_time: 'a t -> int
+
+ val size: 'a t -> int
+end
+
+module Make
+ (Context: sig type t end)
+ (Array:
+ sig
+ type 'a t
+ val create: Context.t -> int -> 'a -> 'a t
+ val get: 'a t -> int -> 'a
+ val set: 'a t -> int -> 'a -> unit
+ end)
+ (Ref:sig
+ type 'a t
+ val create: Context.t -> 'a -> 'a t
+ val get: 'a t -> 'a
+ val set: 'a t -> 'a -> unit
+ end) : S with type context := Context.t = struct
+
+ type 'a cell =
+ | Nil
+ | Cons of { v: 'a; time : int; next: 'a cell }
+
+ type 'a t = {
+ current: int Ref.t;
+ futur: 'a cell Array.t;
+ size: int Ref.t;
+ }
+
+ let new_bits o n = (lnot o) land n
+
+ (* lowest first *)
+ let rec iter_bits f i =
+ if i <> 0 then
+ let j = Int.ctz i in
+ f j;
+ iter_bits f (i land (lnot (1 lsl j)))
+
+
+ let create ctx = {
+ current = Ref.create ctx 0;
+ futur = Array.create ctx Int.num_bits Nil;
+ size = Ref.create ctx 0;
+ }
+
+ let current_time t = Ref.get t.current
+ let size t = Ref.get t.size
+
+ let bucket t time =
+ assert (Ref.get t.current <= time);
+ let i = Int.num_bits - Int.clz (time - (Ref.get t.current)) in
+ (* Caml.Format.eprintf "-> t.current = %i; time = %i; i = %i@." (Ref.get t.current) time i; *)
+ i
+
+ let add_in_bucket t v time =
+ let b = bucket t time in
+ Array.set t.futur b (Cons { v; time; next = Array.get t.futur b })
+
+ let add t v offset =
+ assert (1 <= offset);
+ let time = (Ref.get t.current) + offset in
+ Ref.set t.size ((Ref.get t.size) + 1);
+ add_in_bucket t v time
+
+
+ (* optim *)
+
+ (* let rec find_smallest i =
+ * if Int.num_bits <= i then None
+ * else
+ * match t.futur.(i) with
+ * | Nil -> find_smallest (i+1)
+ * | Cons _ as b ->
+ * let rec find_smallest acc = function
+ * | Nil -> Some acc
+ * | Cons { time; next } ->
+ * find_smallest (min time acc) next
+ * in
+ * find_smallest Int.max_value b
+ * in
+ * match find_smallest 0 with
+ * | None -> ()
+ * | Some next ->
+ * assert ( t.current < next );
+ * (\* We compute all the bit that would have been the at 1 from 0, if we would
+ * go from t.current to next by 1 increment.Arith_status
+ * All the bits are in different categories :
+ * - The leading unchanged bits
+ * - The biggest set bit
+ * - The bits that went from 1 to 0, before the biggest bit is set
+ * - The bits that stayed at 0, after the biggest bit is set
+ * - The other below those that changed multiple times.
+ * *\)
+ * let biggest = Int.clz (next land (lnot t.current)) in
+ * let mask = -1 lsl biggest in
+ * let before_1_0 = Int.clz (lnot (t.current lor mask)) in
+ * let before_stay_0 = Int.clz (t.next land (lnot mask)) in *)
+
+
+ let incr_current t =
+ let bitset = Int.ctz (lnot (Ref.get t.current)) in
+ let bitset = bitset + 2 in
+ Ref.set t.current ((Ref.get t.current) + 1);
+ let empty i =
+ (* Caml.Format.eprintf "empty t.current = %i; i = %i@." (Ref.get t.current) i; *)
+ let b = Array.get t.futur i in
+ Array.set t.futur i Nil;
+ let rec aux = function
+ | Nil -> ()
+ | Cons { v; time; next } ->
+ (* Caml.Format.eprintf "t.current = %i; time = %i; i = %i@." (Ref.get t.current) time i; *)
+ assert ( (Ref.get t.current) <= time );
+ add_in_bucket t v time;
+ aux next
+ in
+ aux b
+ in
+ empty 1; (** always emptied because next but could be just copied *)
+ empty bitset
+
+ let find_next t =
+ if 0 < (Ref.get t.size) then
+ let rec aux t =
+ match Array.get t.futur 0 with
+ | Nil ->
+ incr_current t;
+ aux t
+ | Cons _ -> ()
+ in
+ aux t
+
+ let next t =
+ find_next t;
+ match Array.get t.futur 0 with
+ | Nil -> None
+ | Cons { v; time; next } ->
+ assert ( Int.equal time (Ref.get t.current) );
+ Ref.set t.size (Ref.get t.size - 1);
+ Array.set t.futur 0 next;
+ Some v
+end
+
+include (Make
+ (struct type t = unit end)
+ (struct
+ type 'a t = 'a array
+ let create () i v = Array.create ~len:i v
+ let get = Array.get
+ let set = Array.set
+ end)
+ (struct
+ type 'a t = 'a ref
+ let create () v = ref v
+ let get = Ref.(!)
+ let set = Ref.(:=)
+ end))
diff --git a/src_colibri2/popop_lib/TimeWheel.mli b/src_colibri2/popop_lib/TimeWheel.mli
new file mode 100644
index 000000000..9ea639639
--- /dev/null
+++ b/src_colibri2/popop_lib/TimeWheel.mli
@@ -0,0 +1,46 @@
+(** Time Wheel *)
+
+(** Allows to add timestamp in the futur and get the next timestamp.
+
+ It should be (but not proved) amortized O(log(offset)) for adding an event to
+ an offset in the futur and O(1) amortized to get the next elements
+*)
+
+module type S = sig
+
+ type 'a t
+ type context
+
+ val create: context -> 'a t
+
+
+ val add: 'a t -> 'a -> int -> unit
+ (** [add t v offset] add the event v at the given offset in the futur *)
+
+ val next: 'a t -> 'a option
+
+
+ val current_time: 'a t -> int
+ val size: 'a t -> int
+
+end
+
+
+include (S with type context := unit)
+
+
+module Make
+ (Context: sig type t end)
+ (Array:
+ sig
+ type 'a t
+ val create: Context.t -> int -> 'a -> 'a t
+ val get: 'a t -> int -> 'a
+ val set: 'a t -> int -> 'a -> unit
+ end)
+ (Ref:sig
+ type 'a t
+ val create: Context.t -> 'a -> 'a t
+ val get: 'a t -> 'a
+ val set: 'a t -> 'a -> unit
+ end) : S with type context := Context.t
diff --git a/src_colibri2/popop_lib/intmap.mli b/src_colibri2/popop_lib/intmap.mli
index 1ab848491..ff0c8fd6d 100644
--- a/src_colibri2/popop_lib/intmap.mli
+++ b/src_colibri2/popop_lib/intmap.mli
@@ -34,3 +34,6 @@ module Make(K:Map_intf.TaggedEqualType) :
(** Remarks: *)
(** translate is currently implemented using a complete reconstruction *)
+
+val hsb: int -> int
+(** highest bit set *)
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index a7ed6043d..2795ae7aa 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -45,7 +45,6 @@ exception Contradiction
module Att = struct
type t =
- | Daemon of int * Events.Wait.daemon_key
| Decision of int * Egraph.choice
type prio = float
type db = float Node.H.t
@@ -55,13 +54,9 @@ module Att = struct
let le (x:t) (xp:float) (y:t) (yp:float) =
match x, y with
- | Daemon (x,_) , Daemon (y,_) -> x <= y
| Decision (x,_), Decision (y,_) ->
if xp = yp then x <= y else xp >= yp (** min *)
- | Daemon _ , Decision _ -> true
- | Decision _, Daemon _ -> false
let reprio _ = function
- | Daemon _ -> 0.
| Decision (_,choice) -> float_of_int choice.prio
end
@@ -72,7 +67,7 @@ type bp_kind =
| External
type bp =
- { pre_wakeup_daemons : Prio.t;
+ { pre_choices : Prio.t;
pre_prev_scheduler_state : bp option;
pre_backtrack_point : Context.bp;
kind : bp_kind;
@@ -80,7 +75,8 @@ type bp =
}
type t =
- { mutable wakeup_daemons : Prio.t;
+ { mutable choices : Prio.t;
+ daemons : Events.Wait.daemon_key Context.TimeWheel.t;
mutable prev_scheduler_state : bp option;
solver_state : Egraph.Backtrackable.t;
mutable delayed : Egraph.t option;
@@ -96,8 +92,8 @@ let get_t t = t.solver_state
let print_level fmt t =
let nb_dec =
- Prio.fold (fun acc x _ -> match x with Att.Decision _ -> acc + 1 | _ -> acc)
- 0 t.wakeup_daemons in
+ Prio.fold (fun acc x _ -> match x with Att.Decision _ -> acc + 1)
+ 0 t.choices in
Format.fprintf fmt "%i (dec waiting:%i)" t.level nb_dec
(* let new_handler t =
@@ -113,7 +109,8 @@ let print_level fmt t =
let new_solver () =
let context = Context.create () in
- { wakeup_daemons = Prio.empty;
+ { choices = Prio.empty;
+ daemons = Context.TimeWheel.create (Context.creator context);
prev_scheduler_state = None;
solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
@@ -128,7 +125,7 @@ let push kind t =
Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
Debug.dprintf2 debug_pushpop "[Scheduler] push from %a" print_level t;
let prev =
- { pre_wakeup_daemons = t.wakeup_daemons;
+ { pre_choices = t.choices;
pre_prev_scheduler_state = t.prev_scheduler_state;
pre_backtrack_point = Context.bp t.context;
kind;
@@ -142,7 +139,7 @@ let push kind t =
let pop_to t prev =
Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a"
print_level t;
- t.wakeup_daemons <- prev.pre_wakeup_daemons;
+ t.choices <- prev.pre_choices;
t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
t.level <- prev.pre_level;
Context.pop prev.pre_backtrack_point;
@@ -163,15 +160,14 @@ let new_delayed =
incr daemon_count;
Debug.dprintf1 debug "[Scheduler] New possible daemon:%i"
!daemon_count;
- t.wakeup_daemons <-
- Prio.insert t.decprio (Att.Daemon (!daemon_count,att))
- t.wakeup_daemons in
+ Context.TimeWheel.add t.daemons att (Egraph.Wait.get_priority att)
+ in
let sched_decision dec =
incr dec_count;
Debug.dprintf1 debug "[Scheduler] New possible decisions prio:%i"
!dec_count;
- t.wakeup_daemons <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
- t.wakeup_daemons in
+ t.choices <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
+ t.choices in
Egraph.Backtrackable.new_delayed ~sched_daemon ~sched_decision t.solver_state
(*
@@ -185,7 +181,7 @@ let new_delayed =
S.flush d;
List.iter (fun f -> ignore (f d); S.flush d) l;
run_until_dec t d;
- run_dec t d t.wakeup_daemons
+ run_dec t d t.choices
(fun d dec -> Conflict.make_decision d dec cho k)
with S.Contradiction pexp ->
Debug.dprintf0 debug "[Scheduler] Contradiction during apply learnt";
@@ -230,7 +226,7 @@ let rec conflict_analysis t =
raise Contradiction
| Some prev ->
pop_to t prev;
- t.wakeup_daemons <- Prio.reprio t.decprio t.wakeup_daemons;
+ t.choices <- Prio.reprio t.decprio t.choices;
match prev.kind with
| Choices [] -> rewind ()
| Choices (choice::choices) ->
@@ -244,13 +240,13 @@ and try_run_dec:
(** First we verify its the decision is at this point needed *)
match choice.choice d with
| Egraph.DecNo | Egraph.DecTodo [] ->
- t.wakeup_daemons <- prio;
+ t.choices <- prio;
d (** d can be precised by choose_decision *)
| Egraph.DecTodo (todo::todos) ->
(** We remove the decision it is replaced by the todos,
we can change the interface of choice and in that case
we want to keep the decision in the current branch *)
- t.wakeup_daemons <- prio;
+ t.choices <- prio;
Debug.incr stats_dec;
Egraph.Backtrackable.delayed_stop d;
make_choice t todo todos
@@ -266,12 +262,12 @@ and make_choice t todo todos =
(* let rec run_until_dec t d =
- * let act = Prio.min t.wakeup_daemons in
+ * let act = Prio.min t.choices in
* match act with
* | Some (Att.Daemon (_,att)) -> begin
- * let _, prio = Prio.extract_min t.wakeup_daemons in
+ * let _, prio = Prio.extract_min t.choices in
* Debug.incr stats_propa;
- * t.wakeup_daemons <- prio;
+ * t.choices <- prio;
* Egraph.Backtrackable.run_daemon d att;
* Egraph.Backtrackable.flush d;
* run_until_dec t d
@@ -280,20 +276,21 @@ and make_choice t todo todos =
let run_one_step t d =
- let act, prio = Prio.extract_min t.wakeup_daemons in
- match act with
- | Att.Daemon (_,att) -> begin
+ match Context.TimeWheel.next t.daemons with
+ | Some att -> begin
Debug.incr stats_propa;
- t.wakeup_daemons <- prio;
try
Egraph.Backtrackable.run_daemon d att; d
with Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
conflict_analysis t
end
- | Att.Decision (_,chogen) ->
- Debug.dprintf0 debug "[Scheduler] decision";
- try_run_dec t d prio chogen
+ | None ->
+ let act, prio = Prio.extract_min t.choices in
+ match act with
+ | Att.Decision (_,chogen) ->
+ Debug.dprintf0 debug "[Scheduler] decision";
+ try_run_dec t d prio chogen
let rec flush t d =
try
@@ -309,9 +306,9 @@ let rec run_inf_step ?limit ~nodec t d =
(match limit with | Some n when n <= 0 -> raise ReachStepLimit | _ -> ());
let d = flush t d in
let run =
- match Prio.min t.wakeup_daemons with
+ 0 < Context.TimeWheel.size t.daemons ||
+ match Prio.min t.choices with
| Some (Att.Decision _) -> not nodec
- | Some (Att.Daemon _) -> true
| None -> false
in
if run
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index 6d1ae3f24..c93ee2f71 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -406,3 +406,14 @@ module Hashtbl = struct
end
end
+
+module Array = struct
+ type 'a t = 'a Ref.t array
+ let create ctx i v = Array.init i (fun _ -> Ref.create ctx v)
+ let set t i v = Ref.set (Array.get t i) v
+ let get t i = Ref.get (Array.get t i)
+end
+
+module TimeWheel = Colibri2_popop_lib.TimeWheel.Make
+ (struct type t = creator end)
+ (Array)(Ref)
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index 5d8059fd3..02dbc240e 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -179,3 +179,27 @@ module Queue: sig
val pp: ?sep:unit Fmt.t -> 'a Fmt.t -> 'a t Fmt.t
end
+
+
+module Array: sig
+ type 'a t
+ val create: creator -> int -> 'a -> 'a t
+ val set: 'a t -> int -> 'a -> unit
+ val get: 'a t -> int -> 'a
+end
+module TimeWheel: sig
+ type 'a t
+
+ val create: creator -> 'a t
+
+
+ val add: 'a t -> 'a -> int -> unit
+ (** [add t v offset] add the event v at the given offset in the futur *)
+
+ val next: 'a t -> 'a option
+
+
+ val current_time: 'a t -> int
+
+ val size: 'a t -> int
+end
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index dfdcb7371..727488e80 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -155,7 +155,7 @@ module DaemonPropaNot = struct
Format.fprintf fmt "%a,%a -> %a" Th.pp v Node.pp cl1 Node.pp cl2
end
- let immediate = false
+ let delayed = Some 1
let key = Demon.Fast.create "Bool.DaemonPropaNot"
let throttle = 100
let wakeup d =
@@ -207,7 +207,7 @@ module DaemonPropa = struct
| All thterm -> Format.fprintf fmt "All(%a)" ThE.pp thterm
end
- let immediate = false
+ let delayed = Some 1
let throttle = 100
let wakeup_lit d thterm watched watcher =
@@ -314,7 +314,7 @@ module DaemonInit = struct
module Data = DUnit
- let immediate = false
+ let delayed = Some 1
let throttle = 100
let wakeup d = function
| Events.Fired.EventRegSem(thterm,()) ->
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index b6eb82684..44a554029 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -332,7 +332,7 @@ module DaemonPropa = struct
module Data = DUnit
type info = unit let default = ()
- let immediate = false
+ let delayed = Some 1
let wakeup d v _ev () =
norm_dom d (ThE.index v)
@@ -347,7 +347,7 @@ module DaemonInit = struct
module Data = DUnit
type info = unit let default = ()
- let immediate = true
+ let delayed = None
let wakeup d () ev () =
List.iter
(function Events.Fired.EventRegSem(clsem,()) ->
@@ -422,7 +422,7 @@ module DaemonPropaITE = struct
Egraph.register d branch;
Egraph.merge d own branch
- let immediate = false
+ let delayed = Some 1
let throttle = 100
let wakeup d = function
| Events.Fired.EventValue(cond,dom,_,clsem) ->
@@ -445,7 +445,7 @@ module DaemonInitITE = struct
module Key = DUnit
module Data = DUnit
- let immediate = false
+ let delayed = Some 1
let throttle = 100
let wakeup d = function
| Events.Fired.EventRegSem(clsem,()) ->
@@ -521,7 +521,7 @@ let init_diff_to_value (type a) (type b)
module Data = Val
let key = key
let throttle = 100
- let immediate = false
+ let delayed = Some 1
let wakeup d = function
| Events.Fired.EventDom(_,_,v) ->
diff --git a/src_colibri2/theories/bool/uninterp.ml b/src_colibri2/theories/bool/uninterp.ml
index 39d803681..15569c642 100644
--- a/src_colibri2/theories/bool/uninterp.ml
+++ b/src_colibri2/theories/bool/uninterp.ml
@@ -125,7 +125,7 @@ module DaemonPropa = struct
Demon.Key.attach d key v
[EventChange(f,()); EventChange(g,())]
- let immediate = true (** can be false *)
+ let delayed = None (** can be not None *)
let wakeup d (nodesem:k) _ev () =
match ThE.sem nodesem with
| Th.Fun _ -> Demon.AliveStopped
@@ -148,7 +148,7 @@ module DaemonInit = struct
module Data = DUnit
type info = unit let default = ()
- let immediate = false
+ let delayed = Some 1
let wakeup d () ev () =
List.iter
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index c52ad2c61..7b5fdfbe0 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -796,7 +796,8 @@ let init, attach =
Ground.ThClosedQuantifier.pp th
Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp))
triggers;
- List.iter (add_trigger d) triggers)
+ List.iter (add_trigger d) triggers
+ (* Todo match with current terms *))
let quantifier_registered d th = attach d (Ground.ThClosedQuantifier.node th) th
@@ -833,8 +834,11 @@ let add_info_on_ground_terms d thg =
Context.Queue.iter (fun trg -> Trigger.match_ d trg res) trgs
let init d =
- Demon.Fast.register_change_repr_daemon ~name:"Quantifier.merge" merge d;
- Demon.Fast.register_init_daemon ~name:"Quantifier.new_quantifier"
+ let delayed = Some 10 in
+ Demon.Fast.register_change_repr_daemon ~delayed ~name:"Quantifier.merge" merge
+ d;
+ Demon.Fast.register_init_daemon ~delayed:(Some 1)
+ ~name:"Quantifier.new_quantifier"
(module Ground.ThClosedQuantifier)
quantifier_registered d;
Ground.register_converter d add_info_on_ground_terms;
--
GitLab