diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 110ade1ed2bf6feda7d86d1845d83656f57ddf8b..2b07e5d7b2d5114a4beeee8408687e4ddc686893 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 delayed: int option
+ val delay: Events.delay
val wakeup:
Egraph.t -> Key.t -> Data.t Events.Fired.t ->
info -> Key.t alive
@@ -168,7 +168,7 @@ module Key = struct
Egraph.set_env d D.key.dk_data (module DemTable');
(** wakeup *)
let alive = D.wakeup d k events info in
- (** delayed can be modified *)
+ (** delay can be modified *)
begin match alive with
| AliveStopped | AliveRedirected _ ->
let demstate = match alive with
@@ -257,7 +257,7 @@ module Key = struct
let enqueue = enqueue
let key = D.key.dk_id
- let delayed = D.delayed
+ let delay = D.delay
end in
Egraph.Wait.register_dem (module Dem)
@@ -384,7 +384,7 @@ module Fast = struct
val key: Data.t t
(** never killed *)
- val delayed: int option
+ val delay: Events.delay
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,9 @@ module Fast = struct
D.Data.pp (Events.Fired.get_data event);
D.wakeup d event;
Debug.dprintf0 debug "[Demon] @[Done@]";
- if Option.is_some D.delayed then Egraph.flush_internal d;
+ (match D.delay with
+ | Immediate -> ()
+ | Delayed_by _ | LastEffort _ -> Egraph.flush_internal d);
run_one () in
try
run_one ();
@@ -469,7 +471,7 @@ module Fast = struct
let enqueue = enqueue
let key = D.key.dk_id
- let delayed = D.delayed
+ let delay = D.delay
end in
Egraph.Wait.register_dem (module Dem)
@@ -505,7 +507,7 @@ module Fast = struct
let register_init_daemon
(type a)
~name
- ?(delayed=Some 1)
+ ?(delay=Events.Delayed_by 1)
?(throttle=100)
(thterm: (module Nodes.RegisteredThTerm with type t = a) )
(f:Egraph.t -> a -> unit)
@@ -515,7 +517,7 @@ module Fast = struct
let module DaemonInit = struct
let key = create name
module Data = Popop_stdlib.DUnit
- let delayed = delayed
+ let delay = delay
let throttle = throttle
let wakeup d = function
| Events.Fired.EventRegSem(thterm,()) ->
@@ -530,7 +532,7 @@ module Fast = struct
let register_init_daemon_value
(type a)
~name
- ?(delayed=Some 1)
+ ?(delay=Events.Delayed_by 1)
?(throttle=100)
(value: (module Nodes.RegisteredValue with type t = a) )
(f:Egraph.t -> a -> unit)
@@ -540,7 +542,7 @@ module Fast = struct
let module DaemonInit = struct
let key = create name
module Data = Popop_stdlib.DUnit
- let delayed = delayed
+ let delay = delay
let throttle = throttle
let wakeup d = function
| Events.Fired.EventRegValue(value,()) ->
@@ -554,7 +556,7 @@ module Fast = struct
let register_change_repr_daemon
~name
- ?(delayed=Some 1)
+ ?(delay=Events.Delayed_by 1)
?(throttle=100)
(f:Egraph.t -> Node.t -> unit)
(init_d:Egraph.t)
@@ -562,7 +564,7 @@ module Fast = struct
let module DaemonInit = struct
let key = create name
module Data = Popop_stdlib.DUnit
- let delayed = delayed
+ let delay = delay
let throttle = throttle
let wakeup d = function
| Events.Fired.EventChange(node,()) ->
@@ -576,7 +578,7 @@ module Fast = struct
let register_change_domain_daemon
(type a) (type b)
~name
- ?(delayed=Some 1)
+ ?(delay=Events.Delayed_by 1)
?(throttle=100)
?(pp=Fmt.nop)
(dom:a DomKind.t)
@@ -588,7 +590,7 @@ module Fast = struct
type t = b
let pp = pp
end
- let delayed = delayed
+ let delay = delay
let throttle = throttle
let wakeup d = function
| Events.Fired.EventDom(node,dom',data) ->
@@ -608,7 +610,7 @@ module Fast = struct
let register_get_value_daemon
(type a) (type b)
~name
- ?(delayed=Some 1)
+ ?(delay=Events.Delayed_by 1)
?(throttle=100)
?(pp=Fmt.nop)
(value: (module Nodes.RegisteredValue with type s = a) )
@@ -621,7 +623,7 @@ module Fast = struct
type t = b
let pp = pp
end
- let delayed = delayed
+ let delay = delay
let throttle = throttle
let wakeup d = function
| Events.Fired.EventValue(node,value,v,data) ->
@@ -643,7 +645,7 @@ module Fast = struct
}
let register_simply
- ?(delayed=Some 1)
+ ?(delay=Events.Delayed_by 1)
?(throttle=100)
name
=
@@ -653,7 +655,7 @@ module Fast = struct
type t = Egraph.t -> Node.t -> unit
let pp = Fmt.nop
end
- let delayed = delayed
+ let delay = delay
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 e04f49348c32da145c11ef929da5db72ddccd42e..5c52b1cf15355c574766ca9378c7db8a8bfefd00 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 delayed: int option
+ val delay: Events.delay
val wakeup:
Egraph.t -> Key.t -> Data.t Events.Fired.t ->
info -> Key.t alive
@@ -75,7 +75,7 @@ module Key: sig
module Register (D:S): sig
val init: Egraph.t -> unit
- (** to run for each new delayed *)
+ (** to run for each new delay *)
end
type ('k,'i) state =
@@ -113,7 +113,7 @@ module Fast: sig
val key: Data.t t
(** never killed *)
- val delayed: int option
+ val delay: Events.delay
val throttle: int (** todo int ref? *)
(** number of time run in a row *)
val wakeup: Egraph.t -> Data.t Events.Fired.event -> unit
@@ -122,7 +122,7 @@ module Fast: sig
module Register (D:S): sig
val init: Egraph.t -> unit
- (** to run for each new delayed *)
+ (** to run for each new delay *)
end
val attach: Egraph.t -> 'd t -> 'd Create.t -> unit
@@ -130,7 +130,7 @@ module Fast: sig
(** helper *)
val register_init_daemon:
name:string ->
- ?delayed:int option ->
+ ?delay:Events.delay ->
?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 ->
- ?delayed:int option ->
+ ?delay:Events.delay ->
?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 ->
- ?delayed:int option ->
+ ?delay:Events.delay ->
?throttle:int ->
(Egraph.t -> Node.t -> unit) ->
Egraph.t ->
@@ -162,7 +162,7 @@ module Fast: sig
(** helper *)
val register_change_domain_daemon:
name:string ->
- ?delayed:int option ->
+ ?delay:Events.delay ->
?throttle:int ->
?pp:('b Fmt.t) ->
'a DomKind.t ->
@@ -173,7 +173,7 @@ module Fast: sig
(** helper *)
val register_get_value_daemon:
name:string ->
- ?delayed:int option ->
+ ?delay:Events.delay ->
?throttle:int ->
?pp:('b Fmt.t) ->
(module RegisteredValue with type s = 'a) ->
@@ -188,7 +188,7 @@ module Fast: sig
(** helper *)
val register_simply:
- ?delayed:int option ->
+ ?delay:Events.delay ->
?throttle:int ->
string ->
(Egraph.t -> unit) * waiter
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index b245e071ced200686425747fed9f518745b30a97..c8dd819b334dfcd260a10c62a50cbb30f016a709 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -903,6 +903,9 @@ module Delayed = struct
let register_decision t chogen =
t.sched_decision chogen
+ let register_delayed_event t dem v =
+ t.sched_daemon (Events.Wait.DaemonKey(dem,v))
+
let contradiction d =
d.env.current_delayed <- unsat_delayed;
raise Contradiction
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index 5b9b615faeca31a6a2ad79af3a23b8b28aa9dc56..3acdf6808b53c807265f72f0778d6332b66312e7 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -124,6 +124,9 @@ val register_decision: t -> choice -> unit
[choose_decision] of the [Cho] will be called at that time to know
if the decision is still needed. *)
+val register_delayed_event: t -> (_,'a) Events.Dem.t -> 'a -> unit
+(** register an event for later. *)
+
val contradiction: t -> 'b
(** {3 Low level} *)
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 7f4bc3718aa190fd2322f3dd0d0462132c89e71d..6c67f5657a2a867042de9d37605b6f82fcb24a7e 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -108,6 +108,11 @@ module Fired = struct
type 'b t = 'b event list
end
+type delay =
+ | Immediate
+ | Delayed_by of int
+ | LastEffort of int
+
module Wait = struct
type t =
| Event: ('k,'d) Dem.t * 'k -> t
@@ -163,14 +168,14 @@ 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 delayed : int option
+ val delay : delay
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 get_priority: daemon_key -> delay
val print_dem_event : ('a, 'b) Dem.t -> 'a Format.printer
@@ -212,7 +217,7 @@ module Wait = struct
val enqueue: delayed_ro -> event Fired.event -> runable enqueue
val key: (event,runable) Dem.t
- val delayed: int option
+ val delay: delay
end
module Registry = Dem.Make_Registry(struct
@@ -235,7 +240,7 @@ module Wait = struct
let get_priority = function
| DaemonKey(dem,_) ->
let module Dem = (val get_dem dem) in
- Option.value ~default:1 Dem.delayed
+ Dem.delay
let print_dem_event = Registry.printk
let () = Print.pdem_event.Print.pdem_event <- print_dem_event
@@ -248,9 +253,9 @@ 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 Option.is_none Dem.delayed
- then S.schedule_immediate t daemonkey
- else S.schedule t daemonkey
+ match Dem.delay with
+ | Immediate -> S.schedule_immediate t daemonkey
+ | _ -> S.schedule t daemonkey
let wakeup_event translate t info wevent =
match wevent with
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index 22567d8373083047924b5ae26c8eabb10be54b69..dc54152417182a1a7e0379071f6ffea5849b44e0 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -49,6 +49,13 @@ end
module Dem: Keys.Key2
+type delay =
+ | Immediate
+ | Delayed_by of int
+ (** Must be strictly positive *)
+ | LastEffort of int
+ (** When no decisions remains, must be strictly positive *)
+
module Wait : sig
type t =
| Event: ('k,'d) Dem.t * 'k -> t
@@ -88,14 +95,14 @@ 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 delayed : int option
+ val delay : delay
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 get_priority: daemon_key -> delay
val print_dem_event : ('a, 'b) Dem.t -> 'a Format.printer
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 2795ae7aa45ff4989caa2e01c6212c0db77b5494..69cb1a8d5abde1fc3cdb602a97a54ade3e493a81 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -37,6 +37,7 @@ let debug_dotgui = Debug.register_flag
let var_decay = 1. /. 0.95
let stats_propa = Debug.register_stats_int ~name:"Scheduler.daemon" ~init:0
+let stats_lasteffort = Debug.register_stats_int ~name:"Scheduler.lasteffort" ~init:0
let stats_dec = Debug.register_stats_int ~name:"Scheduler.decision" ~init:0
let stats_con = Debug.register_stats_int ~name:"Scheduler.conflict" ~init:0
@@ -77,6 +78,7 @@ type bp =
type t =
{ mutable choices : Prio.t;
daemons : Events.Wait.daemon_key Context.TimeWheel.t;
+ lasteffort : Events.Wait.daemon_key Context.TimeWheel.t;
mutable prev_scheduler_state : bp option;
solver_state : Egraph.Backtrackable.t;
mutable delayed : Egraph.t option;
@@ -111,6 +113,7 @@ let new_solver () =
let context = Context.create () in
{ choices = Prio.empty;
daemons = Context.TimeWheel.create (Context.creator context);
+ lasteffort = Context.TimeWheel.create (Context.creator context);
prev_scheduler_state = None;
solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
@@ -160,7 +163,11 @@ let new_delayed =
incr daemon_count;
Debug.dprintf1 debug "[Scheduler] New possible daemon:%i"
!daemon_count;
- Context.TimeWheel.add t.daemons att (Egraph.Wait.get_priority att)
+ match Egraph.Wait.get_priority att with
+ | Immediate -> assert false (* absurd *)
+ | Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
+ | LastEffort offset ->
+ Context.TimeWheel.add t.lasteffort att offset
in
let sched_decision dec =
incr dec_count;
@@ -286,11 +293,21 @@ let run_one_step t d =
conflict_analysis t
end
| None ->
- let act, prio = Prio.extract_min t.choices in
- match act with
- | Att.Decision (_,chogen) ->
+ match Prio.extract_min t.choices with
+ | Att.Decision (_,chogen), prio ->
Debug.dprintf0 debug "[Scheduler] decision";
try_run_dec t d prio chogen
+ | exception Leftistheap.Empty ->
+ match Context.TimeWheel.next t.lasteffort with
+ | Some att -> begin
+ Debug.incr stats_lasteffort;
+ try
+ Egraph.Backtrackable.run_daemon d att; d
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction";
+ conflict_analysis t
+ end
+ | None -> d
let rec flush t d =
try
@@ -309,7 +326,7 @@ let rec run_inf_step ?limit ~nodec t d =
0 < Context.TimeWheel.size t.daemons ||
match Prio.min t.choices with
| Some (Att.Decision _) -> not nodec
- | None -> false
+ | None -> 0 < Context.TimeWheel.size t.lasteffort
in
if run
then
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 727488e801ce4b970ec4f0045e5a1136e34553ee..1ed56789125e729d2fe2ecae6e3fb214f7b92b83 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 delayed = Some 1
+ let delay = Events.Delayed_by 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 delayed = Some 1
+ let delay = Events.Delayed_by 1
let throttle = 100
let wakeup_lit d thterm watched watcher =
@@ -314,7 +314,7 @@ module DaemonInit = struct
module Data = DUnit
- let delayed = Some 1
+ let delay = Events.Delayed_by 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 44a5540291b83d481be76e7d4f637b7f807659ba..0052db570c9715a1e253b0c83703a2088b5c8b46 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 delayed = Some 1
+ let delay = Events.Delayed_by 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 delayed = None
+ let delay = Events.Immediate
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 delayed = Some 1
+ let delay = Events.Delayed_by 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 delayed = Some 1
+ let delay = Events.Delayed_by 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 delayed = Some 1
+ let delay = Events.Delayed_by 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 15569c6427a0edaff1856ff147a1846543eadb00..09e734e6069025d6e6ca40545962eb4ff4110978 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 delayed = None (** can be not None *)
+ let delay = Events.Immediate (** 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 delayed = Some 1
+ let delay = Events.Delayed_by 1
let wakeup d () ev () =
List.iter
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 178623387a988d5ebe20728c0d15edecbe212ce9..081775add4263884fc7d0a6d6fe64e67a273f35d 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -396,8 +396,9 @@ module Trigger = struct
[@@deriving eq, ord, hash]
let pp fmt t =
- Fmt.pf fmt "[%a -> %a]" Pattern.pp t.pat Ground.ThClosedQuantifier.pp
- t.form
+ Fmt.pf fmt "[%a, %a -> %a]" Pattern.pp t.pat
+ Fmt.(list ~sep:comma Pattern.pp)
+ t.checks Ground.ThClosedQuantifier.pp t.form
end
include T
@@ -424,7 +425,7 @@ module Trigger = struct
List.fold_left aux pats tl
| _ -> t :: pats
in
- let pats = aux [] t in
+ let pats = List.sort_uniq ~cmp:Expr.Term.compare (aux [] t) in
let tyvs = Expr.Ty.Var.S.of_list tyvs in
let tvs = Expr.Term.Var.S.of_list tvs in
let pats_full, pats_partial =
@@ -445,7 +446,7 @@ module Trigger = struct
aux
( {
pat = a;
- checks = other @ pats_partial;
+ checks = other @ l @ pats_partial;
form = cq;
eager = true;
}
@@ -454,6 +455,13 @@ module Trigger = struct
in
aux [] [] pats_full
in
+ Debug.dprintf6 debug "@[pats_full:%a,@ pats_partial:%a,@ tri:%a@]@."
+ Fmt.(list ~sep:comma Pattern.pp)
+ pats_full
+ Fmt.(list ~sep:comma Pattern.pp)
+ pats_partial
+ Fmt.(list ~sep:comma pp)
+ multi_pats;
multi_pats
let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
@@ -519,6 +527,49 @@ module Trigger = struct
| Var _ -> Datastructure.Queue.push env_vars d t
| App (f, _, _) -> Context.Queue.push (F.EnvApps.find env_tri_by_apps d f) t
+ let instantiate_aux d tri subst =
+ let form = Ground.ThClosedQuantifier.sem tri.form in
+ Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a"
+ Ground.Subst.pp subst Expr.Term.pp form.body Pattern.pp tri.pat
+ Fmt.(list ~sep:comma Pattern.pp)
+ tri.checks;
+ Debug.incr nb_instantiation;
+ let n = Ground.convert ~subst form.body in
+ if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
+ Debug.incr nb_new_instantiation;
+ Egraph.register d n;
+ Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form)
+
+ module Delayed_instantiation = struct
+ type event = unit
+
+ let print_event = Unit.pp
+
+ let enqueue _ _ = assert false
+
+ let key =
+ Events.Dem.create_key
+ ( module struct
+ type d = t * Ground.Subst.t
+
+ type t = unit
+
+ let name = "delayed_instantiation"
+ end )
+
+ let delay = Events.LastEffort 1
+
+ type runable = t * Ground.Subst.t [@@deriving show]
+
+ let print_runable = pp_runable
+
+ let run d (tri, subst) =
+ instantiate_aux d tri subst;
+ None
+ end
+
+ let () = Egraph.Wait.register_dem (module Delayed_instantiation)
+
let instantiate d tri subst =
if
tri.eager
@@ -527,16 +578,8 @@ module Trigger = struct
try not (Node.S.is_empty (Pattern.check_term_exists d subst pat))
with Not_found -> false)
tri.checks
- then (
- let form = Ground.ThClosedQuantifier.sem tri.form in
- Debug.dprintf4 debug "[Quant] %a instantiation found %a" Ground.Subst.pp
- subst Expr.Term.pp form.body;
- Debug.incr nb_instantiation;
- let n = Ground.convert ~subst form.body in
- if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
- Debug.incr nb_new_instantiation;
- Egraph.register d n;
- Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form) )
+ then instantiate_aux d tri subst
+ else Egraph.register_delayed_event d Delayed_instantiation.key (tri, subst)
let match_ d tri n =
Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
@@ -843,7 +886,7 @@ let init, attach =
| ({ binder = Forall; _ } as e), false ->
Egraph.merge d (skolemize d e) n
| { binder = Exists; _ }, false | { binder = Forall; _ }, true ->
- let triggers = Trigger.compute_all_triggers th in
+ let triggers = Trigger.compute_top_triggers th in
Debug.dprintf4 debug "[Quant] For %a adds %a"
Ground.ThClosedQuantifier.pp th
Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp))
@@ -888,10 +931,9 @@ let add_info_on_ground_terms d thg =
Context.Queue.iter (fun trg -> Trigger.match_ d trg res) trgs
let init d =
- let delayed = Some 10 in
- Demon.Fast.register_change_repr_daemon ~delayed ~name:"Quantifier.merge" merge
- d;
- Demon.Fast.register_init_daemon ~delayed ~name:"Quantifier.new_quantifier"
+ let delay = Events.Delayed_by 10 in
+ Demon.Fast.register_change_repr_daemon ~delay ~name:"Quantifier.merge" merge d;
+ Demon.Fast.register_init_daemon ~delay ~name:"Quantifier.new_quantifier"
(module Ground.ThClosedQuantifier)
quantifier_registered d;
Ground.register_converter d add_info_on_ground_terms;