diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index a3bef017eaec8067eea72ee598b860cf2e76be18..5cadadd935415498fd931d392040f86aaec1fa57 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -80,7 +80,7 @@ module Dom = struct
the [d1] and [d2] are the same and doesn't need to be merged *)
val merge :
- Egraph.t -> t option * Node.t -> t option * Node.t -> bool -> unit
+ Egraph.wt -> t option * Node.t -> t option * Node.t -> bool -> unit
(** [merge d (dom1,cl1) (dom2,cl2) inv] called when [cl1] and [cl2] are
going to be merged in the same equivalence class. - if inv is false, cl2 will
be the new representative - if inv is true, cl1 will be the new
@@ -104,11 +104,11 @@ module Dom = struct
val key : t Kind.t
- val inter : Egraph.t -> t -> t -> t option
+ val inter : Egraph.wt -> t -> t -> t option
(** [inter d d1 d2] compute the intersection of [d1] and [d2] return [None]
if it is empty. In this last case a contradiction is reported *)
- val is_singleton : Egraph.t -> t -> Value.t option
+ val is_singleton : Egraph.wt -> t -> Value.t option
(** [is_singleton _ d] if [d] is
restricted to a singleton return the corresponding value *)
end
@@ -116,10 +116,10 @@ module Dom = struct
(** [Lattice(L)] register a domain as a lattice. It returns useful function
for setting and updating the domain *)
module Lattice (L : Lattice) : sig
- val set_dom : Egraph.t -> Node.t -> L.t -> unit
+ val set_dom : Egraph.wt -> Node.t -> L.t -> unit
(** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
- val upd_dom : Egraph.t -> Node.t -> L.t -> unit
+ val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
(** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
[l] with the current value of the domain. *)
end = struct
@@ -179,148 +179,19 @@ module Dom = struct
end
end
-(** {3 Fix the models} *)
-
-(** The module {!Interp} handles:
-
- - Checking the model before answering SAT, the interpretation of the
- application are provided using {!Interp.Register.check}
- - Enumerating the possible values for each node {!Interp.Register.node}
- - Otherwise enumerating the possible values of each type
- {!Interp.Register.ty}
-
-*)
-
module Interp = Interp
-
-(** {3 Custom Environment and data-structures } *)
-
module Env = Env
module Datastructure = Datastructure
-
-(** {3 Events } *)
-
-(**
- The modification of the Egraph (events) can be monitored through daemons.
- *)
-
-module Daemon : sig
- (** Attach a callback executed when different modifications of the Egraph happens *)
-
- (** The callback are not interrupted by other callbacks. They are scheduled to
- run as soon as possible during the propagation phase *)
-
- val attach_dom :
- Egraph.t ->
- ?direct:bool ->
- Node.t ->
- 'a DomKind.t ->
- (Egraph.t -> Node.t -> unit) ->
- unit
- (** [attach_dom d ?direct n dom callback] The callback is scheduled when the
- domain [dom] of the equivalence class of [n] is modified. If direct is true
- (default) the callback is scheduled immediately if the domain is already
- set. *)
-
- val attach_any_dom :
- Egraph.t -> 'a DomKind.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_value :
- Egraph.t ->
- ?direct:bool ->
- Node.t ->
- ('a, 'b) Nodes.ValueKind.t ->
- (Egraph.t -> Node.t -> 'b -> unit) ->
- unit
-
- val attach_any_value :
- Egraph.t ->
- ?direct:bool ->
- Node.t ->
- (Egraph.t -> Node.t -> Value.t -> unit) ->
- unit
-
- val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_reg_node :
- Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_reg_sem :
- Egraph.t -> ('a, 'b) Nodes.ThTermKind.t -> (Egraph.t -> 'b -> unit) -> unit
-
- val attach_reg_value :
- Egraph.t -> ('a, 'b) Nodes.ValueKind.t -> (Egraph.t -> 'b -> unit) -> unit
-
- val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
-end =
- Demon.Simple
-
-module DaemonFixingModel : sig
- (** Attach a callback executed when different modifications of the Egraph happens *)
-
- (** Same as {!Daemon} but they are scheduled to run as soon as possible during
- the FixingModel phase *)
-
- val attach_dom :
- Egraph.t ->
- ?direct:bool ->
- Node.t ->
- 'a DomKind.t ->
- (Egraph.t -> Node.t -> unit) ->
- unit
- (** [attach_dom d ?direct n dom callback] The callback is *)
-
- val attach_any_dom :
- Egraph.t -> 'a DomKind.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_value :
- Egraph.t ->
- ?direct:bool ->
- Node.t ->
- ('a, 'b) Nodes.ValueKind.t ->
- (Egraph.t -> Node.t -> 'b -> unit) ->
- unit
-
- val attach_any_value :
- Egraph.t ->
- ?direct:bool ->
- Node.t ->
- (Egraph.t -> Node.t -> Value.t -> unit) ->
- unit
-
- val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_reg_node :
- Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_reg_sem :
- Egraph.t -> ('a, 'b) Nodes.ThTermKind.t -> (Egraph.t -> 'b -> unit) -> unit
-
- val attach_reg_value :
- Egraph.t -> ('a, 'b) Nodes.ValueKind.t -> (Egraph.t -> 'b -> unit) -> unit
-
- val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
-
- val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
-end =
- Demon.Simple.FixingModel
-
+module Daemon = Demon.Simple
+module DaemonFixingModel = Demon.Simple.FixingModel
module DaemonWithFilter = Demon.WithFilter
module DaemonWithKey = Demon.Key
module Monad = Demon.Monad
module Events = struct
include Egraph
- (** Low level API *)
-
- (** {3 Create daemons } *)
-
module Dem = Events.Dem
- (** {3 Register daemons } *)
-
type delay = Events.delay =
| Immediate
| Delayed_by of int (** Must be strictly positive *)
@@ -348,8 +219,6 @@ module Events = struct
let new_pending_daemon = Egraph.new_pending_daemon
end
-(** {3 Helpers } *)
-
module Init = struct
let add_default_theory = Egraph.add_default_theory
end
@@ -362,10 +231,6 @@ module Debug = struct
let contradiction = Egraph.print_contradiction
end
-(** {3 For schedulers} *)
-
-(** The following functions are necessary only to the scheduler *)
-
module ForSchedulers = struct
module Backtrackable = Egraph.Backtrackable
@@ -385,9 +250,9 @@ end
module Choice = struct
type choice_state = Egraph.choice_state =
| DecNo
- | DecTodo of (Egraph.t -> unit) list
+ | DecTodo of (Egraph.wt -> unit) list
- and t = Egraph.choice = { choice : Egraph.t -> choice_state; prio : int }
+ and t = Egraph.choice = { choice : Egraph.wt -> choice_state; prio : int }
let register = Egraph.register_decision
end
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index 2b00d22c45db117c727353ae294dfbe83e0e9b06..0b2d84901c2cff5f8e06753c807048760dc23528 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -40,89 +40,65 @@
*)
module rec Egraph : sig
- module Ro : sig
- type t
-
- val is_equal : t -> Node.t -> Node.t -> bool
-
- val find_def : t -> Node.t -> Node.t
-
- val get_dom : t -> 'a Dom.Kind.t -> Node.t -> 'a option
- (** dom of the class *)
-
- val get_value : t -> Node.t -> Value.t option
- (** one of the value of the class *)
-
- (** {4 The classes must have been registered} *)
-
- val find : t -> Node.t -> Node.t
+ type 'a t
- val is_repr : t -> Node.t -> bool
+ type rw
- val is_registered : t -> Node.t -> bool
+ type wt = rw t
+ (** Egraph where its structure can be modified *)
- val get_env : t -> 'a Env.Saved.t -> 'a
- (** Can raise UninitializedEnv *)
+ type ro
- val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+ type rt = ro t
+ (** Egraph where its structure can not be modified *)
- val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
+ val is_equal : _ t -> Node.t -> Node.t -> bool
- val context : t -> Context.creator
+ val find_def : _ t -> Node.t -> Node.t
- val register : t -> Node.t -> unit
- (** Add a new node to register *)
- end
-
- type t = private Ro.t
-
- val is_equal : t -> Node.t -> Node.t -> bool
-
- val find_def : t -> Node.t -> Node.t
-
- val get_dom : t -> 'a Dom.Kind.t -> Node.t -> 'a option
+ val get_dom : _ t -> 'a Dom.Kind.t -> Node.t -> 'a option
(** dom of the class *)
- val get_value : t -> Node.t -> Value.t option
+ val get_value : _ t -> Node.t -> Value.t option
(** one of the value of the class *)
(** {4 The classes must have been registered} *)
- val find : t -> Node.t -> Node.t
+ val find : _ t -> Node.t -> Node.t
- val is_repr : t -> Node.t -> bool
+ val is_repr : _ t -> Node.t -> bool
- val is_registered : t -> Node.t -> bool
+ val is_registered : _ t -> Node.t -> bool
- val get_env : t -> 'a Env.Saved.t -> 'a
+ val get_env : _ t -> 'a Env.Saved.t -> 'a
(** Can raise UninitializedEnv *)
- val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+ val set_env : _ t -> 'a Env.Saved.t -> 'a -> unit
- val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
+ val get_unsaved_env : _ t -> 'a Env.Unsaved.t -> 'a
- val context : t -> Context.creator
+ val context : _ t -> Context.creator
- val contradiction : t -> 'a
+ val contradiction : _ t -> 'a
- val register : t -> Node.t -> unit
+ val register : _ t -> Node.t -> unit
(** Add a new node to register *)
(** {3 Immediate modifications} *)
- val set_dom : t -> 'a Dom.Kind.t -> Node.t -> 'a -> unit
+ val set_dom : rw t -> 'a Dom.Kind.t -> Node.t -> 'a -> unit
(** change the dom of the equivalence class *)
- val unset_dom : t -> 'a Dom.Kind.t -> Node.t -> unit
+ val unset_dom : rw t -> 'a Dom.Kind.t -> Node.t -> unit
(** remove the dom of the equivalence class *)
(** {3 Delayed modifications} *)
- val set_thterm : t -> Node.t -> ThTerm.t -> unit
+ val set_thterm : rw t -> Node.t -> ThTerm.t -> unit
(** attach a theory term to an equivalence class *)
- val set_value : t -> Node.t -> Value.t -> unit
+ val set_value : rw t -> Node.t -> Value.t -> unit
(** attach value to an equivalence class *)
- val merge : t -> Node.t -> Node.t -> unit
+ val merge : rw t -> Node.t -> Node.t -> unit
exception Contradiction
end
@@ -225,16 +201,16 @@ and Ground : sig
val apply :
Expr.Term.Const.t -> Ty.t list -> Node.t Colibri2_popop_lib.IArray.t -> s
- val init : Egraph.t -> unit
+ val init : Egraph.wt -> unit
- val register_converter : Egraph.t -> (Egraph.t -> t -> unit) -> unit
+ val register_converter : Egraph.wt -> (Egraph.wt -> t -> unit) -> unit
(** register callback called for each new ground term registered *)
- val tys : Egraph.t -> Node.t -> Ty.S.t
+ val tys : _ Egraph.t -> Node.t -> Ty.S.t
module Defs : sig
val add :
- Egraph.t ->
+ Egraph.wt ->
Dolmen_std.Expr.term_cst ->
Dolmen_std.Expr.ty_var list ->
Dolmen_std.Expr.term_var list ->
@@ -345,25 +321,17 @@ and Node : sig
val create : 'a Format.printer -> string -> 'a t
- val remove : 'a t -> Egraph.t -> key -> unit
-
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
-
- val find : 'a t -> Egraph.t -> key -> 'a
+ val remove : 'a t -> _ Egraph.t -> key -> unit
- val find_opt : 'a t -> Egraph.t -> key -> 'a option
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
- val mem : 'a t -> Egraph.t -> key -> bool
+ val find : 'a t -> _ Egraph.t -> key -> 'a
- val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
+ val find_opt : 'a t -> _ Egraph.t -> key -> 'a option
- module Ro : sig
- val find : 'a t -> Egraph.Ro.t -> key -> 'a
+ val mem : 'a t -> _ Egraph.t -> key -> bool
- val find_opt : 'a t -> Egraph.Ro.t -> key -> 'a option
-
- val mem : 'a t -> Egraph.Ro.t -> key -> bool
- end
+ val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
end
with type key := t
end
@@ -475,7 +443,7 @@ and Value : sig
end
(** Domains are additional informations associated to each equivalence class
- inside the {!Egraph.t}. They can be registered using {!Dom.register} or
+ inside the {!_ Egraph.t}. They can be registered using {!Dom.register} or
when the domain is simple by {!Dom.Lattice} *)
and Dom : sig
@@ -489,7 +457,7 @@ and Dom : sig
the [d1] and [d2] are the same and doesn't need to be merged *)
val merge :
- Egraph.t -> t option * Node.t -> t option * Node.t -> bool -> unit
+ Egraph.wt -> t option * Node.t -> t option * Node.t -> bool -> unit
(** [merge d (dom1,cl1) (dom2,cl2) inv] called when [cl1] and [cl2] are
going to be merged in the same equivalence class. - if inv is false, cl2 will
be the new representative - if inv is true, cl1 will be the new
@@ -511,11 +479,11 @@ and Dom : sig
val key : t Kind.t
- val inter : Egraph.t -> t -> t -> t option
+ val inter : Egraph.wt -> t -> t -> t option
(** [inter d d1 d2] compute the intersection of [d1] and [d2] return [None]
if it is empty. In this last case a contradiction is reported *)
- val is_singleton : Egraph.t -> t -> Value.t option
+ val is_singleton : Egraph.wt -> t -> Value.t option
(** [is_singleton _ d] if [d] is
restricted to a singleton return the corresponding value *)
end
@@ -523,10 +491,10 @@ and Dom : sig
(** [Lattice(L)] register a domain as a lattice. It returns useful function
for setting and updating the domain *)
module Lattice (L : Lattice) : sig
- val set_dom : Egraph.t -> Node.t -> L.t -> unit
+ val set_dom : Egraph.wt -> Node.t -> L.t -> unit
(** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
- val upd_dom : Egraph.t -> Node.t -> L.t -> unit
+ val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
(** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
[l] with the current value of the domain. *)
end
@@ -555,7 +523,7 @@ module Interp : sig
type 'a t
(** Sequence, finite during module fixing *)
- val of_seq : Egraph.t -> 'a Base.Sequence.t -> 'a t
+ val of_seq : _ Egraph.t -> 'a Base.Sequence.t -> 'a t
(** Limit the sequence to the given bound of the iterative deepening.
Sequence used for enumerating the values should be limited for ensuring
fairness. If the sequence contained more elements than limited the top
@@ -576,13 +544,13 @@ module Interp : sig
end
module Register : sig
- val check : Egraph.t -> (Egraph.t -> Ground.t -> bool option) -> unit
+ val check : Egraph.wt -> (Egraph.rt -> Ground.t -> bool option) -> unit
(** Check the value of the arguments corresponds to the the one of the of the term *)
val node :
- Egraph.t ->
- ((Egraph.t -> Node.t -> Value.t SeqLim.t) ->
- Egraph.t ->
+ Egraph.wt ->
+ ((Egraph.wt -> Node.t -> Value.t SeqLim.t) ->
+ Egraph.wt ->
Node.t ->
Value.t SeqLim.t option) ->
unit
@@ -590,17 +558,18 @@ module Interp : sig
information on the domains. It could ask the computation of other nodes *)
val ty :
- Egraph.t -> (Egraph.t -> Ground.Ty.t -> Value.t SeqLim.t option) -> unit
+ Egraph.wt -> (Egraph.rt -> Ground.Ty.t -> Value.t SeqLim.t option) -> unit
(** Register iterators on all the possible value of some types, all the values
must be reached eventually *)
end
- val ty : Egraph.t -> Ground.Ty.t -> Value.t SeqLim.t
+ val ty : _ Egraph.t -> Ground.Ty.t -> Value.t SeqLim.t
(** Iterate on all the possible value of the given type, usually all the values
will be reached eventually *)
module WatchArgs : sig
- val create : Egraph.t -> (Egraph.t -> Ground.t -> unit) -> Ground.t -> unit
+ val create :
+ Egraph.wt -> (Egraph.wt -> Ground.t -> unit) -> Ground.t -> unit
(** call the given function when all the arguments of the ground term have a value *)
end
end
@@ -656,25 +625,17 @@ module Datastructure : sig
val create : 'a Format.printer -> string -> 'a t
- val remove : 'a t -> Egraph.t -> key -> unit
-
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
-
- val find : 'a t -> Egraph.t -> key -> 'a
+ val remove : 'a t -> _ Egraph.t -> key -> unit
- val find_opt : 'a t -> Egraph.t -> key -> 'a option
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
- val mem : 'a t -> Egraph.t -> key -> bool
+ val find : 'a t -> _ Egraph.t -> key -> 'a
- val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
+ val find_opt : 'a t -> _ Egraph.t -> key -> 'a option
- module Ro : sig
- val find : 'a t -> Egraph.Ro.t -> key -> 'a
+ val mem : 'a t -> _ Egraph.t -> key -> bool
- val find_opt : 'a t -> Egraph.Ro.t -> key -> 'a option
-
- val mem : 'a t -> Egraph.Ro.t -> key -> bool
- end
+ val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
end
module Hashtbl (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
@@ -689,19 +650,11 @@ module Datastructure : sig
val create : 'a Format.printer -> string -> (Context.creator -> 'a) -> 'a t
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
-
- val find : 'a t -> Egraph.t -> key -> 'a
-
- val change : ('a -> 'a) -> 'a t -> Egraph.t -> key -> unit
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
- module Ro : sig
- val set : 'a t -> Egraph.Ro.t -> key -> 'a -> unit
+ val find : 'a t -> _ Egraph.t -> key -> 'a
- val find : 'a t -> Egraph.Ro.t -> key -> 'a
-
- val change : ('a -> 'a) -> 'a t -> Egraph.Ro.t -> key -> unit
- end
+ val change : ('a -> 'a) -> 'a t -> _ Egraph.t -> key -> unit
end
module Hashtbl2 (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
@@ -718,11 +671,11 @@ module Datastructure : sig
val create :
'a Format.printer -> string -> (Context.creator -> key -> 'a) -> 'a t
- val find : 'a t -> Egraph.t -> key -> 'a
+ val find : 'a t -> _ Egraph.t -> key -> 'a
- val iter : (key -> 'a -> unit) -> 'a t -> Egraph.t -> unit
+ val iter : (key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
- val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> Egraph.t -> 'acc -> 'acc
+ val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> _ Egraph.t -> 'acc -> 'acc
end
module Memo (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
@@ -733,15 +686,15 @@ module Datastructure : sig
val create : 'a Format.printer -> string -> 'a t
- val push : 'a t -> Egraph.t -> 'a -> unit
+ val push : 'a t -> _ Egraph.t -> 'a -> unit
- val iter : f:('a -> unit) -> 'a t -> Egraph.t -> unit
+ val iter : f:('a -> unit) -> 'a t -> _ Egraph.t -> unit
- val fold : f:('acc -> 'a -> 'acc) -> init:'acc -> 'a t -> Egraph.t -> 'acc
+ val fold : f:('acc -> 'a -> 'acc) -> init:'acc -> 'a t -> _ Egraph.t -> 'acc
- val length : 'a t -> Egraph.t -> int
+ val length : 'a t -> _ Egraph.t -> int
- val get : 'a t -> Egraph.t -> int -> 'a
+ val get : 'a t -> _ Egraph.t -> int -> 'a
end
module Ref : sig
@@ -749,15 +702,9 @@ module Datastructure : sig
val create : 'a Fmt.t -> string -> 'a -> 'a t
- val get : 'a t -> Egraph.t -> 'a
-
- val set : 'a t -> Egraph.t -> 'a -> unit
+ val get : 'a t -> _ Egraph.t -> 'a
- module Ro : sig
- val get : 'a t -> Egraph.Ro.t -> 'a
-
- val set : 'a t -> Egraph.Ro.t -> 'a -> unit
- end
+ val set : 'a t -> _ Egraph.t -> 'a -> unit
end
end
@@ -774,11 +721,11 @@ module Daemon : sig
run as soon as possible during the propagation phase *)
val attach_dom :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
- (Egraph.t -> Node.t -> unit) ->
+ (Egraph.wt -> Node.t -> unit) ->
unit
(** [attach_dom d ?direct n dom callback] The callback is scheduled when the
domain [dom] of the equivalence class of [n] is modified. If direct is true
@@ -786,37 +733,38 @@ module Daemon : sig
set. *)
val attach_any_dom :
- Egraph.t -> 'a Dom.Kind.t -> (Egraph.t -> Node.t -> unit) -> unit
+ _ Egraph.t -> 'a Dom.Kind.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
- (Egraph.t -> Node.t -> 'b -> unit) ->
+ (Egraph.wt -> Node.t -> 'b -> unit) ->
unit
val attach_any_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
- (Egraph.t -> Node.t -> Value.t -> unit) ->
+ (Egraph.wt -> Node.t -> Value.t -> unit) ->
unit
- val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+ val attach_reg_any : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_reg_node :
- Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+ _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_reg_sem :
- Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+ _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
val attach_reg_value :
- Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+ _ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
- val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+ val attach_repr :
+ _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
- val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+ val attach_any_repr : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
end
module DaemonFixingModel : sig
@@ -826,46 +774,47 @@ module DaemonFixingModel : sig
the FixingModel phase *)
val attach_dom :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
- (Egraph.t -> Node.t -> unit) ->
+ (Egraph.wt -> Node.t -> unit) ->
unit
(** [attach_dom d ?direct n dom callback] The callback is *)
val attach_any_dom :
- Egraph.t -> 'a Dom.Kind.t -> (Egraph.t -> Node.t -> unit) -> unit
+ _ Egraph.t -> 'a Dom.Kind.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
- (Egraph.t -> Node.t -> 'b -> unit) ->
+ (Egraph.wt -> Node.t -> 'b -> unit) ->
unit
val attach_any_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
- (Egraph.t -> Node.t -> Value.t -> unit) ->
+ (Egraph.wt -> Node.t -> Value.t -> unit) ->
unit
- val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+ val attach_reg_any : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_reg_node :
- Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+ _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_reg_sem :
- Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+ _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
val attach_reg_value :
- Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+ _ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.wt -> 'b -> unit) -> unit
- val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+ val attach_repr :
+ _ Egraph.t -> Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
- val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+ val attach_any_repr : _ Egraph.t -> (Egraph.wt -> Node.t -> unit) -> unit
end
module DaemonWithFilter : sig
@@ -875,64 +824,64 @@ module DaemonWithFilter : sig
the FixingModel phase *)
val attach_dom :
- Egraph.Ro.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
- (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
(** [attach_dom d ?direct n dom callback] The callback is *)
val attach_any_dom :
- Egraph.Ro.t ->
+ _ Egraph.t ->
'a Dom.Kind.t ->
- (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_value :
- Egraph.Ro.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
- (Egraph.Ro.t -> Node.t -> 'b -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> Node.t -> 'b -> (Egraph.wt -> unit) option) ->
unit
val attach_any_value :
- Egraph.Ro.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
- (Egraph.Ro.t -> Node.t -> Value.t -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> Node.t -> Value.t -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_any :
- Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) -> unit
+ _ Egraph.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
val attach_reg_node :
- Egraph.Ro.t ->
+ _ Egraph.t ->
Node.t ->
- (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_sem :
- Egraph.Ro.t ->
+ _ Egraph.t ->
('a, 'b) ThTerm.Kind.t ->
- (Egraph.Ro.t -> 'b -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> 'b -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_value :
- Egraph.Ro.t ->
+ _ Egraph.t ->
('a, 'b) Value.Kind.t ->
- (Egraph.Ro.t -> 'b -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> 'b -> (Egraph.wt -> unit) option) ->
unit
val attach_repr :
- Egraph.Ro.t ->
+ _ Egraph.t ->
Node.t ->
- (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_any_repr :
- Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) -> unit
+ _ Egraph.t -> (Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) -> unit
end
module Monad : sig
@@ -945,7 +894,7 @@ module Monad : sig
val setd : 'a Dom.Kind.t -> Node.t -> 'a option monad -> sequence
val updd :
- (Egraph.t -> Node.t -> 'a -> unit) -> Node.t -> 'a option monad -> sequence
+ (Egraph.wt -> Node.t -> 'a -> unit) -> Node.t -> 'a option monad -> sequence
val getv : ('a, _) Value.Kind.t -> Node.t -> 'a option monad
@@ -959,7 +908,7 @@ module Monad : sig
val ( && ) : sequence -> sequence -> sequence
- val attach : Egraph.t -> sequence -> unit
+ val attach : _ Egraph.t -> sequence -> unit
end
module rec DaemonWithKey : sig
@@ -970,38 +919,40 @@ module rec DaemonWithKey : sig
val delay : Events.delay
- val run : Egraph.t -> Key.t -> state
+ val run : Egraph.wt -> Key.t -> state
val name : string
end
module Register (S : S) : sig
val attach_dom :
- Egraph.t -> ?direct:bool -> Node.t -> 'a Dom.Kind.t -> S.Key.t -> unit
+ _ Egraph.t -> ?direct:bool -> Node.t -> 'a Dom.Kind.t -> S.Key.t -> unit
- val attach_any_dom : Egraph.t -> 'a Dom.Kind.t -> S.Key.t -> unit
+ val attach_any_dom : _ Egraph.t -> 'a Dom.Kind.t -> S.Key.t -> unit
val attach_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
S.Key.t ->
unit
- val attach_any_value : Egraph.t -> ?direct:bool -> Node.t -> S.Key.t -> unit
+ val attach_any_value :
+ _ Egraph.t -> ?direct:bool -> Node.t -> S.Key.t -> unit
- val attach_reg_any : Egraph.t -> S.Key.t -> unit
+ val attach_reg_any : _ Egraph.t -> S.Key.t -> unit
- val attach_reg_node : Egraph.t -> Node.t -> S.Key.t -> unit
+ val attach_reg_node : _ Egraph.t -> Node.t -> S.Key.t -> unit
- val attach_reg_sem : Egraph.t -> ('a, 'b) ThTerm.Kind.t -> S.Key.t -> unit
+ val attach_reg_sem : _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> S.Key.t -> unit
- val attach_reg_value : Egraph.t -> ('a, 'b) Value.Kind.t -> S.Key.t -> unit
+ val attach_reg_value :
+ _ Egraph.t -> ('a, 'b) Value.Kind.t -> S.Key.t -> unit
- val attach_repr : Egraph.t -> Node.t -> S.Key.t -> unit
+ val attach_repr : _ Egraph.t -> Node.t -> S.Key.t -> unit
- val attach_any_repr : Egraph.t -> S.Key.t -> unit
+ val attach_any_repr : _ Egraph.t -> S.Key.t -> unit
end
end
@@ -1036,7 +987,7 @@ and Events : sig
val print_runable : runable Format.printer
- val run : Egraph.t -> runable -> unit
+ val run : Egraph.wt -> runable -> unit
(** The function run after the delay *)
val key : runable Dem.t
@@ -1049,131 +1000,69 @@ and Events : sig
(** {3 Attach daemons } *)
val attach_dom :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
- (Egraph.Ro.t -> Node.t -> enqueue) ->
+ (Egraph.rt -> Node.t -> enqueue) ->
unit
(** wakeup when the dom of the node change *)
val attach_any_dom :
- Egraph.t -> 'a Dom.Kind.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ _ Egraph.t -> 'a Dom.Kind.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when the dom of any node change *)
val attach_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
- (Egraph.Ro.t -> Node.t -> 'b -> enqueue) ->
+ (Egraph.rt -> Node.t -> 'b -> enqueue) ->
unit
(** wakeup when a value is attached to this equivalence class *)
val attach_any_value :
- Egraph.t ->
+ _ Egraph.t ->
?direct:bool ->
Node.t ->
- (Egraph.Ro.t -> Node.t -> Value.t -> enqueue) ->
+ (Egraph.rt -> Node.t -> Value.t -> enqueue) ->
unit
(** wakeup when any kind of value is attached to this equivalence class *)
- val attach_reg_any : Egraph.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ val attach_reg_any : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when any node is registered *)
val attach_reg_node :
- Egraph.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ _ Egraph.t -> Node.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when this node is registered *)
val attach_reg_sem :
- Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.Ro.t -> 'b -> enqueue) -> unit
+ _ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.rt -> 'b -> enqueue) -> unit
(** wakeup when a new semantical class is registered *)
val attach_reg_value :
- Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.Ro.t -> 'b -> enqueue) -> unit
+ _ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.rt -> 'b -> enqueue) -> unit
(** wakeup when a new value is registered *)
val attach_repr :
- Egraph.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ _ Egraph.t -> Node.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when it is not anymore the representative class *)
- val attach_any_repr : Egraph.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ val attach_any_repr : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when a node is not its representative class anymore *)
- module Ro : sig
- val attach_dom :
- Egraph.Ro.t ->
- ?direct:bool ->
- Node.t ->
- 'a Dom.Kind.t ->
- (Egraph.Ro.t -> Node.t -> enqueue) ->
- unit
- (** wakeup when the dom of the node change *)
-
- val attach_any_dom :
- Egraph.Ro.t -> 'a Dom.Kind.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
- (** wakeup when the dom of any node change *)
-
- val attach_value :
- Egraph.Ro.t ->
- ?direct:bool ->
- Node.t ->
- ('a, 'b) Value.Kind.t ->
- (Egraph.Ro.t -> Node.t -> 'b -> enqueue) ->
- unit
- (** wakeup when a value is attached to this equivalence class *)
-
- val attach_any_value :
- Egraph.Ro.t ->
- ?direct:bool ->
- Node.t ->
- (Egraph.Ro.t -> Node.t -> Value.t -> enqueue) ->
- unit
- (** wakeup when any kind of value is attached to this equivalence class *)
-
- val attach_reg_any :
- Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
- (** wakeup when any node is registered *)
-
- val attach_reg_node :
- Egraph.Ro.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
- (** wakeup when this node is registered *)
-
- val attach_reg_sem :
- Egraph.Ro.t ->
- ('a, 'b) ThTerm.Kind.t ->
- (Egraph.Ro.t -> 'b -> enqueue) ->
- unit
- (** wakeup when a new semantical class is registered *)
-
- val attach_reg_value :
- Egraph.Ro.t ->
- ('a, 'b) Value.Kind.t ->
- (Egraph.Ro.t -> 'b -> enqueue) ->
- unit
- (** wakeup when a new value is registered *)
-
- val attach_repr :
- Egraph.Ro.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
- (** wakeup when it is not anymore the representative class *)
-
- val attach_any_repr :
- Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
- (** wakeup when a node is not its representative class anymore *)
- end
-
- val new_pending_daemon : Egraph.t -> 'a Dem.t -> 'a -> unit
+ val new_pending_daemon : _ Egraph.t -> 'a Dem.t -> 'a -> unit
(** register an event for later (immediate or not). *)
end
(** {3 Choices } *)
module Choice : sig
- type choice_state = DecNo | DecTodo of (Egraph.t -> unit) list
+ type choice_state = DecNo | DecTodo of (Egraph.wt -> unit) list
- and t = { choice : Egraph.t -> choice_state; prio : int }
+ and t = { choice : Egraph.wt -> choice_state; prio : int }
- val register : Egraph.t -> t -> unit
+ val register : Egraph.wt -> t -> unit
(** register a decision that would be scheduled later. The
[choose_decision] of the [Cho] will be called at that time to know
if the decision is still needed. *)
@@ -1182,7 +1071,7 @@ end
(** {3 Helpers } *)
module Init : sig
- val add_default_theory : (Egraph.t -> unit) -> unit
+ val add_default_theory : (Egraph.wt -> unit) -> unit
end
module Debug : sig
@@ -1575,9 +1464,9 @@ module ForSchedulers : sig
t ->
unit
- val get_delayed : t -> Egraph.t
+ val get_delayed : t -> Egraph.wt
- val run_daemon : Egraph.t -> Events.daemon_key -> unit
+ val run_daemon : Egraph.wt -> Events.daemon_key -> unit
(** schedule the run of a deamon *)
val delayed_stop : t -> unit
@@ -1592,23 +1481,23 @@ module ForSchedulers : sig
val output_graph : string -> t -> unit
end
- val default_theories : unit -> (Egraph.t -> unit) list
+ val default_theories : unit -> (Egraph.wt -> unit) list
- val ground_init : Egraph.t -> unit
+ val ground_init : Egraph.wt -> unit
(** Initialize the module ground for later use *)
- val interp_init : Egraph.t -> unit
+ val interp_init : Egraph.wt -> unit
(** Initialize the module interp for later use *)
val get_event_priority : Events.daemon_key -> Events.delay
- val flush_internal : Egraph.t -> unit
+ val flush_internal : Egraph.wt -> unit
module Fix_model : sig
(** The model is search using iterative deepening depth-first search for
ensuring optimality even in presence of infinite choice *)
- val next_dec : Egraph.t -> (Egraph.t -> unit) Base.Sequence.t
+ val next_dec : Egraph.wt -> (Egraph.wt -> unit) Base.Sequence.t
(** Add a level of decision for fixing the model, another level could be
needed. Could raise unsatisfiable if all the model have been tried *)
end
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index 7eac0a8180736d9b7b7b15157cc36bbbd12b38a0..8065d2c294e9cd953d07e60a0c66f3c340fe562a 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -24,17 +24,12 @@ module type Sig = sig
val create: 'a Format.printer -> string -> 'a t
- val remove : 'a t -> Egraph.t -> key -> unit
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
- val find: 'a t -> Egraph.t -> key -> 'a
- val find_opt: 'a t -> Egraph.t -> key -> 'a option
- val mem: 'a t -> Egraph.t -> key -> bool
- val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
- module Ro: sig
- val find: 'a t -> Egraph.Ro.t -> key -> 'a
- val find_opt: 'a t -> Egraph.Ro.t -> key -> 'a option
- val mem: 'a t -> Egraph.Ro.t -> key -> bool
- end
+ val remove : 'a t -> _ Egraph.t -> key -> unit
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
+ val find: 'a t -> _ Egraph.t -> key -> 'a
+ val find_opt: 'a t -> _ Egraph.t -> key -> 'a option
+ val mem: 'a t -> _ Egraph.t -> key -> bool
+ val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
end
module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t = struct
@@ -102,14 +97,6 @@ module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key :
in
S.H.change change h k
- module Ro = struct
-
- let find t d k = find' Egraph.Ro.get_unsaved_env t d k
- let find_opt t d k = find_opt' Egraph.Ro.get_unsaved_env t d k
- let mem t d k = mem' Egraph.Ro.get_unsaved_env t d k
-
- end
-
end
module type Sig2 = sig
@@ -118,15 +105,9 @@ module type Sig2 = sig
val create: 'a Format.printer -> string -> (Context.creator -> 'a) -> 'a t
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
- val find : 'a t -> Egraph.t -> key -> 'a
- val change : ('a -> 'a) -> 'a t -> Egraph.t -> key -> unit
-
- module Ro: sig
- val set : 'a t -> Egraph.Ro.t -> key -> 'a -> unit
- val find : 'a t -> Egraph.Ro.t -> key -> 'a
- val change : ('a -> 'a) -> 'a t -> Egraph.Ro.t -> key -> unit
- end
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
+ val find : 'a t -> _ Egraph.t -> key -> 'a
+ val change : ('a -> 'a) -> 'a t -> _ Egraph.t -> key -> unit
end
@@ -171,31 +152,6 @@ module Hashtbl2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key
let r = find_aux t d k in
let v = f (Context.Ref.get r) in
Context.Ref.set r v
-
- module Ro = struct
-
- let find_aux t d k =
- let h = Egraph.Ro.get_unsaved_env d t in
- match S.H.find_opt h.h k with
- | Some r -> r
- | None ->
- let r = Context.Ref.create (Egraph.Ro.context d) (h.def (Egraph.Ro.context d)) in
- S.H.add h.h k r;
- r
-
- let find t d k =
- Context.Ref.get (find_aux t d k)
-
- let set t d k v =
- let r = find_aux t d k in
- Context.Ref.set r v
-
- let change f t d k =
- let r = find_aux t d k in
- let v = f (Context.Ref.get r) in
- Context.Ref.set r v
-
- end
end
module type Memo = sig
@@ -203,9 +159,9 @@ module type Memo = sig
type key
val create: 'a Format.printer -> string -> (Context.creator -> key -> 'a) -> 'a t
- val find : 'a t -> Egraph.t -> key -> 'a
- val iter : (key -> 'a -> unit) -> 'a t -> Egraph.t -> unit
- val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> Egraph.t -> 'acc -> 'acc
+ val find : 'a t -> _ Egraph.t -> key -> 'a
+ val iter : (key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
+ val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> _ Egraph.t -> 'acc -> 'acc
end
module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t = struct
@@ -294,9 +250,4 @@ module Ref = struct
let get t d = Context.Ref.get (Egraph.get_unsaved_env d t)
let set t d v = Context.Ref.set (Egraph.get_unsaved_env d t) v
-
- module Ro = struct
- let get t d = Context.Ref.get (Egraph.Ro.get_unsaved_env d t)
- let set t d v = Context.Ref.set (Egraph.Ro.get_unsaved_env d t) v
- end
end
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index c5101b8b1db22acb125f1b88ed314ea9bc8385f3..c411f6f263cedff8405cd848f2a90c55049dfe8c 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -26,17 +26,12 @@ module type Sig = sig
val create: 'a Format.printer -> string -> 'a t
- val remove : 'a t -> Egraph.t -> key -> unit
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
- val find: 'a t -> Egraph.t -> key -> 'a
- val find_opt: 'a t -> Egraph.t -> key -> 'a option
- val mem: 'a t -> Egraph.t -> key -> bool
- val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
- module Ro: sig
- val find: 'a t -> Egraph.Ro.t -> key -> 'a
- val find_opt: 'a t -> Egraph.Ro.t -> key -> 'a option
- val mem: 'a t -> Egraph.Ro.t -> key -> bool
- end
+ val remove : 'a t -> _ Egraph.t -> key -> unit
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
+ val find: 'a t -> _ Egraph.t -> key -> 'a
+ val find_opt: 'a t -> _ Egraph.t -> key -> 'a option
+ val mem: 'a t -> _ Egraph.t -> key -> bool
+ val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
end
module Hashtbl (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t
@@ -49,15 +44,9 @@ module type Sig2 = sig
val create: 'a Format.printer -> string -> (Context.creator -> 'a) -> 'a t
- val set : 'a t -> Egraph.t -> key -> 'a -> unit
- val find : 'a t -> Egraph.t -> key -> 'a
- val change : ('a -> 'a) -> 'a t -> Egraph.t -> key -> unit
-
- module Ro: sig
- val set : 'a t -> Egraph.Ro.t -> key -> 'a -> unit
- val find : 'a t -> Egraph.Ro.t -> key -> 'a
- val change : ('a -> 'a) -> 'a t -> Egraph.Ro.t -> key -> unit
- end
+ val set : 'a t -> _ Egraph.t -> key -> 'a -> unit
+ val find : 'a t -> _ Egraph.t -> key -> 'a
+ val change : ('a -> 'a) -> 'a t -> _ Egraph.t -> key -> unit
end
module Hashtbl2 (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key := S.t
@@ -70,9 +59,9 @@ module type Memo = sig
type key
val create: 'a Format.printer -> string -> (Context.creator -> key -> 'a) -> 'a t
- val find : 'a t -> Egraph.t -> key -> 'a
- val iter : (key -> 'a -> unit) -> 'a t -> Egraph.t -> unit
- val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> Egraph.t -> 'acc -> 'acc
+ val find : 'a t -> _ Egraph.t -> key -> 'a
+ val iter : (key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
+ val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> _ Egraph.t -> 'acc -> 'acc
end
module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := S.t
@@ -84,21 +73,17 @@ module Push: sig
type 'a t
val create: 'a Format.printer -> string -> 'a t
- val push: 'a t -> Egraph.t -> 'a -> unit
- val iter: f:('a -> unit) -> 'a t -> Egraph.t -> unit
- val fold: f:('acc -> 'a -> 'acc) -> init:'acc -> 'a t -> Egraph.t -> 'acc
- val length: 'a t -> Egraph.t -> int
- val get: 'a t -> Egraph.t -> int -> 'a
+ val push: 'a t -> _ Egraph.t -> 'a -> unit
+ val iter: f:('a -> unit) -> 'a t -> _ Egraph.t -> unit
+ val fold: f:('acc -> 'a -> 'acc) -> init:'acc -> 'a t -> _ Egraph.t -> 'acc
+ val length: 'a t -> _ Egraph.t -> int
+ val get: 'a t -> _ Egraph.t -> int -> 'a
end
module Ref: sig
type 'a t
val create: 'a Fmt.t -> string -> 'a -> 'a t
- val get: 'a t -> Egraph.t -> 'a
- val set: 'a t -> Egraph.t -> 'a -> unit
- module Ro: sig
- val get: 'a t -> Egraph.Ro.t -> 'a
- val set: 'a t -> Egraph.Ro.t -> 'a -> unit
- end
+ val get: 'a t -> _ Egraph.t -> 'a
+ val set: 'a t -> _ Egraph.t -> 'a -> unit
end
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 09215f27629b6abf19143936d3dac58c2ca861f2..dbe78b2b920e2fc389220050293289a8c550c55e 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -21,47 +21,52 @@
open Nodes
module type Attach = sig
- type 'a arg
+ type ('a, 'b) arg
type 'a env
type result
val attach_dom :
- (?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit)
+ ( ?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit,
+ 'b )
arg
- val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit) arg
+ val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit, 'b) arg
val attach_value :
- (?direct:bool ->
- Node.t ->
- ('a, 'b) ValueKind.t ->
- (Node.t -> 'b -> result) env ->
- unit)
+ ( ?direct:bool ->
+ Node.t ->
+ ('a, 'b) ValueKind.t ->
+ (Node.t -> 'b -> result) env ->
+ unit,
+ 'r )
arg
val attach_any_value :
- (?direct:bool -> Node.t -> (Node.t -> Value.t -> result) env -> unit) arg
+ ( ?direct:bool -> Node.t -> (Node.t -> Value.t -> result) env -> unit,
+ 'b )
+ arg
- val attach_reg_any : ((Node.t -> result) env -> unit) arg
+ val attach_reg_any : ((Node.t -> result) env -> unit, 'b) arg
- val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit) arg
+ val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
- val attach_reg_sem : (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit) arg
+ val attach_reg_sem :
+ (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit, 'r) arg
val attach_reg_value :
- (('a, 'b) ValueKind.t -> ('b -> result) env -> unit) arg
+ (('a, 'b) ValueKind.t -> ('b -> result) env -> unit, 'r) arg
- val attach_repr : (Node.t -> (Node.t -> result) env -> unit) arg
+ val attach_repr : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
- val attach_any_repr : ((Node.t -> result) env -> unit) arg
+ val attach_any_repr : ((Node.t -> result) env -> unit, 'b) arg
end
module type Simple =
Attach
- with type 'a arg := Egraph.t -> 'a
- and type 'a env := Egraph.t -> 'a
+ with type ('a, 'b) arg := 'b Egraph.t -> 'a
+ and type 'a env := Egraph.wt -> 'a
and type result := unit
module Simple = struct
@@ -72,7 +77,7 @@ module Simple = struct
end) =
struct
module D = struct
- type runable = Egraph.t -> unit
+ type runable = Egraph.wt -> unit
let print_runable = Fmt.nop
@@ -81,7 +86,7 @@ module Simple = struct
let key =
Events.Dem.create
(module struct
- type t = Egraph.t -> unit
+ type t = Egraph.wt -> unit
let name = Info.name
end)
@@ -138,7 +143,7 @@ end
module WithFilter = struct
module D = struct
- type runable = Egraph.t -> unit
+ type runable = Egraph.wt -> unit
let print_runable = Fmt.nop
@@ -147,7 +152,7 @@ module WithFilter = struct
let key =
Events.Dem.create
(module struct
- type t = Egraph.t -> unit
+ type t = Egraph.wt -> unit
let name = "Demon.WithFilter"
end)
@@ -173,27 +178,27 @@ module WithFilter = struct
| Some g -> Events.EnqRun (D.key, g)
let attach_dom d ?direct n dom f =
- Egraph.Ro.attach_dom d ?direct n dom (wrap_node f)
+ Egraph.attach_dom d ?direct n dom (wrap_node f)
- let attach_any_dom d dom f = Egraph.Ro.attach_any_dom d dom (wrap_node f)
+ let attach_any_dom d dom f = Egraph.attach_any_dom d dom (wrap_node f)
let attach_value d ?direct n v f =
- Egraph.Ro.attach_value d ?direct n v (wrap_node_and_other f)
+ Egraph.attach_value d ?direct n v (wrap_node_and_other f)
let attach_any_value d ?direct n f =
- Egraph.Ro.attach_any_value d ?direct n (wrap_node_and_other f)
+ Egraph.attach_any_value d ?direct n (wrap_node_and_other f)
- let attach_reg_any d f = Egraph.Ro.attach_reg_any d (wrap_node f)
+ let attach_reg_any d f = Egraph.attach_reg_any d (wrap_node f)
- let attach_reg_node d n f = Egraph.Ro.attach_reg_node d n (wrap_node f)
+ let attach_reg_node d n f = Egraph.attach_reg_node d n (wrap_node f)
- let attach_reg_sem d th f = Egraph.Ro.attach_reg_sem d th (wrap_other f)
+ let attach_reg_sem d th f = Egraph.attach_reg_sem d th (wrap_other f)
- let attach_reg_value d th f = Egraph.Ro.attach_reg_value d th (wrap_other f)
+ let attach_reg_value d th f = Egraph.attach_reg_value d th (wrap_other f)
- let attach_repr d n f = Egraph.Ro.attach_repr d n (wrap_node f)
+ let attach_repr d n f = Egraph.attach_repr d n (wrap_node f)
- let attach_any_repr d f = Egraph.Ro.attach_any_repr d (wrap_node f)
+ let attach_any_repr d f = Egraph.attach_any_repr d (wrap_node f)
end
module Key = struct
@@ -204,7 +209,7 @@ module Key = struct
val delay : Events.delay
- val run : Egraph.t -> Key.t -> state
+ val run : Egraph.wt -> Key.t -> state
val name : string
end
@@ -245,10 +250,10 @@ module Key = struct
end)
let wrap k d =
- match H.Ro.find h d k with
+ match H.find h d k with
| Stop -> Events.EnqStopped
| Wait ->
- H.Ro.set h d k Scheduled;
+ H.set h d k Scheduled;
Events.EnqRun (key, k)
| Scheduled -> Events.EnqAlready
@@ -300,7 +305,7 @@ module Monad = struct
| SetV : Node.t * ('b, _) ValueKind.t * 'b option monad -> sequence
| SetD : Node.t * 'a DomKind.t * 'a option monad -> sequence
| UpdD :
- Node.t * (Egraph.t -> Node.t -> 'a -> unit) * 'a option monad
+ Node.t * (Egraph.wt -> Node.t -> 'a -> unit) * 'a option monad
-> sequence
let getv m n = GetV (n, m)
@@ -326,7 +331,7 @@ module Monad = struct
| SetV : Node.t * Value.t * runable -> runable
| SetD : Node.t * 'a DomKind.t * 'a * runable -> runable
| UpdD :
- Node.t * (Egraph.t -> Node.t -> 'a -> unit) * 'a * runable
+ Node.t * (Egraph.wt -> Node.t -> 'a -> unit) * 'a * runable
-> runable
| Nil : runable
@@ -357,7 +362,7 @@ module Monad = struct
let () = Egraph.Wait.register_dem (module D)
- let rec compute : type a. Egraph.Ro.t -> a monad -> a =
+ let rec compute : type a. _ Egraph.t -> a monad -> a =
fun d -> function
| Both (a, b) -> (
match compute d a with
@@ -368,10 +373,10 @@ module Monad = struct
match compute d a with None -> None | Some v -> Some (f v))
| Bindo (a, f) -> ( match compute d a with None -> None | Some v -> f v)
| GetV (n, m) -> (
- match Egraph.Ro.get_value d n with
+ match Egraph.get_value d n with
| None -> None
| Some v -> Value.value m v)
- | GetD (n, dom) -> Egraph.Ro.get_dom d dom n
+ | GetD (n, dom) -> Egraph.get_dom d dom n
let rec compute_seq d acc : _ -> D.runable = function
| Sequence (a, b) -> compute_seq d (compute_seq d acc a) b
@@ -390,7 +395,7 @@ module Monad = struct
sems : Node.S.t ValueKind.Vector.t;
}
- let rec attach_aux : type a. Egraph.t -> footprint -> a monad -> bool =
+ let rec attach_aux : type a. _ Egraph.t -> footprint -> a monad -> bool =
fun d ft -> function
| Both (a, b) -> Stdlib.( && ) (attach_aux d ft a) (attach_aux d ft b)
| Bind (a, _) -> attach_aux d ft a
@@ -438,7 +443,7 @@ module Monad = struct
in
ValueKind.Vector.iter_initializedi { iteri } ft.sems;
if b then
- match compute_seq (d :> Egraph.Ro.t) D.Nil seq with
+ match compute_seq d D.Nil seq with
| Nil -> ()
| r -> Egraph.new_pending_daemon d D.key r
end
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index ca83bbdf49e75851855718930fe55cb7dd405c42..b02bdb2f472831b9f9b9330b6c32505d2664a7eb 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -21,47 +21,52 @@
open Nodes
module type Attach = sig
- type 'a arg
+ type ('a, 'b) arg
type 'a env
type result
val attach_dom :
- (?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit)
+ ( ?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit,
+ 'b )
arg
- val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit) arg
+ val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit, 'b) arg
val attach_value :
- (?direct:bool ->
- Node.t ->
- ('a, 'b) ValueKind.t ->
- (Node.t -> 'b -> result) env ->
- unit)
+ ( ?direct:bool ->
+ Node.t ->
+ ('a, 'b) ValueKind.t ->
+ (Node.t -> 'b -> result) env ->
+ unit,
+ 'r )
arg
val attach_any_value :
- (?direct:bool -> Node.t -> (Node.t -> Value.t -> result) env -> unit) arg
+ ( ?direct:bool -> Node.t -> (Node.t -> Value.t -> result) env -> unit,
+ 'b )
+ arg
- val attach_reg_any : ((Node.t -> result) env -> unit) arg
+ val attach_reg_any : ((Node.t -> result) env -> unit, 'b) arg
- val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit) arg
+ val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
- val attach_reg_sem : (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit) arg
+ val attach_reg_sem :
+ (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit, 'r) arg
val attach_reg_value :
- (('a, 'b) ValueKind.t -> ('b -> result) env -> unit) arg
+ (('a, 'b) ValueKind.t -> ('b -> result) env -> unit, 'r) arg
- val attach_repr : (Node.t -> (Node.t -> result) env -> unit) arg
+ val attach_repr : (Node.t -> (Node.t -> result) env -> unit, 'b) arg
- val attach_any_repr : ((Node.t -> result) env -> unit) arg
+ val attach_any_repr : ((Node.t -> result) env -> unit, 'b) arg
end
module type Simple =
Attach
- with type 'a arg := Egraph.t -> 'a
- and type 'a env := Egraph.t -> 'a
+ with type ('a, 'b) arg := 'b Egraph.t -> 'a
+ and type 'a env := Egraph.wt -> 'a
and type result := unit
module Simple : sig
@@ -72,9 +77,9 @@ end
module WithFilter :
Attach
- with type 'a arg := Egraph.Ro.t -> 'a
- and type 'a env := Egraph.Ro.t -> 'a
- and type result := (Egraph.t -> unit) option
+ with type ('a, 'b) arg := 'b Egraph.t -> 'a
+ and type 'a env := Egraph.rt -> 'a
+ and type result := (Egraph.wt -> unit) option
module Key : sig
type state = Wait | Stop
@@ -84,7 +89,7 @@ module Key : sig
val delay : Events.delay
- val run : Egraph.t -> Key.t -> state
+ val run : Egraph.wt -> Key.t -> state
val name : string
end
@@ -92,7 +97,7 @@ module Key : sig
module Register (S : S) : sig
include
Attach
- with type 'a arg := Egraph.t -> 'a
+ with type ('a, 'b) arg := 'b Egraph.t -> 'a
and type 'a env := S.Key.t
and type result := unit
end
@@ -108,7 +113,10 @@ module Monad : sig
val setd : 'a DomKind.t -> Node.t -> 'a option monad -> sequence
val updd :
- (Egraph.t -> Node.t -> 'a -> unit) -> Node.t -> 'a option monad -> sequence
+ (Egraph.wt -> Node.t -> 'a -> unit) ->
+ Node.t ->
+ 'a option monad ->
+ sequence
val getv : ('a, _) ValueKind.t -> Node.t -> 'a option monad
@@ -122,5 +130,5 @@ module Monad : sig
val ( && ) : sequence -> sequence -> sequence
- val attach : Egraph.t -> sequence -> unit
+ val attach : _ Egraph.t -> sequence -> unit
end
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 1f227e17c9686df9c9bbd2b5bb580d0433aec51b..d77216e05cbe53c7bf9d8f8c72783472a1389e8b 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -24,6 +24,9 @@ open Nodes
exception Contradiction
+type ro = < >
+type rw = < rw: unit >
+
let debug = Debug.register_flag
~desc:"for the core solver"
"Egraph.all"
@@ -77,17 +80,17 @@ module Def = struct
saved_rang : int Node.M.t;
saved_event_repr : event_node Bag.t Node.M.t;
saved_event_any_repr : event_node Bag.t;
- saved_event_value : (delayed_t -> Node.t -> Value.t -> Events.enqueue) Bag.t Node.M.t;
+ saved_event_value : (ro delayed_t -> Node.t -> Value.t -> Events.enqueue) Bag.t Node.M.t;
saved_event_reg : event_node Bag.t Node.M.t;
saved_event_any_reg : event_node Bag.t;
- saved_dom : delayed_t VDomTable.t;
- saved_sem : delayed_t VSemTable.t;
- saved_value : delayed_t ValueTable.t;
+ saved_dom : ro delayed_t VDomTable.t;
+ saved_sem : ro delayed_t VSemTable.t;
+ saved_value : ro delayed_t ValueTable.t;
saved_values : Value.t Node.M.t;
saved_envs : Env.Saved.VectorH.t;
}
- and event_node = (delayed_t -> Node.t -> Events.enqueue)
+ and event_node = (ro delayed_t -> Node.t -> Events.enqueue)
and t = {
(** Union Find *)
@@ -98,28 +101,28 @@ module Def = struct
(** Events: the representative of any node changed *)
mutable event_any_repr : event_node Bag.t;
(** Events: the value of this node has been set *)
- mutable event_value : (delayed_t -> Node.t -> Value.t -> Events.enqueue) Bag.t Node.M.t;
+ mutable event_value : (ro delayed_t -> Node.t -> Value.t -> Events.enqueue) Bag.t Node.M.t;
(** Events: this node have been registered *)
mutable event_reg : event_node Bag.t Node.M.t;
(** Events: any node have been registered *)
mutable event_any_reg : event_node Bag.t;
(** Events: semantic term of this kind has been registered *)
- sem : delayed_t VSemTable.t;
+ sem : ro delayed_t VSemTable.t;
(** Information on the domains, data is {!'a domtable} *)
- dom : delayed_t VDomTable.t;
+ dom : ro delayed_t VDomTable.t;
(** Value *)
- value : delayed_t ValueTable.t;
+ value : ro delayed_t ValueTable.t;
mutable values: Value.t Node.M.t;
(** Environment saved during backtrack point *)
envs : Env.Saved.VectorH.t;
(** Environment not saved during backtrack point, they should use !{Context} *)
unsaved_envs: Env.Unsaved.VectorH.t;
history : saved Context.history;
- delayed : delayed_t;
+ delayed : rw delayed_t;
}
(** delayed_t is used *)
- and delayed_t = {
+ and 'a delayed_t = {
env: t;
todo_immediate_dem : action_immediate_dem Queue.t;
todo_merge_dom : action_merge_dom Queue.t;
@@ -145,10 +148,10 @@ module Def = struct
and choice_state =
| DecNo
- | DecTodo of (delayed_t -> unit) list
+ | DecTodo of (rw delayed_t -> unit) list
and choice = {
- choice: delayed_t -> choice_state;
+ choice: rw delayed_t -> choice_state;
prio: int;
}
@@ -172,21 +175,20 @@ open Def
type choice = Def.choice = {
- choice: delayed_t -> choice_state;
+ choice: rw delayed_t -> choice_state;
prio: int;
}
type choice_state = Def.choice_state =
| DecNo
- | DecTodo of (delayed_t -> unit) list
+ | DecTodo of (rw delayed_t -> unit) list
(** {2 Define events} *)
module WaitDef = struct
- type delayed = delayed_t
+ type delayed = rw delayed_t
- type delayed_ro = delayed_t
end
-module Wait : Events.Wait.S with type delayed = delayed_t and type delayed_ro = delayed_t =
+module Wait : Events.Wait.S with type delayed = rw delayed_t =
Events.Wait.Make(WaitDef)
let new_pending_daemon (type d) t (dem : d Events.Dem.t) runable =
@@ -197,7 +199,7 @@ let new_pending_daemon (type d) t (dem : d Events.Dem.t) runable =
| _ -> t.sched_daemon daemonkey
(** {2 Define domain registration} *)
-module VDom = DomKind.Make(struct type delayed = delayed_t end)
+module VDom = DomKind.Make(struct type delayed = rw delayed_t end)
include VDom
module Hidden = Context.Make(struct
@@ -454,8 +456,7 @@ let draw_graph =
module Delayed = struct
open T
- type t = delayed_t
- type ro = delayed_t
+ type 'a t = 'a delayed_t
let context t = Hidden.creator t.env.history
@@ -490,7 +491,7 @@ module Delayed = struct
is_registered t.env node
let run_event t apply e =
- match apply t e with
+ match apply (t:> ro t) e with
| Events.EnqStopped -> None
| EnqAlready -> Some e
| EnqRun (dem,runable) ->
@@ -520,7 +521,7 @@ module Delayed = struct
(* deletion of events are not taken into account for that kind *)
ignore (run_events t (fun t e -> e t node new_v) events)
- let add_pending_merge (t : t) node node' =
+ let add_pending_merge (t : rw t) node node' =
Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]"
Node.pp node Node.pp node';
assert (is_registered t node);
@@ -701,7 +702,7 @@ module Delayed = struct
let node1 = find t node1_0 in
let node2 = find t node2_0 in
let dom_done = ref true in
- let iteri (type a) (dom : a DomKind.t) (domtable : (t,a) domtable) =
+ let iteri (type a) (dom : a DomKind.t) (domtable : (ro t,a) domtable) =
let s1 = Node.M.find_opt node1 domtable.table in
let s2 = Node.M.find_opt node2 domtable.table in
let (module Dom) = VDom.get_dom dom in
@@ -795,7 +796,7 @@ module Delayed = struct
end;
(** move dom events *)
- let iteri (type a) (dom : a DomKind.t) (domtable: (t,a) domtable) =
+ let iteri (type a) (dom : a DomKind.t) (domtable: (ro t,a) domtable) =
match Node.M.find_opt other_node domtable.events with
| None -> ()
| Some other_events ->
@@ -994,7 +995,7 @@ module Delayed = struct
| Some _ ->
ignore (run_event t (fun t f -> f t node) f)
- let attach_value (type a b) t ?(direct=true) node (value : (a,b) ValueKind.t) (f: ro -> Node.t -> b -> Events.enqueue) =
+ let attach_value (type a b) t ?(direct=true) node (value : (a,b) ValueKind.t) (f: ro t -> Node.t -> b -> Events.enqueue) =
let node = find_def t node in
match Node.M.find_opt node t.env.values with
| None ->
@@ -1066,7 +1067,7 @@ include Delayed
module Backtrackable = struct
- type delayed = t
+ type delayed = rw t
type t = Hidden.hidden
let new_t context =
@@ -1165,87 +1166,10 @@ module Backtrackable = struct
let t = Hidden.rw t in
T.find_def t node
- let get_getter t =
- (* assert (check_disabled_delayed t); *)
- t
-
let draw_graph ?force t = let t = Hidden.ro t in draw_graph ?force t
let output_graph s t = let t = Hidden.ro t in output_graph s t
end
-module type Getter = sig
- type t
-
- val is_equal : t -> Node.t -> Node.t -> bool
- val find_def : t -> Node.t -> Node.t
- val get_dom : t -> 'a DomKind.t -> Node.t -> 'a option
- (** dom of the nodeass *)
- val get_value : t -> Node.t -> Value.t option
-
- (** {4 The nodeasses must have been marked has registered} *)
-
- val find : t -> Node.t -> Node.t
- val is_repr : t -> Node.t -> bool
-
- val is_registered : t -> Node.t -> bool
-
- val get_env : t -> 'a Env.Saved.t -> 'a
- val set_env : t -> 'a Env.Saved.t -> 'a -> unit
- val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
-
- val context : t -> Context.creator
-
-end
-
-module Getter : Getter with type t = Backtrackable.t = Backtrackable
-
-module type Ro = sig
- type ro
- type t
- include Getter with type t := t
-
- val register : t -> Node.t -> unit
- (** Add a new node to register *)
-
- (** {3 Attach Event} *)
- (** todo rename events and attachment *)
-
- val attach_dom: t -> ?direct:bool -> Node.t -> 'a DomKind.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when the dom of the node change *)
-
- val attach_any_dom: t -> 'a DomKind.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when the dom of any node change *)
-
- val attach_value: t -> ?direct:bool -> Node.t -> ('a,'b) ValueKind.t -> (ro -> Node.t -> 'b -> Events.enqueue) -> unit
- (** wakeup when a value is attached to this equivalence class *)
-
- val attach_any_value: t -> ?direct:bool -> Node.t -> (ro -> Node.t -> Value.t -> Events.enqueue) -> unit
- (** wakeup when any kind of value is attached to this equivalence class *)
-
- val attach_reg_any: t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when any node is registered *)
-
- val attach_reg_node: t -> Node.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when this node is registered *)
-
- val attach_reg_sem: t -> ('a,'b) ThTermKind.t -> (ro -> 'b -> Events.enqueue) -> unit
- (** wakeup when a new semantical class is registered *)
-
- val attach_reg_value: t -> ('a,'b) ValueKind.t -> (ro -> 'b -> Events.enqueue) -> unit
- (** wakeup when a new value is registered *)
-
- val attach_repr: t -> Node.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when it is not anymore the representative class *)
-
- val attach_any_repr: t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when a node is not its representative class anymore *)
-
-end
-
-type ro = Delayed.t
-
-module Ro : Ro with type t = Delayed.t and type ro = Delayed.t = Delayed
-
let check_initialization () =
VDom.is_well_initialized () && Wait.is_well_initialized ()
@@ -1256,8 +1180,15 @@ let () = Exn_printer.register (fun fmt exn ->
| exn -> raise exn
)
-type theory = t -> unit
+type theory = rw t -> unit
let theories = ref []
let add_default_theory th = theories := th::!theories
let default_theories () = !theories
+
+
+ type wt = rw t
+
+ type rt = ro t
+
+let ro x = (x:> ro t)
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index d6a9d018356017317a95aa3606df2441461abcac..adbe647331fbe848fce5bae17e69cb736e3f68df 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -32,131 +32,123 @@ exception UninitializedEnv of string
exception Contradiction
-module type Getter = sig
- type t
+type ro
+type rw
- val is_equal : t -> Node.t -> Node.t -> bool
- val find_def : t -> Node.t -> Node.t
- val get_dom : t -> 'a DomKind.t -> Node.t -> 'a option
- (** dom of the class *)
- val get_value : t -> Node.t -> Value.t option
- (** one of the value of the class *)
+type +'a t
- (** {4 The classes must have been registered} *)
+type wt = rw t
- val find : t -> Node.t -> Node.t
- val is_repr : t -> Node.t -> bool
+type rt = ro t
- val is_registered : t -> Node.t -> bool
+val attach_dom: _ t -> ?direct:bool -> Node.t -> 'a DomKind.t -> (ro t -> Node.t -> Events.enqueue) -> unit
+(** wakeup when the dom of the node change *)
- val get_env : t -> 'a Env.Saved.t -> 'a
- (** Can raise UninitializedEnv *)
- val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+val attach_any_dom: _ t -> 'a DomKind.t -> (ro t -> Node.t -> Events.enqueue) -> unit
+(** wakeup when the dom of any node change *)
- val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
+val attach_value: _ t -> ?direct:bool -> Node.t -> ('a,'b) ValueKind.t -> (ro t -> Node.t -> 'b -> Events.enqueue) -> unit
+(** wakeup when a value is attached to this equivalence class *)
- val context : t -> Context.creator
+val attach_any_value: _ t -> ?direct:bool -> Node.t -> (ro t -> Node.t -> Value.t -> Events.enqueue) -> unit
+(** wakeup when any kind of value is attached to this equivalence class *)
-end
+val attach_reg_any: _ t -> (ro t -> Node.t -> Events.enqueue) -> unit
+(** wakeup when any node is registered *)
-module type Ro = sig
- type ro
- type t
- include Getter with type t := t
+val attach_reg_node: _ t -> Node.t -> (ro t -> Node.t -> Events.enqueue) -> unit
+(** wakeup when this node is registered *)
- val register : t -> Node.t -> unit
- (** Add a new node to register *)
+val attach_reg_sem: _ t -> ('a,'b) ThTermKind.t -> (ro t -> 'b -> Events.enqueue) -> unit
+(** wakeup when a new semantical class is registered *)
- (** {3 Attach Event} *)
- (** todo rename events and attachment *)
+val attach_reg_value: _ t -> ('a,'b) ValueKind.t -> (ro t -> 'b -> Events.enqueue) -> unit
+(** wakeup when a new value is registered *)
- val attach_dom: t -> ?direct:bool -> Node.t -> 'a DomKind.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when the dom of the node change *)
+val attach_repr: _ t -> Node.t -> (ro t -> Node.t -> Events.enqueue) -> unit
+(** wakeup when it is not anymore the representative class *)
- val attach_any_dom: t -> 'a DomKind.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when the dom of any node change *)
+val attach_any_repr: _ t -> (ro t -> Node.t -> Events.enqueue) -> unit
+(** wakeup when a node is not its representative class anymore *)
- val attach_value: t -> ?direct:bool -> Node.t -> ('a,'b) ValueKind.t -> (ro -> Node.t -> 'b -> Events.enqueue) -> unit
- (** wakeup when a value is attached to this equivalence class *)
+val is_equal : _ t -> Node.t -> Node.t -> bool
- val attach_any_value: t -> ?direct:bool -> Node.t -> (ro -> Node.t -> Value.t -> Events.enqueue) -> unit
- (** wakeup when any kind of value is attached to this equivalence class *)
+val find_def : _ t -> Node.t -> Node.t
- val attach_reg_any: t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when any node is registered *)
+val get_dom : _ t -> 'a DomKind.t -> Node.t -> 'a option
+(** dom of the class *)
- val attach_reg_node: t -> Node.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when this node is registered *)
+val get_value : _ t -> Node.t -> Value.t option
+(** one of the value of the class *)
- val attach_reg_sem: t -> ('a,'b) ThTermKind.t -> (ro -> 'b -> Events.enqueue) -> unit
- (** wakeup when a new semantical class is registered *)
+(** {4 The classes must have been registered} *)
- val attach_reg_value: t -> ('a,'b) ValueKind.t -> (ro -> 'b -> Events.enqueue) -> unit
- (** wakeup when a new value is registered *)
+val find : _ t -> Node.t -> Node.t
- val attach_repr: t -> Node.t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when it is not anymore the representative class *)
+val is_repr : _ t -> Node.t -> bool
- val attach_any_repr: t -> (ro -> Node.t -> Events.enqueue) -> unit
- (** wakeup when a node is not its representative class anymore *)
+val is_registered : _ t -> Node.t -> bool
-end
+val get_env : _ t -> 'a Env.Saved.t -> 'a
+(** Can raise UninitializedEnv *)
-type ro
+val set_env : _ t -> 'a Env.Saved.t -> 'a -> unit
+
+val get_unsaved_env : _ t -> 'a Env.Unsaved.t -> 'a
-module Ro : Ro with type t = ro and type ro = ro
+val context : _ t -> Context.creator
-type t = private Ro.t
-include Ro with type t := t and type ro := Ro.t
+val register : _ t -> Node.t -> unit
+(** Add a new node to register *)
(** {3 Immediate modifications} *)
-val set_dom : t -> 'a DomKind.t -> Node.t -> 'a -> unit
+val set_dom : wt -> 'a DomKind.t -> Node.t -> 'a -> unit
(** change the dom of the equivalence class *)
-val unset_dom : t -> 'a DomKind.t -> Node.t -> unit
+val unset_dom : wt -> 'a DomKind.t -> Node.t -> unit
(** remove the dom of the equivalence class *)
(** {3 Delayed modifications} *)
-val set_thterm : t -> Node.t -> ThTerm.t -> unit
+val set_thterm : wt -> Node.t -> ThTerm.t -> unit
(** attach a theory term to an equivalence class *)
-val set_value: t -> Node.t -> Value.t -> unit
+val set_value: wt -> Node.t -> Value.t -> unit
(** attach value to an equivalence class *)
-val merge : t -> Node.t -> Node.t -> unit
+val merge : wt -> Node.t -> Node.t -> unit
type choice_state =
| DecNo
- | DecTodo of (t -> unit) list
+ | DecTodo of (wt -> unit) list
and choice = {
- choice: t -> choice_state;
+ choice: wt -> choice_state;
prio: int;
}
-val register_decision: t -> choice -> unit
+val register_decision: wt -> choice -> unit
(** register a decision that would be scheduled later. The
[choose_decision] of the [Cho] will be called at that time to know
if the decision is still needed. *)
-val new_pending_daemon: t -> 'a Events.Dem.t -> 'a -> unit
+val new_pending_daemon: _ t -> 'a Events.Dem.t -> 'a -> unit
(** register an event for later (immediate or not). *)
-val contradiction: t -> 'b
+val contradiction: _ t -> 'b
(** {3 Low level} *)
-val flush_internal: t -> unit
+val flush_internal: wt -> unit
(** Apply all the modifications and direct consequences.
Should be used only during wakeup of not immediate daemon
*)
-module Wait : Events.Wait.S with type delayed = t and type delayed_ro = Ro.t
+module Wait : Events.Wait.S with type delayed = wt
(** {2 Domains and Semantic Values key creation} *)
-module type Dom = DomKind.Dom_partial with type delayed := t
+module type Dom = DomKind.Dom_partial with type delayed := wt
val register_dom : (module Dom with type t = 'a) -> unit
@@ -166,12 +158,33 @@ val check_initialization: unit -> bool
val print_dom: 'a DomKind.t -> 'a Format.printer
val print_dom_opt: 'a DomKind.t -> 'a option Format.printer
-module Getter : Getter
-
(** {2 External use of the solver} *)
module Backtrackable: sig
- type delayed = t
- include Getter
+ type delayed = wt
+
+ type t
+
+ val is_equal : t -> Node.t -> Node.t -> bool
+ val find_def : t -> Node.t -> Node.t
+ val get_dom : t -> 'a DomKind.t -> Node.t -> 'a option
+ (** dom of the class *)
+ val get_value : t -> Node.t -> Value.t option
+ (** one of the value of the class *)
+
+ (** {4 The classes must have been registered} *)
+
+ val find : t -> Node.t -> Node.t
+ val is_repr : t -> Node.t -> bool
+
+ val is_registered : t -> Node.t -> bool
+
+ val get_env : t -> 'a Env.Saved.t -> 'a
+ (** Can raise UninitializedEnv *)
+ val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+
+ val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
+
+ val context : t -> Context.creator
val new_t :
Context.creator -> t
@@ -193,10 +206,6 @@ module Backtrackable: sig
val flush: t -> unit
(** Apply all the modifications and direct consequences. *)
- (* val make_decisions : delayed -> attached_daemons -> unit *)
-
- val get_getter : t -> Getter.t
-
(** Debug *)
val draw_graph: ?force:bool -> t -> unit
val output_graph : string -> t -> unit
@@ -205,7 +214,9 @@ end
val print_decision: Colibri2_popop_lib.Debug.flag
val print_contradiction: Colibri2_popop_lib.Debug.flag
-type theory = t -> unit
+type theory = wt -> unit
val add_default_theory: theory -> unit
val default_theories: unit -> theory list
+
+val ro: _ t -> ro t
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 7f018748a98cfdbceb71808f5afb9a6c437f2f4c..3fafbd9c4ec434f69327fed7bf7c25209775fc6d 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -49,8 +49,6 @@ module Wait = struct
module type S = sig
type delayed
- type delayed_ro
-
module type Dem = sig
type runable
@@ -76,14 +74,9 @@ module Wait = struct
module Make (S : sig
type delayed
-
- type delayed_ro
- end) : S with type delayed = S.delayed and type delayed_ro = S.delayed_ro =
- struct
+ end) : S with type delayed = S.delayed = struct
type delayed = S.delayed
- type delayed_ro = S.delayed_ro
-
module type Dem = sig
type runable
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index 66cd00bd7f1fd55bb14387eb483e4fd9638f5877..343cf612d3e992c5fa00b320318cd290d2ded32d 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -40,8 +40,6 @@ module Wait : sig
module type S = sig
type delayed
- type delayed_ro
-
module type Dem = sig
type runable
@@ -68,7 +66,5 @@ module Wait : sig
module Make (S : sig
type delayed
-
- type delayed_ro
- end) : S with type delayed = S.delayed and type delayed_ro = S.delayed_ro
+ end) : S with type delayed = S.delayed
end
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index dc081f0d5d8943532def276a86bba711d726e13a..67b24c3e69f5eb982511f56d6cb4cb94556fa1c0 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -117,17 +117,17 @@ val convert : ?subst:Subst.t -> Expr.Term.t -> Node.t
val apply : Expr.Term.Const.t -> Ty.t list -> Node.t IArray.t -> Term.t
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
val register_converter:
- Egraph.t -> (Egraph.t -> t -> unit) -> unit
+ Egraph.wt -> (Egraph.wt -> t -> unit) -> unit
(** register callback called for each new ground term registered *)
-val tys: Egraph.t -> Node.t -> Ty.S.t
+val tys: _ Egraph.t -> Node.t -> Ty.S.t
module Defs : sig
val add:
- Egraph.t ->
+ Egraph.wt ->
Dolmen_std.Expr.term_cst ->
Dolmen_std.Expr.ty_var list ->
Dolmen_std.Expr.term_var list -> Expr.term -> unit
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 6ccb08641f8ff8e9932025065d71a1b878512484..a9fcea355395ddb01396c388387af9a989a36871 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -96,19 +96,19 @@ module SeqLim = struct
end
module Register : sig
- val check : Egraph.t -> (Egraph.t -> Ground.t -> bool option) -> unit
+ val check : Egraph.wt -> (Egraph.rt -> Ground.t -> bool option) -> unit
val node :
- Egraph.t ->
- ((Egraph.t -> Nodes.Node.t -> Nodes.Value.t SeqLim.t) ->
- Egraph.t ->
+ Egraph.wt ->
+ ((Egraph.wt -> Nodes.Node.t -> Nodes.Value.t SeqLim.t) ->
+ Egraph.wt ->
Nodes.Node.t ->
Nodes.Value.t SeqLim.t option) ->
unit
val ty :
- Egraph.t ->
- (Egraph.t -> Ground.Ty.t -> Nodes.Value.t SeqLim.t option) ->
+ Egraph.wt ->
+ (Egraph.rt -> Ground.Ty.t -> Nodes.Value.t SeqLim.t option) ->
unit
end = struct
open Data
@@ -147,7 +147,7 @@ let ty d ty =
get_registered
(fun ty -> raise (CantInterpretTy ty))
Data.ty
- (fun f d x -> f d x)
+ (fun f d x -> f (Egraph.ro d) x)
d ty
in
spy_sequence "ty" (SeqLim.incr_depth d seq)
@@ -176,7 +176,7 @@ let node d n =
if Ground.Ty.S.is_empty (Ground.tys d n') then (
Fmt.epr "@.%a does not have type@." Node.pp n';
raise exn)
- else ty d (Ground.Ty.S.choose (Ground.tys d n'))
+ else ty (Egraph.ro d) (Ground.Ty.S.choose (Ground.tys d n'))
in
Node.H.remove parent n';
@@ -265,7 +265,7 @@ module Fix_model = struct
Egraph.set_env d Data.env (During env);
env
- let next_dec d =
+ let next_dec (d : Egraph.wt) =
match Egraph.get_env d Data.env with
| Before ->
(* The first branching is about the limit *)
@@ -284,7 +284,7 @@ module Fix_model = struct
match Sequence.next nextnode with
| None ->
Debug.dprintf0 debug "FixModel check_ground terms";
- check_ground_terms d;
+ check_ground_terms (Egraph.ro d);
Egraph.set_env d Data.env Before;
Sequence.empty
| Some (n, nextnode) -> (
@@ -339,7 +339,7 @@ module WatchArgs = struct
module Daemon = struct
type t = {
- callback : Egraph.t -> Ground.t -> unit;
+ callback : Egraph.wt -> Ground.t -> unit;
ground : Ground.t;
current : int Context.Ref.t; (** already set before *)
}
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index 3dcfe4ba32a6028fca99df1b202467ec8a2001c6..a0c7a81cda2d84548e311881b95bb5688903f5af 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -24,7 +24,7 @@ module SeqLim : sig
type 'a t
(** Sequence, finite during module fixing *)
- val of_seq : Egraph.t -> 'a Sequence.t -> 'a t
+ val of_seq : _ Egraph.t -> 'a Sequence.t -> 'a t
(** Limit the sequence to the given bound of the iterative deepening.
Sequence used for enumerating the values should be limited for ensuring
fairness. If the sequence contained more elements than limited the top
@@ -45,13 +45,13 @@ module SeqLim : sig
end
module Register : sig
- val check : Egraph.t -> (Egraph.t -> Ground.t -> bool option) -> unit
+ val check : Egraph.wt -> (Egraph.rt -> Ground.t -> bool option) -> unit
(** Check the value of the arguments corresponds to the the one of the of the term *)
val node :
- Egraph.t ->
- ((Egraph.t -> Nodes.Node.t -> Nodes.Value.t SeqLim.t) ->
- Egraph.t ->
+ Egraph.wt ->
+ ((Egraph.wt -> Nodes.Node.t -> Nodes.Value.t SeqLim.t) ->
+ Egraph.wt ->
Nodes.Node.t ->
Nodes.Value.t SeqLim.t option) ->
unit
@@ -59,30 +59,31 @@ module Register : sig
information on the domains. It could ask the computation of other nodes *)
val ty :
- Egraph.t ->
- (Egraph.t -> Ground.Ty.t -> Nodes.Value.t SeqLim.t option) ->
+ Egraph.wt ->
+ (Egraph.rt -> Ground.Ty.t -> Nodes.Value.t SeqLim.t option) ->
unit
(** Register iterators on all the possible value of some types, all the values
must be reached eventually *)
end
-val ty : Egraph.t -> Ground.Ty.t -> Nodes.Value.t SeqLim.t
+val ty : _ Egraph.t -> Ground.Ty.t -> Nodes.Value.t SeqLim.t
(** Iterate on all the possible value of the given type, usually all the values
will be reached eventually *)
-val init : Egraph.t -> unit
+val init : Egraph.wt -> unit
(** Initialize the module for later use *)
module Fix_model : sig
(** The model is search using iterative deepening depth-first search for
ensuring optimality even in presence of infinite choice *)
- val next_dec : Egraph.t -> (Egraph.t -> unit) Sequence.t
+ val next_dec : Egraph.wt -> (Egraph.wt -> unit) Sequence.t
(** Add a level of decision for fixing the model, another level could be
needed. Could raise unsatisfiable if all the model have been tried *)
end
module WatchArgs : sig
- val create : Egraph.t -> (Egraph.t -> Ground.t -> unit) -> Ground.t -> unit
+ val create :
+ Egraph.wt -> (Egraph.wt -> 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/popop_lib/exthtbl.mli b/src_colibri2/popop_lib/exthtbl.mli
index 5f3ea84a901b00e17fb2948095c65232e2895d4c..2ef0e7bbc84faaacbec9240a32a0a47b7ef03dda 100644
--- a/src_colibri2/popop_lib/exthtbl.mli
+++ b/src_colibri2/popop_lib/exthtbl.mli
@@ -27,7 +27,7 @@ val randomize : unit -> unit
the [OCAMLRUNPARAM] environment variable.
It is recommended that applications or Web frameworks that need to
- protect themselves against the denial-of-service attack described
+ prtect themselves against the denial-of-service attack described
in {!Hashtbl.create} call [Hashtbl.randomize()] at initialization
time.
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index c0bc7ec38ee45b8c993984e6eb507c789cd1439f..14911bd2900907457ed4f19cef893fab4ed139ab 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -20,7 +20,7 @@
type ctx = {
scheduler : Scheduler.t;
- mutable state: [`Sat of Egraph.t | `Unknown | `Unsat | `StepLimitReached];
+ mutable state: [`Sat of Egraph.wt | `Unknown | `Unsat | `StepLimitReached];
mutable pushpop: Scheduler.bp list;
}
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index efd423d213dfc0fbe61de48e451f2ac4d4f96835..362fc0fdb37e0760580d2817476e7a27c8e3f0a1 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -63,7 +63,7 @@ end
module Prio = Leftistheap.Make(Att)
type bp_kind =
- | Choices of (Egraph.t -> unit) Base.Sequence.t
+ | Choices of (Egraph.wt -> unit) Base.Sequence.t
| External
type bp =
@@ -285,7 +285,7 @@ and make_choice t todo todos =
* end
* | Some (Att.Decision (_,_)) | None -> () *)
-let [@inline always] protect_against_contradiction t f g =
+let [@inline always] prtect_against_contradiction t f g =
match f () with
| exception Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
@@ -298,7 +298,7 @@ let run_one_step_propagation ~nodec t =
match Context.TimeWheel.next t.daemons with
| Some att -> begin
Debug.incr stats_propa;
- protect_against_contradiction t (fun () ->
+ prtect_against_contradiction t (fun () ->
let d = Backtrackable.get_delayed t.solver_state in
Backtrackable.run_daemon d att
) (fun () -> true)
@@ -310,7 +310,7 @@ let run_one_step_propagation ~nodec t =
Debug.dprintf1 debug "[Scheduler] LastEffort mode remaining: %t"
(fun fmt -> Fmt.int fmt (Context.TimeWheel.size_at_current_time t.lasteffort));
Debug.incr stats_lasteffort;
- protect_against_contradiction t (fun () ->
+ prtect_against_contradiction t (fun () ->
let d = Backtrackable.get_delayed t.solver_state in
Backtrackable.run_daemon d att
) (fun () -> true)
@@ -326,7 +326,7 @@ let run_one_step_propagation ~nodec t =
match Context.TimeWheel.next t.lasteffort with
| Some att -> begin
Debug.incr stats_lasteffort;
- protect_against_contradiction t (fun () ->
+ prtect_against_contradiction t (fun () ->
let d = Backtrackable.get_delayed t.solver_state in
Backtrackable.run_daemon d att
) (fun () -> true)
@@ -339,13 +339,13 @@ let run_one_step_fix_model t =
match Context.Ref.get t.fixing_model with
| att::l -> begin
Context.Ref.set t.fixing_model l;
- protect_against_contradiction t (fun () ->
+ prtect_against_contradiction t (fun () ->
let d = Backtrackable.get_delayed t.solver_state in
Backtrackable.run_daemon d att
) (fun () -> true)
end
| [] ->
- protect_against_contradiction t (fun () ->
+ prtect_against_contradiction t (fun () ->
let d = Backtrackable.get_delayed t.solver_state in
Fix_model.next_dec d
) (fun seq ->
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index 272e1651bb701dbfa9e7efaf6003f79e33d93b3c..6fc9860a15000f8f043b10ac659d6c9d88a143d5 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -22,25 +22,25 @@
val run_exn:
?nodec:unit ->
?limit:int ->
- theories:(Egraph.t -> unit) list ->
- (Egraph.t -> unit) ->
- Egraph.t
+ theories:(Egraph.wt -> unit) list ->
+ (Egraph.wt -> unit) ->
+ Egraph.wt
val run:
?nodec:unit ->
?limit:int ->
- theories:(Egraph.t -> unit) list ->
- (Egraph.t -> unit) ->
+ theories:(Egraph.wt -> unit) list ->
+ (Egraph.wt -> unit) ->
[> `Contradiction
- | `Done of Egraph.t
+ | `Done of Egraph.wt
]
type t
val new_solver: unit -> t
-val init_theories: theories:(Egraph.t -> unit) list -> t -> unit
-val add_assertion: t -> (Egraph.t -> unit) -> unit
-val check_sat: ?limit:int -> t -> [> `Unsat | `Sat of Egraph.t ]
+val init_theories: theories:(Egraph.wt -> unit) list -> t -> unit
+val add_assertion: t -> (Egraph.wt -> unit) -> unit
+val check_sat: ?limit:int -> t -> [> `Unsat | `Sat of Egraph.wt ]
val get_steps: t -> int
type bp
diff --git a/src_colibri2/theories/ADT/adt.mli b/src_colibri2/theories/ADT/adt.mli
index f7e23aa700953a217073d8a4934754d03bb3af4b..c0983bff5845b328e2f2fdc7315183a7583fb821 100644
--- a/src_colibri2/theories/ADT/adt.mli
+++ b/src_colibri2/theories/ADT/adt.mli
@@ -18,4 +18,4 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val init : Egraph.t -> unit
+val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/ADT/adt_value.mli b/src_colibri2/theories/ADT/adt_value.mli
index b1c4fe28724b5bdcc3bf1b39cdd34cc402cb5604..58a5bb810c9b5b28f665e47eb0af9b6bb4128b66 100644
--- a/src_colibri2/theories/ADT/adt_value.mli
+++ b/src_colibri2/theories/ADT/adt_value.mli
@@ -40,9 +40,9 @@ type ts = { adt : MonoAdt.t; case : Case.t; fields : Value.t Field.M.t }
include Value.S with type s := ts
-val th_register : Egraph.t -> unit
+val th_register : Egraph.wt -> unit
-val propagate_value : Egraph.t -> Ground.t -> unit
+val propagate_value : Egraph.wt -> Ground.t -> unit
val sequence_of_cases :
- Egraph.t -> MonoAdt.t -> int Base.Sequence.t -> Value.t Interp.SeqLim.t
+ _ Egraph.t -> MonoAdt.t -> int Base.Sequence.t -> Value.t Interp.SeqLim.t
diff --git a/src_colibri2/theories/FP/float32.mli b/src_colibri2/theories/FP/float32.mli
index 1b971f2a86686e74d3e9c494723ba5f1f2301f19..3d9a3ffe1e876cf88dc01c56c96d5d4df1ace0ad 100644
--- a/src_colibri2/theories/FP/float32.mli
+++ b/src_colibri2/theories/FP/float32.mli
@@ -20,4 +20,4 @@
include Value.S with type s = Farith.B32.t
-val init : Egraph.t -> unit
+val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/FP/float64.mli b/src_colibri2/theories/FP/float64.mli
index f17a8c646a6493ec41fddf1b06016a1b392337de..908b52f61c02a6f79cab51f3bae8fa5156861146 100644
--- a/src_colibri2/theories/FP/float64.mli
+++ b/src_colibri2/theories/FP/float64.mli
@@ -20,4 +20,4 @@
include Value.S with type s = Farith.B64.t
-val init : Egraph.t -> unit
+val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/FP/fp.mli b/src_colibri2/theories/FP/fp.mli
index 839b244b8854e130c7fc4aa3f91a5aaeda9b285a..153fcd6c556be453e675af48595542a1e5fa6d3c 100644
--- a/src_colibri2/theories/FP/fp.mli
+++ b/src_colibri2/theories/FP/fp.mli
@@ -21,5 +21,5 @@
(** FloatingPoint theory as described in SMT-LIB 2 *)
(** Register the theory *)
-val th_register : Egraph.t -> unit
+val th_register : Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli
index a958f427e919cd7c9f193f51e9e888386053c1ec..35f2008aef8efa725ec15e01383d11bdb61ac24e 100644
--- a/src_colibri2/theories/LRA/LRA.mli
+++ b/src_colibri2/theories/LRA/LRA.mli
@@ -27,7 +27,7 @@ module RealValue : sig
end
-val th_register: Egraph.t -> unit
+val th_register: Egraph.wt -> unit
(** helpers to remove *)
diff --git a/src_colibri2/theories/LRA/delta.mli b/src_colibri2/theories/LRA/delta.mli
index 2c3be78f843f3f177336cba990f31766d520e0d3..b54fef6b21f8b05b415ad95ed21d4314b748cac5 100644
--- a/src_colibri2/theories/LRA/delta.mli
+++ b/src_colibri2/theories/LRA/delta.mli
@@ -21,20 +21,20 @@
(** Distance Graph *)
-val add_le: Egraph.t -> Node.t -> Q.t -> Node.t -> unit
+val add_le: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
(* [add_le d n1 q n2] n1 - n2 <= q *)
-val add_lt: Egraph.t -> Node.t -> Q.t -> Node.t -> unit
+val add_lt: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
(* [add_lt d n1 q n2] n1 - n2 < q *)
-val add_ge: Egraph.t -> Node.t -> Q.t -> Node.t -> unit
+val add_ge: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
(* [add_ge d n1 q n2] n1 - n2 >= q *)
-val add_gt: Egraph.t -> Node.t -> Q.t -> Node.t -> unit
+val add_gt: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
(* [add_gt d n1 q n2] n1 - n2 > q *)
-val add: Egraph.t -> Node.t -> Q.t -> Colibri2_theories_LRA_stages_def.Bound.t -> Node.t -> unit
+val add: Egraph.wt -> Node.t -> Q.t -> Colibri2_theories_LRA_stages_def.Bound.t -> Node.t -> unit
(* [add d n1 q bound n2] n1 - n2 <= q or < q *)
-val th_register: Egraph.t -> unit
+val th_register: Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
index 2e5d10ea80a5457dbf9502836ead12b1ffd5d3b9..4a7f75404698ceb723de8b98028a1fcce513e116 100644
--- a/src_colibri2/theories/LRA/dom_interval.mli
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -18,14 +18,14 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
module D: sig type t end
val dom : D.t Dom.Kind.t
-val is_zero_or_positive: Egraph.t -> Node.t -> bool
-val is_not_zero: Egraph.t -> Node.t -> bool
-val is_strictly_positive: Egraph.t -> Node.t -> bool
-val is_strictly_negative: Egraph.t -> Node.t -> bool
-val is_integer: Egraph.t -> Node.t -> bool
+val is_zero_or_positive: _ Egraph.t -> Node.t -> bool
+val is_not_zero: _ Egraph.t -> Node.t -> bool
+val is_strictly_positive: _ Egraph.t -> Node.t -> bool
+val is_strictly_negative: _ Egraph.t -> Node.t -> bool
+val is_integer: _ Egraph.t -> Node.t -> bool
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index bfd1d86e7f17969c659bb2002a5787b28b59a393..ef3a5d7b07be91f7b2dd8afbc9f027b1f9a6804a 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -18,12 +18,12 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val assume_poly_equality: Egraph.t -> Node.t -> Polynome.t -> unit
+val assume_poly_equality: Egraph.wt -> Node.t -> Polynome.t -> unit
val dom: Polynome.t Dom.Kind.t
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
val node_of_polynome: Polynome.t -> Node.t
-val norm: Egraph.t -> Polynome.t -> Polynome.t
+val norm: _ Egraph.t -> Polynome.t -> Polynome.t
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 5d10dbc5e6b4b4c0c0e0982830b2d000096d9bfd..26325d9fcd69ffd355807f0f3c2e70c0299052aa 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -313,7 +313,7 @@ module ChangePos = struct
let init d =
Events.attach_any_dom d Dom_interval.dom
(fun d n ->
- match Node.HC.Ro.find_opt used_in_poly d n with
+ match Node.HC.find_opt used_in_poly d n with
| Some ns -> Events.EnqRun (key,ns)
| None -> Events.EnqAlready)
diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli
index df6be3b0c6d4cd7d167152be31ad4781f305d586..ab1a2f86d7ca0b07ee2effd430ec40604bef6f32 100644
--- a/src_colibri2/theories/LRA/dom_product.mli
+++ b/src_colibri2/theories/LRA/dom_product.mli
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val assume_poly_equality: Egraph.t -> Node.t -> Product.t -> unit
+val assume_poly_equality: Egraph.wt -> Node.t -> Product.t -> unit
val node_of_product: Product.t -> Node.t
@@ -26,6 +26,6 @@ type t
val dom: t Dom.Kind.t
-val get_repr: Egraph.t -> Node.t -> Product.t option
+val get_repr: _ Egraph.t -> Node.t -> Product.t option
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index ebb907c57dbbf052e45a96e229f32c002251dd45..00b87b0305888e55228126f72a0b3ebbaea9da69 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -178,7 +178,7 @@ let make_equations d (eqs,vars) g =
Node.M.union_merge (fun _ _ _ -> Some ()) vars p'.Polynome.poly)
| None -> eqs, vars
-let fm (d:Egraph.t) =
+let fm (d:Egraph.wt) =
Debug.dprintf0 debug "[Fourier]";
Debug.incr stats_run;
Datastructure.Ref.set scheduled d false;
@@ -228,10 +228,10 @@ module Daemon = struct
end )
let enqueue d _ =
- if Datastructure.Ref.Ro.get scheduled d
+ if Datastructure.Ref.get scheduled d
then Events.EnqAlready
else begin
- Datastructure.Ref.Ro.set scheduled d true;
+ Datastructure.Ref.set scheduled d true;
Events.EnqRun (key,())
end
diff --git a/src_colibri2/theories/LRA/fourier.mli b/src_colibri2/theories/LRA/fourier.mli
index 13235f23e5aa83b2c72176f55a447150e456da14..18263c3ca59548bfcb1f8e96383d27b778286fa7 100644
--- a/src_colibri2/theories/LRA/fourier.mli
+++ b/src_colibri2/theories/LRA/fourier.mli
@@ -18,4 +18,4 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/mul.mli b/src_colibri2/theories/LRA/mul.mli
index 13235f23e5aa83b2c72176f55a447150e456da14..18263c3ca59548bfcb1f8e96383d27b778286fa7 100644
--- a/src_colibri2/theories/LRA/mul.mli
+++ b/src_colibri2/theories/LRA/mul.mli
@@ -18,4 +18,4 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 0dc4824cb0edf385ad5ffe7355875d3e03e89b8e..bf72dac0e0133877e5cb29ce40e9abbeb33dcaae 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -25,4 +25,4 @@ val cst: Q.t -> Node.t
val zero: Node.t
-val init: Egraph.t -> unit
+val init: Egraph.wt -> unit
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index ef869aaf58bedd9383e077ed9620a60544228a03..3ffa57185cfcbc8797849e545fb10705d4ef545e 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -131,7 +131,7 @@ module TwoWatchLiteral = struct
from_end : int Context.Ref.t; (** already set after *)
}
- type runable = (Egraph.t -> unit)
+ type runable = (Egraph.wt -> unit)
let print_runable = Fmt.nop
@@ -151,7 +151,7 @@ module TwoWatchLiteral = struct
| ToWatch of int
let rec check_if_set d args absorbent incr stop i =
- match Egraph.Ro.get_value d (IArray.get args i) with
+ match Egraph.get_value d (IArray.get args i) with
| None -> ToWatch i
| Some b when Value.equal b absorbent ->
Absorbent
@@ -164,7 +164,7 @@ module TwoWatchLiteral = struct
match check_if_set d args absorbent incr stop i with
| LimitReached | Absorbent as r -> r
| ToWatch i as r ->
- if not (Egraph.Ro.is_equal d n (IArray.get args i)) then r
+ if not (Egraph.is_equal d n (IArray.get args i)) then r
else
let i = incr + i in
if i = stop then LimitReached else
@@ -172,10 +172,10 @@ module TwoWatchLiteral = struct
let run d r = r d
- let rec attach d r i =
- Events.Ro.attach_value d
+ let rec attach : type a. a Egraph.t -> _ = fun d r i ->
+ Events.attach_value d
(IArray.get (Ground.sem r.ground).args i) BoolValue.key (fun d _ _ -> enqueue d r);
- Events.Ro.attach_repr d (IArray.get (Ground.sem r.ground).args i) (fun d _ -> enqueue d r);
+ Events.attach_repr d (IArray.get (Ground.sem r.ground).args i) (fun d _ -> enqueue d r);
and enqueue d r =
let o_from_start = Context.Ref.get r.from_start in
@@ -183,7 +183,7 @@ module TwoWatchLiteral = struct
let args = (Ground.sem r.ground).args in
if o_from_start = o_from_end then Events.EnqStopped
else
- match Egraph.Ro.get_value d (Ground.node r.ground) with
+ match Egraph.get_value d (Ground.node r.ground) with
| Some v when not (Value.equal v r.absorbent) ->
Context.Ref.set r.from_end o_from_start;
Events.EnqLast(key,fun d -> IArray.iter ~f:(fun a -> Egraph.set_value d a v) args)
@@ -235,7 +235,7 @@ module TwoWatchLiteral = struct
from_end = Context.Ref.create (Egraph.context d) from_end;
}
in
- match check_if_set (d :> Egraph.Ro.t) args absorbent 1 (IArray.length args - 1) 0 with
+ match check_if_set d args absorbent 1 (IArray.length args - 1) 0 with
| LimitReached ->
Egraph.merge d (IArray.get args (IArray.length args - 1)) (Ground.node ground)
| Absorbent ->
@@ -243,7 +243,7 @@ module TwoWatchLiteral = struct
| ToWatch from_start ->
let n_start = IArray.get args from_start in
match
- check_if_equal_or_set (d :> Egraph.Ro.t) args absorbent (-1) from_start (IArray.length args - 1) n_start
+ check_if_equal_or_set d args absorbent (-1) from_start (IArray.length args - 1) n_start
with
| LimitReached ->
Egraph.merge d n_start (Ground.node ground)
@@ -251,8 +251,8 @@ module TwoWatchLiteral = struct
Egraph.set_value d (Ground.node ground) absorbent
| ToWatch from_end ->
let r = r from_start from_end in
- attach (d :> Egraph.Ro.t) r from_start;
- attach (d :> Egraph.Ro.t) r from_end
+ attach d r from_start;
+ attach d r from_end
end
let () = Events.register (module Daemon)
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index defd19ec0194808af665bf565da95d4baf49b747..f34fa775fe66351b832a81e91c42719e2837131d 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -24,19 +24,19 @@ val _and : Node.t list -> Node.t
val _or : Node.t list -> Node.t
val _not : Node.t -> Node.t
-val set_true : Egraph.t -> Node.t -> unit
-val set_false : Egraph.t -> Node.t -> unit
+val set_true : Egraph.wt -> Node.t -> unit
+val set_false : Egraph.wt -> Node.t -> unit
-val is : Egraph.t -> Node.t -> bool option
-val is_true : Egraph.t -> Node.t -> bool
-val is_false : Egraph.t -> Node.t -> bool
+val is : _ Egraph.t -> Node.t -> bool option
+val is_true : _ Egraph.t -> Node.t -> bool
+val is_false : _ Egraph.t -> Node.t -> bool
(** is_true t node = false means the value is not constrained by the
current constraints or due to incompletness *)
-val is_unknown : Egraph.t -> Node.t -> bool
+val is_unknown : _ Egraph.t -> Node.t -> bool
(* val true_is_false : Egraph.d -> Node.t -> Trail.Pexp.t -> 'a *)
-val th_register: Egraph.t -> unit
+val th_register: Egraph.wt -> unit
val chobool: Node.t -> Choice.t
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index b8a6cf32c9a39c40e362eb1e7e8a3f527918e001..b6977b71b764ee0ff562c17c75224d6aeffde1cf 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -403,7 +403,7 @@ let simplify d own cond then_ else_ =
let delay = Events.Delayed_by 1
-let throttle = 100
+let thrttle = 100
let new_ite d own cond then_ else_ =
Daemon.attach_value d cond Boolean.dom (fun d _ v ->
@@ -414,7 +414,8 @@ let new_ite d own cond then_ else_ =
(** If can't be a value it they share a diff tag, are different *)
(** Give for a node the values that are different *)
-let iter_on_value_different ~they_are_different (d : Egraph.t) (own : Node.t) =
+let iter_on_value_different ~they_are_different (d : _ Egraph.t) (own : Node.t)
+ =
let dis = Opt.get_def Dis.empty (Egraph.get_dom d dom own) in
let iter elt =
let iter n =
@@ -430,7 +431,7 @@ let iter_on_value_different ~they_are_different (d : Egraph.t) (own : Node.t) =
(** Give for a value the nodes that are different *)
let init_diff_to_value (type a b) ?(already_registered = ([] : b list)) d0
(module Val : Colibri2_core.Value.S with type s = a and type t = b)
- ~(they_are_different : Egraph.t -> Node.t -> a -> unit) =
+ ~(they_are_different : _ Egraph.t -> Node.t -> a -> unit) =
let propagate_diff d v =
let own = Val.node v in
let dis = Opt.get_def Dis.empty (Egraph.get_dom d dom own) in
diff --git a/src_colibri2/theories/bool/equality.mli b/src_colibri2/theories/bool/equality.mli
index eff0913697bde1c0211595f0b244cdeb3267132d..22cbbe59d6f8db75b69e19f77f99078033c3451e 100644
--- a/src_colibri2/theories/bool/equality.mli
+++ b/src_colibri2/theories/bool/equality.mli
@@ -22,11 +22,11 @@ val equality : Node.t list -> Node.t
val disequality : Node.t list -> Node.t
-val is_equal : Egraph.t -> Node.t -> Node.t -> bool
+val is_equal : _ Egraph.t -> Node.t -> Node.t -> bool
-val is_disequal : Egraph.t -> Node.t -> Node.t -> bool
+val is_disequal : _ Egraph.t -> Node.t -> Node.t -> bool
val iter_on_value_different :
- they_are_different:(Node.t -> Value.t -> unit) -> Egraph.t -> Node.t -> unit
+ they_are_different:(Node.t -> Value.t -> unit) -> Egraph.wt -> Node.t -> unit
-val th_register : Egraph.t -> unit
+val th_register : Egraph.wt -> unit
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index 47c93d5e44ed7cf3a6107fd4b20b65c2deae3b6b..687935c730f2fb11fc7be6a21329177c8ee4e37d 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -26,7 +26,7 @@ type t
val pp : t Fmt.t
val exec :
- Egraph.t ->
+ _ Egraph.t ->
Ground.Subst.S.t Trigger.M.t ->
Ground.Subst.S.t ->
Node.t ->
@@ -35,7 +35,7 @@ val exec :
(** [exec d acc substs n ip] adds to [acc] new substitutions to the triggers
that are obtained by the execution of the invertedpath *)
-val insert_pattern : Egraph.t -> Trigger.t -> unit
+val insert_pattern : _ Egraph.t -> Trigger.t -> unit
(** [insert_pattern d tri] insert the pattern in the database of inverted path
for all its subterms *)
diff --git a/src_colibri2/theories/quantifier/info.mli b/src_colibri2/theories/quantifier/info.mli
index a4c3229f1cd22860aaff7c019534e552eadf328b..11725caba5024391255a93a920a9557c8feded90 100644
--- a/src_colibri2/theories/quantifier/info.mli
+++ b/src_colibri2/theories/quantifier/info.mli
@@ -24,7 +24,7 @@ type t = {
}
[@@deriving show]
-val merge : Egraph.t -> other:Node.t -> repr:Node.t -> t -> t -> t
+val merge : Egraph.wt -> other:Node.t -> repr:Node.t -> t -> t -> t
(** merge the information and apply congruence closure on the parents *)
val empty : t
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index f96c4a5bcae0eba896c631c540bf3e21da005b4c..a71c4405a0b8a5746e8a310245dd24d4443f813f 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -40,7 +40,8 @@ val match_ty : Ground.Subst.S.t -> Ground.Ty.t -> Expr.Ty.t -> Ground.Subst.S.t
(** [match_ty substs ty pat] match the [ty] on [pat] for each substitution of
[substs] *)
-val match_term : Egraph.t -> Ground.Subst.S.t -> Node.t -> t -> Ground.Subst.S.t
+val match_term :
+ _ Egraph.t -> Ground.Subst.S.t -> Node.t -> t -> Ground.Subst.S.t
(** [match_term d substs n pat] match the node [n] on the pattern [pat] for each
substitution. Each return substitution corresponds to one given as input. *)
@@ -48,15 +49,15 @@ val check_ty : Ground.Subst.t -> Ground.Ty.t -> Expr.Ty.t -> bool
(** [check_ty subst ty pat] checks that the pattern [pat] substituted by [subst]
is equal to ty *)
-val check_term : Egraph.t -> Ground.Subst.t -> Node.t -> t -> bool
+val check_term : _ Egraph.t -> Ground.Subst.t -> Node.t -> t -> bool
(** [check_term d subst n pat] checks the pattern [pat] subsituted by [subst] is
equal by congruence of [d] to [n] *)
-val check_term_exists : Egraph.t -> Ground.Subst.t -> t -> Node.S.t
+val check_term_exists : _ Egraph.t -> Ground.Subst.t -> t -> Node.S.t
(** [check_term_exists d subst pat] return nodes that are equal to the pattern
[pat] substituted by the substitution [subst] *)
-val match_any_term : Egraph.t -> Ground.Subst.S.t -> t -> Ground.Subst.S.t
+val match_any_term : _ Egraph.t -> Ground.Subst.S.t -> t -> Ground.Subst.S.t
(** [match_any_term d subst pat] match the pattern [pat] to all the nodes of [d]
for each substitution. Each return substitution corresponds to one given as
input. *)
diff --git a/src_colibri2/theories/quantifier/quantifier.mli b/src_colibri2/theories/quantifier/quantifier.mli
index 164992ff9d314b8f5fddd6a1590b44eda2fea37a..ea1e233032147771b03480dede93c545ff84a82a 100644
--- a/src_colibri2/theories/quantifier/quantifier.mli
+++ b/src_colibri2/theories/quantifier/quantifier.mli
@@ -18,4 +18,4 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val th_register : Egraph.t -> unit
+val th_register : Egraph.wt -> unit
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index df743fb5950685d87965e55fc4f8707dc22edfb8..e0f388774b8ba321a6f11e5196d15d0b553e4380 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -48,10 +48,10 @@ val env_vars : t Datastructure.Push.t
val env_tri_by_apps : t Context.Push.t F.EnvApps.t
(** Triggers sorted by their top symbol *)
-val add_trigger : Egraph.t -> t -> unit
+val add_trigger : Egraph.wt -> t -> unit
(** Register a new trigger *)
-val instantiate : Egraph.t -> t -> Ground.Subst.t -> unit
+val instantiate : Egraph.wt -> t -> Ground.Subst.t -> unit
(** [instantiate d tri subst] instantiates the trigger [tri] with the
substitution [subst]:
@@ -61,6 +61,6 @@ val instantiate : Egraph.t -> t -> Ground.Subst.t -> unit
* at last effort otherwise
*)
-val match_ : Egraph.t -> t -> Node.t -> unit
+val match_ : Egraph.wt -> t -> Node.t -> unit
(** [match_ d tri n] match the pattern of [tri] with [n] and instantiate [tri]
with the resulting substitutions *)
diff --git a/src_colibri2/theories/quantifier/uninterp.mli b/src_colibri2/theories/quantifier/uninterp.mli
index f3a82959478d744b5ebece6c54e7e623ca228b1d..7ec90c489c41fb259f57e5511896f1b04f4f8c0b 100644
--- a/src_colibri2/theories/quantifier/uninterp.mli
+++ b/src_colibri2/theories/quantifier/uninterp.mli
@@ -49,12 +49,12 @@ open Colibri2_core
(* val app_fun: Node.t -> Node.t list -> Node.t *)
-val th_register : Egraph.t -> unit
+val th_register : Egraph.wt -> unit
module On_uninterpreted_domain : sig
(** For model fixing *)
- val propagate : Egraph.t -> Ground.t -> unit
+ val propagate : Egraph.wt -> Ground.t -> unit
- val check : Egraph.t -> Ground.t -> bool
+ val check : Egraph.rt -> Ground.t -> bool
end