diff --git a/Makefile b/Makefile index 611e9da846d69cd4e2687f4d630dd1ae75b25b2e..7a24a046b39cbf6e38d3ef85a034304aecdaf8dc 100644 --- a/Makefile +++ b/Makefile @@ -36,6 +36,9 @@ replay: ide: why3 ide -L src/lib src/lib/cp.mlw +doc: + dune build @doc --root=$$(pwd) + WITH_HEADER_FILES=cp.mlw queens.mlw cp.ml cp.mli DISTRIB_FILES=$(WITH_HEADER_FILES) Makefile dune dune-project cp.opam cp.drv Readme.md \ $(addprefix src/, why3session.xml why3shapes.gz) \ @@ -63,11 +66,6 @@ replay-distrib: distrib headers_colibrics: headache -h CEA_PROPRIETARY -c headache.config $(WITH_HEADER_FILES) -doc: Readme.pdf - -Readme.pdf: Readme.md - pandoc $< --pdf-engine=xelatex --output $@ - test-examples: dune runtest --root=$$(pwd) diff --git a/src_colibri2/core/.ocamlformat-ignore b/src_colibri2/core/.ocamlformat-ignore index 19b3d4c703fef076d4acc0794f90c4245c53aafe..2a3c74d09747f587571bedc1dc8a8eac7cb66849 100644 --- a/src_colibri2/core/.ocamlformat-ignore +++ b/src_colibri2/core/.ocamlformat-ignore @@ -1,24 +1,16 @@ env.ml -events.ml theory.ml structures -structures/nodes.mli structures/term.ml structures/domKind.ml structures/dune structures/domKind.mli structures/expr.ml -structures/nodes.ml -structures/.merlin datastructure.mli -colibri2_core.ml -demon.mli env.mli ground.mli dune datastructure.ml egraph.ml egraph.mli -events.mli -demon.ml ground.ml diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml index f4b1d10b39f53367d031381f1eeb2558f19de618..f6850b4e8d55e38ecc59be8961f2e0b09099d464 100644 --- a/src_colibri2/core/colibri2_core.ml +++ b/src_colibri2/core/colibri2_core.ml @@ -20,74 +20,355 @@ (** Colibri2 core: define basic types and the solver *) +(** {3 Egraph } *) + +(** The Egraph contains all the context of a state of the analysis. Moreover it + handles: + - the consolidation of the unique domain for each equivalence class + - registering on which events daemons are waiting +*) + +module Egraph = Egraph + +(** {3 Ground terms} *) + +(** The main constraints are the ground terms. Each ground terms is associated + to a node in the Egraph. The terms are simplified from the input syntax by + substituting let bindings and separate the other bindings: + + - {!Ground.Term.t} for the total application of a known symbol {!Builtin.t} + - {!Ground.ClosedQuantifier.t} for close quantified formula + - {!Ground.NotTotalyApplied.t} for partial applications and anonymous + lambdas + + This separation allows to consider most of the time only {!Ground.Term.t} terms. + +*) + +module Ground = Ground + +module Builtin = Dolmen_std.Builtin +(** All the symbols predefined in the + language are defined in the {!Builtin} modules. For example {!Builtin.And} + for the conjunction. + +*) + module Expr = Expr -module Term = Expr.Term -module Ty = Expr.Ty +(** The module {!Expr} corresponds to the typed expression + parsed and typed by Dolmen. It is generally not useful. *) + +(** {3 Different Object } *) + +(** The different kind of terms are reunited as {!Node.t} by being indexed into + theory terms {!ThTerm.t}. Predefined theory terms are: -module Keys = Keys + - the theory term of {!Ground.Term.t} is {!Ground.t}; - for + {!Ground.ClosedQuantifier.t} is {!Ground.ThClosedQuantifier.t} - for + {!Ground.NotTotalyApplied.t} is {!Ground.ThNotTotalyApplied.t} + + The theory terms can be transformed without cost directly as {!Node.t}. New + kind of theory terms are obtained by applying the functor {!ThTerm.Register} + + *) module Node = struct include Nodes.Node module HC = Datastructure.HNode end -module ThTermKind = struct - include Nodes.ThTermKind - let print = Nodes.print_thterm +module ThTerm = struct + module Kind : Keys.Key2 with type ('a, 'b) t = ('a, 'b) Nodes.ThTermKind.t = + Nodes.ThTermKind + (** Unique keys associated to each kind + of ThTerm *) + + module type S = Nodes.RegisteredThTerm - module type ThTerm = Nodes.ThTerm - module type Registered = Nodes.RegisteredThTerm + module Register (T : Colibri2_popop_lib.Popop_stdlib.NamedDatatype) : + S with type s = T.t = + Nodes.RegisterThTerm (T) - module Register = Nodes.RegisterThTerm + (** {3 Generic value which unit all the theory terms } *) + + include Nodes.ThTerm end -module ThTerm = Nodes.ThTerm +(** Another kind of nodes are values. They are disjoint but similar to theory + terms. The goal of the solver is to find one {!Value.t} for each expression + of the input problem. They are registered using {!Value.Register}. *) -module Ground = Ground +module Value = struct + module Kind : Keys.Key2 with type ('a, 'b) t = ('a, 'b) Nodes.ValueKind.t = + Nodes.ValueKind -module ValueKind = struct - include Nodes.ValueKind - let print = Nodes.print_value + module type S = Nodes.RegisteredValue - module type Value = Nodes.Value - module type Registered = Nodes.RegisteredValue + module Register (T : Colibri2_popop_lib.Popop_stdlib.NamedDatatype) : + S with type s = T.t = + Nodes.RegisterValue (T) - module Register = Nodes.RegisterValue + (** {3 Generic value which unit all the values } *) - let get = Nodes.get_value - let get_registered = Nodes.get_registered_value + include Nodes.Value end -module Value = Nodes.Value +(** Domains are additional informations associated to each equivalence class + inside the {!Egraph.t}. They can be registered using {!Dom.register} or + {!Dom.register_lattice} when the domain is simple *) -module Interp = Interp +module Dom = struct + module Kind : Keys.Key with type 'a t = 'a DomKind.t = DomKind -module DomKind = struct - include DomKind - let print = Egraph.print_dom + module type S = sig + type t - module type Dom = Egraph.Dom + val merged : t option -> t option -> bool + (** [merged d1 d2] indicates if + the [d1] and [d2] are the same and doesn't need to be merged *) - let register = Egraph.register_dom -end + val merge : + Egraph.t -> 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 + representative *) + + val pp : Format.formatter -> t -> unit + + val key : t Kind.t + end + + let register (s : (module S)) = + let module S = (val s) in + Egraph.register_dom (module S) + + module type Lattice = sig + type t + + val equal : t -> t -> bool + + val pp : Format.formatter -> t -> unit + + val key : t Kind.t + + val inter : t -> t -> t option + (** [inter d1 d2] compute the intersection of + [d1] and [d2] return [None] if it is empty *) -module Dem = struct - include Events.Dem + val is_singleton : t -> Value.t option + (** [is_singleton d] if [d] is + restricted to a singleton return the corresponding value *) + end - module type Dem = Egraph.Wait.Dem + (** [lattice l] register a domain as a lattice. It returns a function for + setting the domain which will the value instead in case of singleton *) + let lattice : + type a. + (module Lattice with type t = a) -> Egraph.t -> Node.t -> a -> unit = + fun l -> + let module L = (val l) in + let module S = struct + type t = L.t - let register = Egraph.Wait.register_dem + let pp = L.pp + + let key = L.key + + let set_dom d node v = + Egraph.set_dom d L.key node v; + match L.is_singleton v with + | Some cst -> Egraph.set_value d node cst + | None -> () + + let merged i1 i2 = + match (i1, i2) with + | None, None -> true + | Some i1, Some i2 -> L.equal i1 i2 + | _ -> false + + let merge d (i1, cl1) (i2, cl2) _ = + assert (not (Egraph.is_equal d cl1 cl2)); + match (i1, cl1, i2, cl2) with + | Some i1, _, Some i2, _ -> ( + match L.inter i1 i2 with + | None -> + Colibri2_popop_lib.Debug.dprintf10 Egraph.print_contradiction + "%a The intersection of %a and %a is empty when\n\ + \ merging %a and %a" Kind.pp L.key L.pp i1 L.pp i2 Node.pp cl1 + Node.pp cl2; + Egraph.contradiction d + | Some i -> + if not (L.equal i i1) then set_dom d cl1 i; + if not (L.equal i i2) then set_dom d cl2 i) + | Some i1, _, _, cl2 | _, cl2, Some i1, _ -> set_dom d cl2 i1 + | None, _, None, _ -> raise Impossible + end in + register (module S); + S.set_dom end -module Env = Env +(** {3 Fix the models} *) -module Egraph = Egraph +(** 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 -module Events = Events -module Demon = Demon +(** {3 Custom Environment } *) + +module Env = Env +(** Environment *) module Datastructure = Datastructure +(** {3 Events } *) + +(** + The modification of the Egraph (events) can be monitored through daemons. + *) + +module Daemon = Demon.Simple +module DaemonWithFilter = Demon.WithFilter +module DaemonWithKey = Demon.Key + +module Events = struct + (** 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 *) + | LastEffort of int + (** Should try to ensure that a model exists, must be strictly positive *) + | FixingModel + + type enqueue = Events.enqueue = + | EnqRun : 'r Dem.t * 'r -> enqueue (** Schedule a daemon run *) + | EnqLast : 'r Dem.t * 'r -> enqueue + (** Same as EnqRun but remove the waiting event *) + | EnqAlready : enqueue (** Don't run but keep the waiting event *) + | EnqStopped : enqueue (** Stop and don't run *) + + type daemon_key = Events.Wait.daemon_key = + | DaemonKey : 'runable Dem.t * 'runable -> daemon_key + + (** Basic daemons *) + module Basic = struct + module type T = Egraph.Wait.Dem + + let register (s : (module T)) = + let module S = (val s) in + Egraph.Wait.register_dem (module S) + end + + (** {3 Attach daemons } *) + + (** wakeup when the dom of the node change *) + let attach_dom : + Egraph.t -> + ?direct:bool -> + Node.t -> + 'a DomKind.t -> + (Egraph.Ro.t -> Node.t -> enqueue) -> + unit = + Egraph.attach_dom + + (** wakeup when the dom of any node change *) + let attach_any_dom : + Egraph.t -> 'a DomKind.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit = + Egraph.attach_any_dom + + (** wakeup when a value is attached to this equivalence class *) + let attach_value : + Egraph.t -> + Node.t -> + ('a, 'b) Value.Kind.t -> + (Egraph.Ro.t -> Node.t -> 'b -> enqueue) -> + unit = + Egraph.attach_value + + (** wakeup when any kind of value is attached to this equivalence class *) + let attach_any_value : + Egraph.t -> + Node.t -> + (Egraph.Ro.t -> Node.t -> Value.t -> enqueue) -> + unit = + Egraph.attach_any_value + + (** wakeup when any node is registered *) + let attach_reg_any : Egraph.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit = + Egraph.attach_reg_any + + (** wakeup when this node is registered *) + let attach_reg_node : + Egraph.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit = + Egraph.attach_reg_node + + (** wakeup when a new semantical class is registered *) + let attach_reg_sem : + Egraph.t -> + ('a, 'b) ThTerm.Kind.t -> + (Egraph.Ro.t -> 'b -> enqueue) -> + unit = + Egraph.attach_reg_sem + + (** wakeup when a new value is registered *) + let attach_reg_value : + Egraph.t -> + ('a, 'b) Value.Kind.t -> + (Egraph.Ro.t -> 'b -> enqueue) -> + unit = + Egraph.attach_reg_value + + (** wakeup when it is not anymore the representative class *) + let attach_repr : + Egraph.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit = + Egraph.attach_repr + + (** wakeup when a node is not its representative class anymore *) + let attach_any_repr : Egraph.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit = + Egraph.attach_any_repr +end + +(** {3 Helpers } *) + +module Init = struct + let add_default_theory = Egraph.add_default_theory +end + +module Debug = struct + include Colibri2_popop_lib.Debug + + let decision = Egraph.print_decision + + let contradiction = Egraph.print_contradiction +end + exception UnwaitedEvent = Nodes.UnwaitedEvent -(** Can be raised by daemon when receiving an event that they don't - waited for. It is the sign of a bug in the core solver *) +(** Can be raised by daemon when + receiving an event that they don't waited for. It is the sign of a bug in the + core solver *) + +(** {3 For schedulers} *) + +(** The following functions are necessary only to the scheduler *) + +module ForSchedulers = struct + module Backtrackable = Egraph.Backtrackable + + let default_theories = Egraph.default_theories +end + +module Demon = Demon diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml index 065b5fe71a0b443d664cfaa3708db3afc759a491..685c9764724b00ab9a1c7b0f1900c4aa97bd49e9 100644 --- a/src_colibri2/core/datastructure.ml +++ b/src_colibri2/core/datastructure.ml @@ -46,7 +46,7 @@ module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key : type t = a option Context.Ref.t S.H.t let name = name end in - let key = Env.Unsaved.create_key (module M) in + let key = Env.Unsaved.create (module M) in let init _ = S.H.create 5 in let iter f = S.H.iter (fun k r -> match Context.Ref.get r with None -> () | Some v -> f k v) in let pp = Colibri2_popop_lib.Pp.(iter2 iter semi arrow S.pp pp) in @@ -121,6 +121,13 @@ module type Sig2 = sig 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 + end module Hashtbl2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key := S.t = struct @@ -137,7 +144,7 @@ module Hashtbl2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key type t = a t' let name = name end in - let key = Env.Unsaved.create_key (module M) in + let key = Env.Unsaved.create (module M) in let init _ = { h = S.H.create 5; def } in let iter f h = S.H.iter (fun k r -> f k (Context.Ref.get r)) h.h in let pp = Colibri2_popop_lib.Pp.(iter2 iter semi arrow S.pp pp) in @@ -165,6 +172,30 @@ module Hashtbl2(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key 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 @@ -191,7 +222,7 @@ module Memo(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key := type t = a t' let name = name end in - let key = Env.Unsaved.create_key (module M) in + let key = Env.Unsaved.create (module M) in let init _ = { h = S.H.create 5; def } in let iter f h = S.H.iter (fun k r -> f k r) h.h in let pp = Colibri2_popop_lib.Pp.(iter2 iter semi arrow S.pp pp) in @@ -227,7 +258,7 @@ module Push = struct type t = a Context.Push.t let name = name end in - let key = Env.Unsaved.create_key (module M) in + let key = Env.Unsaved.create (module M) in let init = Context.Push.create in let pp = Colibri2_popop_lib.Pp.(iter1 Context.Push.iter semi pp) in Env.Unsaved.register ~init ~pp key; @@ -256,7 +287,7 @@ module Ref = struct type t = a Context.Ref.t let name = name end in - let key = Env.Unsaved.create_key (module M) in + let key = Env.Unsaved.create (module M) in let init d = Context.Ref.create d v in let pp = Context.Ref.pp pp in Env.Unsaved.register ~init ~pp key; diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli index bcbbd8eeeeb250b3d77491447ba3c2d8060b5a6d..d64124ca02a8712dc1d415773256b83031278562 100644 --- a/src_colibri2/core/datastructure.mli +++ b/src_colibri2/core/datastructure.mli @@ -52,6 +52,12 @@ module type Sig2 = sig 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 end module Hashtbl2 (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig2 with type key := S.t diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml index 6b04a20947f0ef81b68b1cd8082a7346f2de381e..f01dfb1c49d0bb47d02cf350ccc93dbf14f0e023 100644 --- a/src_colibri2/core/demon.ml +++ b/src_colibri2/core/demon.ml @@ -18,710 +18,260 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -open Colibri2_popop_lib open Nodes -let debug = Debug.register_info_flag - ~desc:"for the specialized demons" - "Demon.all" - - -module Create = struct - type 'b event = - | EventDom : Node.t * 'a DomKind.t * 'b -> 'b event - | EventAnyDom : 'a DomKind.t * 'b -> 'b event - | EventValue : Node.t * 'a ValueKind.t * 'b -> 'b event - | EventAnyValue : Node.t * 'b -> 'b event - | EventRegAny : 'b -> 'b event - | EventRegCl : Node.t * 'b -> 'b event - | EventChange : Node.t * 'b -> 'b event - | EventChangeAny: 'b -> 'b event - | EventRegSem : 'a ThTermKind.t * 'b -> 'b event - | EventRegValue : 'a ValueKind.t * 'b -> 'b event - - - let pp fmt = function - | EventDom (node, dom, _) -> - Format.fprintf fmt "dom:%a of %a" DomKind.pp dom Node.pp node - | EventAnyDom (dom, _) -> - Format.fprintf fmt "dom:%a any" DomKind.pp dom - | EventValue (node, value, _) -> - Format.fprintf fmt "value:%a of %a" ValueKind.pp value Node.pp node - | EventAnyValue (node, _) -> - Format.fprintf fmt "any value of %a" Node.pp node - | EventRegCl (node, _) -> - Format.fprintf fmt "registration of %a" Node.pp node - | EventRegAny (_) -> - Format.fprintf fmt "any registration" - | EventChange (node, _) -> - Format.fprintf fmt "changeNode of %a" Node.pp node - | EventChangeAny (_) -> - Format.fprintf fmt "changeAnyNode" - | EventRegSem (sem, _) -> - Format.fprintf fmt "regsem for %a" ThTermKind.pp sem - | EventRegValue (value, _) -> - Format.fprintf fmt "regvalue for %a" ValueKind.pp value - - - type 'b t = 'b event list +module type Attach = sig + type 'a arg + + type 'a env + + type result + + val attach_dom : + (?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit) + arg + + val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit) arg + + val attach_value : + (Node.t -> ('a, 'b) ValueKind.t -> (Node.t -> 'b -> result) env -> unit) arg + + val attach_any_value : + (Node.t -> (Node.t -> Value.t -> result) env -> unit) arg + + val attach_reg_any : ((Node.t -> result) env -> unit) arg + + val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit) arg + + val attach_reg_sem : (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit) arg + + val attach_reg_value : + (('a, 'b) ValueKind.t -> ('b -> result) env -> unit) arg + + val attach_repr : (Node.t -> (Node.t -> result) env -> unit) arg + + val attach_any_repr : ((Node.t -> result) env -> unit) arg end -type 'k alive = -| AliveReattached -| AliveStopped -| AliveRedirected of 'k +module type Simple = + Attach + with type 'a arg := Egraph.t -> 'a + and type 'a env := Egraph.t -> 'a + and type result := unit -module Key = struct +module Simple = struct + module Make (Info : sig + val name : string - type ('d,'k,'i) daemon_state = - | Alive of 'd Events.Fired.t * 'i - | Dead - | Redirected of 'k - - let print_daemon_state fmt = function - | Alive _ -> Format.fprintf fmt "alive" - | Dead -> Format.fprintf fmt "dead" - | Redirected _ -> Format.fprintf fmt "redirected" - - module type DemTable = sig - module Key: Popop_stdlib.Datatype - type data - type info val default: info - val state : (data, Key.t, info) daemon_state Key.M.t - end + val delay : Events.delay + end) = + struct + module D = struct + type runable = Egraph.t -> unit - type ('k,'d,'i) demtable = - (module DemTable with type Key.t = 'k and type data = 'd - and type info = 'i) - - type ('k,'d,'i) t = { - dk_id : ('k * 'd, 'k) Events.Dem.t; - dk_data : ('k,'d,'i) demtable Env.Saved.t; - } - - let create (type k d i) name = - { dk_id = Events.Dem.create_key (module struct - type t = k * d - type nonrec d = k - let name = name - end); - dk_data = Env.Saved.create_key (module struct - type t = (k,d,i) demtable - let name = name - end) - } + let print_runable = Fmt.nop - module type S = sig - module Key: Popop_stdlib.Datatype + let delay = Info.delay + + let key = + Events.Dem.create + (module struct + type t = Egraph.t -> unit + + let name = Info.name + end) + + let run d f = f d + end + + let () = Egraph.Wait.register_dem (module D) + + let wrap_node f _ n = Events.EnqRun (D.key, fun d -> f d n) + + let wrap_node_and_other f _ n v = Events.EnqRun (D.key, fun d -> f d n v) + + let wrap_other f _ v = Events.EnqRun (D.key, fun d -> f d v) + + let attach_dom d ?direct n dom f = + Egraph.attach_dom d ?direct n dom (wrap_node f) + + let attach_any_dom d dom f = Egraph.attach_any_dom d dom (wrap_node f) + + let attach_value d n v f = Egraph.attach_value d n v (wrap_node_and_other f) + + let attach_any_value d v f = + Egraph.attach_any_value d v (wrap_node_and_other f) + + let attach_reg_any d f = Egraph.attach_reg_any d (wrap_node f) - module Data: Popop_stdlib.Printable + let attach_reg_node d n f = Egraph.attach_reg_node d n (wrap_node f) - type info - val default: info + let attach_reg_sem d th f = Egraph.attach_reg_sem d th (wrap_other f) - val key: (Key.t, Data.t, info) t + let attach_reg_value d th f = Egraph.attach_reg_value d th (wrap_other f) - val delay: Events.delay - val wakeup: - Egraph.t -> Key.t -> Data.t Events.Fired.t -> - info -> Key.t alive - (** the Events.t in wakeup is a subset of the one given in watch *) + let attach_repr d n f = Egraph.attach_repr d n (wrap_node f) + + let attach_any_repr d f = Egraph.attach_any_repr d (wrap_node f) end - (** mark it attached if it is not already the case *) - let mark_dem : - type k d i. Egraph.t -> (k,d,i) t -> k -> unit = - fun d dem k -> - try - let module DemTable = (val (Egraph.get_env d dem.dk_data)) in - let module DemTable' = struct - include DemTable - let state = DemTable.Key.M.change (function - | None -> Some (Alive([],DemTable.default)) - | Some Dead -> raise AlreadyDead - | Some (Redirected _) -> raise AlreadyRedirected - | Some (Alive _) -> raise Exit) - k DemTable.state - end in - Egraph.set_env d dem.dk_data (module DemTable') - with Exit -> () - - module Register(D:S) = struct - - let rec run d k = - let module DemTable = (val (Egraph.get_env d D.key.dk_data)) in - match DemTable.Key.M.find k (DemTable.state) with - | Dead -> - Debug.dprintf4 debug "[Demon] @[Daemon %a for %a is dead@]" - Events.Dem.pp D.key.dk_id DemTable.Key.pp k; - None - | Redirected k' -> - Debug.dprintf6 debug - "[Demon] @[Daemon %a for %a is redirected to %a@]" - Events.Dem.pp D.key.dk_id DemTable.Key.pp - k DemTable.Key.pp k'; - run d k' - | Alive (events,info) -> - Debug.dprintf6 debug "[Demon] @[Run daemon %a for %a:@[%a@]@]" - Events.Dem.pp D.key.dk_id DemTable.Key.pp k - (Format.list ~sep:Format.newline Events.Fired.pp) events; - (** event can be added during wakeup *) - let module DemTable' = struct - include DemTable - let state = DemTable.Key.M.add k (Alive([],info)) (DemTable.state) - end - in - Egraph.set_env d D.key.dk_data (module DemTable'); - (** wakeup *) - let alive = D.wakeup d k events info in - (** delay can be modified *) - begin match alive with - | AliveStopped | AliveRedirected _ -> - let demstate = match alive with - | AliveStopped -> Dead - | AliveRedirected k' -> mark_dem d D.key k'; Redirected k' - | AliveReattached -> assert false in - Debug.dprintf4 debug "[Demon] @[Stop daemon %a %a@]" - Events.Dem.pp D.key.dk_id DemTable.Key.pp k; - begin - let module DemTable = - (val (Egraph.get_env d D.key.dk_data)) in - (** Dead even if event have been added *) - let state' = DemTable.Key.M.add k demstate (DemTable.state) in - let module DemTable' = struct - include DemTable - let state = state' - end - in - Egraph.set_env d D.key.dk_data (module DemTable') - end - | AliveReattached -> - Debug.dprintf0 debug "[Demon] @[Reattach daemon@]"; - end; - None - - let enqueue d event = - let module DemTable = (val (Egraph.Ro.get_env d D.key.dk_data)) in - let change_state k l = - Debug.dprintf6 debug - "[Demon] @[schedule %a for %a with %a@]" - Events.Dem.pp D.key.dk_id D.Key.pp k - Events.Fired.pp event; - let module DemTable' = struct - include DemTable - let state = DemTable.Key.M.add k l DemTable.state - end in - Egraph.Ro.set_env d D.key.dk_data (module DemTable') - in - let rec update_state k data = - match DemTable.Key.M.find_opt k DemTable.state with - | None -> assert false (* should have been marked *) - | Some Dead -> - Debug.dprintf4 debug - "[Demon] @[Dem %a is dead for %a@]" - Events.Dem.pp D.key.dk_id Events.Fired.pp event; - Events.Wait.EnqStopped - | Some (Redirected k') -> update_state k' data - | (Some Alive([],info)) -> - change_state k (Alive([data],info)); - Events.Wait.EnqRun k - | Some Alive(l,info) -> - change_state k (Alive(data::l,info)); - Events.Wait.EnqAlready - in - let k, event = - let open Events.Fired in - match event with - | EventDom (a, b , (k,d)) -> k, EventDom(a, b, d) - | EventValue (a, c, (k,d)) -> k, EventValue(a, c, d) - | EventSem (a, b, c, (k,d)) -> k, EventSem(a, b, c, d) - | EventReg (a, (k,d)) -> k, EventReg(a, d) - | EventRegNode (a, (k,d)) -> k, EventRegNode(a, d) - | EventChange (a, (k,d)) -> k, EventChange(a, d) - | EventRegSem (a, (k,d)) -> k, EventRegSem(a, d) - | EventRegValue (a, (k,d)) -> k, EventRegValue(a, d) in - update_state k event + module FixingModel = Make (struct + let name = "Demon.Simple.FixingModel" + let delay = Events.FixingModel + end) - let () = - let print_demtable fmt ((module DT): (D.Key.t,D.Data.t,D.info) demtable) = - let open Format in - let aux = pair ~sep:(const char ';') D.Key.pp print_daemon_state in - let l = DT.Key.M.bindings DT.state in - Format.list ~sep:newline aux fmt l - in - Env.Saved.register print_demtable D.key.dk_data; - (** Interface for generic daemon *) - let module Dem = struct - type runable = D.Key.t - let print_runable = D.Key.pp - let run = run - - type event = D.Key.t * D.Data.t - let print_event fmt (k,d) = - Format.fprintf fmt "(%a: %a)" D.Key.pp k D.Data.pp d - let enqueue = enqueue - - let key = D.key.dk_id - let delay = D.delay - end in - Egraph.Wait.register_dem (module Dem) - - let init d = - let module DemTable = struct - module Key = D.Key - type data = D.Data.t - type info = D.info let default = D.default - let state = Key.M.empty - end in - Egraph.set_env d D.key.dk_data (module DemTable); + module DelayedBy1 = Make (struct + let name = "Demon.Simple.DelayedBy1" + + let delay = Events.Delayed_by 1 + end) + + include DelayedBy1 +end + +module WithFilter = struct + module D = struct + type runable = Egraph.t -> unit + + let print_runable = Fmt.nop + + let delay = Events.Delayed_by 1 + + let key = + Events.Dem.create + (module struct + type t = Egraph.t -> unit + let name = "Demon.WithFilter" + end) + + let run d f = f d end - let attach : - type k d i. Egraph.t -> (k,d,i) t -> k -> d Create.t -> unit = - fun t dem k events -> - mark_dem t dem k; - (** record waiters *) - let iter ev = - Debug.dprintf2 debug "[Demon] @[Attach event %a@]" - Create.pp ev; - match ev with - | Create.EventDom (node,dom,data) -> - Egraph.attach_dom t node dom dem.dk_id (k,data) - | Create.EventAnyDom (dom,data) -> - Egraph.attach_any_dom t dom dem.dk_id (k,data) - | Create.EventValue (node,value,data) -> - Egraph.attach_value t node value dem.dk_id (k,data) - | Create.EventAnyValue (node,data) -> - Egraph.attach_any_value t node dem.dk_id (k,data) - | Create.EventChange (node,data) -> - Egraph.attach_node t node dem.dk_id (k,data) - | Create.EventChangeAny (data) -> - Egraph.attach_any_node t dem.dk_id (k,data) - | Create.EventRegCl (node,data) -> - Egraph.attach_reg_node t node dem.dk_id (k,data) - | Create.EventRegAny (data) -> - Egraph.attach_reg_any t dem.dk_id (k,data) - | Create.EventRegSem (sem,data) -> - Egraph.attach_reg_sem t sem dem.dk_id (k,data) - | Create.EventRegValue (value,data) -> - Egraph.attach_reg_value t value dem.dk_id (k,data) - in - List.iter iter events - - - type ('k,'i) state = - | SUnborn - | SAlive of 'i - | SDead - | SRedirected of 'k - - let is_attached (type k) (type d) (type i) t (dem: (k,d,i) t) (k:k) = - let module DemTable = (val (Egraph.get_env t dem.dk_data)) in - match DemTable.Key.M.find_opt k DemTable.state with - | None -> SUnborn - | Some (Alive(_,i)) -> SAlive i - | Some Dead -> SDead - | Some (Redirected k') -> SRedirected k' - - exception NotAlive - - let set_info (type k) (type d) (type i) t (dem: (k,d,i) t) (k:k) (i:i) = - let module DemTable = (val (Egraph.get_env t dem.dk_data)) in - match DemTable.Key.M.find_exn NotAlive k DemTable.state with - | Alive(w,_) -> - let module DemTable' = struct - include DemTable - let state = DemTable.Key.M.add k (Alive(w,i)) DemTable.state - end - in - Egraph.set_env t dem.dk_data (module DemTable') - | _ -> raise NotAlive - - - exception CantBeKilled - - let kill (type k) (type d) (type i) t (dem: (k,d,i) t) (k:k) = - try - let module DemTable = (val (Egraph.get_env t dem.dk_data)) in - Debug.dprintf4 debug "[Demon] @[Kill dem %a %a@]" - Events.Dem.pp dem.dk_id DemTable.Key.pp k; - let module DemTable' = struct - include DemTable - let state = DemTable.Key.M.change (function - | Some Dead -> raise Exit - | _ -> Some Dead) - k DemTable.state - end in - Egraph.set_env t dem.dk_data (module DemTable') - with Exit -> () + let () = Egraph.Wait.register_dem (module D) + + let wrap_node f d n = + match f d n with + | None -> Events.EnqAlready + | Some g -> Events.EnqRun (D.key, g) + + let wrap_node_and_other f d n v = + match f d n v with + | None -> Events.EnqAlready + | Some g -> Events.EnqRun (D.key, g) + + let wrap_other f d v = + match f d v with + | None -> Events.EnqAlready + | 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) + + let attach_any_dom d dom f = Egraph.Ro.attach_any_dom d dom (wrap_node f) + + let attach_value d n v f = + Egraph.Ro.attach_value d n v (wrap_node_and_other f) + + let attach_any_value d v f = + Egraph.Ro.attach_any_value d v (wrap_node_and_other f) + + let attach_reg_any d f = Egraph.Ro.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_sem d th f = Egraph.Ro.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_repr d n f = Egraph.Ro.attach_repr d n (wrap_node f) + + let attach_any_repr d f = Egraph.Ro.attach_any_repr d (wrap_node f) end -module Fast = struct - (** Instead of sending every wakeup event to the scheduler, a specific queue - is used. In order to keep some fairness, the number of event hendle each - time is limited by throttle *) - - type 'd t = { - dk_id : ('d, unit) Events.Dem.t; - dk_data : 'd Events.Fired.event Context.Queue.t Env.Unsaved.t; - (** for throttling *) - mutable dk_remaining: int; (** 0 if the demon is not the current one *) - } - - let create (type d) name - = { - dk_id = Events.Dem.create_key (module struct - type t = d - type d = unit - let name = name - end); - dk_data = Env.Unsaved.create_key (module struct - type t = d Events.Fired.event Context.Queue.t - let name = name - end); - dk_remaining = 0; - } +module Key = struct + type state = Wait | Stop module type S = sig + module Key : Colibri2_popop_lib.Popop_stdlib.Datatype - module Data: sig - type t - val pp: t Format.printer - end - - val key: Data.t t + val delay : Events.delay - (** never killed *) - val delay: Events.delay - val throttle: int (** todo int ref? *) - (** number of time run in a row *) - val wakeup: Egraph.t -> Data.t Events.Fired.event -> unit + val run : Egraph.t -> Key.t -> state + val name : string end + module Register (S : S) = struct + type state' = Wait | Scheduled | Stop [@@deriving show] + + module H = Datastructure.Hashtbl2 (S.Key) + + let h = H.create pp_state' S.name (fun _ -> Wait) - module Register(D:S) = struct - - let run d () = - assert (D.key.dk_remaining = 0); - let queue = Egraph.get_unsaved_env d D.key.dk_data in - D.key.dk_remaining <- D.throttle; - let rec run_one () = - match Context.Queue.dequeue queue with - | None -> () - | Some event -> - Debug.dprintf6 debug - "[Demon] @[Run daemon fast %a:@[%a@ %a@]@]" - Events.Dem.pp D.key.dk_id Events.Fired.pp event - D.Data.pp (Events.Fired.get_data event); - D.wakeup d event; - Debug.dprintf0 debug "[Demon] @[Done@]"; - (match D.delay with - | Immediate -> () - | Delayed_by _ | LastEffort _ | FixingModel -> Egraph.flush_internal d); - D.key.dk_remaining <- D.key.dk_remaining - 1; - if 0 < D.key.dk_remaining then run_one () in - try - run_one (); - assert (D.key.dk_remaining >= 0); - D.key.dk_remaining <- 0; - if Context.Queue.is_empty queue then None else begin - Some () - end - with exn -> (** Normally Contradiction *) - assert (D.key.dk_remaining >= 0); - D.key.dk_remaining <- 0; - raise exn - - let enqueue d event = - assert (D.key.dk_remaining >= 0); - Debug.dprintf4 debug - "[Demon] @[schedule %a for %a@]" - Events.Dem.pp D.key.dk_id Events.Fired.pp event; - let queue = Egraph.Ro.get_unsaved_env d D.key.dk_data in - Context.Queue.enqueue queue event; - if D.key.dk_remaining = 0 && Context.Queue.length queue = 1 then - Events.Wait.EnqRun () - else - Events.Wait.EnqAlready + let key = + Events.Dem.create + (module struct + type t = S.Key.t + let name = S.name + end) let () = - let print_demtable = Context.Queue.pp ~sep:Fmt.(any ",") Events.Fired.pp in - Env.Unsaved.register ~init:Context.Queue.create ~pp:print_demtable D.key.dk_data; - (** Interface for generic daemon *) - let module Dem = struct - type runable = unit - let print_runable = Popop_stdlib.DUnit.pp - let run = run - - type event = D.Data.t - let print_event = D.Data.pp - let enqueue = enqueue - - let key = D.key.dk_id - let delay = D.delay - end in - Egraph.Wait.register_dem (module Dem) + Egraph.Wait.register_dem + (module struct + let key = key - end + let delay = S.delay + + let run d k = + match H.find h d k with + | Stop -> () + | Wait -> raise Impossible + | Scheduled -> ( + H.set h d k Wait; + match S.run d k with Wait -> () | Stop -> H.set h d k Stop) + + type runable = S.Key.t + + let print_runable = S.Key.pp + end) + + let wrap k d = + match H.Ro.find h d k with + | Stop -> Events.EnqStopped + | Wait -> + H.Ro.set h d k Scheduled; + Events.EnqRun (key, k) + | Scheduled -> Events.EnqAlready + + let wrap_node k d _ = wrap k d + + let wrap_node_and_other k d _ _ = wrap k d + + let wrap_other k d _ = wrap k d - let attach d dem events = - let open Create in - let iter ev = - Debug.dprintf2 debug "[Demon] @[Attach event %a@]" Create.pp ev; - match ev with - | EventDom (node,dom,data) -> - Egraph.attach_dom d node dom dem.dk_id data - | EventAnyDom (dom,data) -> - Egraph.attach_any_dom d dom dem.dk_id data - | EventValue (node,value,data) -> - Egraph.attach_value d node value dem.dk_id data - | EventAnyValue (node,data) -> - Egraph.attach_any_value d node dem.dk_id data - | EventRegCl (node,data) -> - Egraph.attach_reg_node d node dem.dk_id data - | EventRegAny (data) -> - Egraph.attach_reg_any d dem.dk_id data - | EventChange (node,data) -> - Egraph.attach_node d node dem.dk_id data - | EventChangeAny (data) -> - Egraph.attach_any_node d dem.dk_id data - | EventRegSem (sem,data) -> - Egraph.attach_reg_sem d sem dem.dk_id data - | EventRegValue (value,data) -> - Egraph.attach_reg_value d value dem.dk_id data - in - List.iter iter events - - let register_init_daemon - (type a) - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - (thterm: (module Nodes.RegisteredThTerm with type t = a) ) - (f:Egraph.t -> a -> unit) - (init_d:Egraph.t) - = - let module ThTerm = (val thterm) in - let module DaemonInit = struct - let key = create name - module Data = Popop_stdlib.DUnit - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventRegSem(thterm,()) -> - let thterm = ThTerm.coerce_thterm thterm in - f d thterm - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - attach init_d DaemonInit.key [Create.EventRegSem(ThTerm.key,())] - - let register_init_daemon_value - (type a) - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - (value: (module Nodes.RegisteredValue with type t = a) ) - (f:Egraph.t -> a -> unit) - (init_d:Egraph.t) - = - let module Val = (val value) in - let module DaemonInit = struct - let key = create name - module Data = Popop_stdlib.DUnit - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventRegValue(value,()) -> - let thterm = Val.coerce_nodevalue value in - f d thterm - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - attach init_d DaemonInit.key [Create.EventRegValue(Val.key,())] - - let register_change_repr_daemon - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - (f:Egraph.t -> Node.t -> unit) - (init_d:Egraph.t) - = - let module DaemonInit = struct - let key = create name - module Data = Popop_stdlib.DUnit - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventChange(node,()) -> - f d node - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - attach init_d DaemonInit.key [Create.EventChangeAny(())] - - let register_any_new_node_daemon - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - (f:Egraph.t -> Node.t -> unit) - (init_d:Egraph.t) - = - let module DaemonInit = struct - let key = create name - module Data = Popop_stdlib.DUnit - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventReg(node,()) -> - f d node - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - attach init_d DaemonInit.key [Create.EventRegAny(())] - - let register_change_domain_daemon - (type a) (type b) - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - ?(pp=Fmt.nop) - (dom:a DomKind.t) - (f:Egraph.t -> Node.t -> b -> unit) - = - let module DaemonInit = struct - let key = create name - module Data = struct - type t = b - let pp = pp - end - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventDom(node,dom',data) -> - assert (DomKind.equal dom dom'); - f d node data - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - let attach d n data = - attach d DaemonInit.key [Create.EventDom(n,dom,data)]; - match Egraph.get_dom d dom n with - | None -> () - | Some _ -> f d n data - in - attach - - let register_any_change_domain_daemon - (type a) - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - (dom:a DomKind.t) - (f:Egraph.t -> Node.t -> unit) - = - let module DaemonInit = struct - let key = create name - module Data = Unit - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventDom(node,dom',()) -> - assert (DomKind.equal dom dom'); - f d node - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - (fun d -> - attach d DaemonInit.key [Create.EventAnyDom(dom,())] - ) - - let register_get_value_daemon - (type a) (type b) - ~name - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - ?(pp=Fmt.nop) - (value: (module Nodes.RegisteredValue with type s = a) ) - (f:Egraph.t -> Node.t -> a -> b -> unit) - = - let module Val = (val value) in - let module DaemonInit = struct - let key = create name - module Data = struct - type t = b - let pp = pp - end - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventValue(node,value,data) -> - let v = Opt.get_exn Impossible (Value.value Val.key value) in - f d node v data - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - let attach d n data = - match Egraph.get_value d n with - | None -> attach d DaemonInit.key [Create.EventValue(n,Val.key,data)] - | Some v -> - match Value.value Val.key v with - | None -> attach d DaemonInit.key [Create.EventValue(n,Val.key,data)] - | Some v -> - f d n v data - in - attach - - type waiter = { - for_dom: 'a. Egraph.t -> 'a DomKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit; - for_value: 'a. Egraph.t -> 'a ValueKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit; - for_any_value: 'a. Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit; - } - - let register_simply - ?(delay=Events.Delayed_by 1) - ?(throttle=100) - name - = - let module DaemonInit = struct - let key = create name - module Data = struct - type t = Egraph.t -> Node.t -> unit - let pp = Fmt.nop - end - let delay = delay - let throttle = throttle - let wakeup d = function - | Events.Fired.EventDom(node,_,f) -> - f d node - | Events.Fired.EventValue(node,_,f) -> - f d node - | _ -> raise UnwaitedEvent - end in - let module RDaemonInit = Register(DaemonInit) in - let for_dom d dom n f = - attach d DaemonInit.key [Create.EventDom(n,dom,f)]; - match Egraph.get_dom d dom n with - | None -> () - | Some _ -> f d n - in - let for_value d value n f = - attach d DaemonInit.key [Create.EventValue(n,value,f)]; - match Egraph.get_value d n with - | None -> () - | Some _ -> f d n - in - let for_any_value d n f = - attach d DaemonInit.key [Create.EventAnyValue(n,f)]; - match Egraph.get_value d n with - | None -> () - | Some _ -> f d n - in - {for_dom; for_value; for_any_value} + let attach_dom d ?direct n dom f = + Egraph.attach_dom d ?direct n dom (wrap_node f) + let attach_any_dom d dom f = Egraph.attach_any_dom d dom (wrap_node f) + + let attach_value d n v f = Egraph.attach_value d n v (wrap_node_and_other f) + + let attach_any_value d v f = + Egraph.attach_any_value d v (wrap_node_and_other f) + + let attach_reg_any d f = Egraph.attach_reg_any d (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.attach_reg_sem 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.attach_repr d n (wrap_node f) + + let attach_any_repr d f = Egraph.attach_any_repr d (wrap_node f) + end end diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli index c673010c0d38d3bf6d01c0d16a2c3b5dc9fb3b4e..4b0325822eaa5bcbbf0abc8d0ee64458657860f2 100644 --- a/src_colibri2/core/demon.mli +++ b/src_colibri2/core/demon.mli @@ -18,203 +18,77 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -open Colibri2_popop_lib open Nodes -module Create : sig - type 'b event = - (** the domain dom of the class is watched *) - | EventDom : Node.t * 'a DomKind.t * 'b -> 'b event - (** the domain dom of any class is watched *) - | EventAnyDom : 'a DomKind.t * 'b -> 'b event - (** the value of the class is watched *) - | EventValue : Node.t * 'a ValueKind.t * 'b -> 'b event - (** the values of the class is watched *) - | EventAnyValue : Node.t * 'b -> 'b event - (** Warn when any class registered *) - | EventRegAny : 'b -> 'b event - (** Warn when this class is registered *) - | EventRegCl : Node.t * 'b -> 'b event - (** Warn when the class is not the representant of its eq-class anymore *) - | EventChange : Node.t * 'b -> 'b event - (** Warn when a class is not the representant of its eq-class anymore *) - | EventChangeAny : 'b -> 'b event - (** a new theory term 'a appear *) - | EventRegSem : 'a ThTermKind.t * 'b -> 'b event - (** a new value 'a appear *) - | EventRegValue : 'a ValueKind.t * 'b -> 'b event - - - val pp: 'b event Format.printer - - type 'b t = 'b event list -end - - -type 'k alive = -| AliveReattached -| AliveStopped -| AliveRedirected of 'k +module type Attach = sig + type 'a arg -module Key: sig + type 'a env - type ('k,'d,'i) t - val create: string -> ('k,'d,'i) t + type result - module type S = sig - module Key: Popop_stdlib.Datatype + val attach_dom : + (?direct:bool -> Node.t -> 'a DomKind.t -> (Node.t -> result) env -> unit) + arg - module Data: Popop_stdlib.Printable + val attach_any_dom : ('a DomKind.t -> (Node.t -> result) env -> unit) arg - type info val default: info + val attach_value : + (Node.t -> ('a, 'b) ValueKind.t -> (Node.t -> 'b -> result) env -> unit) arg - val key: (Key.t, Data.t, info) t + val attach_any_value : + (Node.t -> (Node.t -> Value.t -> result) env -> unit) arg - val delay: Events.delay - val wakeup: - Egraph.t -> Key.t -> Data.t Events.Fired.t -> - info -> Key.t alive - (** the Events.t in wakeup is a subset of the one given in watch *) - end + val attach_reg_any : ((Node.t -> result) env -> unit) arg - module Register (_:S): sig - val init: Egraph.t -> unit - (** to run for each new delay *) - end + val attach_reg_node : (Node.t -> (Node.t -> result) env -> unit) arg - type ('k,'i) state = - | SUnborn - | SAlive of 'i - | SDead - | SRedirected of 'k + val attach_reg_sem : (('a, 'b) ThTermKind.t -> ('b -> result) env -> unit) arg - val attach: Egraph.t -> ('k,'d,'i) t -> 'k -> 'd Create.t -> unit - (** raise AlreadyDead if this key is already dead *) + val attach_reg_value : + (('a, 'b) ValueKind.t -> ('b -> result) env -> unit) arg - val is_attached: Egraph.t -> ('k,'d,'i) t -> 'k -> ('k,'i) state + val attach_repr : (Node.t -> (Node.t -> result) env -> unit) arg - val set_info: Egraph.t -> ('k, 'd, 'i) t -> 'k -> 'i -> unit + val attach_any_repr : ((Node.t -> result) env -> unit) arg +end - exception CantBeKilled - val kill : Egraph.t -> ('a, 'b,'c) t -> 'a -> unit +module type Simple = + Attach + with type 'a arg := Egraph.t -> 'a + and type 'a env := Egraph.t -> 'a + and type result := unit +module Simple : sig + include Simple + module FixingModel : Simple 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 -module Fast: sig - - type 'd t - val create: string -> 'd t +module Key : sig + type state = Wait | Stop module type S = sig + module Key : Colibri2_popop_lib.Popop_stdlib.Datatype - module Data: sig - type t - val pp: t Format.printer - end - - val key: Data.t t + val delay : Events.delay - (** never killed *) - val delay: Events.delay - val throttle: int (** todo int ref? *) - (** number of time run in a row *) - val wakeup: Egraph.t -> Data.t Events.Fired.event -> unit + val run : Egraph.t -> Key.t -> state + val name : string end - module Register (_:S): sig + module Register (S : S) : sig + include + Attach + with type 'a arg := Egraph.t -> 'a + and type 'a env := S.Key.t + and type result := unit end - - val attach: Egraph.t -> 'd t -> 'd Create.t -> unit - - (** helper *) - val register_init_daemon: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - (module RegisteredThTerm with type t = 'a) -> - (Egraph.t -> 'a -> unit) -> - Egraph.t -> - unit - (** *) - - (** helper *) - val register_init_daemon_value: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - (module RegisteredValue with type t = 'a) -> - (Egraph.t -> 'a -> unit) -> - Egraph.t -> - unit - (** *) - - (** helper *) - val register_change_repr_daemon: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - (Egraph.t -> Node.t -> unit) -> - Egraph.t -> - unit - (** *) - - (** helper *) - val register_any_new_node_daemon: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - (Egraph.t -> Node.t -> unit) -> - Egraph.t -> - unit - (** *) - - (** helper *) - val register_change_domain_daemon: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - ?pp:('b Fmt.t) -> - 'a DomKind.t -> - (Egraph.t -> Node.t -> 'b -> unit) -> - (Egraph.t -> Node.t -> 'b -> unit) - (** *) - - (** helper *) - val register_any_change_domain_daemon: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - 'a DomKind.t -> - (Egraph.t -> Node.t -> unit) -> - (Egraph.t -> unit) - (** *) - - (** helper *) - val register_get_value_daemon: - name:string -> - ?delay:Events.delay -> - ?throttle:int -> - ?pp:('b Fmt.t) -> - (module RegisteredValue with type s = 'a) -> - (Egraph.t -> Node.t -> 'a -> 'b -> unit) -> - (Egraph.t -> Node.t -> 'b -> unit) - (** *) - - type waiter = { - for_dom: 'a. Egraph.t -> 'a DomKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit; - for_value: 'a. Egraph.t -> 'a ValueKind.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit; - for_any_value: 'a. Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit; - } - - (** helper *) - val register_simply: - ?delay:Events.delay -> - ?throttle:int -> - string -> - waiter - (** *) - end diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml index 06fc49f25f016f74b4bbfb743b8669b68f0155fa..f775c4a1844be966d041910d6c76228d8b8c3e2e 100644 --- a/src_colibri2/core/egraph.ml +++ b/src_colibri2/core/egraph.ml @@ -44,25 +44,28 @@ let stats_register = module DecTag = DInt (** For each kind of domain *) -type 'a domtable = { +type ('ro,'a) domtable = { (** For each representative node its associated domain if any *) table : 'a Node.M.t; (** Events: the domain of this node changed *) - events : Events.Wait.t Bag.t Node.M.t; + events : ('ro -> Node.t -> Events.enqueue) Bag.t Node.M.t; (** Events: the domain of any node changed *) - reg_events : Events.Wait.t list; + reg_events : ('ro -> Node.t -> Events.enqueue) Bag.t; } -module VDomTable = DomKind.MkVector (struct type ('a,'unused) t = 'a domtable end) +module VDomTable = DomKind.MkVector (struct type ('a,'ro) t = ('ro,'a) domtable end) -module VSemTable = ThTermKind.Vector +module VSemTable = ThTermKind.MkVector (struct type (_,'b,'ro) t = ('ro -> 'b -> Events.enqueue) Bag.t end) -type valuetable = { - values : Value.t Node.M.t; - events : Events.Wait.t Bag.t Node.M.t ValueKind.M.t; - reg_events : Events.Wait.t list ValueKind.M.t; +type ('ro,'a) valuetable = { + (** Events: the value of this node changed *) + events : ('ro -> Node.t -> 'a -> Events.enqueue) Bag.t Node.M.t; + (** Events: the value has been registered *) + reg_events : ('ro -> 'a -> Events.enqueue) Bag.t; } +module ValueTable = ValueKind.MkVector (struct type (_,'b,'ro) t = ('ro,'b) valuetable end) + (** Environnement *) (** mutable but only contain persistent structure *) @@ -72,38 +75,41 @@ module Def = struct type saved = { saved_repr : Node.t Node.M.t; saved_rang : int Node.M.t; - saved_event_repr : Events.Wait.t Bag.t Node.M.t; - saved_event_any_repr : Events.Wait.t list; - saved_event_value : Events.Wait.t Bag.t Node.M.t; - saved_event_reg : Events.Wait.t list Node.M.t; - saved_event_any_reg : Events.Wait.t list; + 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_reg : event_node Bag.t Node.M.t; + saved_event_any_reg : event_node Bag.t; saved_dom : delayed_t VDomTable.t; - saved_sem : Events.Wait.t list VSemTable.t; - saved_value : valuetable; + saved_sem : delayed_t VSemTable.t; + saved_value : 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 t = { (** Union Find *) mutable repr : Node.t Node.M.t; mutable rang : int Node.M.t; (** Events: the representative of this node changed *) - mutable event_repr : Events.Wait.t Bag.t Node.M.t; + mutable event_repr : event_node Bag.t Node.M.t; (** Events: the representative of any node changed *) - mutable event_any_repr : Events.Wait.t list; + mutable event_any_repr : event_node Bag.t; (** Events: the value of this node has been set *) - mutable event_value : Events.Wait.t Bag.t Node.M.t; + mutable event_value : (delayed_t -> Node.t -> Value.t -> Events.enqueue) Bag.t Node.M.t; (** Events: this node have been registered *) - mutable event_reg : Events.Wait.t list Node.M.t; + mutable event_reg : event_node Bag.t Node.M.t; (** Events: any node have been registered *) - mutable event_any_reg : Events.Wait.t list; + mutable event_any_reg : event_node Bag.t; (** Events: semantic term of this kind has been registered *) - sem : Events.Wait.t list VSemTable.t; + sem : delayed_t VSemTable.t; (** Information on the domains, data is {!'a domtable} *) dom : delayed_t VDomTable.t; (** Value *) - mutable value : valuetable; + value : 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} *) @@ -175,13 +181,13 @@ type choice_state = Def.choice_state = (** {2 Define events} *) +let schedule_immediate t d = Queue.push (RunDem d) t.todo_immediate_dem +let schedule t d = t.sched_daemon d + module WaitDef = struct type delayed = delayed_t - let schedule_immediate t d = Queue.push (RunDem d) t.todo_immediate_dem - let schedule t d = t.sched_daemon d type delayed_ro = delayed_t - let readonly x = x end module Wait : Events.Wait.S with type delayed = delayed_t and type delayed_ro = delayed_t = Events.Wait.Make(WaitDef) @@ -205,20 +211,22 @@ module Hidden = Context.Make(struct saved_event_any_reg = t.event_any_reg; saved_dom = VDomTable.copy t.dom; saved_sem = VSemTable.copy t.sem; - saved_value = t.value; + saved_value = ValueTable.copy t.value; + saved_values = t.values; saved_envs = Env.Saved.VectorH.copy t.envs; } let restore (s:saved) (t:t) = t.repr <- s.saved_repr; t.rang <- s.saved_rang; + t.values <- s.saved_values; t.event_repr <- s.saved_event_repr ; t.event_value <- s.saved_event_value ; t.event_reg <- s.saved_event_reg ; t.event_any_reg <- s.saved_event_any_reg; - t.value <- s.saved_value; VDomTable.move ~from:s.saved_dom ~to_:t.dom; VSemTable.move ~from:s.saved_sem ~to_:t.sem; + ValueTable.move ~from:s.saved_value ~to_:t.value; Env.Saved.VectorH.move ~from:s.saved_envs ~to_:t.envs; Def.emptied t.delayed @@ -232,11 +240,18 @@ let get_table_dom t k = VDomTable.get_def t.dom k { table = Node.M.empty; events = Node.M.empty; - reg_events = [] } + reg_events = Bag.empty } let get_table_sem t k = Nodes.check_thterm_registered k; - ThTermKind.Vector.get_def t.sem k [] + VSemTable.get_def t.sem k Bag.empty + +let get_table_value t k = + Nodes.check_value_registered k; + ValueTable.get_def t.value k + { events = Node.M.empty; + reg_events = Bag.empty; + } exception UninitializedEnv of string @@ -275,7 +290,7 @@ module T = struct get_direct_dom t dom node let get_direct_value t node = - Node.M.find_opt node t.value.values + Node.M.find_opt node t.values let get_value t node = let node = find_def t node in @@ -312,19 +327,6 @@ end open T (** {2 For debugging and display} *) -let _print_env fmt t = - let printd (type a) dom fmt (domtable:a domtable) = - let aux = - Format.(pair ~sep:(const char ';') Node.pp (Bag.pp (const char ',') Events.Wait.pp)) - in - let aux fmt m = Node.M.bindings m |> Format.(list ~sep:newline aux) fmt in - Format.fprintf fmt "%a:@[%a@]" DomKind.pp dom aux domtable.events - in - VDomTable.pp Format.newline Format.silent - {VDomTable.printk = Format.silent} - {VDomTable.printd} fmt t.dom - - let dot_to_escape = Str.regexp "[{}|<>]" let escape_for_dot pp v = @@ -364,13 +366,14 @@ let output_graph filename t = DomKind.pp dom (escape_for_dot (VDom.print_dom dom) s); with Not_found -> () in - let print_value fmt valuetable = + let print_value fmt values = try - let s = Node.M.find node valuetable.values in + let s = Node.M.find node values in (match Value.kind s with | Value.Value (kind, value) -> - Format.fprintf fmt "| {%a | %s}" - ValueKind.pp kind (escape_for_dot (print_value kind) value)) + let (module S) = Nodes.get_value kind in + Format.fprintf fmt "| {%a | %s}" + ValueKind.pp kind (escape_for_dot S.pp value)) with Not_found -> () in let print_sem fmt node = @@ -381,7 +384,7 @@ let output_graph filename t = | Some thterm -> match Only_for_solver.sem_of_node thterm with | Only_for_solver.ThTerm(sem,v) -> - let (module S) = get_thterm sem in + let (module S) = Nodes.get_thterm sem in Format.fprintf fmt "| {%a | %s}" ThTermKind.pp sem (escape_for_dot S.pp v) end @@ -399,7 +402,7 @@ let output_graph filename t = (if is_repr t node then print_value else Format.silent) - t.value + t.values let vertex_attributes node = let label = Format.to_string pp node in @@ -448,6 +451,7 @@ let draw_graph = module Delayed = struct open T type t = delayed_t + type ro = delayed_t let context t = Hidden.creator t.env.history @@ -481,28 +485,43 @@ module Delayed = struct let is_registered t node = is_registered t.env node + let new_pending_daemon (type d) t (dem : d Events.Dem.t) runable = + let module Dem = (val Wait.get_dem dem) in + let daemonkey = Events.Wait.DaemonKey (dem, runable) in + match Dem.delay with + | Immediate -> schedule_immediate t daemonkey + | _ -> schedule t daemonkey + + let run_event t apply e = + match apply t e with + | Events.EnqStopped -> None + | EnqAlready -> Some e + | EnqRun (dem,runable) -> + new_pending_daemon t dem runable; + Some e + | EnqLast (dem,runable) -> + new_pending_daemon t dem runable; + None + + let run_events t apply events = + Bag.filter_map_homo (run_event t apply) events + let set_value_direct t node0 new_v = Debug.incr stats_set_value; let node = find t node0 in - let valuetable = t.env.value in - let valuetable = { - valuetable with - values = Node.M.add node new_v valuetable.values; - } in - t.env.value <- valuetable; + t.env.values <- Node.M.add node new_v t.env.values; (match Value.kind new_v with - | Value.Value(valuekind,_) -> + | Value.Value(valuekind,new_v) -> let events = - let open Option in - let* events = ValueKind.M.find_opt valuekind valuetable.events in - Node.M.find_opt node events + let events = (get_table_value t.env valuekind).events in + Node.M.find_def Bag.empty node events in (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)) + ignore (run_events t (fun t e -> e t node new_v) events) ); - let events = Node.M.find_opt node t.env.event_value in + let events = Node.M.find_def Bag.empty node t.env.event_value in (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_bag Events.Wait.translate_value t events (node,new_v)) + ignore (run_events t (fun t e -> e t node new_v) events) let add_pending_merge (t : t) node node' = Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]" @@ -530,29 +549,25 @@ module Delayed = struct let new_events, node_events = Node.M.find_remove node t.env.event_reg in t.env.event_reg <- new_events; (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_list Events.Wait.translate_regnode t node_events node); + ignore (Opt.map (run_events t (fun t e -> e t node)) node_events); (** reg *) (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_list Events.Wait.translate_reg - t (Some t.env.event_any_reg) node); + ignore (run_events t (fun t e -> e t node) t.env.event_any_reg); (** reg_sem *) match Only_for_solver.open_node node with | Only_for_solver.ThTerm thterm -> begin match Only_for_solver.sem_of_node thterm with - | Only_for_solver.ThTerm(sem,_) -> + | Only_for_solver.ThTerm(sem,thterm) -> let reg_events = get_table_sem t.env sem in (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_list Events.Wait.translate_regsem - t (Some reg_events) (thterm)) + ignore (run_events t (fun t e -> e t thterm) reg_events); end | Only_for_solver.Value nodevalue -> begin match Value.kind nodevalue with - | Value(value,_) -> - let valuetable = t.env.value in - let reg_events = ValueKind.M.find_opt value valuetable.reg_events in + | Value(value,nodevalue') -> + let reg_events = (get_table_value t.env value).reg_events in (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_list Events.Wait.translate_regvalue - t reg_events (nodevalue)); + ignore (run_events t (fun t e -> e t nodevalue') reg_events); set_value_direct t node nodevalue end end @@ -571,12 +586,12 @@ module Delayed = struct (** wakeup the daemons register_node *) let event, other_event = Node.M.find_remove node0' t.env.event_repr in (* can be always removed *) - ignore (Wait.wakeup_events_bag Events.Wait.translate_change t other_event node0'); + ignore (Opt.map (run_events t (fun t e -> e t node0')) other_event); t.env.event_repr <- event; (* deletion of events are not taken into account for that kind *) - ignore (Wait.wakeup_events_list Events.Wait.translate_change t (Some t.env.event_any_repr) node0'); + ignore (run_events t (fun t e -> e t node0') t.env.event_any_repr); (** set the value if node0' is one *) - match Node.M.find_opt node t.env.value.values, Nodes.Only_for_solver.nodevalue node0' with + match Node.M.find_opt node t.env.values, Nodes.Only_for_solver.nodevalue node0' with | _, None -> () | None, Some value -> set_value_direct t node0 value @@ -617,7 +632,7 @@ module Delayed = struct let other_events, woken_events = Node.M.find_remove node domtable.events in let domtable = { domtable with table = new_table; events = other_events } in VDomTable.set t.env.dom dom domtable; - let woken_events = Wait.wakeup_events_bag Events.Wait.translate_dom t woken_events (node,dom) in + let woken_events = Opt.map (run_events t (fun t e -> e t node)) woken_events in begin match woken_events with | None -> () | Some woken_events -> @@ -630,7 +645,7 @@ module Delayed = struct VDomTable.set t.env.dom dom domtable; end; (* deletion of events are not taken into account *) - ignore (Wait.wakeup_events_list Events.Wait.translate_dom t (Some domtable.reg_events) (node,dom)) + ignore (run_events t (fun t e -> e t node) domtable.reg_events) let flag_choose_repr_no_value = Debug.register_flag @@ -688,28 +703,30 @@ module Delayed = struct let merge_dom ?(dry_run=false) t node1_0 node2_0 inv = let node1 = find t node1_0 in let node2 = find t node2_0 in - let dom_not_done = ref false in - let iteri (type a) (dom : a DomKind.t) (domtable : a domtable) = + let dom_done = ref true in + let iteri (type a) (dom : a DomKind.t) (domtable : (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 if not (Dom.merged s1 s2) then begin - dom_not_done := true; + dom_done := false; if not dry_run then Queue.push (SetMergeDomNode(dom,node1_0,node2_0,inv)) t.todo_merge_dom + else + Debug.dprintf6 debug_few "[Egraph.few] Domain %a not merged between %a and %a" + DomKind.pp dom Node.pp node1 Node.pp node2 end in VDomTable.iter_initializedi {VDomTable.iteri} t.env.dom; - !dom_not_done + !dom_done let merge_values t node0 node0' = let node = find t node0 in let node' = find t node0' in - let valuetable = t.env.value in - let old_s = Node.M.find_opt node valuetable.values in - let old_s' = Node.M.find_opt node' valuetable.values in + let old_s = Node.M.find_opt node t.env.values in + let old_s' = Node.M.find_opt node' t.env.values in Debug.dprintf12 debug "[Egraph] @[merge value (%a(%a),%a)@ and (%a(%a),%a)@]" Node.pp node Node.pp node0 @@ -735,8 +752,8 @@ module Delayed = struct end let check_mergeable_values t node node' = - let old_s = Node.M.find_opt node t.env.value.values in - let old_s' = Node.M.find_opt node' t.env.value.values in + let old_s = Node.M.find_opt node t.env.values in + let old_s' = Node.M.find_opt node' t.env.values in match old_s, old_s' with | None, None | Some _, None @@ -767,8 +784,8 @@ module Delayed = struct Node.pp repr_node Node.pp repr_node0; let event, other_event = Node.M.find_remove other_node t.env.event_repr in - let other_event = Wait.wakeup_events_bag - Events.Wait.translate_change t other_event other_node + let other_event = + Opt.map (run_events t (fun t e -> e t other_node)) other_event in (** move node events *) @@ -781,7 +798,7 @@ module Delayed = struct end; (** move dom events *) - let iteri (type a) (dom : a DomKind.t) (domtable: a domtable) = + let iteri (type a) (dom : a DomKind.t) (domtable: (t,a) domtable) = match Node.M.find_opt other_node domtable.events with | None -> () | Some other_events -> @@ -794,16 +811,16 @@ module Delayed = struct VDomTable.iter_initializedi {VDomTable.iteri} t.env.dom; (** move value events by valuekind *) - let mapi _ events = - match Node.M.find_opt other_node events with - | None -> events - | Some other_events -> - Node.M.add_change (fun x -> x) Bag.concat repr_node other_events - events + let mapi _ (table: _ valuetable) = + { table with events = + match Node.M.find_opt other_node table.events with + | None -> table.events + | Some other_events -> + Node.M.add_change (fun x -> x) Bag.concat repr_node other_events + table.events + } in - t.env.value <- { t.env.value with events = - ValueKind.M.mapi {mapi} t.env.value.events - }; + ValueTable.map_initializedi {mapi} t.env.value; begin let event, other_event = Node.M.find_remove other_node t.env.event_value in @@ -820,12 +837,10 @@ module Delayed = struct (** wakeup the daemons *) t.env.event_any_repr <- - Option.value ~default:[] @@ - Wait.wakeup_events_list - Events.Wait.translate_change t (Some t.env.event_any_repr) other_node + run_events t (fun t e -> e t other_node) t.env.event_any_repr let continue_merge t node1_0 node2_0 inv = - let dom_not_done = merge_dom t node1_0 node2_0 inv in + let dom_not_done = not (merge_dom t node1_0 node2_0 inv) in if dom_not_done then begin Debug.dprintf4 debug "[Egraph] @[merge %a %a dom not done@]" @@ -860,9 +875,7 @@ module Delayed = struct let rec do_pending_daemon delayed (Events.Wait.DaemonKey (dem,runable)) = let (module Dem) = Wait.get_dem dem in - match Dem.run delayed runable with - | None -> () - | Some runable -> Wait.new_pending_daemon delayed dem runable + Dem.run delayed runable and do_pending t = draw_graph t.env; @@ -882,7 +895,7 @@ module Delayed = struct else match t.todo_delayed_merge with | Some(node1_0,node2_0,inv) -> t.todo_delayed_merge <- None; - assert (not (merge_dom ~dry_run:true t node1_0 node2_0 inv)); + assert (merge_dom ~dry_run:true t node1_0 node2_0 inv); (** understand why that happend. Is it really needed to do a fixpoint? *) continue_merge t node1_0 node2_0 inv; @@ -969,82 +982,82 @@ module Delayed = struct (** {2 API for attaching event} *) - let attach_dom (type a) t node (dom : a DomKind.t) dem event = + let attach_dom (type a) t ?(direct=true) node (dom : a DomKind.t) f = let node = find_def t node in - let event = Events.Wait.Event (dem,event) in let domtable = get_table_dom t.env dom in let domtable = { domtable with - events = Node.M.add_change Bag.elt Bag.add node event domtable.events + events = Node.M.add_change Bag.elt Bag.add node f domtable.events } in - VDomTable.set t.env.dom dom domtable + VDomTable.set t.env.dom dom domtable; + if direct then + match get_dom t dom node with + | None -> () + | Some _ -> + ignore (run_event t (fun t f -> f t node) f) - let attach_value (type a) t node (value : a ValueKind.t) dem event = + let attach_value (type a b) t node (value : (a,b) ValueKind.t) (f: ro -> Node.t -> b -> Events.enqueue) = let node = find_def t node in - let event = Events.Wait.Event (dem,event) in - let valuetable = t.env.value in - let valuetable = { - valuetable with - events = - ValueKind.M.add_change - (fun event -> Node.M.singleton node (Bag.elt event)) - (Node.M.add_change Bag.elt Bag.add node) - value event valuetable.events - } in - t.env.value <- valuetable - - let attach_node t node dem event = + match Node.M.find_opt node t.env.values with + | None -> + let valuetable = get_table_value t.env value in + let valuetable = { + valuetable with + events = Node.M.add_change Bag.elt Bag.add node f valuetable.events + } + in + ValueTable.set t.env.value value valuetable + | Some v -> + match Nodes.Value.kind v with + | Value (value',v) -> + match ValueKind.Eq.eq_type value value' with + | Neq -> (* Already registered with different value *) + Debug.dprintf0 debug_few "[Egraph] Strange value wait with different value than already set"; + | Eq -> + ignore (run_events t (fun t f -> f t node v) (Bag.elt f)) + + let attach_repr t node f = let node = find_def t node in - let event = Events.Wait.Event (dem,event) in - t.env.event_repr <- Node.M.add_change Bag.elt Bag.add node event t.env.event_repr + t.env.event_repr <- Node.M.add_change Bag.elt Bag.add node f t.env.event_repr - let attach_any_node t dem event = - let event = Events.Wait.Event (dem,event) in - t.env.event_any_repr <- event :: t.env.event_any_repr + let attach_any_repr t f = + t.env.event_any_repr <- Bag.add f t.env.event_any_repr - let attach_any_value t node dem event = + let attach_any_value t node f = let node = find_def t node in - let event = Events.Wait.Event (dem,event) in - t.env.event_value <- Node.M.add_change Bag.elt Bag.add node event t.env.event_value - - let attach_reg_node t node dem event = - let event = Events.Wait.Event (dem,event) in + match Node.M.find_opt node t.env.values with + | None -> + let node = find_def t node in + t.env.event_value <- Node.M.add_change Bag.elt Bag.add node f t.env.event_value + | Some v -> + ignore (run_event t (fun t f -> f t node v) f) + + let attach_reg_node t node f = match find t node with | node -> (** already registered *) - ignore (Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node) + ignore (run_event t (fun t e -> e t node) f) | exception NotRegistered -> - (* deletion of events are not taken into account *) - ignore (t.env.event_reg <- - Node.M.add_change Lists.singleton Lists.add node event t.env.event_reg) + t.env.event_reg <- + Node.M.add_change Bag.elt Bag.add node f t.env.event_reg - let attach_reg_any t dem event = - let event = Events.Wait.Event (dem,event) in + let attach_reg_any t f = (* todo already registered ? *) - (* match find t node with - * | node -> (\** already registered *\) - * Wait.wakeup_events_list Events.Wait.translate_regnode t (Some [event]) node - * | exception NotRegistered -> *) - t.env.event_any_reg <- event::t.env.event_any_reg - - let attach_reg_sem (type a) t (sem : a ThTermKind.t) dem event = - let event = Events.Wait.Event (dem,event) in + t.env.event_any_reg <- Bag.add f t.env.event_any_reg + + let attach_reg_sem (type a) t (sem : (a,_) ThTermKind.t) f = let reg_events = get_table_sem t.env sem in - let reg_events = event::reg_events in - ThTermKind.Vector.set t.env.sem sem reg_events - - let attach_reg_value (type a) t (value : a ValueKind.t) dem event = - let event = Events.Wait.Event (dem,event) in - let value_table = t.env.value in - let reg_events = event::(ValueKind.M.find_def [] value value_table.reg_events) in - t.env.value <- - {value_table with reg_events = - ValueKind.M.add value reg_events value_table.reg_events} - - let attach_any_dom (type a) t (dom : a DomKind.t) dem event = - let event = Events.Wait.Event (dem,event) in + let reg_events = Bag.add f reg_events in + VSemTable.set t.env.sem sem reg_events + + let attach_reg_value (type a) t (value : (a,_) ValueKind.t) f = + let table = get_table_value t.env value in + ValueTable.set t.env.value value + { table with reg_events = Bag.add f table.reg_events } + + let attach_any_dom (type a) t (dom : a DomKind.t) f = let dom_table = get_table_dom t.env dom in - let reg_events = event::dom_table.reg_events in + let reg_events = Bag.add f dom_table.reg_events in VDomTable.set t.env.dom dom {dom_table with reg_events} @@ -1062,16 +1075,14 @@ module Backtrackable = struct repr = Node.M.empty; rang = Node.M.empty; event_repr = Node.M.empty; - event_any_repr = []; + event_any_repr = Bag.empty; event_value = Node.M.empty; event_reg = Node.M.empty; - event_any_reg = []; + event_any_reg = Bag.empty; dom = VDomTable.create 5; sem = VSemTable.create 5; - value = { reg_events = ValueKind.M.empty; - values = Node.M.empty; - events = ValueKind.M.empty; - }; + value = ValueTable.create 5; + values = Node.M.empty; envs = Env.Saved.VectorH.create 5; unsaved_envs = Env.Unsaved.VectorH.create 5; delayed; @@ -1190,39 +1201,51 @@ end module Getter : Getter with type t = Backtrackable.t = Backtrackable module type Ro = sig + type ro type t include Getter with type t := t - (** {3 Immediate information} *) val register : t -> Node.t -> unit + (** Add a new node to register *) (** {3 Attach Event} *) (** todo rename events and attachment *) - val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + 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 -> ('event,'r) Events.Dem.t -> 'event -> unit + + 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 -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_value: t -> 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 -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_any_value: t -> 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 -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_reg_any: t -> (ro -> Node.t -> Events.enqueue) -> unit (** wakeup when any node is registered *) - val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + 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 ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + 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 ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_reg_value: t -> ('a,'b) ValueKind.t -> (ro -> 'b -> Events.enqueue) -> unit (** wakeup when a new value is registered *) - val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_repr: t -> Node.t -> (ro -> Node.t -> Events.enqueue) -> unit (** wakeup when it is not anymore the representative class *) - val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_any_repr: t -> (ro -> Node.t -> Events.enqueue) -> unit (** wakeup when a node is not its representative class anymore *) end -module Ro : Ro with type t = Delayed.t = Delayed +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 () diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli index 9473dbe2013c30307c62de870d4eb27a215cbad5..6e9d69e5ee3808f3de60bf99381a1c80d1e4019f 100644 --- a/src_colibri2/core/egraph.mli +++ b/src_colibri2/core/egraph.mli @@ -60,6 +60,7 @@ module type Getter = sig end module type Ro = sig + type ro type t include Getter with type t := t @@ -69,33 +70,44 @@ module type Ro = sig (** {3 Attach Event} *) (** todo rename events and attachment *) - val attach_dom: t -> Node.t -> 'a DomKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + 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 -> ('event,'r) Events.Dem.t -> 'event -> unit + + 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 -> Node.t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_value: t -> 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 -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_any_value: t -> 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 -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_reg_any: t -> (ro -> Node.t -> Events.enqueue) -> unit (** wakeup when any node is registered *) - val attach_reg_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + 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 ThTermKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + 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 ValueKind.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_reg_value: t -> ('a,'b) ValueKind.t -> (ro -> 'b -> Events.enqueue) -> unit (** wakeup when a new value is registered *) - val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_repr: t -> Node.t -> (ro -> Node.t -> Events.enqueue) -> unit (** wakeup when it is not anymore the representative class *) - val attach_any_node: t -> ('event,'r) Events.Dem.t -> 'event -> unit + + val attach_any_repr: t -> (ro -> Node.t -> Events.enqueue) -> unit (** wakeup when a node is not its representative class anymore *) end -module Ro : Ro +type ro + +module Ro : Ro with type t = ro and type ro = ro type t = private Ro.t -include Ro with type t := t +include Ro with type t := t and type ro := Ro.t (** {3 Immediate modifications} *) val set_dom : t -> 'a DomKind.t -> Node.t -> 'a -> unit @@ -128,7 +140,7 @@ val register_decision: t -> choice -> unit [choose_decision] of the [Cho] will be called at that time to know if the decision is still needed. *) -val register_delayed_event: t -> (_,'a) Events.Dem.t -> 'a -> unit +val register_delayed_event: t -> 'a Events.Dem.t -> 'a -> unit (** register an event for later. *) val contradiction: t -> 'b diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml index bad08ebd9776cb66695537c8ebde5dacd3059d08..7f018748a98cfdbceb71808f5afb9a6c437f2f4c 100644 --- a/src_colibri2/core/events.ml +++ b/src_colibri2/core/events.ml @@ -18,274 +18,109 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -open Colibri2_popop_lib -open Nodes - -let debug = Debug.register_info_flag ~desc:"for the events" "Egraph.events" - (** Dem *) -module Dem = Keys.Make_key2(struct end) - -module Print = struct (** Cutting the knot for pp *) - - type pdem_event = { mutable - pdem_event : 'k 'd. ('k,'d) Dem.t -> 'k Format.printer} +module Dem = Keys.Make_key () - let pdem_event : pdem_event = - {pdem_event = fun _ _ _ -> assert false} (** called too early *) - let dem_event dem fmt s = pdem_event.pdem_event dem fmt s +module Print = struct + (** Cutting the knot for pp *) - type pdem_runable = { mutable - pdem_runable : 'k 'd. ('k,'d) Dem.t -> 'd Format.printer} + type pdem_runable = { + mutable pdem_runable : 'd. 'd Dem.t -> 'd Format.printer; + } + (** called too early *) let pdem_runable : pdem_runable = - {pdem_runable = fun _ _ _ -> assert false} (** called too early *) - + { pdem_runable = (fun _ _ _ -> assert false) } end +type delay = Immediate | Delayed_by of int | LastEffort of int | FixingModel -module Fired = struct - type 'b event = - (** the domain dom of the class change *) - | EventDom : Node.t * 'a DomKind.t * 'b -> 'b event - (** the value of the class has been set *) - | EventValue : Node.t * Value.t * 'b -> 'b event - (** a new theory term 'a point to this class (not complete) *) - | EventSem : Node.t * 'a ThTermKind.t * 'a * 'b -> 'b event - (** we want to register a class *) - | EventReg : Node.t * 'b -> 'b event - (** we want to register this class *) - | EventRegNode : Node.t * 'b -> 'b event - (** This class is not the representant of its eq-class anymore *) - | EventChange : Node.t * 'b -> 'b event - (** a new semantical term 'a appear *) - | EventRegSem : ThTerm.t * 'b -> 'b event - (** a new value 'a appear *) - | EventRegValue : Value.t * 'b -> 'b event - - let pp fmt = function - | EventDom (node, dom, _) -> - Format.fprintf fmt "dom:%a of %a" DomKind.pp dom Node.pp node - | EventValue (node, value, _) -> - Format.fprintf fmt "value:%a of %a" Value.pp value Node.pp node - | EventSem (node, sem, v, _) -> - Format.fprintf fmt "sem:%a of %a with %a" - ThTermKind.pp sem Node.pp node (print_thterm sem) v - | EventReg (node, _) -> - Format.fprintf fmt "any registration of %a" Node.pp node - | EventRegNode (node, _) -> - Format.fprintf fmt "registration of %a" Node.pp node - | EventChange (node, _) -> - Format.fprintf fmt "change of %a" Node.pp node - | EventRegSem (thterm, _) -> - let node = Only_for_solver.node_of_thterm thterm in - begin match Only_for_solver.sem_of_node thterm with - | Only_for_solver.ThTerm(sem,v) -> - Format.fprintf fmt "registration of sem:%a of %a with %a" - ThTermKind.pp sem Node.pp node (print_thterm sem) v - end - | EventRegValue (nodevalue, _) -> - let node = Only_for_solver.node_of_nodevalue nodevalue in - begin match Value.kind nodevalue with - | Value(value,v) -> - Format.fprintf fmt "registration of value:%a of %a with %a" - ValueKind.pp value Node.pp node (print_value value) v - end - - let get_data = function - | EventDom (_, _ , d) -> d - | EventValue (_, _ , d) -> d - | EventSem (_, _, _, d) -> d - | EventReg (_, d) -> d - | EventRegNode (_, d) -> d - | EventChange (_, d) -> d - | EventRegSem (_, d) -> d - | EventRegValue (_,d) -> d - - type 'b t = 'b event list -end - -type delay = - | Immediate - | Delayed_by of int - | LastEffort of int - | FixingModel +type enqueue = + | EnqRun : 'r Dem.t * 'r -> enqueue (** Schedule a daemon run *) + | EnqLast : 'r Dem.t * 'r -> enqueue + (** Same as EnqRun but remove the waiting event *) + | EnqAlready : enqueue (** Don't run but keep the waiting event *) + | EnqStopped : enqueue (** Stop and don't run *) module Wait = struct - type t = - | Event: ('k,'d) Dem.t * 'k -> t - - let pp fmt = function - | Event (dem, event) -> - let f (type k) (type d) (dem:(k,d) Dem.t) (event : k) = - Format.fprintf fmt "Demon %a event %a" - Dem.pp dem (Print.dem_event dem) event - in - f dem event - - type _ enqueue = - | EnqRun: 'r -> 'r enqueue - | EnqLast: 'r -> 'r enqueue - | EnqAlready: _ enqueue - | EnqRedirected: ('e,'r) Dem.t * 'e -> _ enqueue - | EnqStopped: _ enqueue - - type daemon_key = - | DaemonKey: ('k,'runable) Dem.t * 'runable -> daemon_key - - - type 'a translate = { translate : 'd. 'a -> 'd -> 'd Fired.event} - - let translate_dom = - {translate = fun (node,dom) data -> EventDom(node,dom,data)} - let translate_value = - {translate = fun (node,value) data -> EventValue(node,value,data)} - let translate_reg = - {translate = fun node data -> EventReg(node,data)} - let translate_regnode = - {translate = fun node data -> EventRegNode(node,data)} - let translate_change = - {translate = fun node data -> EventChange(node,data)} - let translate_regsem = - {translate = fun thterm data -> EventRegSem(thterm,data)} - let translate_regvalue = - {translate = fun nodeval data -> EventRegValue(nodeval,data)} - + type daemon_key = DaemonKey : 'runable Dem.t * 'runable -> daemon_key module type S = sig type delayed + type delayed_ro - module type Dem = - sig + module type Dem = sig type runable - val print_runable : runable Format.printer - val run : delayed -> runable -> runable option - type event - val print_event : event Format.printer - val enqueue : delayed_ro -> event Fired.event -> runable enqueue - val key : (event, runable) Dem.t - val delay : delay - end - - val register_dem : (module Dem with type event = 'k and type runable = 'd) -> unit - val get_dem : ('k, 'd) Dem.t -> (module Dem with type event = 'k and type runable = 'd) + val print_runable : runable Format.printer - val get_priority: daemon_key -> delay + val run : delayed -> runable -> unit - val print_dem_event : ('a, 'b) Dem.t -> 'a Format.printer + val key : runable Dem.t - val print_dem_runable : ('a, 'b) Dem.t -> 'b Format.printer + val delay : delay + end - val new_pending_daemon : delayed -> ('a, 'b) Dem.t -> 'b -> unit + val register_dem : (module Dem with type runable = 'd) -> unit - val wakeup_event : 'a translate -> delayed -> 'a -> t -> t option + val get_dem : 'd Dem.t -> (module Dem with type runable = 'd) - val wakeup_events_list : - 'a translate -> delayed -> t list option -> 'a -> t list option + val get_priority : daemon_key -> delay - val wakeup_events_bag : - 'a translate -> delayed -> t Bag.t option -> 'a -> t Bag.t option + val print_dem_runable : 'b Dem.t -> 'b Format.printer val is_well_initialized : unit -> bool end - module Make(S:sig - type delayed - val schedule_immediate: delayed -> daemon_key -> unit - val schedule: delayed -> daemon_key -> unit - - type delayed_ro - val readonly : delayed -> delayed_ro - end) : S with type delayed = S.delayed - and type delayed_ro = S.delayed_ro = 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 type delayed = S.delayed + type delayed_ro = S.delayed_ro module type Dem = sig type runable - val print_runable: runable Format.printer - val run: delayed -> runable -> runable option - type event - val print_event: event Format.printer - val enqueue: delayed_ro -> event Fired.event -> runable enqueue + val print_runable : runable Format.printer + + val run : delayed -> runable -> unit + + val key : runable Dem.t - val key: (event,runable) Dem.t - val delay: delay + val delay : delay end - module Registry = Dem.Make_Registry(struct - type ('k,'d) data = (module Dem with type event = 'k and type runable = 'd) - let ppk (type k) (type d) (dem: (k,d) data) = - let module Dem = (val dem) in - Dem.print_event - let ppd (type k) (type d) (dem: (k,d) data) = - let module Dem = (val dem) in - Dem.print_runable - let key (type k) (type d) (dem: (k,d) data) = - let module Dem = (val dem) in - Dem.key - end - ) + module Registry = Dem.Make_Registry (struct + type 'd data = (module Dem with type runable = 'd) + + let pp (type d) (dem : d data) = + let module Dem = (val dem) in + Dem.print_runable + + let key (type d) (dem : d data) = + let module Dem = (val dem) in + Dem.key + end) let register_dem = Registry.register + let get_dem = Registry.get let get_priority = function - | DaemonKey(dem,_) -> - let module Dem = (val get_dem dem) in - Dem.delay + | DaemonKey (dem, _) -> + let module Dem = (val get_dem dem) in + Dem.delay - let print_dem_event = Registry.printk - let () = Print.pdem_event.Print.pdem_event <- print_dem_event + let print_dem_runable = Registry.print - let print_dem_runable = Registry.printd let () = Print.pdem_runable.Print.pdem_runable <- print_dem_runable let is_well_initialized = Registry.is_well_initialized - - let new_pending_daemon (type k) (type d) t (dem:(k,d) Dem.t) runable = - let module Dem = (val get_dem dem) in - let daemonkey = DaemonKey(dem, runable) in - match Dem.delay with - | Immediate -> S.schedule_immediate t daemonkey - | _ -> S.schedule t daemonkey - - let wakeup_event translate t info wevent = - match wevent with - | Event (dem,event) -> - let rec f : type event r. S.delayed -> (event,r) Dem.t -> event -> _ -> _ = - fun t dem event wevent -> - let module Dem = (val get_dem dem) in - let event = translate.translate info event in - match Dem.enqueue (S.readonly t) event with - | EnqStopped -> None - | EnqAlready -> Some wevent - | EnqRedirected(dem,event) -> f t dem event (Event(dem,event)) - | EnqRun runable -> new_pending_daemon t dem runable; Some wevent - | EnqLast runable -> new_pending_daemon t dem runable; None - in - f t dem event wevent - - let wakeup_events_list translate t events info = - match events with - | None | Some [] -> - Debug.dprintf0 debug "[Egraph] @[No scheduling@]"; - None - | Some events -> - Some (Lists.filter_map_homo (wakeup_event translate t info) events) - - let wakeup_events_bag translate t events info = - let is_empty = match events with - | None -> true - | Some events -> Bag.is_empty events in - if is_empty then (Debug.dprintf0 debug "[Egraph] @[No scheduling@]"; None) - else Some (Bag.filter_map_homo (wakeup_event translate t info) (Opt.get events)) - - end end diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli index 1ea2393049b9d076400d0623bbf65d0410adebb0..66cd00bd7f1fd55bb14387eb483e4fd9638f5877 100644 --- a/src_colibri2/core/events.mli +++ b/src_colibri2/core/events.mli @@ -18,126 +18,57 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -open Colibri2_popop_lib -open Nodes - -module Fired : sig - type 'b event = - (** the domain dom of the class change *) - | EventDom : Node.t * 'a DomKind.t * 'b -> 'b event - (** the value of the node has been set *) - | EventValue : Node.t * Value.t * 'b -> 'b event - (** a new semantical term 'a point to this class (not complete) *) - | EventSem : Node.t * 'a ThTermKind.t * 'a * 'b -> 'b event - (** we want to register a class *) - | EventReg : Node.t * 'b -> 'b event - (** we want to register this class *) - | EventRegNode : Node.t * 'b -> 'b event - (** This class is not the representant of its eq-class anymore *) - | EventChange : Node.t * 'b -> 'b event - (** a new semantical term 'a appear *) - | EventRegSem : ThTerm.t * 'b -> 'b event - (** a new value 'a appear *) - | EventRegValue : Value.t * 'b -> 'b event - - val pp: 'b event Format.printer - val get_data: 'b event -> 'b - - type 'b t = 'b event list - -end - -module Dem: Keys.Key2 +module Dem : Keys.Key type delay = | Immediate - | Delayed_by of int - (** Must be strictly positive *) + | Delayed_by of int (** Must be strictly positive *) | LastEffort of int - (** Should try to ensure that a model exists, must be strictly positive *) + (** Should try to ensure that a model exists, must be strictly positive *) | FixingModel -module Wait : sig - type t = - | Event: ('k,'d) Dem.t * 'k -> t - - - type _ enqueue = - | EnqRun: 'r -> 'r enqueue - (** Schedule a daemon run *) - | EnqLast: 'r -> 'r enqueue - (** Same as EnqRun but remove the waiting event *) - | EnqAlready: _ enqueue - (** Don't run but keep the waiting event *) - | EnqRedirected: ('e,'r) Dem.t * 'e -> _ enqueue - (** Run another daemon *) - | EnqStopped: _ enqueue - (** Stop and don't run *) +type enqueue = + | EnqRun : 'r Dem.t * 'r -> enqueue (** Schedule a daemon run *) + | EnqLast : 'r Dem.t * 'r -> enqueue + (** Same as EnqRun but remove the waiting event *) + | EnqAlready : enqueue (** Don't run but keep the waiting event *) + | EnqStopped : enqueue (** Stop and don't run *) - type daemon_key = - | DaemonKey: ('k,'runable) Dem.t * 'runable -> daemon_key - - val pp: t Format.printer - - type 'a translate = { translate : 'd. 'a -> 'd -> 'd Fired.event} - - val translate_dom : (Node.t * 'a DomKind.t) translate - val translate_value : (Node.t * Value.t) translate - val translate_reg : Node.t translate - val translate_regnode : Node.t translate - val translate_change : Node.t translate - val translate_regsem : ThTerm.t translate - val translate_regvalue : Value.t translate +module Wait : sig + type daemon_key = DaemonKey : 'runable Dem.t * 'runable -> daemon_key module type S = sig type delayed + type delayed_ro - module type Dem = - sig + module type Dem = sig type runable - val print_runable : runable Format.printer - val run : delayed -> runable -> runable option - (** The function run after the delay, - a new run can be scheduled using the result *) - - type event - val print_event : event Format.printer - val enqueue : delayed_ro -> event Fired.event -> runable enqueue - val key : (event, runable) Dem.t - val delay : delay - end - val register_dem : (module Dem with type event = 'k and type runable = 'd) -> unit - - val get_dem : ('k, 'd) Dem.t -> (module Dem with type event = 'k and type runable = 'd) + val print_runable : runable Format.printer - val get_priority: daemon_key -> delay + val run : delayed -> runable -> unit + (** The function run after the delay *) - val print_dem_event : ('a, 'b) Dem.t -> 'a Format.printer + val key : runable Dem.t - val print_dem_runable : ('a, 'b) Dem.t -> 'b Format.printer + val delay : delay + end - val new_pending_daemon : delayed -> ('a, 'b) Dem.t -> 'b -> unit + val register_dem : (module Dem with type runable = 'd) -> unit - val wakeup_event : 'a translate -> delayed -> 'a -> t -> t option + val get_dem : 'd Dem.t -> (module Dem with type runable = 'd) - val wakeup_events_list : - 'a translate -> delayed -> t list option -> 'a -> t list option + val get_priority : daemon_key -> delay - val wakeup_events_bag : - 'a translate -> delayed -> t Bag.t option -> 'a -> t Bag.t option + val print_dem_runable : 'b Dem.t -> 'b Format.printer val is_well_initialized : unit -> bool end + module Make (S : sig + type delayed - module Make(S:sig - type delayed - val schedule_immediate: delayed -> daemon_key -> unit - val schedule: delayed -> daemon_key -> unit - - type delayed_ro - val readonly : delayed -> delayed_ro - end) : S with type delayed = S.delayed and type delayed_ro = S.delayed_ro + type delayed_ro + end) : S with type delayed = S.delayed and type delayed_ro = S.delayed_ro end diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml index a4bf75be8e63dea8943ea45bfb725326921ac96b..28dd54fe5112e8df3dbe9b1f46423ef84e754e2e 100644 --- a/src_colibri2/core/ground.ml +++ b/src_colibri2/core/ground.ml @@ -210,7 +210,7 @@ module Term = struct include T include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T) - let key = ThTermKind.create_key (module struct type t = T.t let name = "ground" end) + let name = "ground" end @@ -244,7 +244,7 @@ module ClosedQuantifier = struct include T include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T) - let key = ThTermKind.create_key (module struct type t = T.t let name = "ClosedQuantifier" end) + let name = "ClosedQuantifier" end @@ -289,7 +289,7 @@ module NotTotalyApplied = struct include T include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T) - let key = ThTermKind.create_key (module struct type t = T.t let name = "ClosedLambda" end) + let name = "ClosedLambda" end @@ -423,7 +423,7 @@ let register_converter d f = Datastructure.Push.push registered_converter d f let dom_tys = - DomKind.create_key + DomKind.create (module struct type nonrec t = Ty.S.t @@ -458,21 +458,19 @@ let add_ty d n ty = ) let init d = - Demon.Fast.register_init_daemon ~name:"Ground.convert" - (module ThTerm) + Demon.Simple.attach_reg_sem d + ThTerm.key (fun d g -> let n = ThTerm.node g in let s = ThTerm.sem g in add_ty d n s.ty; Defs.converter d g; - Datastructure.Push.iter registered_converter d ~f:(fun f -> f d g)) - d; - Demon.Fast.register_init_daemon ~name:"Ground.convert" - (module ThClosedQuantifier) + Datastructure.Push.iter registered_converter d ~f:(fun f -> f d g)); + Demon.Simple.attach_reg_sem d + ThClosedQuantifier.key (fun d g -> let n = ThClosedQuantifier.node g in add_ty d n Ty.bool ) - d include ThTerm diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli index 9439eb7131906185519cd392375dd6e7cc060774..cefc6c277c9ee412884149c61950056076e5f271 100644 --- a/src_colibri2/core/ground.mli +++ b/src_colibri2/core/ground.mli @@ -67,7 +67,7 @@ module Ty: sig (** The type of propositions *) val bool : t - (** Alias for {prop}. *) + (** Alias for {!prop}. *) val unit : t (** The unit type. *) @@ -101,8 +101,6 @@ module Term: sig ty:Ty.t } - val key: t ThTermKind.t - include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t end @@ -145,3 +143,25 @@ module ClosedQuantifier : sig end module ThClosedQuantifier : RegisteredThTerm with type s = ClosedQuantifier.t + +module NotTotalyApplied : sig + type t = + | Lambda of { + subst: Subst.t; + ty_vars: Expr.Ty.Var.t list; + term_vars: Expr.Term.Var.t list; + body: Expr.Term.t; + ty: Ty.t; + } + | Cst of Expr.Term.Const.t + | App of { + app: Node.t; + tyargs : Ty.t list; + args : Node.t IArray.t; + ty: Ty.t; + } + [@@deriving eq, ord, hash] + +end + +module ThNotTotalyApplied : RegisteredThTerm with type s = NotTotalyApplied.t diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml index b66b688d07a1a27026b247f9e369e7db8ca0a345..6ccb08641f8ff8e9932025065d71a1b878512484 100644 --- a/src_colibri2/core/interp.ml +++ b/src_colibri2/core/interp.ml @@ -47,7 +47,7 @@ module Data = struct (* let reg_node = Datastructure.Push.create Fmt.nop "Interp.reg_node" *) let env = - Env.Saved.create_key + Env.Saved.create (module struct type t = env @@ -348,21 +348,10 @@ module WatchArgs = struct let print_runable = Fmt.nop - type event = t - - let print_event = Fmt.nop - - let enqueue _ event = - match event with - | Events.Fired.EventValue (_, _, d) -> Events.Wait.EnqRun d - | _ -> raise Impossible - let key = - Events.Dem.create_key + Events.Dem.create (module struct - type d = runable - - type t = event + type t = runable let name = "Interp.WatchArgs" end) @@ -376,17 +365,17 @@ module WatchArgs = struct if IArray.length args <= i then None else check_if_set d args i let attach d r i = - Egraph.attach_any_value d (IArray.get (Ground.sem r.ground).args i) key r + Egraph.attach_any_value d (IArray.get (Ground.sem r.ground).args i) + (fun _ _ _ -> Events.EnqRun (key, r)) let run d r = let o_current = Context.Ref.get r.current in assert (o_current < IArray.length (Ground.sem r.ground).args); - (match check_if_set d (Ground.sem r.ground).args o_current with + match check_if_set d (Ground.sem r.ground).args o_current with | None -> r.callback d r.ground | Some current -> assert (current <> o_current); - attach d r current); - None + attach d r current let create d callback ground = if IArray.is_empty (Ground.sem ground).args then callback d ground diff --git a/src_colibri2/core/structures/nodes.ml b/src_colibri2/core/structures/nodes.ml index 5e6239f6a12cee646f716971f28fcba9485884df..e64e0eab1076bc98f4d92fff51e38a9c73999d66 100644 --- a/src_colibri2/core/structures/nodes.ml +++ b/src_colibri2/core/structures/nodes.ml @@ -22,63 +22,40 @@ open Colibri2_popop_lib open Popop_stdlib exception BrokenInvariant of string -exception SolveSameRepr -exception UnwaitedEvent -exception AlreadyDead -exception AlreadyRedirected - -let debug_create = Debug.register_info_flag - ~desc:"for the core solver class creation information" - "index" - -module ThTermKind = Keys.Make_key(struct end) -module ValueKind = Keys.Make_key(struct end) +exception SolveSameRepr -module type ThTerm = sig - include Popop_stdlib.Datatype - val key: t ThTermKind.t -end +exception UnwaitedEvent -module ThTermRegistry = ThTermKind.Make_Registry(struct - type 'a data = (module ThTerm with type t = 'a) - let pp (type a) ((module ThTerm): a data) = ThTerm.pp - let key (type a) ((module ThTerm): a data) = ThTerm.key - end) +exception AlreadyDead -let check_thterm_registered = ThTermRegistry.check_is_registered -let print_thterm = ThTermRegistry.print -let get_thterm = ThTermRegistry.get +exception AlreadyRedirected -module type Value = sig - include Popop_stdlib.Datatype - val key: t ValueKind.t -end +let debug_create = + Debug.register_info_flag + ~desc:"for the core solver class creation information" "index" -module ValueRegistry = ValueKind.Make_Registry(struct - type 'a data = (module Value with type t = 'a) - let pp (type a) ((module V): a data) = V.pp - let key (type a) ((module V): a data) = V.key - end) +module ThTermKind = Keys.Make_key2 () -let check_value_registered = ValueRegistry.check_is_registered -let print_value = ValueRegistry.print -let get_value = ValueRegistry.get +module ValueKind = Keys.Make_key2 () module Node = struct type 'a r = - | ThTerm : int * 'a ThTermKind.t * 'a -> [`ThTerm] r - | Value : int * 'a ValueKind.t * 'a -> [`Value] r + | ThTerm : int * ('a, _) ThTermKind.t * 'a -> [ `ThTerm ] r + | Value : int * ('a, _) ValueKind.t * 'a -> [ `Value ] r type t' = All : _ r -> t' [@@unboxed] - type thterm = [`ThTerm] r - type nodevalue = [`Value] r - let tag: t' -> int = function - | All(ThTerm(tag,_,_)) -> tag - | All(Value(tag,_,_)) -> tag + type thterm = [ `ThTerm ] r + + type nodevalue = [ `Value ] r + + let tag : t' -> int = function + | All (ThTerm (tag, _, _)) -> tag + | All (Value (tag, _, _)) -> tag let names = Simple_vector.create 100 + let used_names : (* next id to use *) int DStr.H.t = DStr.H.create 100 (** remove the empty string *) @@ -88,10 +65,13 @@ module Node = struct Format.pp_print_char fmt '@'; Format.pp_print_string fmt (Simple_vector.get names (tag x)) - module T = Popop_stdlib.MakeMSH(struct - type t = t' let tag = tag - let pp = pp - end) + module T = Popop_stdlib.MakeMSH (struct + type t = t' + + let tag = tag + + let pp = pp + end) include T @@ -101,330 +81,388 @@ module Node = struct let s = Strings.find_new_name used_names s in Simple_vector.set names (tag node) s - module ThTermIndex = ThTermKind.MkVector - (struct type ('a,_) t = 'a -> thterm end) + module ThTermIndex = ThTermKind.MkVector (struct + type ('a, _, _) t = 'a -> thterm + end) let semindex : unit ThTermIndex.t = ThTermIndex.create 8 - let thterm sem v : thterm = - ThTermRegistry.check_is_registered sem; - ThTermIndex.get semindex sem v + let thterm sem v : thterm = ThTermIndex.get semindex sem v - module ValueIndex = ValueKind.MkVector - (struct type ('a,'unedeed) t = 'a -> nodevalue end) + module ValueIndex = ValueKind.MkVector (struct + type ('a, 'unedeed, _) t = 'a -> nodevalue + end) let valueindex : unit ValueIndex.t = ValueIndex.create 8 - let nodevalue value v : nodevalue = - ValueRegistry.check_is_registered value; - ValueIndex.get valueindex value v + let nodevalue value v : nodevalue = ValueIndex.get valueindex value v let of_thterm : thterm -> t = fun t -> All t + let of_nodevalue : nodevalue -> t = fun t -> All t - let index_sem sem v = of_thterm (thterm sem v) - let index_value sem v = of_nodevalue (nodevalue sem v) + let index_sem sem v = of_thterm (thterm sem v) + let index_value sem v = of_nodevalue (nodevalue sem v) end -module ThTerm = struct - include Popop_stdlib.MakeMSH(struct - type t = Node.thterm - let tag: t -> int = function - | Node.ThTerm(tag,_,_) -> tag - let pp fmt : t -> unit = function - | Node.ThTerm(_,sem,v) -> print_thterm sem fmt v - end) - - let index = Node.thterm - let node = Node.of_thterm +module type NamedDatatype = sig + include Popop_stdlib.Datatype + val name : string end module type RegisteredThTerm = sig type s - val key: s ThTermKind.t - (** thterm *) + + module SD : NamedDatatype with type t = s + include Datatype + (** thterm *) + + val key : (s, t) ThTermKind.t - val index: s -> t + val index : s -> t (** Return a thterm from a semantical value *) - val node: t -> Node.t + val node : t -> Node.t (** Return a node from a thterm *) - val sem: t -> s + val sem : t -> s (** Return the sem from a thterm *) - val thterm: t -> ThTerm.t - val of_thterm: ThTerm.t -> t option + val thterm : t -> Node.thterm + + val of_thterm : Node.thterm -> t option + + val coerce_thterm : Node.thterm -> t +end + +module ThTermRegistry = ThTermKind.Make_Registry (struct + type ('k, 'd) data = + (module RegisteredThTerm with type s = 'k and type t = 'd) + + let ppk (type k d) ((module ThTerm) : (k, d) data) = ThTerm.SD.pp + + let ppd (type k d) ((module ThTerm) : (k, d) data) = ThTerm.pp + + let key (type k d) ((module ThTerm) : (k, d) data) = ThTerm.key +end) + +let check_thterm_registered = ThTermRegistry.check_is_registered + +let print_thterm = ThTermRegistry.printk + +let get_thterm = ThTermRegistry.get + +module type RegisteredValue = sig + type s + + module SD : NamedDatatype with type t = s + + include Datatype + (** nodevalue *) + + val key : (s, t) ValueKind.t + + val index : ?basename:string -> s -> t + (** Return a nodevalue from a valueantical value *) + + val node : t -> Node.t + (** Return a class from a nodevalue *) + + val value : t -> s + (** Return the value from a nodevalue *) + + val nodevalue : t -> Node.nodevalue + + val of_nodevalue : Node.nodevalue -> t option + + val coerce_nodevalue : Node.nodevalue -> t +end + +module ValueRegistry = ValueKind.Make_Registry (struct + type ('k, 'd) data = (module RegisteredValue with type s = 'k and type t = 'd) + + let ppk (type k d) ((module Value) : (k, d) data) = Value.SD.pp + + let ppd (type k d) ((module Value) : (k, d) data) = Value.pp + + let key (type k d) ((module Value) : (k, d) data) = Value.key +end) + +let check_value_registered = ValueRegistry.check_is_registered + +let print_value = ValueRegistry.printk + +let get_value = ValueRegistry.get + +module ThTerm = struct + include Popop_stdlib.MakeMSH (struct + type t = Node.thterm + + let tag : t -> int = function Node.ThTerm (tag, _, _) -> tag - val coerce_thterm: ThTerm.t -> t + let pp fmt : t -> unit = function + | Node.ThTerm (_, sem, v) -> print_thterm sem fmt v + end) + let index = Node.thterm + + let node = Node.of_thterm end +module RegisterThTerm (D : NamedDatatype) : RegisteredThTerm with type s = D.t = +struct + module All = struct + module SD = D + + let key = + ThTermKind.create + (module struct + let name = D.name + type t = D.t -module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t = struct + type d = Node.thterm + end) - module HC = Hashcons.MakeTag(struct + module HC = Hashcons.MakeTag (struct open Node + type t = thterm let next_tag = Node.next_tag - let incr_tag = Node.incr_tag - let equal: t -> t -> bool = fun a b -> - match a, b with - | ThTerm(_,sema,va), ThTerm(_,semb,vb) -> - match ThTermKind.Eq.coerce_type sema D.key, - ThTermKind.Eq.coerce_type semb D.key with - | Poly.Eq, Poly.Eq -> D.equal va vb + let incr_tag = Node.incr_tag - let hash: t -> int = fun a -> + let equal : t -> t -> bool = + fun a b -> + match (a, b) with + | ThTerm (_, sema, va), ThTerm (_, semb, vb) -> ( + match + ( ThTermKind.Eq.coerce_type sema key, + ThTermKind.Eq.coerce_type semb key ) + with + | Poly.Eq, Poly.Eq -> D.equal va vb) + + let hash : t -> int = + fun a -> match a with - | ThTerm(_,sema,va) -> - let Poly.Eq = ThTermKind.Eq.coerce_type sema D.key in - (D.hash va) + | ThTerm (_, sema, va) -> + let Poly.Eq = ThTermKind.Eq.coerce_type sema key in + D.hash va - let set_tag: int -> t -> t = - fun tag (ThTerm(_,sem,v)) -> ThTerm(tag,sem,v) + let set_tag : int -> t -> t = + fun tag (ThTerm (_, sem, v)) -> ThTerm (tag, sem, v) - let tag: t -> int = fun (ThTerm(tag,_,_)) -> tag + let tag : t -> int = fun (ThTerm (tag, _, _)) -> tag let pp fmt x = Format.pp_print_char fmt '@'; Format.pp_print_string fmt (Simple_vector.get names (tag x)) end) - include HC - - type s = D.t - let key = D.key - - let tag: t -> int = function - | Node.ThTerm(tag,_,_) -> tag - - let index v = - let node = - HC.hashcons2 - (fun tag sem v -> Node.ThTerm(tag,sem,v)) - D.key v in - let i = tag node in - Simple_vector.inc_size (i+1) Node.names; - begin - if Simple_vector.is_uninitialized Node.names i then - let s = Strings.find_new_name Node.used_names "" - (** TODO use ThTerm.pp or Sem.print_debug *) in - Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]" - s D.pp v; - Simple_vector.set Node.names i s - end; - node - - let node = Node.of_thterm + include HC - let sem : t -> D.t = - fun (Node.ThTerm(_,sem,v)) -> - let Poly.Eq = ThTermKind.Eq.coerce_type sem D.key in v + type s = D.t - let thterm: t -> ThTerm.t = fun x -> x + let tag : t -> int = function Node.ThTerm (tag, _, _) -> tag - let of_thterm: ThTerm.t -> t option = function - | Node.ThTerm(_,sem',_) as v when ThTermKind.equal sem' D.key -> Some v - | _ -> None + let index v = + let node = + HC.hashcons2 (fun tag sem v -> Node.ThTerm (tag, sem, v)) key v + in + let i = tag node in + Simple_vector.inc_size (i + 1) Node.names; + if Simple_vector.is_uninitialized Node.names i then ( + let s = + Strings.find_new_name Node.used_names "" + (* TODO use ThTerm.pp or Sem.print_debug *) + in + Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]" s D.pp v; + Simple_vector.set Node.names i s); + node - let coerce_thterm: ThTerm.t -> t = - fun (Node.ThTerm(_,sem',_) as v) -> assert (ThTermKind.equal sem' D.key); v + let node = Node.of_thterm - let () = - ThTermRegistry.register (module D: ThTerm with type t = D.t); - Node.ThTermIndex.set Node.semindex D.key index + let sem : t -> D.t = + fun (Node.ThTerm (_, sem, v)) -> + let Poly.Eq = ThTermKind.Eq.coerce_type sem key in + v -end + let thterm : t -> ThTerm.t = fun x -> x -module Value = struct - include Popop_stdlib.MakeMSH(struct - type t = Node.nodevalue - let tag: t -> int = function - | Node.Value(tag,_,_) -> tag - let pp fmt : t -> unit = function - | Node.Value(_,value,v) -> print_value value fmt v - end) + let of_thterm : ThTerm.t -> t option = function + | Node.ThTerm (_, sem', _) as v when ThTermKind.equal sem' key -> Some v + | _ -> None - let index = Node.nodevalue - let node = Node.of_nodevalue - - let value : type a. a ValueKind.t -> t -> a option = - fun value (Node.Value(_,value',v)) -> - match ValueKind.Eq.eq_type value value' with - | Poly.Neq -> None - | Poly.Eq -> Some v - - type kind = - | Value: 'a ValueKind.t * 'a -> kind + let coerce_thterm : ThTerm.t -> t = + fun (Node.ThTerm (_, sem', _) as v) -> + assert (ThTermKind.equal sem' key); + v + end - let kind: t -> kind = function - | Node.Value (_,value,v) -> Value(value,v) + let () = + ThTermRegistry.register + (module All : RegisteredThTerm with type s = D.t and type t = All.t); + Node.ThTermIndex.set Node.semindex All.key All.index + include All end -module type RegisteredValue = sig - type s - module V : Value with type t = s - val key: s ValueKind.t - (** nodevalue *) - include Datatype - - val index: ?basename:string -> s -> t - (** Return a nodevalue from a valueantical value *) +module Value = struct + include Popop_stdlib.MakeMSH (struct + type t = Node.nodevalue - val node: t -> Node.t - (** Return a class from a nodevalue *) + let tag : t -> int = function Node.Value (tag, _, _) -> tag - val value: t -> s - (** Return the value from a nodevalue *) + let pp fmt : t -> unit = function + | Node.Value (_, value, v) -> print_value value fmt v + end) - val nodevalue: t -> Value.t - val of_nodevalue: Value.t -> t option + let index = Node.nodevalue - val coerce_nodevalue: Value.t -> t + let node = Node.of_nodevalue -end + let value : type a b. (a, b) ValueKind.t -> t -> a option = + fun value (Node.Value (_, value', v)) -> + match ValueKind.Eq.eq_type value value' with + | Poly.Neq -> None + | Poly.Eq -> Some v + type kind = Value : (_, 'b) ValueKind.t * 'b -> kind -module RegisteredValueRegistry = ValueKind.Make_Registry(struct - type 'a data = (module RegisteredValue with type s = 'a) - let pp (type a) (value: a data) = - let module RegisteredValue = (val value) in - RegisteredValue.V.pp - let key (type a) (value: a data) = - let module RegisteredValue = (val value) in - RegisteredValue.key - end) + let kind : t -> kind = function + | Node.Value (_, value, _) as x -> Value (value, Obj.magic x) +end -let get_registered_value = RegisteredValueRegistry.get +module RegisterValue (D : NamedDatatype) : RegisteredValue with type s = D.t = +struct + module All = struct + let key = + ValueKind.create + (module struct + let name = D.name + type t = D.t -module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct + type d = Node.nodevalue + end) - module All = struct + module SD = D - module V = D - module HC = Hashcons.MakeTag(struct + module HC = Hashcons.MakeTag (struct open Node + type t = nodevalue let next_tag = Node.next_tag - let incr_tag = Node.incr_tag - let equal: t -> t -> bool = fun a b -> - match a, b with - | Value(_,valuea,va), Value(_,valueb,vb) -> - match ValueKind.Eq.coerce_type valuea D.key, - ValueKind.Eq.coerce_type valueb D.key with - | Poly.Eq, Poly.Eq -> D.equal va vb + let incr_tag = Node.incr_tag - let hash: t -> int = fun a -> + let equal : t -> t -> bool = + fun a b -> + match (a, b) with + | Value (_, valuea, va), Value (_, valueb, vb) -> ( + match + ( ValueKind.Eq.coerce_type valuea key, + ValueKind.Eq.coerce_type valueb key ) + with + | Poly.Eq, Poly.Eq -> D.equal va vb) + + let hash : t -> int = + fun a -> match a with - | Value(_,valuea,va) -> - let Poly.Eq = ValueKind.Eq.coerce_type valuea D.key in - (D.hash va) + | Value (_, valuea, va) -> + let Poly.Eq = ValueKind.Eq.coerce_type valuea key in + D.hash va - let set_tag: int -> t -> t = fun tag x -> - match x with - | Value(_,value,v) -> Value(tag,value,v) + let set_tag : int -> t -> t = + fun tag x -> match x with Value (_, value, v) -> Value (tag, value, v) - let tag: t -> int = function - | Value(tag,_,_) -> tag + let tag : t -> int = function Value (tag, _, _) -> tag let pp fmt x = Format.pp_print_char fmt '@'; Format.pp_print_string fmt (Simple_vector.get names (tag x)) end) - include HC + include HC - type s = D.t - let key = D.key + type s = D.t - let tag: t -> int = function - | Node.Value(tag,_,_) -> tag + let tag : t -> int = function Node.Value (tag, _, _) -> tag - let index ?(basename="") v = - let node = - HC.hashcons2 - (fun tag value v -> Node.Value(tag,value,v)) - D.key v in - let i = tag node in - Simple_vector.inc_size (i+1) Node.names; - begin - if Simple_vector.is_uninitialized Node.names i then + let index ?(basename = "") v = + let node = + HC.hashcons2 (fun tag value v -> Node.Value (tag, value, v)) key v + in + let i = tag node in + Simple_vector.inc_size (i + 1) Node.names; + if Simple_vector.is_uninitialized Node.names i then ( let s = Strings.find_new_name Node.used_names basename in - Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]" - s D.pp v; - Simple_vector.set Node.names i s - end; - node - - let node = Node.of_nodevalue + Debug.dprintf3 debug_create "[Egraph] @[@@%s is %a@]" s D.pp v; + Simple_vector.set Node.names i s); + node - let value : t -> D.t = function - | Node.Value(_,value,v) -> - let Poly.Eq = ValueKind.Eq.coerce_type value D.key in v + let node = Node.of_nodevalue - let nodevalue: t -> Value.t = fun x -> x + let value : t -> D.t = function + | Node.Value (_, value, v) -> + let Poly.Eq = ValueKind.Eq.coerce_type value key in + v - let of_nodevalue: Value.t -> t option = function - | Node.Value(_,value',_) as v when ValueKind.equal value' D.key -> Some v - | _ -> None + let nodevalue : t -> Value.t = fun x -> x - let coerce_nodevalue: Value.t -> t = function - | Node.Value(_,value',_) as v -> assert (ValueKind.equal value' D.key); v + let of_nodevalue : Value.t -> t option = function + | Node.Value (_, value', _) as v when ValueKind.equal value' key -> Some v + | _ -> None + let coerce_nodevalue : Value.t -> t = function + | Node.Value (_, value', _) as v -> + assert (ValueKind.equal value' key); + v end include All - let () = - ValueRegistry.register (module D: Value with type t = D.t); - RegisteredValueRegistry.register (module All: RegisteredValue with type s = D.t); - Node.ValueIndex.set Node.valueindex D.key index + let () = + ValueRegistry.register + (module All : RegisteredValue with type s = D.t and type t = All.t); + Node.ValueIndex.set Node.valueindex All.key index end module Only_for_solver = struct - type sem_of_node = - | ThTerm: 'a ThTermKind.t * 'a -> sem_of_node + type sem_of_node = ThTerm : (_, 'b) ThTermKind.t * 'b -> sem_of_node - let thterm: Node.t -> ThTerm.t option = function - | Node.All Node.Value _ -> None + let thterm : Node.t -> ThTerm.t option = function + | Node.All (Node.Value _) -> None | Node.All (Node.ThTerm _ as x) -> Some x - let sem_of_node: ThTerm.t -> sem_of_node = function - | Node.ThTerm (_,sem,v) -> ThTerm(sem,v) + let sem_of_node : ThTerm.t -> sem_of_node = function + | Node.ThTerm (_, sem, _) as v -> ThTerm (sem, Obj.magic v) - let nodevalue: Node.t -> Value.t option = function - | Node.All Node.ThTerm _ -> None + let nodevalue : Node.t -> Value.t option = function + | Node.All (Node.ThTerm _) -> None | Node.All (Node.Value _ as x) -> Some x let node_of_thterm : ThTerm.t -> Node.t = ThTerm.node + let node_of_nodevalue : Value.t -> Node.t = Value.node type opened_node = | ThTerm : ThTerm.t -> opened_node - | Value : Value.t -> opened_node + | Value : Value.t -> opened_node let open_node : Node.t -> opened_node = function | Node.All (Node.ThTerm _ as x) -> ThTerm x | Node.All (Node.Value _ as x) -> Value x let is_value : Node.t -> bool = function - | Node.All(Node.ThTerm _) -> false - | Node.All(Node.Value _) -> true - + | Node.All (Node.ThTerm _) -> false + | Node.All (Node.Value _) -> true end - let check_initialization () = - ThTermRegistry.is_well_initialized () && - ValueRegistry.is_well_initialized () + ThTermRegistry.is_well_initialized () && ValueRegistry.is_well_initialized () diff --git a/src_colibri2/core/structures/nodes.mli b/src_colibri2/core/structures/nodes.mli index 200d5181a5de5ca588fc39f4a0065106d2d92ad9..0740eff1a694076fd87a7c4f4e353f78034d57a9 100644 --- a/src_colibri2/core/structures/nodes.mli +++ b/src_colibri2/core/structures/nodes.mli @@ -26,28 +26,32 @@ open Popop_stdlib (** {2 General exceptions (to move away) } *) exception BrokenInvariant of string + exception SolveSameRepr + exception UnwaitedEvent + exception AlreadyDead + exception AlreadyRedirected +module ThTermKind : Keys.Key2 -module ThTermKind: Keys.Key -module ValueKind: Keys.Key +module ValueKind : Keys.Key2 (** Node *) module Node : sig include Datatype - val rename: t -> string -> unit + val rename : t -> string -> unit (** Change the pretty printed string for this node, to use with care preferably at the start *) - val index_sem: 'a ThTermKind.t -> 'a -> t + val index_sem : ('a, _) ThTermKind.t -> 'a -> t (** Return the corresponding node from a theory term *) - val index_value: 'a ValueKind.t -> 'a -> t + val index_value : ('a, _) ValueKind.t -> 'a -> t (** Return the corresponding node from a value *) end @@ -55,27 +59,19 @@ end (** Basically a theory term type is just something with an ordering. For each theory terms a unique node is associated. *) -module type ThTerm = sig - include Datatype - - val key: t ThTermKind.t -end - +val check_thterm_registered : _ ThTermKind.t -> unit (** {3 Generic Handling of theory terms} *) -val get_thterm: 'a ThTermKind.t -> (module ThTerm with type t = 'a) -val check_thterm_registered: 'a ThTermKind.t -> unit -val print_thterm : 'a ThTermKind.t -> 'a Format.printer +val print_thterm : ('a, _) ThTermKind.t -> 'a Format.printer -module ThTerm: sig +module ThTerm : sig include Datatype - val index: 'a ThTermKind.t -> 'a -> t + val index : ('a, _) ThTermKind.t -> 'a -> t (** Return the corresponding node from a theory term *) - val node: t -> Node.t + val node : t -> Node.t (** Returns the node associated to this theory term *) - end (** {3 Construction of a theory terms } *) @@ -85,31 +81,37 @@ module type RegisteredThTerm = sig type s (** the user given type *) - val key: s ThTermKind.t + module SD : NamedDatatype with type t = s - (** thterm *) include Datatype + (** thterm *) + + val key : (s, t) ThTermKind.t - val index: s -> t + val index : s -> t (** Return a theory term from the user type *) - val node: t -> Node.t + val node : t -> Node.t (** Return a class from a thterm *) - val sem: t -> s + val sem : t -> s (** Return the sem from a thterm *) - val thterm: t -> ThTerm.t - val of_thterm: ThTerm.t -> t option + val thterm : t -> ThTerm.t + + val of_thterm : ThTerm.t -> t option (** Return the user type if the ThTerm belongs to this module *) - val coerce_thterm: ThTerm.t -> t + val coerce_thterm : ThTerm.t -> t (** Return the user type. Raise if the ThTerm does not belong to this module *) - end -module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t +module RegisterThTerm (D : NamedDatatype) : RegisteredThTerm with type s = D.t + +val get_thterm : + ('a, 'b) ThTermKind.t -> + (module RegisteredThTerm with type s = 'a and type t = 'b) (** {2 Values } *) @@ -118,101 +120,93 @@ module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t terms is that only one value of a kind can be in an equivalence class. The solver keep track of which value is associated to an equivalence class (like it does for domains) *) -module type Value = sig - include Datatype - val key: t ValueKind.t -end +val print_value : ('a, _) ValueKind.t -> 'a Format.printer -val print_value : 'a ValueKind.t -> 'a Format.printer -val get_value: 'a ValueKind.t -> (module Value with type t = 'a) -val check_value_registered: 'a ValueKind.t -> unit +val check_value_registered : _ ValueKind.t -> unit (** {3 Module for handling generically values} *) -module Value: sig +module Value : sig include Datatype - val index: 'a ValueKind.t -> 'a -> t + val index : ('a, _) ValueKind.t -> 'a -> t (** Return the corresponding node from a value *) - val node: t -> Node.t - - val value: 'a ValueKind.t -> t -> 'a option + val node : t -> Node.t - type kind = - | Value: 'a ValueKind.t * 'a -> kind + val value : ('a, _) ValueKind.t -> t -> 'a option - val kind: t -> kind - (** give the value associated with a node, make sense only for not merged - class. So only the module solver can use it *) + type kind = Value : (_, 'b) ValueKind.t * 'b -> kind + val kind : t -> kind + (** unpack a value *) end (** {3 For building a particular value} *) module type RegisteredValue = sig type s - module V : Value with type t = s - val key: s ValueKind.t - (** nodevalue *) + module SD : NamedDatatype with type t = s + include Datatype + (** nodevalue *) - val index: ?basename:string -> s -> t + val key : (s, t) ValueKind.t + + val index : ?basename:string -> s -> t (** Return a nodevalue from a valueantical term. Basename is used only for debug *) - val node: t -> Node.t + val node : t -> Node.t (** Return a class from a nodevalue *) - val value: t -> s + val value : t -> s (** Return the value from a nodevalue *) - val nodevalue: t -> Value.t - val of_nodevalue: Value.t -> t option + val nodevalue : t -> Value.t - val coerce_nodevalue: Value.t -> t + val of_nodevalue : Value.t -> t option + val coerce_nodevalue : Value.t -> t end -module RegisterValue (D:Value) : RegisteredValue with type s = D.t +module RegisterValue (D : NamedDatatype) : RegisteredValue with type s = D.t -val get_registered_value: 'a ValueKind.t -> (module RegisteredValue with type s = 'a) +val get_value : + ('a, 'b) ValueKind.t -> + (module RegisteredValue with type t = 'b and type s = 'a) -val check_initialization: unit -> bool +val check_initialization : unit -> bool (** Check if the initialization of all the sem and value have been done *) - (** {2 Only for the solver } *) -module Only_for_solver: sig - type sem_of_node = - | ThTerm: 'a ThTermKind.t * 'a -> sem_of_node +module Only_for_solver : sig + type sem_of_node = ThTerm : (_, 'b) ThTermKind.t * 'b -> sem_of_node - val thterm: - Node.t -> ThTerm.t option - (** give the sem associated with a node, make sense only for not merged + val thterm : Node.t -> ThTerm.t option + (** give the sem associated with a node, make sense only for not merged class. So only the module solver can use it *) - val sem_of_node: - ThTerm.t -> sem_of_node - (** give the sem associated with a node, make sense only for not merged + val sem_of_node : ThTerm.t -> sem_of_node + (** give the sem associated with a node, make sense only for not merged class. So only the module solver can use it *) - val nodevalue: - Node.t -> Value.t option - (** give the value associated with a node, make sense only for not merged + val nodevalue : Node.t -> Value.t option + (** give the value associated with a node, make sense only for not merged class. So only the module solver can use it *) - val node_of_thterm: ThTerm.t -> Node.t - val node_of_nodevalue: Value.t -> Node.t + val node_of_thterm : ThTerm.t -> Node.t + + val node_of_nodevalue : Value.t -> Node.t type opened_node = | ThTerm : ThTerm.t -> opened_node - | Value : Value.t -> opened_node + | Value : Value.t -> opened_node - val open_node: Node.t -> opened_node - val is_value: Node.t -> bool + val open_node : Node.t -> opened_node + val is_value : Node.t -> bool end diff --git a/src_colibri2/popop_lib/popop_stdlib.ml b/src_colibri2/popop_lib/popop_stdlib.ml index f7701f5154de40ddd74850e9eb0f6527d973e2d4..fa2e3fafe04f2d02b98d95d37e2ab76b707ba025 100644 --- a/src_colibri2/popop_lib/popop_stdlib.ml +++ b/src_colibri2/popop_lib/popop_stdlib.ml @@ -85,6 +85,12 @@ module type Datatype = sig include Base.Hashtbl.Key.S with type t := t end +module type NamedDatatype = sig + include Datatype + + val name : string +end + module type Printable = sig include OrderedHashedType val pp: t Pp.pp diff --git a/src_colibri2/popop_lib/popop_stdlib.mli b/src_colibri2/popop_lib/popop_stdlib.mli index 48930dafdfcc6a31a37fa23fd2fbdda97679d66d..df138f324f21f46649a6adf1f8241504cec7da7f 100644 --- a/src_colibri2/popop_lib/popop_stdlib.mli +++ b/src_colibri2/popop_lib/popop_stdlib.mli @@ -44,6 +44,12 @@ module type Datatype = sig include Base.Hashtbl.Key.S with type t := t end +module type NamedDatatype = sig + include Datatype + + val name : string +end + module type Printable = sig include OrderedHashedType val pp: t Pp.pp diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml index f596b2303855406ceb8bec21f5f65db909f4a9fe..d892f816a1f919369281ec6f3ff17c8838e53d0b 100644 --- a/src_colibri2/solver/scheduler.ml +++ b/src_colibri2/solver/scheduler.ml @@ -79,9 +79,9 @@ type solve_step = type t = { mutable choices : Prio.t; - daemons : Events.Wait.daemon_key Context.TimeWheel.t; - lasteffort : Events.Wait.daemon_key Context.TimeWheel.t; - fixing_model : Events.Wait.daemon_key list Context.Ref.t; + daemons : Events.daemon_key Context.TimeWheel.t; + lasteffort : Events.daemon_key Context.TimeWheel.t; + fixing_model : Events.daemon_key list Context.Ref.t; mutable prev_scheduler_state : bp option; solver_state : Egraph.Backtrackable.t; (* global *) diff --git a/src_colibri2/stdlib/comp_keys.ml b/src_colibri2/stdlib/comp_keys.ml index 22c2d756a0f92bac88eb82b040e5640f3febbe04..fc875259cc256f4ce5424357d88f9567a3d51d1b 100644 --- a/src_colibri2/stdlib/comp_keys.ml +++ b/src_colibri2/stdlib/comp_keys.ml @@ -87,7 +87,7 @@ module type Key = sig argument otherwise taise BadCoercion *) end - val create_key: (module NamedType with type t = 'a) -> 'a t + val create: (module NamedType with type t = 'a) -> 'a t module MkVector(D:sig type ('a,'b) t end) : Vector_hetero.S1 with @@ -125,7 +125,7 @@ module Make_key(X:sig end): Key = struct let fold f acc = K.fold f.fold acc let hint_size = K.hint_size - let create_key (type a) (module NT : NamedType with type t = a) : a t = + let create (type a) (module NT : NamedType with type t = a) : a t = K.create NT.name (** the 'a k can be used as equality witness because K gives fresh values *) @@ -272,7 +272,7 @@ module type Key2 = sig type iter = {iter : 'k 'd. ('k,'d) t -> unit} val iter : iter -> unit - val create_key: (module NamedType2 with type t = 'a1 + val create: (module NamedType2 with type t = 'a1 and type d = 'a2) -> ('a1,'a2) t @@ -310,7 +310,7 @@ module Make_key2(X:sig end) : Key2 = struct type iter = {iter : 'k 'd. ('k,'d) t -> unit} let iter f = K.iter f.iter - let create_key (type a1) (type a2) (module NT : NamedType2 with type t = a1 + let create (type a1) (type a2) (module NT : NamedType2 with type t = a1 and type d = a2) : (a1,a2) t = K.create NT.name diff --git a/src_colibri2/stdlib/comp_keys.mli b/src_colibri2/stdlib/comp_keys.mli index b7cf2fca4b45acb9fcd04e10ba7d530c0386f28d..b5647cc6b6dbb15f9e9228baeb92fc8e3160aef0 100644 --- a/src_colibri2/stdlib/comp_keys.mli +++ b/src_colibri2/stdlib/comp_keys.mli @@ -104,7 +104,7 @@ module type Key = sig argument otherwise taise BadCoercion *) end - val create_key: (module NamedType with type t = 'a) -> 'a t + val create: (module NamedType with type t = 'a) -> 'a t module MkVector(D:sig type ('a,'b) t end) : Vector_hetero.S1 with @@ -156,7 +156,7 @@ module type Key2 = sig type iter = {iter : 'k 'd. ('k,'d) t -> unit} val iter : iter -> unit - val create_key: (module NamedType2 with type t = 'a1 + val create: (module NamedType2 with type t = 'a1 and type d = 'a2) -> ('a1,'a2) t diff --git a/src_colibri2/stdlib/hashtbl_hetero.ml b/src_colibri2/stdlib/hashtbl_hetero.ml index ecca80e99837dd79f522048ab2803504ca297ef5..0c6a46d4fd50c4e9b61406a8bdac1736e9432b51 100644 --- a/src_colibri2/stdlib/hashtbl_hetero.ml +++ b/src_colibri2/stdlib/hashtbl_hetero.ml @@ -201,6 +201,11 @@ module Make2 let fold_initializedi (f: ('b, 'c) fold_initializedi) (seed : 'c) (m : 'b t) : 'c = H.fold (fun _ (Pair(k,v)) sofar -> f.foldi sofar k v) m seed + type ('b,'c) map_initializedi = + { mapi: 'a1 'a2. ('a1,'a2) key -> ('a1,'a2,'b) data -> ('a1,'a2,'b) data } + let map_initializedi (f: ('b, 'c) map_initializedi) (m : 'b t) : unit = + H.filter_map_inplace (fun _ (Pair(k,v)) -> Some (Pair(k,f.mapi k v))) m + let copy : 'b t -> 'b t = H.copy let move ~from ~to_ = H.reset to_; diff --git a/src_colibri2/stdlib/hashtbl_hetero_sig.ml b/src_colibri2/stdlib/hashtbl_hetero_sig.ml index 9aa896b0ba47880160c8cc0ff2b8b051213e15e0..7c5d33527f7142794d2fd756587a565605e2ea0a 100644 --- a/src_colibri2/stdlib/hashtbl_hetero_sig.ml +++ b/src_colibri2/stdlib/hashtbl_hetero_sig.ml @@ -162,6 +162,11 @@ module type S2 = sig val fold_initializedi : ('b,'c) fold_initializedi -> 'c -> 'b t -> 'c + type ('b,'c) map_initializedi = + { mapi: 'a1 'a2. ('a1,'a2) key -> ('a1,'a2,'b) data -> ('a1,'a2,'b) data} + val map_initializedi : + ('b,'c) map_initializedi -> 'b t -> unit + val copy : 'b t -> 'b t (* shallow *) val move: from:'b t -> to_:'b t -> unit diff --git a/src_colibri2/stdlib/keys.ml b/src_colibri2/stdlib/keys.ml index b6f03cf5364bab65a36a13cc959cade8e5534771..a107a843c21b8c46a0ba521adcd4e2796d81c7de 100644 --- a/src_colibri2/stdlib/keys.ml +++ b/src_colibri2/stdlib/keys.ml @@ -63,7 +63,7 @@ module Make_key(X:sig end) = struct let all_keys = AllKeys.create 17 let used_names : (* next id to use *) int StringH.t = StringH.create 17 - let create_key (type a) (module NT : NamedType with type t = a) : a t = + let create (type a) (module NT : NamedType with type t = a) : a t = let module TMP = struct type _ gadt += K : NT.t gadt end in @@ -163,7 +163,7 @@ module Make_key2(X:sig end) : Key2 = struct id : int; iseq : 'b1 'b2. ('b1,'b2) gadt -> ('k*'d,'b1*'b2) Poly.iseq } - let pp fmt x = String.pp fmt x.name + let pp fmt x = Format.pp_print_string fmt x.name let equal a b = a.id = b.id let hash x = x.id let tag = hash @@ -185,7 +185,7 @@ module Make_key2(X:sig end) : Key2 = struct let all_keys = AllKeys.create 17 let used_names : (* next id to use *) int StringH.t = StringH.create 17 - let create_key (type a1) (type a2) (module NT : NamedType2 with type t = a1 + let create (type a1) (type a2) (module NT : NamedType2 with type t = a1 and type d = a2) : (a1,a2) t = let module TMP = struct diff --git a/src_colibri2/stdlib/keys_sig.ml b/src_colibri2/stdlib/keys_sig.ml index 8db21311c6f01872bc3f459637d553d577ba6ce4..c0d9ce5b266799b68d16869fa980b561d79695ee 100644 --- a/src_colibri2/stdlib/keys_sig.ml +++ b/src_colibri2/stdlib/keys_sig.ml @@ -87,7 +87,7 @@ module type Key = sig argument otherwise taise BadCoercion *) end - val create_key: (module NamedType with type t = 'a) -> 'a t + val create: (module NamedType with type t = 'a) -> 'a t module MkVector(D:sig type ('a,'b) t end) : Hashtbl_hetero.S1 with type 'a key = 'a t @@ -147,7 +147,7 @@ module type Key2 = sig type 'b fold = {fold : 'a1 'a2. ('a1,'a2) t -> 'b -> 'b} [@@unboxed] val fold : 'b fold -> 'b -> 'b - val create_key: (module NamedType2 with type t = 'a1 + val create: (module NamedType2 with type t = 'a1 and type d = 'a2) -> ('a1,'a2) t diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml index 6c24422329b0c2f217e31e6c33fce841e4396843..6d7adb8417fc354cd827c04337c6f0da7907196e 100644 --- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml +++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml @@ -23,7 +23,7 @@ let result = Sys.argv.(2) let print_test cout file = Printf.fprintf cout - "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-steps 3000 %%{dep:%s}))))\n" + "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-steps 3500 %%{dep:%s}))))\n" file file; Printf.fprintf cout "(rule (alias runtest) (action (diff oracle %s.res)))\n" diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune.inc b/src_colibri2/tests/solve/all/steplimitreached/dune.inc index 48f937957eb462da83d35d80ccfca909dcd9bb71..6a6fa62c3b2d4adecd3fd70fb3128104a0728a29 100644 --- a/src_colibri2/tests/solve/all/steplimitreached/dune.inc +++ b/src_colibri2/tests/solve/all/steplimitreached/dune.inc @@ -1,3 +1,3 @@ (rule (action (with-stdout-to oracle (echo "steplimitreached\n")))) -(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bag-BagImpl-addqtvc.psmt2})))) +(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:bag-BagImpl-addqtvc.psmt2})))) (rule (alias runtest) (action (diff oracle bag-BagImpl-addqtvc.psmt2.res))) diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc index ec4a39965e799e3178a163e86cdeb2484a60859c..21e378d7bccbe68edb2acac47cb1166461dd6bfb 100644 --- a/src_colibri2/tests/solve/all/unsat/dune.inc +++ b/src_colibri2/tests/solve/all/unsat/dune.inc @@ -1,9 +1,9 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bag-BagImpl-createqtvc.psmt2})))) +(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:bag-BagImpl-createqtvc.psmt2})))) (rule (alias runtest) (action (diff oracle bag-BagImpl-createqtvc.psmt2.res))) -(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))) +(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))) (rule (alias runtest) (action (diff oracle fact-FactRecursive-fact_recqtvc.psmt2.res))) -(rule (action (with-stdout-to interval-Convexe-exists_memqtvc_1.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))) +(rule (action (with-stdout-to interval-Convexe-exists_memqtvc_1.psmt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))) (rule (alias runtest) (action (diff oracle interval-Convexe-exists_memqtvc_1.psmt2.res))) -(rule (action (with-stdout-to interval-Convexe-exists_memqtvc_2.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))) +(rule (action (with-stdout-to interval-Convexe-exists_memqtvc_2.psmt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))) (rule (alias runtest) (action (diff oracle interval-Convexe-exists_memqtvc_2.psmt2.res))) diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc index 578b32831c3fd812e85ceff19ccca6161aa6254e..2d7a5ec3a2015600cd13976f525c9ad248aaea6b 100644 --- a/src_colibri2/tests/solve/dimacs/sat/dune.inc +++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc @@ -1,23 +1,23 @@ (rule (action (with-stdout-to oracle (echo "sat\n")))) -(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold.cnf})))) +(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:anomaly_agetooold.cnf})))) (rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res))) -(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold2.cnf})))) +(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:anomaly_agetooold2.cnf})))) (rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res))) -(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:assertion_fail.cnf})))) +(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:assertion_fail.cnf})))) (rule (alias runtest) (action (diff oracle assertion_fail.cnf.res))) -(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:fuzzing1.cnf})))) +(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:fuzzing1.cnf})))) (rule (alias runtest) (action (diff oracle fuzzing1.cnf.res))) -(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:fuzzing2.cnf})))) +(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:fuzzing2.cnf})))) (rule (alias runtest) (action (diff oracle fuzzing2.cnf.res))) -(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:par8-1-c.cnf})))) +(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:par8-1-c.cnf})))) (rule (alias runtest) (action (diff oracle par8-1-c.cnf.res))) -(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-2.cnf})))) +(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-2.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-2.cnf.res))) -(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-3.cnf})))) +(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-3.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-3.cnf.res))) -(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-4.cnf})))) +(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-4.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-4.cnf.res))) -(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:quinn.cnf})))) +(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:quinn.cnf})))) (rule (alias runtest) (action (diff oracle quinn.cnf.res))) -(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_v3_c2.cnf})))) +(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:simple_v3_c2.cnf})))) (rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res))) diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc index cb881c5555cb36fc878dce306b706fbe0be2b3a1..f060f046117550fd6f693617b6d1c9d07c433deb 100644 --- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc +++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc @@ -1,13 +1,13 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold.cnf})))) +(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:anomaly_agetooold.cnf})))) (rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res))) -(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:modus_ponens.cnf})))) +(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:modus_ponens.cnf})))) (rule (alias runtest) (action (diff oracle modus_ponens.cnf.res))) -(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-1.cnf})))) +(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-1.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-1.cnf.res))) -(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-2.cnf})))) +(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-2.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-2.cnf.res))) -(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-3.cnf})))) +(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-3.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-3.cnf.res))) -(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-4.cnf})))) +(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3500 %{dep:pigeon-4.cnf})))) (rule (alias runtest) (action (diff oracle pigeon-4.cnf.res))) diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc index 93d4bd67568d47dac28580bdbc1c4f836a291e66..7dc32608e260b0236e41253773d347366a1f1d03 100644 --- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc +++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc @@ -1,13 +1,13 @@ (rule (action (with-stdout-to oracle (echo "sat\n")))) -(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum.smt2})))) +(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:enum.smt2})))) (rule (alias runtest) (action (diff oracle enum.smt2.res))) -(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list0.smt2})))) +(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list0.smt2})))) (rule (alias runtest) (action (diff oracle list0.smt2.res))) -(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list1.smt2})))) +(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list1.smt2})))) (rule (alias runtest) (action (diff oracle list1.smt2.res))) -(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree1.smt2})))) +(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:tree1.smt2})))) (rule (alias runtest) (action (diff oracle tree1.smt2.res))) -(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree2.smt2})))) +(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:tree2.smt2})))) (rule (alias runtest) (action (diff oracle tree2.smt2.res))) -(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree3.smt2})))) +(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:tree3.smt2})))) (rule (alias runtest) (action (diff oracle tree3.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc index a8533a27862f09c30bf1b203a5752c139452a91c..43124451796e7a753ea06db538ce63790a9524fc 100644 --- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc +++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc @@ -1,17 +1,17 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum.smt2})))) +(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:enum.smt2})))) (rule (alias runtest) (action (diff oracle enum.smt2.res))) -(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum2.smt2})))) +(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:enum2.smt2})))) (rule (alias runtest) (action (diff oracle enum2.smt2.res))) -(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list0.smt2})))) +(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list0.smt2})))) (rule (alias runtest) (action (diff oracle list0.smt2.res))) -(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list1.smt2})))) +(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list1.smt2})))) (rule (alias runtest) (action (diff oracle list1.smt2.res))) -(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list2.smt2})))) +(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list2.smt2})))) (rule (alias runtest) (action (diff oracle list2.smt2.res))) -(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list3.smt2})))) +(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list3.smt2})))) (rule (alias runtest) (action (diff oracle list3.smt2.res))) -(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list4.smt2})))) +(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:list4.smt2})))) (rule (alias runtest) (action (diff oracle list4.smt2.res))) -(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:parlist0.psmt2})))) +(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:parlist0.psmt2})))) (rule (alias runtest) (action (diff oracle parlist0.psmt2.res))) diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc index 20107a851d46527c8e306dea242e5faac1b5ff36..4af3d51a2a9ae86431b5bec4da2031a545b29fe2 100644 --- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc +++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc @@ -1,67 +1,67 @@ (rule (action (with-stdout-to oracle (echo "sat\n")))) -(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_CombiRepr_normalize.smt2})))) +(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_CombiRepr_normalize.smt2})))) (rule (alias runtest) (action (diff oracle arith_CombiRepr_normalize.smt2.res))) -(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_conflict_add_disequality.smt2})))) +(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_conflict_add_disequality.smt2})))) (rule (alias runtest) (action (diff oracle arith_conflict_add_disequality.smt2.res))) -(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_conpoly.smt2})))) +(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_conpoly.smt2})))) (rule (alias runtest) (action (diff oracle arith_conpoly.smt2.res))) -(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2})))) +(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_decide_must_test_is_dis_equal.smt2})))) (rule (alias runtest) (action (diff oracle arith_decide_must_test_is_dis_equal.smt2.res))) -(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_init_always_merge_itself.smt2})))) +(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_init_always_merge_itself.smt2})))) (rule (alias runtest) (action (diff oracle arith_init_always_merge_itself.smt2.res))) -(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2})))) +(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_init_and_propa_must_be_ordered.smt2})))) (rule (alias runtest) (action (diff oracle arith_init_and_propa_must_be_ordered.smt2.res))) -(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case1.smt2})))) +(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_case1.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_case1.smt2.res))) -(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case_4.smt2})))) +(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_case_4.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res))) -(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case_4_bis.smt2})))) +(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_case_4_bis.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_case_4_bis.smt2.res))) -(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))) +(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_itself_coef_of_repr_is_one.smt2.res))) -(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_last_case.smt2})))) +(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_itself_last_case.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_itself_last_case.smt2.res))) -(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))) +(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_itself_pivot_not_in_p12.smt2.res))) -(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_must_use_find.smt2})))) +(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_must_use_find.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_must_use_find.smt2.res))) -(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_mult_explication.smt2})))) +(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_mult_explication.smt2})))) (rule (alias runtest) (action (diff oracle arith_mult_explication.smt2.res))) -(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_mult_not_linear_in_conflict.smt2})))) +(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_mult_not_linear_in_conflict.smt2})))) (rule (alias runtest) (action (diff oracle arith_mult_not_linear_in_conflict.smt2.res))) -(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_normalize_use_find_def.smt2})))) +(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_normalize_use_find_def.smt2})))) (rule (alias runtest) (action (diff oracle arith_normalize_use_find_def.smt2.res))) -(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_own_repr.smt2})))) +(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_own_repr.smt2})))) (rule (alias runtest) (action (diff oracle arith_own_repr.smt2.res))) -(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_propacl.smt2})))) +(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_propacl.smt2})))) (rule (alias runtest) (action (diff oracle arith_propacl.smt2.res))) -(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_subst_and_conflict_add.smt2})))) +(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_subst_and_conflict_add.smt2})))) (rule (alias runtest) (action (diff oracle arith_subst_and_conflict_add.smt2.res))) -(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_zero_dom.smt2})))) +(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_zero_dom.smt2})))) (rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res))) -(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:attach_only_when_dom_present.smt2})))) +(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:attach_only_when_dom_present.smt2})))) (rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res))) -(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:init_not_repr.smt2})))) +(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:init_not_repr.smt2})))) (rule (alias runtest) (action (diff oracle init_not_repr.smt2.res))) -(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le.smt2})))) +(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:le.smt2})))) (rule (alias runtest) (action (diff oracle le.smt2.res))) -(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le2.smt2})))) +(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:le2.smt2})))) (rule (alias runtest) (action (diff oracle le2.smt2.res))) -(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul.smt2})))) +(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul.smt2})))) (rule (alias runtest) (action (diff oracle mul.smt2.res))) -(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:sem_invariant_in_learnt_dec.smt2})))) +(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:sem_invariant_in_learnt_dec.smt2})))) (rule (alias runtest) (action (diff oracle sem_invariant_in_learnt_dec.smt2.res))) -(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_add_pexp_cl.smt2})))) +(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_add_pexp_cl.smt2})))) (rule (alias runtest) (action (diff oracle solver_add_pexp_cl.smt2.res))) -(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2})))) +(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_arith_homogeneous_dist_sign.smt2})))) (rule (alias runtest) (action (diff oracle solver_arith_homogeneous_dist_sign.smt2.res))) -(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_merge_itself_repr_inside.smt2})))) +(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_merge_itself_repr_inside.smt2})))) (rule (alias runtest) (action (diff oracle solver_merge_itself_repr_inside.smt2.res))) -(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_set_pending_merge_expsameexp.smt2})))) +(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_set_pending_merge_expsameexp.smt2})))) (rule (alias runtest) (action (diff oracle solver_set_pending_merge_expsameexp.smt2.res))) -(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_subst_eventdom_find.smt2})))) +(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_subst_eventdom_find.smt2})))) (rule (alias runtest) (action (diff oracle solver_subst_eventdom_find.smt2.res))) -(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real.smt2})))) +(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:to_real.smt2})))) (rule (alias runtest) (action (diff oracle to_real.smt2.res))) -(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real2.smt2})))) +(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:to_real2.smt2})))) (rule (alias runtest) (action (diff oracle to_real2.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc index 419d393cfccef4da531d9e087e2fabf5ba6cef78..d4988bfdf2d2cc584e6f6ad851a944922e140084 100644 --- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc +++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc @@ -1,23 +1,23 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_ExpMult_by_zero.smt2})))) +(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_ExpMult_by_zero.smt2})))) (rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res))) -(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case2.smt2})))) +(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:arith_merge_case2.smt2})))) (rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res))) -(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le.smt2})))) +(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:le.smt2})))) (rule (alias runtest) (action (diff oracle le.smt2.res))) -(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le2.smt2})))) +(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:le2.smt2})))) (rule (alias runtest) (action (diff oracle le2.smt2.res))) -(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul.smt2})))) +(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul.smt2})))) (rule (alias runtest) (action (diff oracle mul.smt2.res))) -(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:repr_and_poly.smt2})))) +(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:repr_and_poly.smt2})))) (rule (alias runtest) (action (diff oracle repr_and_poly.smt2.res))) -(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:repr_fourier.smt2})))) +(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:repr_fourier.smt2})))) (rule (alias runtest) (action (diff oracle repr_fourier.smt2.res))) -(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_merge_itself_repr_empty.smt2})))) +(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_merge_itself_repr_empty.smt2})))) (rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res))) -(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_set_sem_merge_sign.smt2})))) +(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:solver_set_sem_merge_sign.smt2})))) (rule (alias runtest) (action (diff oracle solver_set_sem_merge_sign.smt2.res))) -(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real.smt2})))) +(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:to_real.smt2})))) (rule (alias runtest) (action (diff oracle to_real.smt2.res))) -(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real2.smt2})))) +(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:to_real2.smt2})))) (rule (alias runtest) (action (diff oracle to_real2.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc index 9904173a9ceadcd5d4d6d675b1b7c55ed0b28162..8a3302bc18e0bd2d5233a658cf8fb1ba3a30c1db 100644 --- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc +++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc @@ -1,15 +1,15 @@ (rule (action (with-stdout-to oracle (echo "sat\n")))) -(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ceil.smt2})))) +(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:ceil.smt2})))) (rule (alias runtest) (action (diff oracle ceil.smt2.res))) -(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos.smt2})))) +(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:div_pos.smt2})))) (rule (alias runtest) (action (diff oracle div_pos.smt2.res))) -(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt.smt2})))) +(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:div_pos_lt.smt2})))) (rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res))) -(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut.smt2})))) +(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_commut.smt2})))) (rule (alias runtest) (action (diff oracle mul_commut.smt2.res))) -(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut2.smt2})))) +(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_commut2.smt2})))) (rule (alias runtest) (action (diff oracle mul_commut2.smt2.res))) -(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos.smt2})))) +(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_pos.smt2})))) (rule (alias runtest) (action (diff oracle mul_pos.smt2.res))) -(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_lt.smt2})))) +(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_pos_lt.smt2})))) (rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc index 483f0dfccf76337a4b2436647b0ae1de9dfd445e..661c1882464a1189eba2d55d72b83a708b312028 100644 --- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc +++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc @@ -1,21 +1,21 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ceil.smt2})))) +(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:ceil.smt2})))) (rule (alias runtest) (action (diff oracle ceil.smt2.res))) -(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos.smt2})))) +(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:div_pos.smt2})))) (rule (alias runtest) (action (diff oracle div_pos.smt2.res))) -(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt.smt2})))) +(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:div_pos_lt.smt2})))) (rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res))) -(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt_to_real.smt2})))) +(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:div_pos_lt_to_real.smt2})))) (rule (alias runtest) (action (diff oracle div_pos_lt_to_real.smt2.res))) -(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:floor.smt2})))) +(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:floor.smt2})))) (rule (alias runtest) (action (diff oracle floor.smt2.res))) -(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut.smt2})))) +(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_commut.smt2})))) (rule (alias runtest) (action (diff oracle mul_commut.smt2.res))) -(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut2.smt2})))) +(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_commut2.smt2})))) (rule (alias runtest) (action (diff oracle mul_commut2.smt2.res))) -(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos.smt2})))) +(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_pos.smt2})))) (rule (alias runtest) (action (diff oracle mul_pos.smt2.res))) -(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_lt.smt2})))) +(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_pos_lt.smt2})))) (rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res))) -(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_zero_le.smt2})))) +(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:mul_pos_zero_le.smt2})))) (rule (alias runtest) (action (diff oracle mul_pos_zero_le.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc index f03644ff11dc708744ba02c95ab5a26aa37fa940..2e21c514e04c4db3a805c130a80ea0de677dfbef 100644 --- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc +++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc @@ -1,9 +1,9 @@ (rule (action (with-stdout-to oracle (echo "sat\n")))) -(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists.smt2})))) +(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:exists.smt2})))) (rule (alias runtest) (action (diff oracle exists.smt2.res))) -(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall0.smt2})))) +(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall0.smt2})))) (rule (alias runtest) (action (diff oracle forall0.smt2.res))) -(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall3.smt2})))) +(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall3.smt2})))) (rule (alias runtest) (action (diff oracle forall3.smt2.res))) -(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall4.smt2})))) +(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall4.smt2})))) (rule (alias runtest) (action (diff oracle forall4.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc index 9d7e931a83a87583f90c59ccd88351d54860474a..331cd6230bd9baab9562f94f65fd3e301e644bf7 100644 --- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc +++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc @@ -1,23 +1,23 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists.smt2})))) +(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:exists.smt2})))) (rule (alias runtest) (action (diff oracle exists.smt2.res))) -(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists2.smt2})))) +(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:exists2.smt2})))) (rule (alias runtest) (action (diff oracle exists2.smt2.res))) -(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall0.smt2})))) +(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall0.smt2})))) (rule (alias runtest) (action (diff oracle forall0.smt2.res))) -(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall1.smt2})))) +(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall1.smt2})))) (rule (alias runtest) (action (diff oracle forall1.smt2.res))) -(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall2.smt2})))) +(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall2.smt2})))) (rule (alias runtest) (action (diff oracle forall2.smt2.res))) -(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall3.smt2})))) +(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall3.smt2})))) (rule (alias runtest) (action (diff oracle forall3.smt2.res))) -(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall4.smt2})))) +(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall4.smt2})))) (rule (alias runtest) (action (diff oracle forall4.smt2.res))) -(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall5.smt2})))) +(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall5.smt2})))) (rule (alias runtest) (action (diff oracle forall5.smt2.res))) -(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall6.smt2})))) +(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall6.smt2})))) (rule (alias runtest) (action (diff oracle forall6.smt2.res))) -(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall7.smt2})))) +(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall7.smt2})))) (rule (alias runtest) (action (diff oracle forall7.smt2.res))) -(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall8.smt2})))) +(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:forall8.smt2})))) (rule (alias runtest) (action (diff oracle forall8.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc index a6b45388bcccc559f1b349d06104d8f8b162193d..e532036814aec383ac6023897dc7e627dbf8735c 100644 --- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc +++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc @@ -1,43 +1,43 @@ (rule (action (with-stdout-to oracle (echo "sat\n")))) -(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bad_conflict.smt2})))) +(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:bad_conflict.smt2})))) (rule (alias runtest) (action (diff oracle bad_conflict.smt2.res))) -(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bcp_dont_like_duplicate.smt2})))) +(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:bcp_dont_like_duplicate.smt2})))) (rule (alias runtest) (action (diff oracle bcp_dont_like_duplicate.smt2.res))) -(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bool_not_propa.smt2})))) +(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:bool_not_propa.smt2})))) (rule (alias runtest) (action (diff oracle bool_not_propa.smt2.res))) -(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:boolexpup.smt2})))) +(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:boolexpup.smt2})))) (rule (alias runtest) (action (diff oracle boolexpup.smt2.res))) -(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:clause_normalization.smt2})))) +(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:clause_normalization.smt2})))) (rule (alias runtest) (action (diff oracle clause_normalization.smt2.res))) -(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:clmerge.smt2})))) +(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:clmerge.smt2})))) (rule (alias runtest) (action (diff oracle clmerge.smt2.res))) -(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:conflict_complete_needed_cl.smt2})))) +(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:conflict_complete_needed_cl.smt2})))) (rule (alias runtest) (action (diff oracle conflict_complete_needed_cl.smt2.res))) -(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:directdom_not.smt2})))) +(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:directdom_not.smt2})))) (rule (alias runtest) (action (diff oracle directdom_not.smt2.res))) -(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:dis_dom_before_first_age.smt2})))) +(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:dis_dom_before_first_age.smt2})))) (rule (alias runtest) (action (diff oracle dis_dom_before_first_age.smt2.res))) -(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:dom_merge_equality.smt2})))) +(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:dom_merge_equality.smt2})))) (rule (alias runtest) (action (diff oracle dom_merge_equality.smt2.res))) -(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality.smt2})))) +(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:equality.smt2})))) (rule (alias runtest) (action (diff oracle equality.smt2.res))) -(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_condis.smt2})))) +(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:equality_condis.smt2})))) (rule (alias runtest) (action (diff oracle equality_condis.smt2.res))) -(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_get_sem.smt2})))) +(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:equality_get_sem.smt2})))) (rule (alias runtest) (action (diff oracle equality_get_sem.smt2.res))) -(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exp_sem_equality.smt2})))) +(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:exp_sem_equality.smt2})))) (rule (alias runtest) (action (diff oracle exp_sem_equality.smt2.res))) -(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:explimit_cl_equality.smt2})))) +(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:explimit_cl_equality.smt2})))) (rule (alias runtest) (action (diff oracle explimit_cl_equality.smt2.res))) -(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:implication.smt2})))) +(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:implication.smt2})))) (rule (alias runtest) (action (diff oracle implication.smt2.res))) -(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:intmap_set_disjoint.smt2})))) +(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:intmap_set_disjoint.smt2})))) (rule (alias runtest) (action (diff oracle intmap_set_disjoint.smt2.res))) -(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:is_equal_not_propagated.smt2})))) +(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:is_equal_not_propagated.smt2})))) (rule (alias runtest) (action (diff oracle is_equal_not_propagated.smt2.res))) -(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ite_sem_bool.smt2})))) +(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:ite_sem_bool.smt2})))) (rule (alias runtest) (action (diff oracle ite_sem_bool.smt2.res))) -(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality.smt2})))) +(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:polyeq_genequality.smt2})))) (rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res))) -(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:substupfalse_equality.smt2})))) +(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:substupfalse_equality.smt2})))) (rule (alias runtest) (action (diff oracle substupfalse_equality.smt2.res))) diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc index 0b7a4dca9cc8d3f43e5f2ed509635a6279e7cb1f..7bb19eb5e0420b61af2f6969d7d59ab682eaac7e 100644 --- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc +++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc @@ -1,27 +1,27 @@ (rule (action (with-stdout-to oracle (echo "unsat\n")))) -(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:NEQ004_size4__decide_eq_us.smt2})))) +(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:NEQ004_size4__decide_eq_us.smt2})))) (rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res))) -(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:deltaed0.smt2})))) +(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:deltaed0.smt2})))) (rule (alias runtest) (action (diff oracle deltaed0.smt2.res))) -(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:diff_to_value_for_bool.smt2})))) +(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:diff_to_value_for_bool.smt2})))) (rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res))) -(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:diff_value_substupfalse.smt2})))) +(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:diff_value_substupfalse.smt2})))) (rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res))) -(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:distinct.smt2})))) +(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:distinct.smt2})))) (rule (alias runtest) (action (diff oracle distinct.smt2.res))) -(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:eq_diamond2.smt2})))) +(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:eq_diamond2.smt2})))) (rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res))) -(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_norm_set.smt2})))) +(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:equality_norm_set.smt2})))) (rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res))) -(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fundef.smt2})))) +(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:fundef.smt2})))) (rule (alias runtest) (action (diff oracle fundef.smt2.res))) -(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))) +(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))) (rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res))) -(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:many_distinct.smt2})))) +(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:many_distinct.smt2})))) (rule (alias runtest) (action (diff oracle many_distinct.smt2.res))) -(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality.smt2})))) +(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:polyeq_genequality.smt2})))) (rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res))) -(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality_deltaed.smt2})))) +(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:polyeq_genequality_deltaed.smt2})))) (rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res))) -(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:xor.smt2})))) +(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-steps 3500 %{dep:xor.smt2})))) (rule (alias runtest) (action (diff oracle xor.smt2.res))) diff --git a/src_colibri2/tests/tests_fp.ml b/src_colibri2/tests/tests_fp.ml index 51a9ce69f2d30f956986a413419e638ce385fc49..686905671b7ff6b57ec6ad3bcdafb5a61130bc37 100644 --- a/src_colibri2/tests/tests_fp.ml +++ b/src_colibri2/tests/tests_fp.ml @@ -13,9 +13,9 @@ let ($$) f x = f x let run = Scheduler.run_exn ~nodec:() ~theories let recognize_float32 _ = - let a = fresht (Ty.float 8 24) "a" in - let b = fresht (Ty.float 8 24) "b" in - let t = Term.eq a b in + let a = fresht (Expr.Ty.float 8 24) "a" in + let b = fresht (Expr.Ty.float 8 24) "b" in + let t = Expr.Term.eq a b in let an = Ground.convert a in let bn = Ground.convert b in let tn = Ground.convert t in @@ -28,9 +28,9 @@ let recognize_float32 _ = assert_bool "a = b" (is_equal env an bn) let recognize_float64 _ = - let a = fresht (Ty.float 11 53) "a" in - let b = fresht (Ty.float 11 53) "b" in - let t = Term.eq a b in + let a = fresht (Expr.Ty.float 11 53) "a" in + let b = fresht (Expr.Ty.float 11 53) "b" in + let t = Expr.Term.eq a b in let an = Ground.convert a in let bn = Ground.convert b in let tn = Ground.convert t in @@ -43,4 +43,4 @@ let recognize_float64 _ = assert_bool "a = b" (is_equal env an bn) let basic = "FP.Basic" &: [ recognize_float32; recognize_float64 ] -let tests = test_list [basic] \ No newline at end of file +let tests = test_list [basic] diff --git a/src_colibri2/tests/tests_lib.ml b/src_colibri2/tests/tests_lib.ml index 7126bab7c23707334873dfe130c8a66467ff3558..07e0ada52eeb78c99778f4c4a68aa0f49fb54269 100644 --- a/src_colibri2/tests/tests_lib.ml +++ b/src_colibri2/tests/tests_lib.ml @@ -19,7 +19,6 @@ (*************************************************************************) open OUnit2 -open Colibri2_popop_lib open Colibri2_core let debug = Debug.register_flag @@ -42,7 +41,7 @@ let is_equal = Egraph.is_equal (** without decisions *) type t = - { wakeup_daemons : Events.Wait.daemon_key Queue.t; + { wakeup_daemons : Events.daemon_key Queue.t; solver_state : Egraph.Backtrackable.t; context : Colibri2_stdlib.Context.context; } diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml index 724351bf9c80e8dcf9fecfe0bc6c6dcf3afa3847..71a6e05cf689dd3f3c17a81bf3dcd3d704ebccc0 100644 --- a/src_colibri2/theories/ADT/adt.ml +++ b/src_colibri2/theories/ADT/adt.ml @@ -36,7 +36,7 @@ module D = struct | One c -> Fmt.pf fmt "%i(%a)" c.case (Field.M.pp Node.pp) c.fields let key = - DomKind.create_key + Dom.Kind.create (module struct type nonrec t = t @@ -96,7 +96,7 @@ module D = struct Egraph.set_dom d key n2 s end -let () = DomKind.register (module D) +let () = Dom.register (module D) let upd_dom d n d2 = match Egraph.get_dom d D.key n with @@ -170,8 +170,8 @@ end = struct Option.bind (Egraph.get_value d n') (Value.value key) let[@ocaml.always inline] set_value (type b) - (value : (module ValueKind.Registered with type s = b)) n' - (v' : b option option monad) : unit monad = + (value : (module Value.S with type s = b)) n' (v' : b option option monad) + : unit monad = fun d n -> if Node.equal n n' then () else @@ -191,9 +191,8 @@ end = struct let[@ocaml.always inline] ( let+ ) a (f : 'b -> 'a) d n = Option.map f (a d n) end -let wait = Demon.Fast.register_simply "GotDomInterval" - (** {2 Initialization} *) + let converter d (f : Ground.t) = let r = Ground.node f in let reg n = Egraph.register d n in @@ -202,19 +201,20 @@ let converter d (f : Ground.t) = | { app = { builtin = Expr.Tester { adt; case; _ }; _ }; args; _ } -> let e = IArray.extract1_exn args in reg e; - wait.for_value d Boolean.BoolValue.key r - (set e - (let+ vr = getb r in - if vr then D.Unk (Case.S.singleton case) - else - let s = Case.S.remove case (case_of_adt adt) in - if Case.S.is_empty s then ( - Debug.dprintf4 Egraph.print_contradiction - "[ADT] tester %a removed the only case %a of the type" Node.pp - r Case.pp case; - Egraph.contradiction d) - else D.Unk s)); - wait.for_dom d D.key e + Daemon.attach_value d r Boolean.BoolValue.key (fun d n _ -> + (set e + (let+ vr = getb r in + if vr then D.Unk (Case.S.singleton case) + else + let s = Case.S.remove case (case_of_adt adt) in + if Case.S.is_empty s then ( + Debug.dprintf4 Egraph.print_contradiction + "[ADT] tester %a removed the only case %a of the type" + Node.pp r Case.pp case; + Egraph.contradiction d) + else D.Unk s)) + d n); + Daemon.attach_dom d e D.key (setb r (let+ ve = get e in match ve with @@ -238,7 +238,7 @@ let converter d (f : Ground.t) = upd_dom d e (One { case; fields = Field.M.singleton field r }) in let nothing _ = () in - wait.for_dom d D.key e + Daemon.attach_dom d e D.key (unit (let+ ve = get e in match ve with diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml index 8fc328b3a3252052a0c73f367869d6b34828b0d6..7ff8d23570141c500b815864140fd30d52a5c3ad 100644 --- a/src_colibri2/theories/ADT/adt_value.ml +++ b/src_colibri2/theories/ADT/adt_value.ml @@ -48,16 +48,10 @@ module T' = struct include T include MkDatatype (T) - let key = - ValueKind.create_key - (module struct - include T - - let name = "ADT.value" - end) + let name = "ADT.value" end -include ValueKind.Register (T') +include Value.Register (T') let interp d n = Opt.get_exn Impossible (Egraph.get_value d n) diff --git a/src_colibri2/theories/ADT/adt_value.mli b/src_colibri2/theories/ADT/adt_value.mli index 65b7b63746c381d8b3cac34aa42f78d6a31cb360..7b88e25c6943a6c180f72d4c6edfe8f10e14ffe2 100644 --- a/src_colibri2/theories/ADT/adt_value.mli +++ b/src_colibri2/theories/ADT/adt_value.mli @@ -29,7 +29,7 @@ type ts = { fields : Value.t Field.M.t; } -include ValueKind.Registered with type s := ts +include Value.S with type s := ts val th_register : Egraph.t -> unit @@ -37,8 +37,8 @@ val propagate_value : Egraph.t -> Ground.t -> unit val sequence_of_cases : Egraph.t -> - Term.ty_const -> + Expr.Term.ty_const -> Ground.All.ty list -> - Ty.adt_case array -> + Expr.Ty.adt_case array -> int Base.Sequence.t -> Value.t Interp.SeqLim.t diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml index 413086f981a0d5c7660eb7d864cf64e78f149b72..7da6179fb3975c9c2852d232cf9765c96049edb4 100644 --- a/src_colibri2/theories/FP/float32.ml +++ b/src_colibri2/theories/FP/float32.ml @@ -21,7 +21,7 @@ open Fp_value module N32 = struct let name = "Float32" end -module Float32 = ValueKind.Register(MakeFloat(Farith.B32)(N32)) +module Float32 = Value.Register(MakeFloat(Farith.B32)(N32)) include Float32 @@ -44,4 +44,4 @@ let init_ty d = (* let init_check d = Interp.Register.check d (...) *) let init env = - init_ty env \ No newline at end of file + init_ty env diff --git a/src_colibri2/theories/FP/float32.mli b/src_colibri2/theories/FP/float32.mli index 51b03a489ade1b941073cae6020a125e70e17e85..1b971f2a86686e74d3e9c494723ba5f1f2301f19 100644 --- a/src_colibri2/theories/FP/float32.mli +++ b/src_colibri2/theories/FP/float32.mli @@ -18,6 +18,6 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -include ValueKind.Registered with type s = Farith.B32.t +include Value.S with type s = Farith.B32.t -val init : Egraph.t -> unit \ No newline at end of file +val init : Egraph.t -> unit diff --git a/src_colibri2/theories/FP/float64.ml b/src_colibri2/theories/FP/float64.ml index 5150c7d99feb21bac7a1000d62b75e8bf6ef88dc..eb1d80dce0889d82ef6333f1b26d1346516c7a94 100644 --- a/src_colibri2/theories/FP/float64.ml +++ b/src_colibri2/theories/FP/float64.ml @@ -20,7 +20,7 @@ open Fp_value module N64 = struct let name = "Float64" end -module Float64 = ValueKind.Register(MakeFloat(Farith.B64)(N64)) +module Float64 = Value.Register(MakeFloat(Farith.B64)(N64)) include Float64 @@ -43,4 +43,4 @@ let init_ty d = (* let init_check d = Interp.Register.check d (...) *) let init env = - init_ty env \ No newline at end of file + init_ty env diff --git a/src_colibri2/theories/FP/float64.mli b/src_colibri2/theories/FP/float64.mli index 60539cac2f7beb609d9310a98704d7a05023d88d..f17a8c646a6493ec41fddf1b06016a1b392337de 100644 --- a/src_colibri2/theories/FP/float64.mli +++ b/src_colibri2/theories/FP/float64.mli @@ -18,6 +18,6 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -include ValueKind.Registered with type s = Farith.B64.t +include Value.S with type s = Farith.B64.t val init : Egraph.t -> unit diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml index 4a5142a5c605e24048e017de20ec189c363cdf78..a40c709cb78884624f70a3a98f9876919677afe0 100644 --- a/src_colibri2/theories/FP/fp_value.ml +++ b/src_colibri2/theories/FP/fp_value.ml @@ -23,7 +23,7 @@ open Popop_stdlib module type FloatName = sig val name : string end -(** Extends a module of type [Farith.S] to be of type [ValueKind.Value] *) +(** Extends a module of type [Farith.S] to be of type [Value.Kind.Value] *) module MakeFloat (F : Farith.S) (N : FloatName) = struct (** Extends a module of type [Farith.S] with [hash_fold_t] and [sexp_of_t] *) @@ -38,7 +38,7 @@ module MakeFloat (F : Farith.S) (N : FloatName) = struct module S = Extset.MakeOfMap(M) module H = XHashtbl.Make(HF) - let key = ValueKind.create_key (module struct type t = F.t let name = N.name end) + let name = N.name end @@ -52,4 +52,4 @@ let posint_sequence_without_zero = (** Generate the sequence of positive integers (without 0) *) let posint_sequence = - Base.Sequence.shift_right posint_sequence_without_zero Z.zero \ No newline at end of file + Base.Sequence.shift_right posint_sequence_without_zero Z.zero diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli index 5d2caa0eec9f3cd65a75bc026282e66844e7c288..876601c9fb35d08360686845036b3e8a9ae4ef69 100644 --- a/src_colibri2/theories/FP/fp_value.mli +++ b/src_colibri2/theories/FP/fp_value.mli @@ -26,8 +26,8 @@ val posint_sequence : Z.t Base.Sequence.t (** Names (string) wrapped in a module *) module type FloatName = sig val name : string end -(** +(** Helper to extend a module of type [Farith.S] into a module of - type [ValueKind.Value] + type [Value.Kind.Value] *) -module MakeFloat (F : Farith.S) (N : FloatName) : ValueKind.Value with type t = F.t \ No newline at end of file +module MakeFloat (F : Farith.S) (N : FloatName) : Colibri2_popop_lib.Popop_stdlib.NamedDatatype with type t = F.t diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli index 040771d54e0d48c4e944fafa3da4bc4bbff7b026..a958f427e919cd7c9f193f51e9e888386053c1ec 100644 --- a/src_colibri2/theories/LRA/LRA.mli +++ b/src_colibri2/theories/LRA/LRA.mli @@ -19,7 +19,7 @@ (*************************************************************************) module RealValue : sig - include ValueKind.Registered with type s = Q.t + include Value.S with type s = Q.t val cst': Q.t -> t val cst: Q.t -> Node.t diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml index a9787bc8c2dca817a9cc6d7dc4a77d1b1fd391d4..1670f393e79e0b96ce7fd4a271a8189f103d79a7 100644 --- a/src_colibri2/theories/LRA/dom_interval.ml +++ b/src_colibri2/theories/LRA/dom_interval.ml @@ -28,39 +28,15 @@ let debug = Debug.register_info_flag module D = Colibri2_theories_LRA_stages.Interval_domain -let dom = DomKind.create_key (module struct type t = D.t let name = "ARITH" end) +let dom = Dom.Kind.create (module struct type t = D.t let name = "ARITH" end) -let () = DomKind.register(module struct +let set_dom = Dom.lattice (module struct include D let key = dom - let merged i1 i2 = - match i1, i2 with - | None, None -> true - | Some i1, Some i2 -> D.equal i1 i2 - | _ -> false - - let merge d (i1,cl1) (i2,cl2) _ = - assert (not (Egraph.is_equal d cl1 cl2)); - match i1, cl1, i2, cl2 with - | Some i1,_, Some i2,_ -> - begin match D.inter i1 i2 with - | None -> - Debug.dprintf8 Egraph.print_contradiction - "[LRA/Dom] The intersection of %a and %a is empty when merging %a and %a" - D.pp i1 D.pp i2 - Node.pp cl1 - Node.pp cl2; - Egraph.contradiction d - | Some i -> - if not (D.equal i i1) then - Egraph.set_dom d dom cl1 i; - if not (D.equal i i2) then - Egraph.set_dom d dom cl2 i - end - | Some i1, _, _, cl2 | _, cl2, Some i1, _ -> - Egraph.set_dom d dom cl2 i1 - | None,_,None,_ -> raise Impossible - end) + let is_singleton d = + Option.map (fun x -> RealValue.nodevalue @@ RealValue.index x) (is_singleton d) + end +) let is_zero_or_positive d n = match Egraph.get_dom d dom n with @@ -93,15 +69,6 @@ let is_integer d n = | None -> false | Some p -> D.is_integer p -let set_dom d node v = - match D.is_singleton v with - | Some q -> - let cst = RealValue.cst' q in - Egraph.set_value d node (RealValue.nodevalue cst) - | None -> - (** the pexp must be in the dom *) - Egraph.set_dom d dom node v - module ChoLRA = struct let make_decision node v env = @@ -155,7 +122,7 @@ end = struct type 'a monad = Egraph.t -> Node.t -> 'a let [@ocaml.always inline] get_dom dom n' = fun d _ -> Egraph.get_dom d dom n' - let [@ocaml.always inline] set_dom (type b) (dom:b DomKind.t) n' v' d n = + let [@ocaml.always inline] set_dom (type b) (dom:b Dom.Kind.t) n' v' d n = if Node.equal n n' then () else Option.iter (fun (v':b) -> Egraph.set_dom d dom n' v') @@ -171,7 +138,7 @@ end = struct let* v = Egraph.get_value d n' in Value.value key v let [@ocaml.always inline] set_value (type b) - (value:(module ValueKind.Registered with type s = b)) + (value:(module Value.S with type s = b)) n' (v':b option option monad) : unit monad = fun d n -> if Node.equal n n' then () else @@ -188,9 +155,6 @@ end = struct end -let wait = - Demon.Fast.register_simply "GotDomInterval" - let neg_cmp = function | `Lt -> `Ge | `Le -> `Gt @@ -224,8 +188,8 @@ let converter d (f:Ground.t) = set a (let+ vb = get b and+ vr = getb r in backward (if vr then cmp else (neg_cmp cmp)) vb) in - List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b]; - wait.for_value d Boolean.BoolValue.key r wakeup + List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;b]; + Daemon.attach_value d r Boolean.BoolValue.key (fun d n _ -> wakeup d n) in match Ground.sem f with | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty } @@ -243,7 +207,7 @@ let converter d (f:Ground.t) = set a (let+ vb = get b and+ vr = get r in D.minus vr vb) && set b (let+ va = get a and+ vr = get r in D.minus vr va) in - List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b;r] + List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;b;r] | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } -> let (a,b) = IArray.extract2_exn args in reg a; reg b; @@ -252,7 +216,7 @@ let converter d (f:Ground.t) = set a (let+ vb = get b and+ vr = get r in D.add vr vb) && set b (let+ va = get a and+ vr = get r in D.minus va vr) in - List.iter (fun n -> wait.for_dom d dom n wakeup) [a;b;r] + List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;b;r] | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } -> let a = IArray.extract1_exn args in reg a; @@ -260,7 +224,7 @@ let converter d (f:Ground.t) = set r (let+ va = get a in D.mult_cst Q.minus_one va) && set a (let+ vr = get r in D.mult_cst Q.minus_one vr) in - List.iter (fun n -> wait.for_dom d dom n wakeup) [a;r] + List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;r] | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } -> let a,b = IArray.extract2_exn args in cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false) `Lt a b @@ -276,12 +240,11 @@ let converter d (f:Ground.t) = | _ -> () let init env = - Demon.Fast.register_init_daemon_value - ~name:"RealValueToDomInterval" - (module RealValue) + Daemon.attach_reg_value env + RealValue.key (fun d value -> let v = RealValue.value value in let s = D.singleton v in Egraph.set_dom d dom (RealValue.node value) s - ) env; + ); Ground.register_converter env converter diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli index d610137c389c06797c86bd4540d4f8b1dcb2fa97..2e5d10ea80a5457dbf9502836ead12b1ffd5d3b9 100644 --- a/src_colibri2/theories/LRA/dom_interval.mli +++ b/src_colibri2/theories/LRA/dom_interval.mli @@ -22,7 +22,7 @@ val init: Egraph.t -> unit module D: sig type t end -val dom : D.t DomKind.t +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 diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml index 539e44f5fd722c4c1cc8b5feb5419b807888136c..243272c3b33f13f0d664292078aea63276b6ecab 100644 --- a/src_colibri2/theories/LRA/dom_polynome.ml +++ b/src_colibri2/theories/LRA/dom_polynome.ml @@ -26,14 +26,14 @@ let debug = Debug.register_info_flag ~desc:"for the arithmetic theory of polynome" "LRA.polynome" -let dom = DomKind.create_key (module struct type t = Polynome.t let name = "ARITH_POLY" end) +let dom = Dom.Kind.create (module struct type t = Polynome.t let name = "ARITH_POLY" end) module T = struct include Polynome - let key = ThTermKind.create_key (module struct type nonrec t = t let name = "SARITH_POLY" end) + let name = "SARITH_POLY" end -module ThE = ThTermKind.Register(T) +module ThE = ThTerm.Register(T) let node_of_polynome t = ThE.node (ThE.index t) @@ -215,13 +215,12 @@ let converter d (f:Ground.t) = | _ -> () let init env = - Demon.Fast.register_init_daemon_value - ~name:"RealValueToDomPoly" - (module RealValue) + Daemon.attach_reg_value env + RealValue.key (fun d value -> let v = RealValue.value value in let cl = RealValue.node value in let p1 = Polynome.of_list v [] in assume_poly_equality d cl p1 - ) env; + ); Ground.register_converter env converter diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli index 1b28c48f4a6b1caa39bbc569fd08eb67edcfcf0b..bfd1d86e7f17969c659bb2002a5787b28b59a393 100644 --- a/src_colibri2/theories/LRA/dom_polynome.mli +++ b/src_colibri2/theories/LRA/dom_polynome.mli @@ -20,7 +20,7 @@ val assume_poly_equality: Egraph.t -> Node.t -> Polynome.t -> unit -val dom: Polynome.t DomKind.t +val dom: Polynome.t Dom.Kind.t val init: Egraph.t -> unit diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml index f12b3a0ee0c515c2d3325da17d42ed197506871a..9ca609428c7e779783267e56bb87524cfbbf79de 100644 --- a/src_colibri2/theories/LRA/dom_product.ml +++ b/src_colibri2/theories/LRA/dom_product.ml @@ -36,14 +36,14 @@ type t = { let pp fmt t = Fmt.pf fmt "%a,%a" Product.pp t.repr Product.S.pp t.eqs -let dom = DomKind.create_key (module struct type nonrec t = t let name = "ARITH_PROD" end) +let dom = Dom.Kind.create (module struct type nonrec t = t let name = "ARITH_PROD" end) module T = struct include Product - let key = ThTermKind.create_key (module struct type nonrec t = t let name = "SARITH_PROD" end) + let name = "SARITH_PROD" end -module ThE = ThTermKind.Register(T) +module ThE = ThTerm.Register(T) let node_of_product t = ThE.node (ThE.index t) @@ -305,21 +305,18 @@ module ChangePos = struct let l = Th.part d (p.repr::Product.S.elements p.eqs) in let l = Lists.product l l in ignore (Th.solve d l)) - ns; - None - type event = unit - let print_event = Unit.pp - let enqueue d = function - | Events.Fired.EventDom(n,dom',()) -> begin - assert (DomKind.equal Dom_interval.dom dom'); - match Node.HC.Ro.find_opt used_in_poly d n with - | Some ns -> Events.Wait.EnqRun ns - | None -> Events.Wait.EnqAlready - end - | _ -> assert false + ns let delay = Events.Delayed_by 10 - let key = Events.Dem.create_key (module struct type t = unit type d = Node.S.t + let key = Events.Dem.create (module struct type t = Node.S.t let name = "Dom_product.ChangePos" end) + + 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 + | Some ns -> Events.EnqRun (key,ns) + | None -> Events.EnqAlready) + end let () = Egraph.Wait.register_dem (module ChangePos) @@ -351,9 +348,6 @@ let factorize res a coef b d _ = | _ -> () -let wait = - Demon.Fast.register_simply "GotDomInterval" - (** {2 Initialization} *) let converter d (f:Ground.t) = let res = Ground.node f in @@ -366,7 +360,7 @@ let converter d (f:Ground.t) = | { app = {builtin = Expr.Div}; tyargs = []; args; _ } -> let num,den = IArray.extract2_exn args in reg num; reg den; - wait.for_dom d Dom_interval.dom den + Daemon.attach_dom d den Dom_interval.dom (fun d _ -> if Dom_interval.is_not_zero d den then assume_poly_equality d num (Product.of_list [res,Q.one;den,Q.one]) @@ -374,16 +368,15 @@ let converter d (f:Ground.t) = | { app = {builtin = Expr.Add}; tyargs = []; args; _ } -> let a,b = IArray.extract2_exn args in reg a; reg b; - List.iter (fun x -> wait.for_dom d dom x (factorize res a Q.one b)) [a;b] + List.iter (fun x -> Daemon.attach_dom d x dom (factorize res a Q.one b)) [a;b] | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } -> let a,b = IArray.extract2_exn args in reg a; reg b; - List.iter (fun x -> wait.for_dom d dom x (factorize res a Q.minus_one b)) [a;b] + List.iter (fun x -> Daemon.attach_dom d x dom (factorize res a Q.minus_one b)) [a;b] | _ -> () let init env = - Demon.Fast.register_any_change_domain_daemon - ~name:"DomPolyToDomProd" + Daemon.attach_any_dom env Dom_polynome.dom (fun d n -> match Egraph.get_dom d Dom_polynome.dom n with @@ -394,10 +387,9 @@ let init env = if Q.equal q Q.one then let p1 = Product.of_list [cl,Q.one] in assume_poly_equality d n p1 - ) env; - Demon.Fast.register_any_change_domain_daemon - ~name:"DomProdToDomPoly" - dom + ); + Daemon.attach_any_dom env + Dom_polynome.dom (fun d n -> match Egraph.get_dom d dom n with | None -> () @@ -411,6 +403,6 @@ let init env = in aux p.repr; Product.S.iter aux p.eqs - ) env; + ); Ground.register_converter env converter; - Egraph.attach_any_dom env Dom_interval.dom ChangePos.key () + ChangePos.init env diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli index 06de5f286628f1df6f0ae564b9260b9243b97757..df6be3b0c6d4cd7d167152be31ad4781f305d586 100644 --- a/src_colibri2/theories/LRA/dom_product.mli +++ b/src_colibri2/theories/LRA/dom_product.mli @@ -24,7 +24,7 @@ val node_of_product: Product.t -> Node.t type t -val dom: t DomKind.t +val dom: t Dom.Kind.t val get_repr: Egraph.t -> Node.t -> Product.t option diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml index 4258775bb400f47a2c0d5818e4a1939dfb98bf2c..a751a3b826a09420be203c431941c10ce8c42312 100644 --- a/src_colibri2/theories/LRA/fourier.ml +++ b/src_colibri2/theories/LRA/fourier.ml @@ -220,33 +220,28 @@ let fm (d:Egraph.t) = aux eqs vars module Daemon = struct - type event = unit - - let print_event = Unit.pp + let key = + Events.Dem.create + ( module struct + type t = unit + let name = "LRA.fourier" + end ) let enqueue d _ = if Datastructure.Ref.Ro.get scheduled d - then Events.Wait.EnqAlready + then Events.EnqAlready else begin Datastructure.Ref.Ro.set scheduled d true; - Events.Wait.EnqRun () + Events.EnqRun (key,()) end - let key = - Events.Dem.create_key - ( module struct - type d = unit - type t = unit - let name = "LRA.fourier" - end ) - let delay = Events.Delayed_by 64 type runable = unit let print_runable = Unit.pp - let run d () = fm d; None + let run d () = fm d end let () = Egraph.Wait.register_dem (module Daemon) @@ -257,11 +252,11 @@ let converter d (f:Ground.t) = match Ground.sem f with | { app = {builtin = (Expr.Lt|Expr.Leq|Expr.Geq|Expr.Gt)}; tyargs = []; args } -> let attach n = - Egraph.attach_dom d n Dom_polynome.dom Daemon.key (); - Egraph.attach_node d n Daemon.key (); + Egraph.attach_dom d n Dom_polynome.dom Daemon.enqueue; + Egraph.attach_repr d n Daemon.enqueue; in IArray.iter ~f:attach args; - Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key (); + Egraph.attach_value d (Ground.node f) Boolean.dom (fun d n _ -> Daemon.enqueue d n); Datastructure.Push.push comparisons d f; Egraph.register_delayed_event d Daemon.key (); Egraph.register_decision d (Boolean.chobool (Ground.node f)) diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml index 415dd7e449738d7e7f19521d0d139b5391cb6c1e..2d078b586480accbd5f4adbdb065c903fa07151e 100644 --- a/src_colibri2/theories/LRA/mul.ml +++ b/src_colibri2/theories/LRA/mul.ml @@ -18,12 +18,11 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -let attach = - Demon.Fast.register_get_value_daemon - ~name:"Mul.get_value" - (module RealValue) - (fun d _ q (mul,other) -> - Dom_polynome.assume_poly_equality d mul (Polynome.monome q other) +let attach d n (mul,other) = + Daemon.attach_value d n + RealValue.key + (fun d _ q -> + Dom_polynome.assume_poly_equality d mul (Polynome.monome (RealValue.value q) other) ) let converter d (f:Ground.t) = diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml index 4cc827f26275e8b7e66e231cef3a268e2419f9d1..fa6ef5cdc155d10d864faa4e3f39dc25851e14f5 100644 --- a/src_colibri2/theories/LRA/realValue.ml +++ b/src_colibri2/theories/LRA/realValue.ml @@ -22,9 +22,9 @@ open Colibri2_core open Colibri2_popop_lib open Colibri2_stdlib.Std -module RealValue = ValueKind.Register(struct +module RealValue = Value.Register(struct include Q - let key = ValueKind.create_key (module struct type t = Q.t let name = "Q" end) + let name = "Q" end) include RealValue @@ -35,25 +35,11 @@ let cst c = node (cst' c) let zero = cst Q.zero let one = cst Q.one -let wait_for_this_node_get_a_value = - Demon.Fast.register_get_value_daemon - ~name:"GotRealValue" - ~pp:Fmt.nop - (module RealValue) - (fun d n v f -> f d n v) - -let wait_for_this_node_get_a_value_bool = - Demon.Fast.register_get_value_daemon - ~name:"GotRealValue.bool" - ~pp:Fmt.nop - (module Boolean.BoolValue) - (fun d n v f -> f d n v) - module Monad : sig type ('a,'b) monad = Egraph.t -> Node.t -> 'a -> 'b - val get: Node.t -> (Q.t,Q.t option) monad + val get: Node.t -> (RealValue.t,Q.t option) monad val set: Node.t -> ('a,Q.t option) monad -> ('a,unit) monad - val getb: Node.t -> (bool,bool option) monad + val getb: Node.t -> (Boolean.BoolValue.t,bool option) monad val setb: Node.t -> ('a,bool option) monad -> ('a,unit) monad val (let+): ('a,'b option) monad -> ('b -> 'c) -> ('a,'c option) monad val (let*): ('a,'b option) monad -> ('b -> 'c option) -> ('a,'c option) monad @@ -61,13 +47,17 @@ module Monad : sig val (&&): ('a,unit) monad -> ('a,unit) monad -> ('a,unit) monad end = struct type ('a,'b) monad = Egraph.t -> Node.t -> 'a -> 'b - let [@ocaml.always inline] get' key n' = fun d n v -> - if Node.equal n n' then Some v else + let [@ocaml.always inline] get' : type c b. + (module Value.S with type s = b and type t = c) -> + Node.t -> (c, b option) monad = + fun value n' d n v -> + let module V = (val value) in + if Node.equal n n' then Some (V.value v) else let open CCOpt in let* v = Egraph.get_value d n' in - Value.value key v - let [@ocaml.always inline] set' : type b. - (module ValueKind.Registered with type s = b) -> + Base.Option.map ~f:V.value (V.of_nodevalue v) + let [@ocaml.always inline] set' : type c b. + (module Value.S with type s = b and type t = c) -> Node.t -> ('a,b option) monad -> ('a, unit) monad = fun value n' v' d n v -> let module V = (val value) in @@ -75,9 +65,9 @@ end = struct Option.iter (fun (v':b) -> Egraph.set_value d n' (V.nodevalue (V.index v'))) (v' d n v) - let [@ocaml.always inline] get a = get' key a + let [@ocaml.always inline] get a = get' (module RealValue) a let [@ocaml.always inline] set a = set' (module RealValue) a - let getb a = get' Boolean.BoolValue.key a + let getb a = get' (module Boolean.BoolValue) a let setb a = set' (module Boolean.BoolValue) a let [@ocaml.always inline] (let+) a (f:'b -> 'a) = fun d n v -> Option.map f (a d n v) let [@ocaml.always inline] (let*) a (f:'b -> 'a option) = fun d n v -> Option.bind (a d n v) f @@ -199,6 +189,9 @@ module Check = struct Interp.WatchArgs.create d f g end +let wait_for_this_node_get_a_value d n = + Daemon.attach_value d n RealValue.key + (** {2 Initialization} *) let converter d (f:Ground.t) = let r = Ground.node f in diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli index 4bfd3fa336fa206dc010cf97db1ed7af15cb0b69..0dc4824cb0edf385ad5ffe7355875d3e03e89b8e 100644 --- a/src_colibri2/theories/LRA/realValue.mli +++ b/src_colibri2/theories/LRA/realValue.mli @@ -18,7 +18,7 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -include ValueKind.Registered with type s = Q.t +include Value.S with type s = Q.t val cst': Q.t -> t val cst: Q.t -> Node.t diff --git a/src_colibri2/theories/bool/.ocamlformat-ignore b/src_colibri2/theories/bool/.ocamlformat-ignore index 79df3ce7b5a14dceda726de31dd2728842dc0de5..63183a891144f98b32f068b6ce03543d924f2864 100644 --- a/src_colibri2/theories/bool/.ocamlformat-ignore +++ b/src_colibri2/theories/bool/.ocamlformat-ignore @@ -1,4 +1,2 @@ -equality.ml boolean.ml boolean.mli -equality.mli diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml index 8598cef8ec2c402e0e2e104e0335ef7baf0269a6..fdcb9c426996611fab5cba71f88dd50da9ef291a 100644 --- a/src_colibri2/theories/bool/boolean.ml +++ b/src_colibri2/theories/bool/boolean.ml @@ -29,13 +29,13 @@ let debug = Debug.register_info_flag ~desc:"for the boolean theory" "bool" -let dom = ValueKind.create_key (module struct type t = bool let name = "bool" end) - -module BoolValue = ValueKind.Register(struct +module BoolValue = Value.Register(struct include DBool - let key = dom + let name = "bool" end) +let dom = BoolValue.key + let value_true = BoolValue.index ~basename:"⊤" true let values_true = BoolValue.nodevalue value_true let node_true = BoolValue.node value_true @@ -135,16 +135,10 @@ module TwoWatchLiteral = struct let print_runable = Fmt.nop - type event = t - - let print_event fmt r = Ground.pp fmt r.ground - let key = - Events.Dem.create_key + Events.Dem.create (module struct - type d = runable - - type t = event + type t = runable let name = "Interp.TwoWatchLiteral" end) @@ -176,32 +170,32 @@ module TwoWatchLiteral = struct if i = stop then LimitReached else check_if_equal_or_set d args absorbent incr stop i n - let attach d r i = - Egraph.Ro.attach_value d - (IArray.get (Ground.sem r.ground).args i) BoolValue.key key r; - Egraph.Ro.attach_node d (IArray.get (Ground.sem r.ground).args i) key r + let run d r = r d - let run d r = r d; None + let rec attach d r i = + Egraph.Ro.attach_value d + (IArray.get (Ground.sem r.ground).args i) BoolValue.key (fun d _ _ -> enqueue d r); + Egraph.Ro.attach_repr d (IArray.get (Ground.sem r.ground).args i) (fun d _ -> enqueue d r); - let enqueue d r = + and enqueue d r = let o_from_start = Context.Ref.get r.from_start in let o_from_end = Context.Ref.get r.from_end in let args = (Ground.sem r.ground).args in - if o_from_start = o_from_end then Events.Wait.EnqStopped + if o_from_start = o_from_end then Events.EnqStopped else match Egraph.Ro.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.Wait.EnqLast(fun d -> IArray.iter ~f:(fun a -> Egraph.set_value d a v) args) + Events.EnqLast(key,fun d -> IArray.iter ~f:(fun a -> Egraph.set_value d a v) args) | _ -> let n_end = IArray.get args o_from_end in match check_if_equal_or_set d args r.absorbent (+1) o_from_end o_from_start n_end with | LimitReached -> Context.Ref.set r.from_start o_from_end; - Events.Wait.EnqLast(fun d -> Egraph.merge d n_end (Ground.node r.ground)) + Events.EnqLast(key,fun d -> Egraph.merge d n_end (Ground.node r.ground)) | Absorbent -> - Events.Wait.EnqLast(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent) + Events.EnqLast(key,fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent) | ToWatch from_start -> if from_start <> o_from_start then ( Context.Ref.set r.from_start from_start; @@ -211,22 +205,15 @@ module TwoWatchLiteral = struct match check_if_equal_or_set d args r.absorbent (-1) from_start o_from_end n_start with | LimitReached -> Context.Ref.set r.from_end from_start; - Events.Wait.EnqLast (fun d -> Egraph.merge d n_start (Ground.node r.ground)) + Events.EnqLast (key,fun d -> Egraph.merge d n_start (Ground.node r.ground)) | Absorbent -> - Events.Wait.EnqLast (fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent) + Events.EnqLast (key,fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent) | ToWatch from_end when from_end = o_from_end -> - Events.Wait.EnqAlready + Events.EnqAlready | ToWatch from_end -> Context.Ref.set r.from_end from_end; attach d r from_end; - Events.Wait.EnqAlready - - let enqueue d event = - match event with - | Events.Fired.EventValue (_, _, r) - | Events.Fired.EventChange (_, r) -> - enqueue d r - | _ -> raise Impossible + Events.EnqAlready let create d absorbent ground = let args = (Ground.sem ground).args in @@ -273,13 +260,8 @@ module TwoWatchLiteral = struct let create = Daemon.create end -let wait_for_this_node_get_a_value = - Demon.Fast.register_get_value_daemon - ~name:"GotBoolValue.bool" - ~pp:Fmt.nop - (module BoolValue) - (fun d n v f -> f d n v) - +let wait_for_this_node_get_a_value d n = + Daemon.attach_value d n BoolValue.key let converter d (f:Ground.t) = let res = Ground.node f in @@ -302,12 +284,13 @@ let converter d (f:Ground.t) = let a,b = IArray.extract2_exn args in reg_args args; let wait d n v = - if Node.equal n res then + let v = BoolValue.value v in + if Egraph.is_equal d n res then if not v then (set_bool d a true; set_bool d b false); - if Node.equal n a then - (if v then (if is_true d res then set_bool d b true) + if Egraph.is_equal d n a then + (if v then Egraph.merge d res b else set_bool d res true); - if Node.equal n b then + if Egraph.is_equal d n b then if v then set_bool d res true else if is_true d res then set_bool d a false in @@ -315,8 +298,8 @@ let converter d (f:Ground.t) = | { app = {builtin = Expr.Neg}; tyargs = []; args; _ } -> let a = IArray.extract1_exn args in reg_args args; - wait_for_this_node_get_a_value d a (fun d _ v -> set_bool d res (not v)); - wait_for_this_node_get_a_value d res (fun d _ v -> set_bool d a (not v)) + wait_for_this_node_get_a_value d a (fun d _ v -> set_bool d res (not (BoolValue.value v))); + wait_for_this_node_get_a_value d res (fun d _ v -> set_bool d a (not (BoolValue.value v))) | { app = {builtin = Expr.True}; tyargs = []; args; _ } -> assert ( IArray.is_empty args); reg _true diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli index b44c27b845cb39f81a58dc55d464365e65fba9e6..013097eb5fda964b7a2a9340c022f7d594deee2f 100644 --- a/src_colibri2/theories/bool/boolean.mli +++ b/src_colibri2/theories/bool/boolean.mli @@ -18,8 +18,6 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -val dom: bool ValueKind.t - val _true : Node.t val _false : Node.t val _and : Node.t list -> Node.t @@ -44,7 +42,9 @@ val chobool: Node.t -> Egraph.choice (* val make_dec: Variable.make_dec *) -module BoolValue : ValueKind.Registered with type s = bool +module BoolValue : Value.S with type s = bool + +val dom: (bool,BoolValue.t) Value.Kind.t val value_true : BoolValue.t val value_false: BoolValue.t diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml index 8afe5938cc30724cf8ada117b4584b9caedc9884..0819e59297ec946de213bac1279301da2c95a6ff 100644 --- a/src_colibri2/theories/bool/equality.ml +++ b/src_colibri2/theories/bool/equality.ml @@ -22,143 +22,183 @@ open Colibri2_popop_lib open Popop_stdlib open Colibri2_core -let debug = Debug.register_info_flag - ~desc:"for the equality and disequality predicate" - "disequality" +let debug = + Debug.register_info_flag ~desc:"for the equality and disequality predicate" + "disequality" (** {2 theory term} *) -type t = Node.S.t (** Is there two elements equal *) -let sem = ThTermKind.create_key (module struct type nonrec t = t let name = "Eq" end) - module Th = struct - let inv s = not (Node.M.is_empty s || Node.M.is_num_elt 1 s) let only_two s = assert (inv s); if Node.M.is_num_elt 2 s then let enum = Node.M.start_enum s in - let (cl1,()), enum = Opt.get (Node.M.val_enum enum), Node.M.next_enum enum in - let (cl2,()) = Opt.get (Node.M.val_enum enum) in - Some (cl1,cl2) + let (cl1, ()), enum = + (Opt.get (Node.M.val_enum enum), Node.M.next_enum enum) + in + let cl2, () = Opt.get (Node.M.val_enum enum) in + Some (cl1, cl2) else None - module T : OrderedHashedType with type t = Node.S.t = struct include Node.S - let hash s = Node.S.fold (fun e acc -> Hashcons.combine acc (Node.hash e)) s 29 + let hash s = + Node.S.fold (fun e acc -> Hashcons.combine acc (Node.hash e)) s 29 let pp fmt s = assert (inv s); match only_two s with - | Some (cl1,cl2) -> - Format.fprintf fmt "%a=@,%a" Node.pp cl1 Node.pp cl2 + | Some (cl1, cl2) -> Format.fprintf fmt "%a=@,%a" Node.pp cl1 Node.pp cl2 | None -> - let aux fmt m = Node.S.elements m - |> Format.(list ~sep:(const char ',') Node.pp) fmt - in - Format.fprintf fmt "or=(%a)" aux s + let aux fmt m = + Node.S.elements m |> Format.(list ~sep:(const char ',') Node.pp) fmt + in + Format.fprintf fmt "or=(%a)" aux s end include T - include MkDatatype(T) - - let key = sem + include MkDatatype (T) + let name = "Eq" end -module ThE = ThTermKind.Register(Th) +module ThE = ThTerm.Register (Th) (** {2 disequality domains} *) module Dis : sig type t + type elt - val pp: t Format.printer - val pp_elt: elt Format.printer - val empty: t - val of_node: ThE.t -> elt - val to_node: elt -> ThE.t - val test_disjoint: (elt -> unit) -> t -> t -> t + + val pp : t Format.printer + + val pp_elt : elt Format.printer + + val empty : t + + val of_node : ThE.t -> elt + + val to_node : elt -> ThE.t + + val test_disjoint : (elt -> unit) -> t -> t -> t + val disjoint : t -> t -> bool + val singleton : elt -> t + val inter : t -> t -> t + val is_empty : t -> bool + val choose : t -> elt + val iter : (elt -> unit) -> t -> unit end = struct type t = ThE.S.t + type elt = ThE.t + let empty = ThE.S.empty + let pp_elt = ThE.pp + let pp fmt s = let aux fmt m = ThE.M.bindings m - |> Format.(list ~sep:(const char ';') - (pair ~sep:(const char ',') ThE.pp Pp.nothing)) fmt + |> Format.( + list ~sep:(const char ';') + (pair ~sep:(const char ',') ThE.pp Pp.nothing)) + fmt in Format.fprintf fmt "{%a}" aux s + let of_node x = x + let to_node x = x + let test_disjoint f m1 m2 = - ThE.M.union (fun k () () -> f k; Some ()) m1 m2 + ThE.M.union + (fun k () () -> + f k; + Some ()) + m1 m2 + let disjoint = ThE.S.disjoint + let singleton = ThE.S.singleton + let is_empty = ThE.S.is_empty + let inter m1 m2 = ThE.S.inter m1 m2 + let choose m1 = ThE.S.choose m1 + let iter = ThE.S.iter end -let dom = DomKind.create_key (module struct type t = Dis.t let name = "dis" end) +let dom = + Dom.Kind.create + (module struct + type t = Dis.t -(** For each value key give the value *) -module MValues = ValueKind.MkMap(struct type ('a, _) t = 'a end) + let name = "dis" + end) module D = struct type t = Dis.t - let merged (b1:t option) (b2 :t option) = - match b1,b2 with - | Some b1, Some b2 -> Equal.physical b1 b2 (** not Dis.equality *) + let merged (b1 : t option) (b2 : t option) = + match (b1, b2) with + | Some b1, Some b2 -> Equal.physical b1 b2 (* not Dis.equality *) (* Really? Explanation needed...*) | None, None -> true | _ -> false - let merge d (s1,cl1) (s2,cl2) _ = - match s1, s2 with + let merge d (s1, cl1) (s2, cl2) _ = + match (s1, s2) with | None, None -> raise Impossible - | Some s, None -> - Egraph.set_dom d dom cl2 s - | None, Some s -> - Egraph.set_dom d dom cl1 s + | Some s, None -> Egraph.set_dom d dom cl2 s + | None, Some s -> Egraph.set_dom d dom cl1 s | Some s1, Some s2 -> - let s = Dis.test_disjoint (fun c -> - Debug.dprintf6 Egraph.print_contradiction - "[Equality] The currently merged %a and %a are different since %a" - Node.pp cl1 Node.pp cl2 Dis.pp_elt c; - Egraph.contradiction d) s1 s2 in - Egraph.set_dom d dom cl1 s; - Egraph.set_dom d dom cl2 s - + let s = + Dis.test_disjoint + (fun c -> + Debug.dprintf6 Egraph.print_contradiction + "[Equality] The currently merged %a and %a are different since \ + %a" + Node.pp cl1 Node.pp cl2 Dis.pp_elt c; + Egraph.contradiction d) + s1 s2 + in + Egraph.set_dom d dom cl1 s; + Egraph.set_dom d dom cl2 s let pp fmt s = Dis.pp fmt s + let key = dom end -let () = DomKind.register(module D) +let () = Dom.register (module D) let set_dom d cl s = - let s = match Egraph.get_dom d dom cl with + let s = + match Egraph.get_dom d dom cl with | Some s' -> - Debug.dprintf4 debug "[%a %a]" Dis.pp s Dis.pp s'; - Dis.test_disjoint (fun _ -> (* append if after a decision the truth value - is set before removing the daemon *)()) s' s - | None -> s in + Debug.dprintf4 debug "[%a %a]" Dis.pp s Dis.pp s'; + Dis.test_disjoint + (fun _ -> + (* append if after a decision the truth value + is set before removing the daemon *) + ()) + s' s + | None -> s + in Egraph.set_dom d dom cl s let check_sem v cl = @@ -172,333 +212,225 @@ let equality cll = let fold acc e = Node.S.add_new Exit e acc in let s = List.fold_left fold Node.S.empty cll in ThE.node (ThE.index s) - with Exit -> - Boolean._true + with Exit -> Boolean._true let disequality cll = Boolean._not (equality cll) let is_equal t cl1 cl2 = Egraph.is_equal t cl1 cl2 + let is_disequal t cl1 cl2 = - not (Egraph.is_equal t cl1 cl2) && + (not (Egraph.is_equal t cl1 cl2)) + && let dom1 = Egraph.get_dom t dom cl1 in let dom2 = Egraph.get_dom t dom cl2 in - match dom1, dom2 with + match (dom1, dom2) with | Some s1, Some s2 -> not (Dis.disjoint s1 s2) | _ -> false +(** each instance of this tag must not be == *) let new_tag n = let n = Dis.of_node n in - n, fun () -> Dis.singleton n (** each instance of this tag must not be == *) + (n, fun () -> Dis.singleton n) exception Found of Node.t * Node.t let find_not_disequal d s = - let is_disequal (dis1,values1) (dis2,values2) = - (match dis1, dis2 with - | Some dis1, Some dis2 when not (Dis.disjoint dis1 dis2) -> true - | _ -> false) || - (match values1, values2 with - | Some v1, Some v2 -> not (Value.equal v1 v2) - | _ -> false) + let is_disequal (dis1, values1) (dis2, values2) = + (match (dis1, dis2) with + | Some dis1, Some dis2 when not (Dis.disjoint dis1 dis2) -> true + | _ -> false) + || + match (values1, values2) with + | Some v1, Some v2 -> not (Value.equal v1 v2) + | _ -> false in let get_dis_and_values cl = - Egraph.get_dom d dom cl, - Egraph.get_value d cl + (Egraph.get_dom d dom cl, Egraph.get_value d cl) in assert (Th.inv s); let rec inner_loop cl1 s1 enum2 = - match enum2, s1 with - | [],_ -> () - | (_,d1)::enum2,d2 when is_disequal d1 d2 -> - inner_loop cl1 s1 enum2 - | (cl2,_)::_,_ -> - raise (Found (cl1,cl2)) + match (enum2, s1) with + | [], _ -> () + | (_, d1) :: enum2, d2 when is_disequal d1 d2 -> inner_loop cl1 s1 enum2 + | (cl2, _) :: _, _ -> raise (Found (cl1, cl2)) in let rec outer_loop enum1 = match enum1 with | [] -> () - | (cl1,s1)::enum1 -> - inner_loop cl1 s1 enum1; - outer_loop enum1 in + | (cl1, s1) :: enum1 -> + inner_loop cl1 s1 enum1; + outer_loop enum1 + in try - let s = Node.M.fold_left (fun acc cl () -> - (cl,get_dis_and_values cl)::acc) [] s in + let s = + Node.M.fold_left + (fun acc cl () -> (cl, get_dis_and_values cl) :: acc) + [] s + in outer_loop s; - (** Here we are keeping data because currently + (* Here we are keeping data because currently we are not keeping data for domains globally *) `AllDiff s - with Found (cl1,cl2) -> - `Found (cl1,cl2) + with Found (cl1, cl2) -> `Found (cl1, cl2) let norm_set d the = let v = ThE.sem the in let own = ThE.node the in try - ignore (Node.S.fold_left (fun acc e0 -> - let e = Egraph.find_def d e0 in - Node.M.add_change (fun _ -> e0) - (fun e0 e0' -> raise (Found(e0',e0))) - e e0 acc) - Node.M.empty v); + ignore + (Node.S.fold_left + (fun acc e0 -> + let e = Egraph.find_def d e0 in + Node.M.add_change + (fun _ -> e0) + (fun e0 e0' -> raise (Found (e0', e0))) + e e0 acc) + Node.M.empty v); false - with Found (_e1,_e2) -> - (** TODO remove that and choose what to do. ex: int real *) + with Found (_e1, _e2) -> + (* TODO remove that and choose what to do. ex: int real *) Boolean.set_true d own; true module ChoEquals = struct - let make_equal the (cl1,cl2) d = + let make_equal the (cl1, cl2) d = Debug.dprintf6 Egraph.print_decision - "[Equality] @[decide on merge of %a and %a in %a@]" - Node.pp cl1 Node.pp cl2 ThE.pp the; + "[Equality] @[decide on merge of %a and %a in %a@]" Node.pp cl1 Node.pp + cl2 ThE.pp the; Egraph.register d cl1; Egraph.register d cl2; Egraph.merge d cl1 cl2 - let make_disequal the (cl1,cl2) d = + let make_disequal the (cl1, cl2) d = Debug.dprintf6 Egraph.print_decision - "[Equality] @[decide on merge of %a and %a in %a@]" - Node.pp cl1 Node.pp cl2 ThE.pp the; + "[Equality] @[decide on merge of %a and %a in %a@]" Node.pp cl1 Node.pp + cl2 ThE.pp the; Egraph.register d cl1; Egraph.register d cl2; let _dis, stag = new_tag the in - List.iter (fun cl -> set_dom d cl (stag ())) [cl1;cl2] + List.iter (fun cl -> set_dom d cl (stag ())) [ cl1; cl2 ] let choose_decision the d = let v = ThE.sem the in let own = ThE.node the in - Debug.dprintf4 debug "[Equality] @[dec on %a for %a@]" - Node.pp own ThE.pp the; - if Boolean.is_false d own - then Egraph.DecNo - else if norm_set d the - then Egraph.DecNo - else - match find_not_disequal d v with - | `AllDiff _ -> + Debug.dprintf4 debug "[Equality] @[dec on %a for %a@]" Node.pp own ThE.pp + the; + if Boolean.is_false d own then Egraph.DecNo + else if norm_set d the then Egraph.DecNo + else + match find_not_disequal d v with + | `AllDiff _ -> Boolean.set_false d own; DecNo - | `Found (cl1,cl2) -> - DecTodo [make_equal the (cl1,cl2);make_disequal the (cl1,cl2)] - - let mk_choice the = { - Egraph.choice = choose_decision the; - prio = 1; - } + | `Found (cl1, cl2) -> + DecTodo [ make_equal the (cl1, cl2); make_disequal the (cl1, cl2) ] + let mk_choice the = { Egraph.choice = choose_decision the; prio = 1 } end let norm_dom d the = let v = ThE.sem the in let own = ThE.node the in - if norm_set d the - then Demon.AliveStopped - else begin - Debug.dprintf4 debug "[Equality] @[norm_dom %a %a@]" - Node.pp own Th.pp v; + if norm_set d the then DaemonWithKey.Stop + else ( + Debug.dprintf4 debug "[Equality] @[norm_dom %a %a@]" Node.pp own Th.pp v; match Boolean.is d own with | Some false -> - let _dis, stag = new_tag the in - Debug.dprintf2 debug "[Dis: %a]" Dis.pp (stag ()); - Node.S.iter (fun cl -> set_dom d cl (stag ())) v; - Demon.AliveStopped - | Some true -> - begin match Th.only_two v with - | Some (cl1,cl2) -> - Egraph.merge d cl1 cl2; Demon.AliveStopped - | None -> - match find_not_disequal d v with - | `AllDiff _ -> - Boolean.set_false d own; (** contradiction *) - raise Impossible - | `Found _ -> - Demon.AliveStopped - end - | None -> - match find_not_disequal d v with - | `AllDiff _ -> - Boolean.set_false d own; - Demon.AliveStopped - | `Found _ -> (** they are still not proved disequal *) - Demon.AliveReattached - end + let _dis, stag = new_tag the in + Debug.dprintf2 debug "[Dis: %a]" Dis.pp (stag ()); + Node.S.iter (fun cl -> set_dom d cl (stag ())) v; + DaemonWithKey.Stop + | Some true -> ( + match Th.only_two v with + | Some (cl1, cl2) -> + Egraph.merge d cl1 cl2; + DaemonWithKey.Stop + | None -> ( + match find_not_disequal d v with + | `AllDiff _ -> + Boolean.set_false d own; + (* contradiction *) + raise Impossible + | `Found _ -> DaemonWithKey.Stop)) + | None -> ( + match find_not_disequal d v with + | `AllDiff _ -> + Boolean.set_false d own; + DaemonWithKey.Stop + | `Found _ -> + (* they are still not proved disequal *) + DaemonWithKey.Wait)) (** Propagation *) -module DaemonPropa = struct - let key = Demon.Key.create "Equality.DaemonPropa" - - module Key = Th - module Data = DUnit - type info = unit let default = () +module DaemonPropa = Demon.Key.Register (struct + module Key = ThE let delay = Events.Delayed_by 1 - let wakeup d v _ev () = - norm_dom d (ThE.index v) - -end - -module RDaemonPropa = Demon.Key.Register(DaemonPropa) - -module DaemonInit = struct - let key = Demon.Key.create "Equality.DaemonInit" - - module Key = DUnit - module Data = DUnit - type info = unit let default = () - - let delay = Events.Immediate - let wakeup d () ev () = - List.iter - (function Events.Fired.EventRegSem(clsem,()) -> - begin - let clsem = ThE.coerce_thterm clsem in - let v = ThE.sem clsem in - let own = ThE.node clsem in - Node.S.iter (Egraph.register d) v; - let r = norm_dom d clsem in - begin match r with - | Demon.AliveReattached -> - let events = Node.S.fold (fun cl acc -> - (Demon.Create.EventChange(cl,())):: - (Demon.Create.EventDom(cl,dom,())):: - (Demon.Create.EventAnyValue(cl,())):: - acc - ) v [] in - let events = Demon.Create.EventValue(own,Boolean.dom,())::events in - Demon.Key.attach d DaemonPropa.key v events; - if true (* GenEquality.dodec (Th.get_ty v) *) then begin - Debug.dprintf4 debug "[Equality] @[ask_dec on %a for %a@]" - Node.pp own Th.pp v; - Egraph.register_decision d (ChoEquals.mk_choice clsem) - end - | _ -> () - end - end - | _ -> raise UnwaitedEvent - ) ev; - Demon.AliveReattached -end - -module RDaemonInit = Demon.Key.Register(DaemonInit) + let run = norm_dom + + let name = "Equality.DaemonPropa" +end) + +let attach_new_equalities d = + Daemon.attach_reg_sem d ThE.key (fun d clsem -> + let v = ThE.sem clsem in + let own = ThE.node clsem in + Node.S.iter (Egraph.register d) v; + let r = norm_dom d clsem in + match r with + | DaemonWithKey.Wait -> + Node.S.iter + (fun cl -> + DaemonPropa.attach_repr d cl clsem; + DaemonPropa.attach_dom d cl dom clsem; + DaemonPropa.attach_any_value d cl clsem) + v; + DaemonPropa.attach_value d own Boolean.dom clsem; + if true (* GenEquality.dodec (Th.get_ty v) *) then ( + Debug.dprintf4 debug "[Equality] @[ask_dec on %a for %a@]" Node.pp + own Th.pp v; + Egraph.register_decision d (ChoEquals.mk_choice clsem)) + | _ -> ()) (** ITE *) -module ITE = struct - - module TITE = struct - type t = {cond: Node.t; then_: Node.t; else_: Node.t} - [@@deriving eq,ord,hash] - let pp fmt x = - Format.fprintf fmt "ite(%a,%a,%a)" - Node.pp x.cond Node.pp x.then_ Node.pp x.else_ - end - - include TITE - include MkDatatype(TITE) - - let key = ThTermKind.create_key (module struct type nonrec t = t let name = "ite" end) - -end - -type ite = ITE.t = {cond: Node.t; then_: Node.t; else_: Node.t} - - -module EITE = ThTermKind.Register(ITE) +let simplify d own cond then_ else_ = + let branch = if cond then then_ else else_ in + (* Egraph.register d branch; *) + Egraph.merge d own branch -let ite cond then_ else_ = - Node.index_sem ITE.key { cond; then_; else_} +let delay = Events.Delayed_by 1 -module DaemonPropaITE = struct - let key = Demon.Fast.create "ITE.propa" +let throttle = 100 - module Data = EITE - - let simplify d the b = - let v = EITE.sem the in - let own = EITE.node the in - let branch = if b then v.then_ else v.else_ in - Egraph.register d branch; - Egraph.merge d own branch - - let delay = Events.Delayed_by 1 - let throttle = 100 - let wakeup d = function - | Events.Fired.EventValue(cond,_,clsem) -> - let v = EITE.sem clsem in - assert (Egraph.is_equal d cond v.cond); - begin match Boolean.is d v.cond with - | None -> assert false - | Some b -> simplify d clsem b - end - | _ -> raise UnwaitedEvent - -end - -module RDaemonPropaITE = Demon.Fast.Register(DaemonPropaITE) - -module DaemonInitITE = struct - let key = Demon.Fast.create "ITE.init" - - module Key = DUnit - module Data = DUnit - - let delay = Events.Delayed_by 1 - let throttle = 100 - let wakeup d = function - | Events.Fired.EventRegSem(clsem,()) -> - begin - let clsem = EITE.coerce_thterm clsem in - let v = EITE.sem clsem in - let own = EITE.node clsem in - match Boolean.is d v.cond with - | Some b -> - DaemonPropaITE.simplify d clsem b - | None -> - let clsem = EITE.index v in - assert (Node.equal (EITE.node clsem) own); - Egraph.register d v.cond; - Egraph.register d v.then_; - Egraph.register d v.else_; - Egraph.register_decision d (Boolean.chobool v.cond); - let events = [Demon.Create.EventValue(v.cond,Boolean.dom,clsem)] in - Demon.Fast.attach d DaemonPropaITE.key events - end - | _ -> raise UnwaitedEvent - -end - -module RDaemonInitITE = Demon.Fast.Register(DaemonInitITE) +let new_ite d own cond then_ else_ = + Daemon.attach_value d cond Boolean.dom (fun d _ v -> + simplify d own (Boolean.BoolValue.value v) then_ else_) (** {2 Link between diff and values} *) + (** 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 = if not (Egraph.is_equal d own n) then match Egraph.get_value d n with | None -> () - | Some v -> - they_are_different n v + | Some v -> they_are_different n v in Node.S.iter iter (ThE.sem (Dis.to_node elt)) in Dis.iter iter dis (** Give for a value the nodes that are different *) -let init_diff_to_value (type a) (type b) - ?(already_registered=([]: b list)) - d0 - ((module Val): (module Colibri2_core.ValueKind.Registered with type s = a and type t = b)) - ~(they_are_different:(Egraph.t -> Node.t -> a -> unit)) = - +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) = 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 @@ -511,133 +443,85 @@ let init_diff_to_value (type a) (type b) in Dis.iter iter dis in - let key = Demon.Fast.create (Format.asprintf "DiffToValue.%a" ValueKind.pp Val.key) - in - let module D = Demon.Fast.Register(struct - module Data = Val - let key = key - let throttle = 100 - let delay = Events.Delayed_by 1 - - let wakeup d = function - | Events.Fired.EventDom(_,_,v) -> - propagate_diff d v - | _ -> raise Impossible - end) - in - - let init d (v:Val.t) = + let init d (v : Val.t) = propagate_diff d v; - Demon.Fast.attach d key [Demon.Create.EventDom(Val.node v,dom,v)] + Daemon.attach_dom d (Val.node v) dom (fun d _ -> propagate_diff d v) in - Demon.Fast.register_init_daemon_value - ~name:(Format.asprintf "DiffToValue.Init.%a" ValueKind.pp Val.key) - (module Val) - init - d0; List.iter (init d0) already_registered (** {3 For booleans} *) (* Since the module Bool is linked before *) let bool_init_diff_to_value d = - init_diff_to_value - d (module Boolean.BoolValue) + init_diff_to_value d + (module Boolean.BoolValue) ~they_are_different:(fun d n b -> - if not b then Boolean.set_true d n - else Boolean.set_false d n - ) - ~already_registered:[Boolean.value_true;Boolean.value_false] + if not b then Boolean.set_true d n else Boolean.set_false d n) + ~already_registered:[ Boolean.value_true; Boolean.value_false ] (** {2 Interpretations} *) -(* let () = - * let interp ~interp t = - * try - * let fold acc e = Value.S.add_new Exit (interp e) acc in - * let _ = Node.S.fold_left fold Value.S.empty t in - * Boolean.values_false - * with Exit -> - * Boolean.values_true - * in - * Interp.Register.thterm sem interp - * - * let () = - * let interp ~interp (t:ITE.t) = - * let c = Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp t.cond)) in - * if c then interp t.then_ else interp t.else_ - * in - * Interp.Register.thterm ITE.key interp *) - let init_check d = Interp.Register.check d (fun d t -> let interp n = Opt.get_exn Impossible (Egraph.get_value d n) in - let (!>) n = - Boolean.BoolValue.value - (Boolean.BoolValue.coerce_nodevalue (interp n)) + let ( !> ) n = + Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp n)) in - let check r = - Some (Value.equal r (interp (Ground.node t))) - in - let (!<) b = + let check r = Some (Value.equal r (interp (Ground.node t))) in + let ( !< ) b = let r = if b then Boolean.values_true else Boolean.values_false in check r in match Ground.sem t with - | { app = {builtin = Expr.Equal}; tyargs = [_]; args; ty = _ } -> - assert (IArray.not_empty args); - !< (IArray.for_alli_non_empty_exn ~init:interp ~f:(fun _ a t -> Value.equal a (interp t)) args) - | { app = {builtin = Expr.Equiv}; tyargs = [_]; args; ty = _ } -> - let a,b = IArray.extract2_exn args in - !< (Value.equal (interp a) (interp b)) - | { app = {builtin = Expr.Distinct}; tyargs = [_]; args; ty = _ } -> - begin + | { app = { builtin = Expr.Equal }; tyargs = [ _ ]; args; ty = _ } -> + assert (IArray.not_empty args); + !<(IArray.for_alli_non_empty_exn ~init:interp + ~f:(fun _ a t -> Value.equal a (interp t)) + args) + | { app = { builtin = Expr.Equiv }; tyargs = [ _ ]; args; ty = _ } -> + let a, b = IArray.extract2_exn args in + !<(Value.equal (interp a) (interp b)) + | { app = { builtin = Expr.Distinct }; tyargs = [ _ ]; args; ty = _ } -> ( try let fold acc v = Value.S.add_new Exit (interp v) acc in let _ = IArray.fold ~f:fold ~init:Value.S.empty args in check Boolean.values_true - with Exit -> - check Boolean.values_false - end - | { app = {builtin = Expr.Ite}; tyargs = [_]; args; ty = _ } -> - let c,a,b = IArray.extract3_exn args in - check (if (!> c) then interp a else interp b) - | _ -> None - ) - + with Exit -> check Boolean.values_false) + | { app = { builtin = Expr.Ite }; tyargs = [ _ ]; args; ty = _ } -> + let c, a, b = IArray.extract3_exn args in + check (if !>c then interp a else interp b) + | _ -> None) -let converter d (t:Ground.t) = +let converter d (t : Ground.t) = let res = Ground.node t in let of_term n = Egraph.register d n; n in - let reg n = + let reg n = Egraph.register d n in + let reg_and_merge n = Egraph.register d n; Egraph.merge d res n in match Ground.sem t with - | { app = {builtin = Expr.Equal}; tyargs = [_]; args = l; _ } -> - reg (equality (List.map of_term (IArray.to_list l))) - | { app = {builtin = Expr.Equiv}; tyargs = [_]; args; _ } -> - let a,b = IArray.extract2_exn args in - reg (equality [of_term a;of_term b]) - | { app = {builtin = Expr.Distinct}; tyargs = [_]; args; _ } -> - reg (disequality (List.map of_term (IArray.to_list args))) - | { app = {builtin = Expr.Ite}; tyargs = [_]; args; _ } -> - let c,a,b = IArray.extract3_exn args in - reg (ite (of_term c) (of_term a) (of_term b)) - | { app = {builtin = Expr.Xor}; tyargs = []; args; _ } -> - let a,b = IArray.extract2_exn args in - reg (disequality ([of_term a;of_term b])) + | { app = { builtin = Expr.Equal }; tyargs = [ _ ]; args = l; _ } -> + IArray.iter ~f:reg l; + reg_and_merge (equality (IArray.to_list l)) + | { app = { builtin = Expr.Equiv }; tyargs = [ _ ]; args; _ } -> + let a, b = IArray.extract2_exn args in + reg_and_merge (equality [ of_term a; of_term b ]) + | { app = { builtin = Expr.Distinct }; tyargs = [ _ ]; args; _ } -> + IArray.iter ~f:reg args; + reg_and_merge (disequality (IArray.to_list args)) + | { app = { builtin = Expr.Ite }; tyargs = [ _ ]; args; _ } -> + let c, a, b = IArray.extract3_exn args in + new_ite d res (of_term c) (of_term a) (of_term b) + | { app = { builtin = Expr.Xor }; tyargs = []; args; _ } -> + let a, b = IArray.extract2_exn args in + reg_and_merge (disequality [ of_term a; of_term b ]) | _ -> () let th_register env = - RDaemonPropa.init env; - RDaemonInit.init env; - Demon.Key.attach env - DaemonInit.key () [Demon.Create.EventRegSem(sem,())]; - Demon.Fast.attach env - DaemonInitITE.key [Demon.Create.EventRegSem(ITE.key,())]; + attach_new_equalities env; Ground.register_converter env converter; bool_init_diff_to_value env; init_check env; diff --git a/src_colibri2/theories/bool/equality.mli b/src_colibri2/theories/bool/equality.mli index c9cbc7b0fbf16c1aa381443bd10d751ac3e123a6..eff0913697bde1c0211595f0b244cdeb3267132d 100644 --- a/src_colibri2/theories/bool/equality.mli +++ b/src_colibri2/theories/bool/equality.mli @@ -18,17 +18,15 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (*************************************************************************) -val equality : Node.t list -> Node.t -val disequality : Node.t list -> Node.t +val equality : Node.t list -> Node.t -val is_equal : Egraph.t -> Node.t -> Node.t -> bool -val is_disequal : Egraph.t -> Node.t -> Node.t -> bool +val disequality : Node.t list -> Node.t -val ite : Node.t -> Node.t -> Node.t -> Node.t +val is_equal : 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 +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 val th_register : Egraph.t -> unit diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml index 632f809a725f105ee129c8f8dc530b3bd4ef786f..c8e4a7c398b22cda0ed40c4effe7468ee8771be8 100644 --- a/src_colibri2/theories/quantifier/info.ml +++ b/src_colibri2/theories/quantifier/info.ml @@ -29,6 +29,8 @@ type t = { let _ = pp +(* let pp fmt _ = Fmt.pf fmt "Info" *) + (** because it is currently not hidden and too long *) let pp = Fmt.nop @@ -82,7 +84,7 @@ let merge d ~other ~repr info info' = let empty = { parents = F_Pos.M.empty; apps = F.M.empty } let dom = - DomKind.create_key + Dom.Kind.create (module struct type nonrec t = t diff --git a/src_colibri2/theories/quantifier/info.mli b/src_colibri2/theories/quantifier/info.mli index 700c2c538a4cbe16f3b91485ac9b686258d70c5a..a4c3229f1cd22860aaff7c019534e552eadf328b 100644 --- a/src_colibri2/theories/quantifier/info.mli +++ b/src_colibri2/theories/quantifier/info.mli @@ -29,4 +29,4 @@ val merge : Egraph.t -> other:Node.t -> repr:Node.t -> t -> t -> t val empty : t -val dom : t DomKind.t +val dom : t Dom.Kind.t diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml index 31107280f8f21a9800064e623412c6f94d6193c6..dc5d72ea103b97e03847b1856a39e97dcbb20f1b 100644 --- a/src_colibri2/theories/quantifier/pattern.ml +++ b/src_colibri2/theories/quantifier/pattern.ml @@ -150,7 +150,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) : Ground.S.fold_left (fun acc n -> let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in - assert (Term.Const.equal f pf); + assert (Expr.Term.Const.equal f pf); let substs = List.fold_left2 match_ty substs tyl ptyl in if Ground.Subst.S.is_empty substs then acc else @@ -193,7 +193,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool = Ground.S.exists (fun n -> let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in - assert (Term.Const.equal f pf); + assert (Expr.Term.Const.equal f pf); List.for_all2 (check_ty subst) tyl ptyl && IArray.for_all2_exn ~f:(check_term d subst) args pargs) s @@ -322,7 +322,7 @@ let match_any_term d subst (p : t) : Ground.Subst.S.t = Context.Push.fold (fun acc n -> let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in - assert (Term.Const.equal f pf); + assert (Expr.Term.Const.equal f pf); let substs = List.fold_left2 match_ty subst tyl ptyl in let substs = IArray.fold2_exn args pargs ~init:substs ~f:(match_term d) diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli index c32d8c7bee7114c4493fd93f759010dd464a8c16..f96c4a5bcae0eba896c631c540bf3e21da005b4c 100644 --- a/src_colibri2/theories/quantifier/pattern.mli +++ b/src_colibri2/theories/quantifier/pattern.mli @@ -61,7 +61,7 @@ val match_any_term : Egraph.t -> Ground.Subst.S.t -> t -> Ground.Subst.S.t for each substitution. Each return substitution corresponds to one given as input. *) -val get_pps : t -> PP.t list Term.Var.M.t +val get_pps : t -> PP.t list Expr.Term.Var.M.t (** [get_pps pat] return the parent-parent pairs in [pat] for each variables *) val env_ground_by_apps : Ground.t Context.Push.t F.EnvApps.t diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml index b450256768b8fe6895c6e4aa75733fe46b2f8ed6..421efa0654a3933030bda635773042490c9aa003 100644 --- a/src_colibri2/theories/quantifier/quantifier.ml +++ b/src_colibri2/theories/quantifier/quantifier.ml @@ -138,18 +138,10 @@ let process_inverted_path d n acc = acc module Delayed_find_new_event = struct - type event = unit - - let print_event = Unit.pp - - let enqueue _ _ = assert false - let key = - Events.Dem.create_key + Events.Dem.create (module struct - type d = Node.t * InvertedPath.t list - - type t = unit + type t = Node.t * InvertedPath.t list let name = "Quantifier.new_event" end) @@ -160,15 +152,13 @@ module Delayed_find_new_event = struct let print_runable = pp_runable - let run d (n, ips) = - process_inverted_path d n ips; - None + let run d (n, ips) = process_inverted_path d n ips end let () = Egraph.Wait.register_dem (module Delayed_find_new_event) let () = - DomKind.register + Dom.register (module struct type t = Info.t [@@deriving show] @@ -215,11 +205,10 @@ let skolemize d (e : Ground.ClosedQuantifier.t) = Egraph.register d n; n -let attach = - Demon.Fast.register_get_value_daemon ~name:"Quantifier.get_value" - (module Boolean.BoolValue) - (fun d n b th -> - match (Ground.ThClosedQuantifier.sem th, b) with +let attach d th = + Daemon.attach_value d (Ground.ThClosedQuantifier.node th) + Boolean.BoolValue.key (fun d n b -> + match (Ground.ThClosedQuantifier.sem th, Boolean.BoolValue.value b) with | ({ binder = Exists; _ } as e), true | ({ binder = Forall; _ } as e), false -> Debug.dprintf2 debug "[Quant] Skolemize %a" @@ -241,7 +230,7 @@ let attach = let quantifier_registered d th = let n = Ground.ThClosedQuantifier.node th in if Boolean.is_unknown d n then Egraph.register_decision d (Boolean.chobool n); - attach d n th + attach d th (** Verify that this term is congruent closure to another already existing term So it is useless. f(a) is useless if a == b and f(a) == f(b) and f(b) is @@ -300,10 +289,8 @@ let add_info_on_ground_terms d thg = Context.Push.iter (fun trg -> Trigger.match_ d trg res) trgs let th_register d = - let delay = Events.Delayed_by 10 in - Demon.Fast.register_init_daemon ~delay ~name:"Quantifier.new_quantifier" - (module Ground.ThClosedQuantifier) - quantifier_registered d; + (* let delay = Events.Delayed_by 10 in *) + Daemon.attach_reg_sem d Ground.ThClosedQuantifier.key quantifier_registered; Ground.register_converter d (fun d g -> if not (application_useless d g) then add_info_on_ground_terms d g) diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml index b087c792fb5d680e8bd62fec7fb1110583f243e4..06bcff579d6b6382a5868e70aa7fcc059154c875 100644 --- a/src_colibri2/theories/quantifier/trigger.ml +++ b/src_colibri2/theories/quantifier/trigger.ml @@ -172,7 +172,9 @@ let get_user_triggers (cq : Ground.ThClosedQuantifier.t) = (function | [ pat ] -> let sty, st = - Expr.Term.free_vars (Ty.Var.S.empty, Term.Var.S.empty) pat + Expr.Term.free_vars + (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) + pat in if Expr.Ty.Var.S.subset tyvs sty && Expr.Term.Var.S.subset tvs st then @@ -212,18 +214,10 @@ let instantiate_aux d tri subst = Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form) module Delayed_instantiation = struct - type event = unit - - let print_event = Unit.pp - - let enqueue _ _ = assert false - let key = - Events.Dem.create_key + Events.Dem.create (module struct - type d = t * Ground.Subst.t - - type t = unit + type nonrec t = t * Ground.Subst.t let name = "delayed_instantiation" end) @@ -240,8 +234,7 @@ module Delayed_instantiation = struct subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp tri.pat Fmt.(list ~sep:comma Pattern.pp) tri.checks; - instantiate_aux d tri subst; - None + instantiate_aux d tri subst end let () = Egraph.Wait.register_dem (module Delayed_instantiation) diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml index 1dcca5ac3ffbde7fd6f8c463f709d1b69980586e..490978b0830bdcca1cda506eea1dbca186ceca3c 100644 --- a/src_colibri2/theories/quantifier/uninterp.ml +++ b/src_colibri2/theories/quantifier/uninterp.ml @@ -48,7 +48,7 @@ open Colibri2_core * include T * include MkDatatype(T) * - * let key = ThTermKind.create_key (module struct type nonrec t = t let name = "UF" end) + * let key = ThTermKind.create (module struct type nonrec t = t let name = "UF" end) * * end * @@ -206,7 +206,7 @@ open Colibri2_core module USModel = struct type usv = { id : DInt.t; ty : Ground.Ty.t } - module US = ValueKind.Register (struct + module US = Value.Register (struct module T = struct type t = usv = { id : DInt.t; ty : Ground.Ty.t } [@@deriving eq, ord, hash] @@ -217,13 +217,7 @@ module USModel = struct include T include MkDatatype (T) - let key = - ValueKind.create_key - (module struct - type nonrec t = t - - let name = "US" - end) + let name = "US" end) module H = Datastructure.Memo (Ground.Ty) @@ -300,12 +294,8 @@ module UFModel = struct let h = HConst.find env d { tc = g.app; ta = g.tyargs } in Hargs.set h lv v - let waiter = - Demon.Fast.register_simply ~delay:FixingModel - "Uninterp.UFModel.propagate_value" - let on_uninterpreted_domain d g = - let check_or_update g d _ = + let check_or_update g d _ _ = let interp n = Base.Option.value_exn (Egraph.get_value d n) in let s = Ground.sem g in let lv = IArray.map ~f:interp s.args in @@ -319,7 +309,9 @@ module UFModel = struct Egraph.contradiction d) | None -> set d s lv v in - let f d g = waiter.for_any_value d (Ground.node g) (check_or_update g) in + let f d g = + Daemon.FixingModel.attach_any_value d (Ground.node g) (check_or_update g) + in f d g let init_attach_value d g =