diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index dd46a65033a1d1b7dcf884cb394d9678efd76ef7..929fecfcf39f570480baa2c55dc4da10753e72e3 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -333,7 +333,7 @@ let () =
| exn -> raise exn)
(** Helpers *)
-module TwoWatchLiteral = struct
+module WatchArgs = struct
(** todo move the check to enqueue; but it requires to be able to attach event
in delayed_ro *)
@@ -342,8 +342,7 @@ module TwoWatchLiteral = struct
callback : Egraph.t -> Ground.t -> unit;
ground : Ground.t; (** perhaps ground should have an array for args *)
args : Node.t array;
- from_start : int Context.Ref.t; (** already set before *)
- from_end : int Context.Ref.t; (** already set after *)
+ current : int Context.Ref.t; (** already set before *)
}
type runable = t
@@ -366,68 +365,47 @@ module TwoWatchLiteral = struct
type t = event
- let name = "Interp.TwoWatchLiteral"
+ let name = "Interp.WatchArgs"
end)
let delay = Events.FixingModel
- let rec check_if_set d args incr stop i =
- if Option.is_none (Egraph.get_value d args.(i)) then i
+ let rec check_if_set d args i =
+ if Option.is_none (Egraph.get_value d args.(i)) then Some i
else
- let i = incr + i in
- if i = stop then stop else check_if_set d args incr stop i
+ let i = 1 + i in
+ if Array.length args <= i then None else check_if_set d args i
let attach d r i = Egraph.attach_any_value d r.args.(i) key r
let run d r =
- let o_from_start = Context.Ref.get r.from_start in
- let o_from_end = Context.Ref.get r.from_end in
- (if o_from_end < o_from_start then ()
- else
- let from_start =
- check_if_set d r.args 1 (o_from_end + 1) o_from_start
- in
- if o_from_end < from_start then (
- Context.Ref.set r.from_start from_start;
- r.callback d r.ground)
- else (
- if from_start <> o_from_start then (
- Context.Ref.set r.from_start from_start;
- attach d r from_start);
- if o_from_end = from_start then ()
- else
- let from_end = check_if_set d r.args (-1) from_start o_from_end in
- Context.Ref.set r.from_end from_end));
+ let o_current = Context.Ref.get r.current in
+ assert (o_current < Array.length r.args);
+ (match check_if_set d r.args o_current with
+ | None -> r.callback d r.ground
+ | Some current ->
+ assert (current <> o_current);
+ attach d r current);
None
let create d callback ground =
match (Ground.sem ground).args with
| [] -> callback d ground
- | _ ->
+ | _ -> (
let args = Array.of_list (Ground.sem ground).args in
- let r from_start from_end =
- assert (from_start <= from_end);
- Debug.dprintf4 debug "Interp create %a (%i-%i)" Ground.pp ground
- from_start from_end;
+ let r current =
+ (* Debug.dprintf3 debug "Interp create %a (%i)" Ground.pp ground
+ * current; *)
{
callback;
ground;
args;
- from_start = Context.Ref.create (Egraph.context d) from_start;
- from_end = Context.Ref.create (Egraph.context d) from_end;
+ current = Context.Ref.create (Egraph.context d) current;
}
in
- let from_start = check_if_set d args 1 (Array.length args) 0 in
- if from_start = Array.length args then callback d ground
- else if from_start = Array.length args - 1 then
- attach d (r from_start from_start) from_start
- else
- let from_end =
- check_if_set d args (-1) from_start (Array.length args - 1)
- in
- let r = r from_start from_end in
- attach d r from_start;
- attach d r from_end
+ match check_if_set d args 0 with
+ | None -> callback d ground
+ | Some current -> attach d (r current) current)
end
let () = Egraph.Wait.register_dem (module Daemon)
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index 7bf4fe34c8d8810fe93844e17081208b7ee3ef59..ec5491375600e21b9d2c058dde5c1aa5ef4e70a3 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -82,7 +82,7 @@ module Fix_model : sig
needed. Could raise unsatisfiable if all the model have been tried *)
end
-module TwoWatchLiteral : sig
+module WatchArgs : sig
val create : Egraph.t -> (Egraph.t -> Ground.t -> unit) -> Ground.t -> unit
(** call the given function when all the arguments of the ground term have a value *)
end
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index d622348a265a487f6772ee4633a99a60ca360cb9..e00920dfd28727fa7a78ab8dee9056964bef0c10 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -92,7 +92,7 @@ let propagate_value d g =
Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate
d g
in
- Interp.TwoWatchLiteral.create d f g
+ Interp.WatchArgs.create d f g
let sequence_of_cases d ty tyargs all_cases cases =
let open Interp.SeqLim in
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 70d14e86d5d655ef0c0073398f2a579b46a553bd..32e1544694d7842ee8ae69d5e882bac6c09df2c1 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -182,7 +182,7 @@ module Check = struct
| `Some v -> Egraph.set_value d (Ground.node g) v
| `Uninterp -> Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain.propagate d g
in
- Interp.TwoWatchLiteral.create d f g
+ Interp.WatchArgs.create d f g
end
(** {2 Initialization} *)
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index 81c29343f3b6fdc636ec7a3b614c4d91fe3c5979..5ca45cb49fff70e59d0bf7ada1c81de451be6515 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -320,7 +320,7 @@ module UFModel = struct
f d g
let init_attach_value d g =
- Interp.TwoWatchLiteral.create d on_uninterpreted_domain g
+ Interp.WatchArgs.create d on_uninterpreted_domain g
end
module On_uninterpreted_domain = struct