From a9605bef464f13c4f6d4f5f464a2d7413c20218b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 11 Jun 2021 11:08:32 +0200
Subject: [PATCH] Restructure the interface of core
---
src_colibri2/bin/main.ml | 2 +-
src_colibri2/core/.ocamlformat-ignore | 1 -
src_colibri2/core/colibri2_core.ml | 294 +--
src_colibri2/core/colibri2_core.mli | 1615 +++++++++++++++++
src_colibri2/core/datastructure.ml | 1 -
src_colibri2/core/datastructure.mli | 1 -
src_colibri2/core/dune | 11 +-
src_colibri2/core/ground.ml | 68 +-
src_colibri2/core/ground.mli | 23 +-
src_colibri2/core/structures/dune | 13 -
src_colibri2/core/structures/expr.ml | 13 +-
src_colibri2/popop_lib/map_intf.ml | 2 +-
src_colibri2/solver/dune | 2 +-
src_colibri2/solver/scheduler.ml | 75 +-
src_colibri2/tests/tests_lib.ml | 8 +-
src_colibri2/theories/ADT/adt.ml | 24 +-
src_colibri2/theories/ADT/dune | 2 +-
src_colibri2/theories/FP/dune | 1 -
src_colibri2/theories/FP/float32.ml | 2 +-
src_colibri2/theories/FP/float64.ml | 2 +-
src_colibri2/theories/FP/fp.ml | 2 +-
src_colibri2/theories/LRA/LRA.ml | 2 +-
src_colibri2/theories/LRA/dom_interval.ml | 6 +-
src_colibri2/theories/LRA/dom_polynome.ml | 6 +-
src_colibri2/theories/LRA/dom_product.ml | 4 +-
src_colibri2/theories/LRA/dune | 2 +-
src_colibri2/theories/LRA/fourier.ml | 14 +-
src_colibri2/theories/LRA/stages/stage0/dune | 2 +-
src_colibri2/theories/LRA/stages/stage1/dune | 2 +-
src_colibri2/theories/bool/boolean.ml | 18 +-
src_colibri2/theories/bool/boolean.mli | 2 +-
src_colibri2/theories/bool/dune | 2 +-
src_colibri2/theories/bool/equality.ml | 18 +-
.../theories/quantifier/InvertedPath.ml | 2 +-
src_colibri2/theories/quantifier/dune | 2 +-
src_colibri2/theories/quantifier/info.ml | 5 +-
src_colibri2/theories/quantifier/pattern.ml | 6 +-
.../theories/quantifier/quantifier.ml | 26 +-
src_colibri2/theories/quantifier/trigger.ml | 29 +-
src_colibri2/theories/quantifier/trigger.mli | 8 +-
src_colibri2/theories/quantifier/uninterp.ml | 12 +-
41 files changed, 1987 insertions(+), 343 deletions(-)
create mode 100644 src_colibri2/core/colibri2_core.mli
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
index 6038d19ee..3d5e6f39f 100644
--- a/src_colibri2/bin/main.ml
+++ b/src_colibri2/bin/main.ml
@@ -35,7 +35,7 @@ let () =
| None -> "n/a"
| Some v -> Build_info.V1.Version.to_string v in
let info = Cmdliner.Term.info ~man ~version "Colibri2" in
- let theories = Colibri2_core.Egraph.default_theories () in
+ let theories = Colibri2_core.ForSchedulers.default_theories () in
let st,step_limit,show_steps = match Cmdliner.Term.eval (Options.state theories, info) with
| `Version | `Help -> exit 0
| `Error `Parse | `Error `Term | `Error `Exn -> exit 2
diff --git a/src_colibri2/core/.ocamlformat-ignore b/src_colibri2/core/.ocamlformat-ignore
index 2a3c74d09..bdfe1b0b3 100644
--- a/src_colibri2/core/.ocamlformat-ignore
+++ b/src_colibri2/core/.ocamlformat-ignore
@@ -5,7 +5,6 @@ structures/term.ml
structures/domKind.ml
structures/dune
structures/domKind.mli
-structures/expr.ml
datastructure.mli
env.mli
ground.mli
diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index 021442de6..a3bef017e 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -18,59 +18,10 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-(** 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
-(** 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:
-
- - 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
@@ -80,8 +31,7 @@ end
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 *)
+ (** Unique keys associated to each kind of ThTerm *)
module type S = Nodes.RegisteredThTerm
@@ -98,6 +48,8 @@ end
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}. *)
+(** One {!Value.t} can be associated to an equivalence class and a {!Value.t}
+ is associated to an uniq {!Node.t} *)
module Value = struct
module Kind : Keys.Key2 with type ('a, 'b) t = ('a, 'b) Nodes.ValueKind.t =
Nodes.ValueKind
@@ -115,7 +67,7 @@ end
(** 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 *)
+ when the domain is simple by {!Dom.Lattice} *)
module Dom = struct
module Kind : Keys.Key with type 'a t = 'a DomKind.t = DomKind
@@ -153,17 +105,24 @@ module Dom = struct
val key : t Kind.t
val inter : Egraph.t -> t -> t -> t option
- (** [inter d d1 d2] compute the intersection of
- [d1] and [d2] return [None] if it is empty *)
+ (** [inter d d1 d2] compute the intersection of [d1] and [d2] return [None]
+ if it is empty. In this last case a contradiction is reported *)
val is_singleton : Egraph.t -> t -> Value.t option
(** [is_singleton _ d] if [d] is
restricted to a singleton return the corresponding value *)
end
- (** [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 *)
- module Lattice (L : Lattice) = struct
+ (** [Lattice(L)] register a domain as a lattice. It returns useful function
+ for setting and updating the domain *)
+ module Lattice (L : Lattice) : sig
+ val set_dom : Egraph.t -> Node.t -> L.t -> unit
+ (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
+
+ val upd_dom : Egraph.t -> Node.t -> L.t -> unit
+ (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
+ [l] with the current value of the domain. *)
+ end = struct
module S = struct
type t = L.t
@@ -225,19 +184,18 @@ end
(** 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}
+ application are provided using {!Interp.Register.check}
+ - Enumerating the possible values for each node {!Interp.Register.node}
+ - Otherwise enumerating the possible values of each type
+ {!Interp.Register.ty}
*)
module Interp = Interp
-(** {3 Custom Environment } *)
+(** {3 Custom Environment and data-structures } *)
module Env = Env
-(** Environment *)
-
module Datastructure = Datastructure
(** {3 Events } *)
@@ -246,12 +204,115 @@ module Datastructure = Datastructure
The modification of the Egraph (events) can be monitored through daemons.
*)
-module Daemon = Demon.Simple
+module Daemon : sig
+ (** Attach a callback executed when different modifications of the Egraph happens *)
+
+ (** The callback are not interrupted by other callbacks. They are scheduled to
+ run as soon as possible during the propagation phase *)
+
+ val attach_dom :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a DomKind.t ->
+ (Egraph.t -> Node.t -> unit) ->
+ unit
+ (** [attach_dom d ?direct n dom callback] The callback is scheduled when the
+ domain [dom] of the equivalence class of [n] is modified. If direct is true
+ (default) the callback is scheduled immediately if the domain is already
+ set. *)
+
+ val attach_any_dom :
+ Egraph.t -> 'a DomKind.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Nodes.ValueKind.t ->
+ (Egraph.t -> Node.t -> 'b -> unit) ->
+ unit
+
+ val attach_any_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.t -> Node.t -> Value.t -> unit) ->
+ unit
+
+ val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_node :
+ Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_sem :
+ Egraph.t -> ('a, 'b) Nodes.ThTermKind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_reg_value :
+ Egraph.t -> ('a, 'b) Nodes.ValueKind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+end =
+ Demon.Simple
+
+module DaemonFixingModel : sig
+ (** Attach a callback executed when different modifications of the Egraph happens *)
+
+ (** Same as {!Daemon} but they are scheduled to run as soon as possible during
+ the FixingModel phase *)
+
+ val attach_dom :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a DomKind.t ->
+ (Egraph.t -> Node.t -> unit) ->
+ unit
+ (** [attach_dom d ?direct n dom callback] The callback is *)
+
+ val attach_any_dom :
+ Egraph.t -> 'a DomKind.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Nodes.ValueKind.t ->
+ (Egraph.t -> Node.t -> 'b -> unit) ->
+ unit
+
+ val attach_any_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.t -> Node.t -> Value.t -> unit) ->
+ unit
+
+ val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_node :
+ Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_sem :
+ Egraph.t -> ('a, 'b) Nodes.ThTermKind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_reg_value :
+ Egraph.t -> ('a, 'b) Nodes.ValueKind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+end =
+ Demon.Simple.FixingModel
+
module DaemonWithFilter = Demon.WithFilter
module DaemonWithKey = Demon.Key
module Monad = Demon.Monad
module Events = struct
+ include Egraph
(** Low level API *)
(** {3 Create daemons } *)
@@ -277,84 +338,14 @@ module Events = struct
type daemon_key = Events.Wait.daemon_key =
| DaemonKey : 'runable Dem.t * 'runable -> daemon_key
+ module type T = Egraph.Wait.Dem
(** 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
+ let register (s : (module T)) =
+ let module S = (val s) in
+ Egraph.Wait.register_dem (module S)
- (** {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 ->
- ?direct:bool ->
- 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 ->
- ?direct:bool ->
- 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
+ let new_pending_daemon = Egraph.new_pending_daemon
end
(** {3 Helpers } *)
@@ -371,11 +362,6 @@ module Debug = struct
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 *)
-
(** {3 For schedulers} *)
(** The following functions are necessary only to the scheduler *)
@@ -384,6 +370,24 @@ module ForSchedulers = struct
module Backtrackable = Egraph.Backtrackable
let default_theories = Egraph.default_theories
+
+ let ground_init = Ground.init
+
+ let interp_init = Interp.init
+
+ module Fix_model = Interp.Fix_model
+
+ let get_event_priority = Events.Wait.get_priority
+
+ let flush_internal = Egraph.flush_internal
end
-module Demon = Demon
+module Choice = struct
+ type choice_state = Egraph.choice_state =
+ | DecNo
+ | DecTodo of (Egraph.t -> unit) list
+
+ and t = Egraph.choice = { choice : Egraph.t -> choice_state; prio : int }
+
+ let register = Egraph.register_decision
+end
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
new file mode 100644
index 000000000..2b00d22c4
--- /dev/null
+++ b/src_colibri2/core/colibri2_core.mli
@@ -0,0 +1,1615 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+(** 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
+ - execute callbacks when some events happens
+
+ The Egraph is piloted by a scheduler which distinguished four different phases:
+ + Propagation phase
+ + Decision phase
+ + LastEffort phase
+ + FixingModel phase
+
+ Each phase starts when there is nothing more to do in the previous phase,
+ but a later phase can add work to a previous phase. A decision adds new
+ possible propagations
+
+*)
+
+module rec Egraph : sig
+ module Ro : sig
+ type t
+
+ val is_equal : t -> Node.t -> Node.t -> bool
+
+ val find_def : t -> Node.t -> Node.t
+
+ val get_dom : t -> 'a Dom.Kind.t -> Node.t -> 'a option
+ (** dom of the class *)
+
+ val get_value : t -> Node.t -> Value.t option
+ (** one of the value of the class *)
+
+ (** {4 The classes must have been registered} *)
+
+ val find : t -> Node.t -> Node.t
+
+ val is_repr : t -> Node.t -> bool
+
+ val is_registered : t -> Node.t -> bool
+
+ val get_env : t -> 'a Env.Saved.t -> 'a
+ (** Can raise UninitializedEnv *)
+
+ val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+
+ val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
+
+ val context : t -> Context.creator
+
+ val register : t -> Node.t -> unit
+ (** Add a new node to register *)
+ end
+
+ type t = private Ro.t
+
+ val is_equal : t -> Node.t -> Node.t -> bool
+
+ val find_def : t -> Node.t -> Node.t
+
+ val get_dom : t -> 'a Dom.Kind.t -> Node.t -> 'a option
+ (** dom of the class *)
+
+ val get_value : t -> Node.t -> Value.t option
+ (** one of the value of the class *)
+
+ (** {4 The classes must have been registered} *)
+
+ val find : t -> Node.t -> Node.t
+
+ val is_repr : t -> Node.t -> bool
+
+ val is_registered : t -> Node.t -> bool
+
+ val get_env : t -> 'a Env.Saved.t -> 'a
+ (** Can raise UninitializedEnv *)
+
+ val set_env : t -> 'a Env.Saved.t -> 'a -> unit
+
+ val get_unsaved_env : t -> 'a Env.Unsaved.t -> 'a
+
+ val context : t -> Context.creator
+
+ val contradiction : t -> 'a
+
+ val register : t -> Node.t -> unit
+ (** Add a new node to register *)
+
+ (** {3 Immediate modifications} *)
+ val set_dom : t -> 'a Dom.Kind.t -> Node.t -> 'a -> unit
+ (** change the dom of the equivalence class *)
+
+ val unset_dom : t -> 'a Dom.Kind.t -> Node.t -> unit
+ (** remove the dom of the equivalence class *)
+
+ (** {3 Delayed modifications} *)
+ val set_thterm : t -> Node.t -> ThTerm.t -> unit
+ (** attach a theory term to an equivalence class *)
+
+ val set_value : t -> Node.t -> Value.t -> unit
+ (** attach value to an equivalence class *)
+
+ val merge : t -> Node.t -> Node.t -> unit
+
+ exception Contradiction
+end
+
+(** {3 Ground terms} *)
+(** The main representations of 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.
+
+*)
+
+and Ground : sig
+ module rec Subst : sig
+ type ty = Ty.t Expr.Ty.Var.M.t [@@deriving show, hash, ord, eq]
+
+ type t = { term : Node.t Expr.Term.Var.M.t; ty : ty }
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+ val empty : t
+
+ val distinct_union : t -> t -> t
+ end
+
+ and Ty : sig
+ type t = { app : Expr.Ty.Const.t; args : t list }
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+ val convert : Subst.ty -> Expr.Ty.t -> t
+
+ val prop : t
+ (** The type of propositions *)
+
+ val bool : t
+ (** Alias for {!prop}. *)
+
+ val unit : t
+ (** The unit type. *)
+
+ val base : t
+ (** An arbitrary type. *)
+
+ val int : t
+ (** The type of integers *)
+
+ val rat : t
+ (** The type of rationals *)
+
+ val real : t
+ (** The type of reals. *)
+
+ val string : t
+ (** The type of strings *)
+
+ val string_reg_lang : t
+ (** The type of regular language over strings. *)
+
+ val definition : Expr.Ty.Const.t -> Expr.Ty.def
+ end
+
+ type s = {
+ app : Expr.Term.Const.t;
+ tyargs : Ty.t list;
+ args : Node.t Colibri2_popop_lib.IArray.t;
+ ty : Ty.t;
+ }
+
+ module Term : Colibri2_popop_lib.Popop_stdlib.Datatype with type t = s
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+
+ val node : t -> Node.t
+ (** Return a class from a thterm *)
+
+ val sem : t -> s
+ (** Return the sem from a thterm *)
+
+ val index : s -> t
+ (** Return a theory term from the user type *)
+
+ 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
+ (** Return the user type. Raise if the ThTerm does not belong to this
+ module *)
+
+ val convert : ?subst:Subst.t -> Expr.Term.t -> Node.t
+
+ val apply :
+ Expr.Term.Const.t -> Ty.t list -> Node.t Colibri2_popop_lib.IArray.t -> s
+
+ val init : Egraph.t -> unit
+
+ val register_converter : Egraph.t -> (Egraph.t -> t -> unit) -> unit
+ (** register callback called for each new ground term registered *)
+
+ val tys : Egraph.t -> Node.t -> Ty.S.t
+
+ module Defs : sig
+ val add :
+ Egraph.t ->
+ Dolmen_std.Expr.term_cst ->
+ Dolmen_std.Expr.ty_var list ->
+ Dolmen_std.Expr.term_var list ->
+ Expr.term ->
+ unit
+ end
+
+ module ClosedQuantifier : sig
+ type binder = Forall | Exists
+
+ type s = {
+ binder : binder;
+ subst : Subst.t;
+ ty_vars : Expr.Ty.Var.t list;
+ term_vars : Expr.Term.Var.t list;
+ body : Expr.Term.t;
+ }
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+
+ val key : (s, t) ThTerm.Kind.t
+
+ val node : t -> Node.t
+ (** Return a class from a thterm *)
+
+ val sem : t -> s
+ (** Return the sem from a thterm *)
+
+ 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
+ (** Return the user type. Raise if the ThTerm does not belong to this
+ module *)
+ end
+
+ module NotTotalyApplied : sig
+ type s =
+ | 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 Colibri2_popop_lib.IArray.t;
+ ty : Ty.t;
+ }
+
+ type t
+
+ val key : (s, t) ThTerm.Kind.t
+
+ val node : t -> Node.t
+ (** Return a class from a thterm *)
+
+ val sem : t -> s
+ (** Return the sem from a thterm *)
+
+ 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
+ (** Return the user type. Raise if the ThTerm does not belong to this
+ module *)
+ end
+end
+
+(** {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:
+
+ - the theory term of {!Ground.s} is {!Ground.t};
+ - for {!Ground.ClosedQuantifier.s} is {!Ground.ClosedQuantifier.t}
+ - for {!Ground.NotTotalyApplied.s} is {!Ground.NotTotalyApplied.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}
+
+ *)
+
+(** The nodes form equivalence class inside the Egraph *)
+and Node : sig
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+
+ 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, _) ThTerm.Kind.t -> 'a -> t
+ (** Return the corresponding node from a theory term *)
+
+ val index_value : ('a, _) Value.Kind.t -> 'a -> t
+ (** Return the corresponding node from a value *)
+
+ module HC : sig
+ type 'a t
+
+ type key
+
+ val create : 'a Format.printer -> string -> 'a t
+
+ val remove : 'a t -> Egraph.t -> key -> unit
+
+ val set : 'a t -> Egraph.t -> key -> 'a -> unit
+
+ val find : 'a t -> Egraph.t -> key -> 'a
+
+ val find_opt : 'a t -> Egraph.t -> key -> 'a option
+
+ val mem : 'a t -> Egraph.t -> key -> bool
+
+ val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
+
+ module Ro : sig
+ val find : 'a t -> Egraph.Ro.t -> key -> 'a
+
+ val find_opt : 'a t -> Egraph.Ro.t -> key -> 'a option
+
+ val mem : 'a t -> Egraph.Ro.t -> key -> bool
+ end
+ end
+ with type key := t
+end
+
+(** ThTerm allows to associates an OCaml type to a uniq {!Node.t} using an
+ indexing table *)
+and ThTerm : sig
+ module Kind : Keys.Key2
+ (** Unique keys associated to each kind of ThTerm *)
+
+ module type S = sig
+ type s
+ (** the user given type *)
+
+ module SD : Colibri2_popop_lib.Popop_stdlib.NamedDatatype with type t = s
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+ (** thterm *)
+
+ val key : (s, t) Kind.t
+
+ val index : s -> t
+ (** Return a theory term from the user type *)
+
+ val node : t -> Node.t
+ (** Return a class from a thterm *)
+
+ val sem : t -> s
+ (** Return the sem from a thterm *)
+
+ 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
+ (** Return the user type. Raise if the ThTerm does not belong to this
+ module *)
+ end
+
+ module Register (T : Colibri2_popop_lib.Popop_stdlib.NamedDatatype) :
+ S with type s = T.t
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+ (** {3 Generic value which units all the theory terms } *)
+
+ val index : ('a, _) Kind.t -> 'a -> t
+ (** Return the corresponding node from a theory term *)
+
+ val node : t -> Node.t
+ (** Returns the node associated to this theory term *)
+end
+
+(** 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}. *)
+
+(** One {!Value.t} can be associated to an equivalence class and a {!Value.t}
+ is associated to an uniq {!Node.t} *)
+and Value : sig
+ module Kind : Keys.Key2
+
+ (** {3 Generic value which unit all the values } *)
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+
+ val index : ('a, _) Value.Kind.t -> 'a -> t
+ (** Return the corresponding node from a value *)
+
+ val node : t -> Node.t
+
+ val value : ('a, _) Kind.t -> t -> 'a option
+
+ type kind = Value : (_, 'b) Kind.t * 'b -> kind
+
+ val kind : t -> kind
+ (** unpack a value *)
+
+ module type S = sig
+ type s
+
+ module SD : Colibri2_popop_lib.Popop_stdlib.NamedDatatype with type t = s
+
+ include Colibri2_popop_lib.Popop_stdlib.Datatype
+ (** nodevalue *)
+
+ val key : (s, t) Kind.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
+ (** Return a class from a nodevalue *)
+
+ val value : t -> s
+ (** Return the value from a nodevalue *)
+
+ val nodevalue : t -> Value.t
+
+ val of_nodevalue : Value.t -> t option
+
+ val coerce_nodevalue : Value.t -> t
+ end
+
+ module Register (T : Colibri2_popop_lib.Popop_stdlib.NamedDatatype) :
+ S with type s = T.t
+end
+
+(** Domains are additional informations associated to each equivalence class
+ inside the {!Egraph.t}. They can be registered using {!Dom.register} or
+ when the domain is simple by {!Dom.Lattice} *)
+
+and Dom : sig
+ module Kind : Keys.Key
+
+ module type S = sig
+ type t
+
+ 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 *)
+
+ 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
+
+ val register : (module S) -> unit
+
+ module type Lattice = sig
+ type t
+
+ val equal : t -> t -> bool
+
+ val pp : Format.formatter -> t -> unit
+
+ val key : t Kind.t
+
+ val inter : Egraph.t -> t -> t -> t option
+ (** [inter d d1 d2] compute the intersection of [d1] and [d2] return [None]
+ if it is empty. In this last case a contradiction is reported *)
+
+ val is_singleton : Egraph.t -> t -> Value.t option
+ (** [is_singleton _ d] if [d] is
+ restricted to a singleton return the corresponding value *)
+ end
+
+ (** [Lattice(L)] register a domain as a lattice. It returns useful function
+ for setting and updating the domain *)
+ module Lattice (L : Lattice) : sig
+ val set_dom : Egraph.t -> Node.t -> L.t -> unit
+ (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
+
+ val upd_dom : Egraph.t -> Node.t -> L.t -> unit
+ (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
+ [l] with the current value of the domain. *)
+ end
+end
+
+module Expr = Expr
+(** The module {!Expr} corresponds to the typed expression
+ parsed and typed by Dolmen. It is generally not useful. *)
+
+module Builtin = Dolmen_std.Builtin
+
+(** {3 Fix the models} *)
+
+(** The module {!Interp} handles:
+
+ - Checking the model before answering SAT, the interpretation of the
+ application are provided using {!Interp.Register.check}
+ - Enumerating the possible values for each node {!Interp.Register.node}
+ - Otherwise enumerating the possible values of each type
+ {!Interp.Register.ty}
+
+*)
+
+module Interp : sig
+ module SeqLim : sig
+ type 'a t
+ (** Sequence, finite during module fixing *)
+
+ val of_seq : Egraph.t -> 'a Base.Sequence.t -> 'a t
+ (** Limit the sequence to the given bound of the iterative deepening.
+ Sequence used for enumerating the values should be limited for ensuring
+ fairness. If the sequence contained more elements than limited the top
+ decision will restart with a bigger limit
+ *)
+
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+ val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
+ (** cartesian product {!Base.Sequence.cartesian_product} *)
+
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+ val map : 'a t -> f:('a -> 'b) -> 'b t
+
+ val unfold_with :
+ 'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Base.Sequence.Step.t) -> 'c t
+ end
+
+ module Register : sig
+ val check : Egraph.t -> (Egraph.t -> Ground.t -> bool option) -> unit
+ (** Check the value of the arguments corresponds to the the one of the of the term *)
+
+ val node :
+ Egraph.t ->
+ ((Egraph.t -> Node.t -> Value.t SeqLim.t) ->
+ Egraph.t ->
+ Node.t ->
+ Value.t SeqLim.t option) ->
+ unit
+ (** Register the computation of possible values for a node using the
+ information on the domains. It could ask the computation of other nodes *)
+
+ val ty :
+ Egraph.t -> (Egraph.t -> Ground.Ty.t -> Value.t SeqLim.t option) -> unit
+ (** Register iterators on all the possible value of some types, all the values
+ must be reached eventually *)
+ end
+
+ val ty : Egraph.t -> Ground.Ty.t -> Value.t SeqLim.t
+ (** Iterate on all the possible value of the given type, usually all the values
+ will be reached eventually *)
+
+ module WatchArgs : sig
+ val create : Egraph.t -> (Egraph.t -> Ground.t -> unit) -> Ground.t -> unit
+ (** call the given function when all the arguments of the ground term have a value *)
+ end
+end
+
+(** {3 Custom Environment and data-structures } *)
+
+module Env : sig
+ (** Theory specific environment *)
+
+ module Saved : sig
+ (** Environment should currently be persistent data-structure in order
+ to be backtracked correctly *)
+
+ include Keys.Key
+
+ val register : 'a Format.printer -> 'a t -> unit
+ (** Only a pretty printer is needed for registration *)
+
+ val print : 'a t -> 'a Format.printer
+ (** Get a pretty printer for a particular environment *)
+
+ val check_is_registered : 'a t -> unit
+ (** Check if all the keys created have been registered *)
+ end
+
+ module Unsaved : sig
+ (** These environment are not saved automatically *)
+
+ include Keys.Key
+
+ val register :
+ init:(Context.creator -> 'a) -> pp:'a Format.printer -> 'a t -> unit
+ (** Only a pretty printer and an initialization function is needed for registration *)
+
+ val print : 'a t -> 'a Format.printer
+ (** Get a pretty printer for a particular environment *)
+
+ val check_is_registered : 'a t -> unit
+ (** Check if all the keys created have been registered *)
+
+ val init : Context.creator -> 'a t -> 'a
+ (** Create the initial value *)
+ end
+end
+
+module Datastructure : sig
+ (** {2 An hashtable context aware } *)
+
+ module type Sig = sig
+ type 'a t
+
+ type key
+
+ val create : 'a Format.printer -> string -> 'a t
+
+ val remove : 'a t -> Egraph.t -> key -> unit
+
+ val set : 'a t -> Egraph.t -> key -> 'a -> unit
+
+ val find : 'a t -> Egraph.t -> key -> 'a
+
+ val find_opt : 'a t -> Egraph.t -> key -> 'a option
+
+ val mem : 'a t -> Egraph.t -> key -> bool
+
+ val change : ('a option -> 'a option) -> 'a t -> Egraph.t -> key -> unit
+
+ module Ro : sig
+ val find : 'a t -> Egraph.Ro.t -> key -> 'a
+
+ val find_opt : 'a t -> Egraph.Ro.t -> key -> 'a option
+
+ val mem : 'a t -> Egraph.Ro.t -> key -> bool
+ end
+ end
+
+ module Hashtbl (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
+ Sig with type key := S.t
+
+ (** {2 An hashtable context aware, where data are automatically initialized } *)
+
+ module type Sig2 = sig
+ type 'a t
+
+ type key
+
+ val create : 'a Format.printer -> string -> (Context.creator -> 'a) -> 'a t
+
+ val set : 'a t -> Egraph.t -> key -> 'a -> unit
+
+ val find : 'a t -> Egraph.t -> key -> 'a
+
+ val change : ('a -> 'a) -> 'a t -> Egraph.t -> key -> unit
+
+ module Ro : sig
+ val set : 'a t -> Egraph.Ro.t -> key -> 'a -> unit
+
+ val find : 'a t -> Egraph.Ro.t -> key -> 'a
+
+ val change : ('a -> 'a) -> 'a t -> Egraph.Ro.t -> key -> unit
+ end
+ end
+
+ module Hashtbl2 (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
+ Sig2 with type key := S.t
+
+ (** {2 A table where data are initialized on the fly, and can't be modified. It
+ is used with other context aware mutable data-structure as data } *)
+
+ module type Memo = sig
+ type 'a t
+
+ type key
+
+ val create :
+ 'a Format.printer -> string -> (Context.creator -> key -> 'a) -> 'a t
+
+ val find : 'a t -> Egraph.t -> key -> 'a
+
+ val iter : (key -> 'a -> unit) -> 'a t -> Egraph.t -> unit
+
+ val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> Egraph.t -> 'acc -> 'acc
+ end
+
+ module Memo (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
+ Memo with type key := S.t
+
+ module Push : sig
+ type 'a t
+
+ val create : 'a Format.printer -> string -> 'a t
+
+ val push : 'a t -> Egraph.t -> 'a -> unit
+
+ val iter : f:('a -> unit) -> 'a t -> Egraph.t -> unit
+
+ val fold : f:('acc -> 'a -> 'acc) -> init:'acc -> 'a t -> Egraph.t -> 'acc
+
+ val length : 'a t -> Egraph.t -> int
+
+ val get : 'a t -> Egraph.t -> int -> 'a
+ end
+
+ module Ref : sig
+ type 'a t
+
+ val create : 'a Fmt.t -> string -> 'a -> 'a t
+
+ val get : 'a t -> Egraph.t -> 'a
+
+ val set : 'a t -> Egraph.t -> 'a -> unit
+
+ module Ro : sig
+ val get : 'a t -> Egraph.Ro.t -> 'a
+
+ val set : 'a t -> Egraph.Ro.t -> 'a -> unit
+ end
+ end
+end
+
+(** {3 Events } *)
+
+(**
+ The modification of the Egraph (events) can be monitored through daemons.
+ *)
+
+module Daemon : sig
+ (** Attach a callback executed when different modifications of the Egraph happens *)
+
+ (** The callback are not interrupted by other callbacks. They are scheduled to
+ run as soon as possible during the propagation phase *)
+
+ val attach_dom :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a Dom.Kind.t ->
+ (Egraph.t -> Node.t -> unit) ->
+ unit
+ (** [attach_dom d ?direct n dom callback] The callback is scheduled when the
+ domain [dom] of the equivalence class of [n] is modified. If direct is true
+ (default) the callback is scheduled immediately if the domain is already
+ set. *)
+
+ val attach_any_dom :
+ Egraph.t -> 'a Dom.Kind.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.t -> Node.t -> 'b -> unit) ->
+ unit
+
+ val attach_any_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.t -> Node.t -> Value.t -> unit) ->
+ unit
+
+ val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_node :
+ Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_sem :
+ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_reg_value :
+ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+end
+
+module DaemonFixingModel : sig
+ (** Attach a callback executed when different modifications of the Egraph happens *)
+
+ (** Same as {!Daemon} but they are scheduled to run as soon as possible during
+ the FixingModel phase *)
+
+ val attach_dom :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a Dom.Kind.t ->
+ (Egraph.t -> Node.t -> unit) ->
+ unit
+ (** [attach_dom d ?direct n dom callback] The callback is *)
+
+ val attach_any_dom :
+ Egraph.t -> 'a Dom.Kind.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.t -> Node.t -> 'b -> unit) ->
+ unit
+
+ val attach_any_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.t -> Node.t -> Value.t -> unit) ->
+ unit
+
+ val attach_reg_any : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_node :
+ Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_reg_sem :
+ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_reg_value :
+ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.t -> 'b -> unit) -> unit
+
+ val attach_repr : Egraph.t -> Node.t -> (Egraph.t -> Node.t -> unit) -> unit
+
+ val attach_any_repr : Egraph.t -> (Egraph.t -> Node.t -> unit) -> unit
+end
+
+module DaemonWithFilter : sig
+ (** Attach a callback executed when different modifications of the Egraph happens *)
+
+ (** Same as {!Daemon} but they are scheduled to run as soon as possible during
+ the FixingModel phase *)
+
+ val attach_dom :
+ Egraph.Ro.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a Dom.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ unit
+ (** [attach_dom d ?direct n dom callback] The callback is *)
+
+ val attach_any_dom :
+ Egraph.Ro.t ->
+ 'a Dom.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_value :
+ Egraph.Ro.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> 'b -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_any_value :
+ Egraph.Ro.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.Ro.t -> Node.t -> Value.t -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_reg_any :
+ Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) -> unit
+
+ val attach_reg_node :
+ Egraph.Ro.t ->
+ Node.t ->
+ (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_reg_sem :
+ Egraph.Ro.t ->
+ ('a, 'b) ThTerm.Kind.t ->
+ (Egraph.Ro.t -> 'b -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_reg_value :
+ Egraph.Ro.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.Ro.t -> 'b -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_repr :
+ Egraph.Ro.t ->
+ Node.t ->
+ (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) ->
+ unit
+
+ val attach_any_repr :
+ Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> (Egraph.t -> unit) option) -> unit
+end
+
+module Monad : sig
+ type 'a monad
+
+ type sequence
+
+ val getd : 'a Dom.Kind.t -> Node.t -> 'a option monad
+
+ val setd : 'a Dom.Kind.t -> Node.t -> 'a option monad -> sequence
+
+ val updd :
+ (Egraph.t -> Node.t -> 'a -> unit) -> Node.t -> 'a option monad -> sequence
+
+ val getv : ('a, _) Value.Kind.t -> Node.t -> 'a option monad
+
+ val setv : ('a, _) Value.Kind.t -> Node.t -> 'a option monad -> sequence
+
+ val ( let+ ) : 'a option monad -> ('a -> 'c) -> 'c option monad
+
+ val ( let* ) : 'a option monad -> ('a -> 'c option) -> 'c option monad
+
+ val ( and+ ) : 'a option monad -> 'b option monad -> ('a * 'b) option monad
+
+ val ( && ) : sequence -> sequence -> sequence
+
+ val attach : Egraph.t -> sequence -> unit
+end
+
+module rec DaemonWithKey : sig
+ type state = Wait | Stop
+
+ module type S = sig
+ module Key : Colibri2_popop_lib.Popop_stdlib.Datatype
+
+ val delay : Events.delay
+
+ val run : Egraph.t -> Key.t -> state
+
+ val name : string
+ end
+
+ module Register (S : S) : sig
+ val attach_dom :
+ Egraph.t -> ?direct:bool -> Node.t -> 'a Dom.Kind.t -> S.Key.t -> unit
+
+ val attach_any_dom : Egraph.t -> 'a Dom.Kind.t -> S.Key.t -> unit
+
+ val attach_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Value.Kind.t ->
+ S.Key.t ->
+ unit
+
+ val attach_any_value : Egraph.t -> ?direct:bool -> Node.t -> S.Key.t -> unit
+
+ val attach_reg_any : Egraph.t -> S.Key.t -> unit
+
+ val attach_reg_node : Egraph.t -> Node.t -> S.Key.t -> unit
+
+ val attach_reg_sem : Egraph.t -> ('a, 'b) ThTerm.Kind.t -> S.Key.t -> unit
+
+ val attach_reg_value : Egraph.t -> ('a, 'b) Value.Kind.t -> S.Key.t -> unit
+
+ val attach_repr : Egraph.t -> Node.t -> S.Key.t -> unit
+
+ val attach_any_repr : Egraph.t -> S.Key.t -> unit
+ end
+end
+
+and Events : sig
+ (** Low level API *)
+
+ (** {3 Create daemons } *)
+
+ module Dem : Keys.Key
+
+ (** {3 Register daemons } *)
+
+ type 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 =
+ | 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 : 'runable Dem.t * 'runable -> daemon_key
+
+ (** {3 Basic daemons} *)
+ module type T = sig
+ type runable
+
+ val print_runable : runable Format.printer
+
+ val run : Egraph.t -> runable -> unit
+ (** The function run after the delay *)
+
+ val key : runable Dem.t
+
+ val delay : delay
+ end
+
+ val register : (module T) -> unit
+
+ (** {3 Attach daemons } *)
+
+ val attach_dom :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a Dom.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> enqueue) ->
+ unit
+ (** wakeup when the dom of the node change *)
+
+ val attach_any_dom :
+ Egraph.t -> 'a Dom.Kind.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when the dom of any node change *)
+
+ val attach_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> 'b -> enqueue) ->
+ unit
+ (** wakeup when a value is attached to this equivalence class *)
+
+ val attach_any_value :
+ Egraph.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.Ro.t -> Node.t -> Value.t -> enqueue) ->
+ unit
+ (** wakeup when any kind of value is attached to this equivalence class *)
+
+ val attach_reg_any : Egraph.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when any node is registered *)
+
+ val attach_reg_node :
+ Egraph.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when this node is registered *)
+
+ val attach_reg_sem :
+ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.Ro.t -> 'b -> enqueue) -> unit
+ (** wakeup when a new semantical class is registered *)
+
+ val attach_reg_value :
+ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.Ro.t -> 'b -> enqueue) -> unit
+ (** wakeup when a new value is registered *)
+
+ val attach_repr :
+ Egraph.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when it is not anymore the representative class *)
+
+ val attach_any_repr : Egraph.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when a node is not its representative class anymore *)
+
+ module Ro : sig
+ val attach_dom :
+ Egraph.Ro.t ->
+ ?direct:bool ->
+ Node.t ->
+ 'a Dom.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> enqueue) ->
+ unit
+ (** wakeup when the dom of the node change *)
+
+ val attach_any_dom :
+ Egraph.Ro.t -> 'a Dom.Kind.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when the dom of any node change *)
+
+ val attach_value :
+ Egraph.Ro.t ->
+ ?direct:bool ->
+ Node.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.Ro.t -> Node.t -> 'b -> enqueue) ->
+ unit
+ (** wakeup when a value is attached to this equivalence class *)
+
+ val attach_any_value :
+ Egraph.Ro.t ->
+ ?direct:bool ->
+ Node.t ->
+ (Egraph.Ro.t -> Node.t -> Value.t -> enqueue) ->
+ unit
+ (** wakeup when any kind of value is attached to this equivalence class *)
+
+ val attach_reg_any :
+ Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when any node is registered *)
+
+ val attach_reg_node :
+ Egraph.Ro.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when this node is registered *)
+
+ val attach_reg_sem :
+ Egraph.Ro.t ->
+ ('a, 'b) ThTerm.Kind.t ->
+ (Egraph.Ro.t -> 'b -> enqueue) ->
+ unit
+ (** wakeup when a new semantical class is registered *)
+
+ val attach_reg_value :
+ Egraph.Ro.t ->
+ ('a, 'b) Value.Kind.t ->
+ (Egraph.Ro.t -> 'b -> enqueue) ->
+ unit
+ (** wakeup when a new value is registered *)
+
+ val attach_repr :
+ Egraph.Ro.t -> Node.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when it is not anymore the representative class *)
+
+ val attach_any_repr :
+ Egraph.Ro.t -> (Egraph.Ro.t -> Node.t -> enqueue) -> unit
+ (** wakeup when a node is not its representative class anymore *)
+ end
+
+ val new_pending_daemon : Egraph.t -> 'a Dem.t -> 'a -> unit
+ (** register an event for later (immediate or not). *)
+end
+
+(** {3 Choices } *)
+
+module Choice : sig
+ type choice_state = DecNo | DecTodo of (Egraph.t -> unit) list
+
+ and t = { choice : Egraph.t -> choice_state; prio : int }
+
+ val register : Egraph.t -> t -> unit
+ (** register a decision that would be scheduled later. The
+ [choose_decision] of the [Cho] will be called at that time to know
+ if the decision is still needed. *)
+end
+
+(** {3 Helpers } *)
+
+module Init : sig
+ val add_default_theory : (Egraph.t -> unit) -> unit
+end
+
+module Debug : sig
+ type flag = Colibri2_popop_lib.Debug.flag
+
+ val register_flag : desc:Colibri2_popop_lib.Pp.formatted -> string -> flag
+ (** Register a new flag. It is allowed to register twice the same flag *)
+
+ val register_info_flag :
+ desc:Colibri2_popop_lib.Pp.formatted -> string -> flag
+ (** Register a new info flag. It is allowed to register twice the same flag.
+ Info flags are set by --debug-all and must not change the behaviour. *)
+
+ val dprintf0 :
+ ?nobox:unit -> flag -> (unit, Format.formatter, unit) format -> unit
+ (** Print only if the flag is set *)
+
+ val dprintf1 :
+ ?nobox:unit ->
+ flag ->
+ ('a -> unit, Format.formatter, unit) format ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf2 :
+ ?nobox:unit ->
+ flag ->
+ ('b -> 'a -> unit, Format.formatter, unit) format ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf3 :
+ ?nobox:unit ->
+ flag ->
+ ('c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf4 :
+ ?nobox:unit ->
+ flag ->
+ ('d -> 'c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf5 :
+ ?nobox:unit ->
+ flag ->
+ ('e -> 'd -> 'c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf6 :
+ ?nobox:unit ->
+ flag ->
+ ('f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit, Format.formatter, unit) format ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf7 :
+ ?nobox:unit ->
+ flag ->
+ ( 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf8 :
+ ?nobox:unit ->
+ flag ->
+ ( 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf9 :
+ ?nobox:unit ->
+ flag ->
+ ( 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf10 :
+ ?nobox:unit ->
+ flag ->
+ ( 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf11 :
+ ?nobox:unit ->
+ flag ->
+ ( 'k -> 'j -> 'i -> 'h -> 'g -> 'f -> 'e -> 'd -> 'c -> 'b -> 'a -> unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf12 :
+ ?nobox:unit ->
+ flag ->
+ ( 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf13 :
+ ?nobox:unit ->
+ flag ->
+ ( 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf14 :
+ ?nobox:unit ->
+ flag ->
+ ( 'n ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'n ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintf15 :
+ ?nobox:unit ->
+ flag ->
+ ( 'o ->
+ 'n ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit,
+ Format.formatter,
+ unit )
+ format ->
+ 'o ->
+ 'n ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ unit
+ (** Print only if the flag is set *)
+
+ val dprintfn :
+ ?nobox:unit ->
+ flag ->
+ ( 'o ->
+ 'n ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ 'z,
+ Format.formatter,
+ unit )
+ format ->
+ 'o ->
+ 'n ->
+ 'm ->
+ 'l ->
+ 'k ->
+ 'j ->
+ 'i ->
+ 'h ->
+ 'g ->
+ 'f ->
+ 'e ->
+ 'd ->
+ 'c ->
+ 'b ->
+ 'a ->
+ 'z
+ (** Print only if the flag is set *)
+
+ val decision : flag
+
+ val contradiction : flag
+
+ type 'a stat
+
+ val register_stats_int : name:string -> init:int -> int stat
+
+ val incr : int stat -> unit
+
+ val decr : int stat -> unit
+end
+
+(** {3 For schedulers} *)
+
+(** The following functions are necessary only to the scheduler *)
+
+module ForSchedulers : sig
+ module Backtrackable : sig
+ type t
+
+ val new_t : Context.creator -> t
+
+ val set_sched :
+ sched_daemon:(Events.daemon_key -> unit) ->
+ sched_decision:(Choice.t -> unit) ->
+ t ->
+ unit
+
+ val get_delayed : t -> Egraph.t
+
+ val run_daemon : Egraph.t -> Events.daemon_key -> unit
+ (** schedule the run of a deamon *)
+
+ val delayed_stop : t -> unit
+ (** Check that not work need to be done. *)
+
+ val flush : t -> unit
+ (** Apply all the modifications and direct consequences. *)
+
+ val draw_graph : ?force:bool -> t -> unit
+ (** Debug *)
+
+ val output_graph : string -> t -> unit
+ end
+
+ val default_theories : unit -> (Egraph.t -> unit) list
+
+ val ground_init : Egraph.t -> unit
+ (** Initialize the module ground for later use *)
+
+ val interp_init : Egraph.t -> unit
+ (** Initialize the module interp for later use *)
+
+ val get_event_priority : Events.daemon_key -> Events.delay
+
+ val flush_internal : Egraph.t -> unit
+
+ module Fix_model : sig
+ (** The model is search using iterative deepening depth-first search for
+ ensuring optimality even in presence of infinite choice *)
+
+ val next_dec : Egraph.t -> (Egraph.t -> unit) Base.Sequence.t
+ (** Add a level of decision for fixing the model, another level could be
+ needed. Could raise unsatisfiable if all the model have been tried *)
+ end
+end
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index 685c97647..7eac0a818 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -247,7 +247,6 @@ end
module HNode = Hashtbl(Nodes.Node)
-module HTermConst = Hashtbl(Expr.Term.Const)
module Push = struct
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index d64124ca0..c5101b8b1 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -79,7 +79,6 @@ module Memo (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Memo with type key :=
module HNode : Sig with type key := Nodes.Node.t
-module HTermConst : Sig with type key := Expr.Term.Const.t
module Push: sig
type 'a t
diff --git a/src_colibri2/core/dune b/src_colibri2/core/dune
index 12453f2f4..2709e1eb3 100644
--- a/src_colibri2/core/dune
+++ b/src_colibri2/core/dune
@@ -2,11 +2,14 @@
(name colibri2_core)
(public_name colibri2.core)
(synopsis "core for colibri2, e.g. trail, egraph")
- (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib
- colibri2_core_structures)
+ (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib dolmen.std)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
- Containers -open Colibri2_stdlib -open Std -open Colibri2_core_structures)
+ Containers -open Colibri2_stdlib -open Std)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
- -unbox-closures-factor 20))
+ -unbox-closures-factor 20)
+ (private_modules nodes egraph domKind demon events datastructure)
+)
+
+(copy_files structures/*.ml*)
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 28dd54fe5..63c38331d 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -214,11 +214,18 @@ module Term = struct
end
+type s = All.term = {
+ app: Expr.Term.Const.t;
+ tyargs : Ty.t list;
+ args : Node.t IArray.t;
+ ty:Ty.t
+}
+
module ThTerm = RegisterThTerm(Term)
-module ClosedQuantifier = struct
+module ClosedQuantifier0 = struct
module T = struct
open! Base
@@ -248,10 +255,19 @@ module ClosedQuantifier = struct
end
-module ThClosedQuantifier = RegisterThTerm(ClosedQuantifier)
-
+module ClosedQuantifier = struct
+ type binder = ClosedQuantifier0.binder = Forall | Exists
+ type s = ClosedQuantifier0.t = {
+ binder: binder;
+ subst: Subst.t;
+ ty_vars: Expr.Ty.Var.t list;
+ term_vars: Expr.Term.Var.t list;
+ body: Expr.Term.t;
+ }
+ include (RegisterThTerm(ClosedQuantifier0): RegisteredThTerm with type s := s)
+end
-module NotTotalyApplied = struct
+module NotTotalyApplied0 = struct
module T = struct
open! Base
@@ -293,8 +309,24 @@ module NotTotalyApplied = struct
end
-module ThNotTotalyApplied = RegisterThTerm(NotTotalyApplied)
-
+module NotTotalyApplied = struct
+ type s = NotTotalyApplied0.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;
+ }
+ include (RegisterThTerm(NotTotalyApplied0):RegisteredThTerm with type s := s)
+end
let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
match t.term_descr with
@@ -308,7 +340,7 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
begin match ty.app.builtin, f.term_descr with
| (Ty.Arrow, _) | (_, (Match _ | App _ | Var _ | Binder _))
->
- ThNotTotalyApplied.node @@ ThNotTotalyApplied.index @@
+ NotTotalyApplied.node @@ NotTotalyApplied.index @@
App { app = convert ~subst f;
tyargs = List.map (Ty.convert subst.ty) tyargs;
args = IArray.of_list_map ~f:(convert ~subst) args;
@@ -330,19 +362,19 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
{ Term.app = f; tyargs = []; args = IArray.empty;
ty = Ty.convert subst.ty ty }
end else
- ThNotTotalyApplied.node @@ ThNotTotalyApplied.index @@
+ NotTotalyApplied.node @@ NotTotalyApplied.index @@
Cst f
| Expr.Binder (Exists(ty_vars,term_vars) as b, body)
| Expr.Binder (Forall(ty_vars,term_vars) as b, body) ->
let binder = match b with
- | Exists _ -> ClosedQuantifier.Exists
- | Forall _ -> ClosedQuantifier.Forall
+ | Exists _ -> ClosedQuantifier0.Exists
+ | Forall _ -> ClosedQuantifier0.Forall
| Let_seq _ | Let_par _ | Lambda _ -> assert false
in
- ThClosedQuantifier.node @@ ThClosedQuantifier.index @@
+ ClosedQuantifier.node @@ ClosedQuantifier.index @@
{ binder; ty_vars; term_vars; body; subst }
| Expr.Binder (Lambda(ty_vars,term_vars), body) ->
- ThNotTotalyApplied.node @@ ThNotTotalyApplied.index @@
+ NotTotalyApplied.node @@ NotTotalyApplied.index @@
(Lambda { ty_vars; term_vars; body; subst;
ty = Ty.convert subst.ty t.term_ty; })
| Expr.Binder (Let_seq l, body) ->
@@ -395,16 +427,16 @@ module Defs = struct
let pp_fundef _ _ = ()
- let fundefs = Datastructure.HTermConst.create pp_fundef "SynTerm.fundefs"
+ let fundefs = Expr.Term.Const.HC.create pp_fundef "SynTerm.fundefs"
let add d tc tyl tvl body =
- Datastructure.HTermConst.set fundefs d tc {tyl;tvl;body}
+ Expr.Term.Const.HC.set fundefs d tc {tyl;tvl;body}
let converter d (v:ThTerm.t) =
let cl = ThTerm.node v in
match ThTerm.sem v with
| { app = tc; tyargs = tyl; args = tvl; ty = _ } ->
- begin match Datastructure.HTermConst.find fundefs d tc with
+ begin match Expr.Term.Const.HC.find fundefs d tc with
| exception Not_found -> ()
| fundef ->
let subst = {
@@ -467,10 +499,10 @@ let init d =
Defs.converter d g;
Datastructure.Push.iter registered_converter d ~f:(fun f -> f d g));
Demon.Simple.attach_reg_sem d
- ThClosedQuantifier.key
+ ClosedQuantifier.key
(fun d g ->
- let n = ThClosedQuantifier.node g in
+ let n = ClosedQuantifier.node g in
add_ty d n Ty.bool
)
-include ThTerm
+include (ThTerm : RegisteredThTerm with type s := s and type t = ThTerm.t)
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index cefc6c277..dc081f0d5 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -104,6 +104,13 @@ module Term: sig
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
end
+type s = All.term = {
+ app: Expr.Term.Const.t;
+ tyargs : Ty.t list;
+ args : Node.t IArray.t;
+ ty:Ty.t
+}
+
include RegisteredThTerm with type s := Term.t
val convert : ?subst:Subst.t -> Expr.Term.t -> Node.t
@@ -129,23 +136,20 @@ module Defs : sig
module ClosedQuantifier : sig
type binder = Forall | Exists
- [@@deriving eq, ord, hash]
- type t = {
+ type s = {
binder: binder;
subst: Subst.t;
ty_vars: Expr.Ty.Var.t list;
term_vars: Expr.Term.Var.t list;
body: Expr.Term.t;
}
- [@@deriving eq, ord, hash]
-
- end
-module ThClosedQuantifier : RegisteredThTerm with type s = ClosedQuantifier.t
+ include RegisteredThTerm with type s := s
+end
module NotTotalyApplied : sig
- type t =
+ type s =
| Lambda of {
subst: Subst.t;
ty_vars: Expr.Ty.Var.t list;
@@ -160,8 +164,7 @@ module NotTotalyApplied : sig
args : Node.t IArray.t;
ty: Ty.t;
}
- [@@deriving eq, ord, hash]
-end
+ include RegisteredThTerm with type s := s
-module ThNotTotalyApplied : RegisteredThTerm with type s = NotTotalyApplied.t
+end
diff --git a/src_colibri2/core/structures/dune b/src_colibri2/core/structures/dune
index 92ee09425..e69de29bb 100644
--- a/src_colibri2/core/structures/dune
+++ b/src_colibri2/core/structures/dune
@@ -1,13 +0,0 @@
-(library
- (name colibri2_core_structures)
- (public_name colibri2.core.structures)
- (synopsis
- "core structures for colibri2, e.g. terms, semantic terms, values, etc")
- (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib str
- dolmen.std)
- (preprocess
- (pps ppx_deriving.std))
- (flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
- Containers -open Colibri2_stdlib -open Std)
- (ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
- -unbox-closures-factor 20))
diff --git a/src_colibri2/core/structures/expr.ml b/src_colibri2/core/structures/expr.ml
index 7982d431a..b5c34015f 100644
--- a/src_colibri2/core/structures/expr.ml
+++ b/src_colibri2/core/structures/expr.ml
@@ -90,17 +90,24 @@ module Term = struct
end)
module Const = struct
+
+ module D = struct
include Dolmen_std.Expr.Term.Const
let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t
-
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
type nonrec t = t
let equal = equal
let compare = compare
let hash = hash
let pp = pp
let hash_fold_t s t = Base.Hash.fold_int s (hash t)
- end)
+ end)
+ end
+
+ include D
+
+ module HC = Datastructure.Hashtbl(D)
+
end
module Var = struct
diff --git a/src_colibri2/popop_lib/map_intf.ml b/src_colibri2/popop_lib/map_intf.ml
index fd296c728..d0d2ae68b 100644
--- a/src_colibri2/popop_lib/map_intf.ml
+++ b/src_colibri2/popop_lib/map_intf.ml
@@ -176,7 +176,7 @@ module type Map =
(** Same as {!Extmap.S.map}, but the function receives as arguments both
the key and the associated value for each binding of the map. *)
- (** @Added in Why3 *)
+ (** Added in Why3 *)
val change :
('a data option -> 'a data option) -> key -> 'a data t -> 'a data t
diff --git a/src_colibri2/solver/dune b/src_colibri2/solver/dune
index f8ee1077e..b58f23fde 100644
--- a/src_colibri2/solver/dune
+++ b/src_colibri2/solver/dune
@@ -3,7 +3,7 @@
(public_name colibri2.solver)
(synopsis "colibri2's solver")
(libraries containers zarith ocamlgraph gen dolmen spelll colibri2.stdlib
- colibri2.popop_lib str colibri2.core colibri2.core.structures dolmen_loop
+ colibri2.popop_lib str colibri2.core dolmen_loop
dolmen_type)
(preprocess
(pps ppx_deriving.std))
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index d892f816a..efd423d21 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -20,6 +20,7 @@
open Colibri2_popop_lib
open Colibri2_core
+open ForSchedulers
let debug = Debug.register_info_flag
~desc:"for the scheduler in the simple version"
@@ -47,7 +48,7 @@ exception Contradiction
module Att = struct
type t =
- | Decision of int * Egraph.choice
+ | Decision of int * Choice.t
type prio = float
type db = float Node.H.t
@@ -83,7 +84,7 @@ type 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;
+ solver_state : Backtrackable.t;
(* global *)
decprio : Att.db;
var_inc : float ref;
@@ -123,7 +124,7 @@ let new_solver () =
lasteffort = Context.TimeWheel.create (Context.creator context);
fixing_model = Context.Ref.create (Context.creator context) [];
prev_scheduler_state = None;
- solver_state = Egraph.Backtrackable.new_t (Context.creator context);
+ solver_state = Backtrackable.new_t (Context.creator context);
context;
decprio = Node.H.create 100;
var_inc = ref 1.;
@@ -135,7 +136,7 @@ let new_solver () =
let sched_daemon att =
incr daemon_count;
Debug.dprintf0 debug "[Scheduler] New waiting daemon";
- match Egraph.Wait.get_priority att with
+ match get_event_priority att with
| Immediate -> assert false (* absurd *)
| Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
| LastEffort offset ->
@@ -148,13 +149,13 @@ let new_solver () =
!dec_count;
t.choices <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
t.choices in
- Egraph.Backtrackable.set_sched ~sched_daemon ~sched_decision t.solver_state;
+ Backtrackable.set_sched ~sched_daemon ~sched_decision t.solver_state;
t
let push kind t =
- if Debug.test_flag debug_dotgui then
- Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
+ if Colibri2_popop_lib.Debug.test_flag debug_dotgui then
+ Backtrackable.draw_graph ~force:true t.solver_state;
Debug.dprintf2 debug_pushpop "[Scheduler] push from %a" print_level t;
let prev =
{ pre_choices = t.choices;
@@ -175,7 +176,7 @@ let pop_to t prev =
t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
t.level <- prev.pre_level;
Context.pop prev.pre_backtrack_point;
- Egraph.Backtrackable.draw_graph t.solver_state;
+ Backtrackable.draw_graph t.solver_state;
Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
print_level t
@@ -224,8 +225,8 @@ let pop_to t prev =
*)
let rec conflict_analysis t =
- if Debug.test_flag debug_dotgui then
- Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
+ if Colibri2_popop_lib.Debug.test_flag debug_dotgui then
+ Backtrackable.draw_graph ~force:true t.solver_state;
Debug.incr stats_con;
t.var_inc := !(t.var_inc) *. var_decay;
let rec rewind () =
@@ -248,25 +249,25 @@ let rec conflict_analysis t =
rewind ()
and try_run_dec:
- t -> Prio.t -> Egraph.choice -> unit = fun t prio choice ->
+ t -> Prio.t -> Choice.t -> unit = fun t prio choice ->
(** First we verify its the decision is at this point needed *)
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
+ let d = Backtrackable.get_delayed t.solver_state in
match choice.choice d with
- | Egraph.DecNo | Egraph.DecTodo [] ->
+ | Choice.DecNo | Choice.DecTodo [] ->
t.choices <- prio
- | Egraph.DecTodo (todo::todos) ->
+ | Choice.DecTodo (todo::todos) ->
(** We remove the decision it is replaced by the todos,
we can change the interface of choice and in that case
we want to keep the decision in the current branch *)
t.choices <- prio;
Debug.incr stats_dec;
- Egraph.Backtrackable.delayed_stop t.solver_state;
+ Backtrackable.delayed_stop t.solver_state;
make_choice t todo (Base.Sequence.of_list todos)
and make_choice t todo todos =
ignore (push (Choices todos) t);
try
- todo (Egraph.Backtrackable.get_delayed t.solver_state)
+ todo (Backtrackable.get_delayed t.solver_state)
with Egraph.Contradiction ->
conflict_analysis t
@@ -278,8 +279,8 @@ and make_choice t todo todos =
* let _, prio = Prio.extract_min t.choices in
* Debug.incr stats_propa;
* t.choices <- prio;
- * Egraph.Backtrackable.run_daemon d att;
- * Egraph.Backtrackable.flush d;
+ * Backtrackable.run_daemon d att;
+ * Backtrackable.flush d;
* run_until_dec t d
* end
* | Some (Att.Decision (_,_)) | None -> () *)
@@ -298,8 +299,8 @@ let run_one_step_propagation ~nodec t =
| Some att -> begin
Debug.incr stats_propa;
protect_against_contradiction t (fun () ->
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
- Egraph.Backtrackable.run_daemon d att
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d att
) (fun () -> true)
end
| None when nodec -> false
@@ -310,8 +311,8 @@ let run_one_step_propagation ~nodec t =
(fun fmt -> Fmt.int fmt (Context.TimeWheel.size_at_current_time t.lasteffort));
Debug.incr stats_lasteffort;
protect_against_contradiction t (fun () ->
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
- Egraph.Backtrackable.run_daemon d att
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d att
) (fun () -> true)
end
| None ->
@@ -326,8 +327,8 @@ let run_one_step_propagation ~nodec t =
| Some att -> begin
Debug.incr stats_lasteffort;
protect_against_contradiction t (fun () ->
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
- Egraph.Backtrackable.run_daemon d att
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d att
) (fun () -> true)
end
| None ->
@@ -339,19 +340,19 @@ let run_one_step_fix_model t =
| att::l -> begin
Context.Ref.set t.fixing_model l;
protect_against_contradiction t (fun () ->
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
- Egraph.Backtrackable.run_daemon d att
+ let d = Backtrackable.get_delayed t.solver_state in
+ Backtrackable.run_daemon d att
) (fun () -> true)
end
| [] ->
protect_against_contradiction t (fun () ->
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
- Interp.Fix_model.next_dec d
+ let d = Backtrackable.get_delayed t.solver_state in
+ Fix_model.next_dec d
) (fun seq ->
match Base.Sequence.next seq with
| None -> false
| Some (todo,todos) ->
- Egraph.Backtrackable.delayed_stop t.solver_state;
+ Backtrackable.delayed_stop t.solver_state;
make_choice t todo todos;
true
)
@@ -372,7 +373,7 @@ let run_one_step ~nodec t =
let rec flush t =
try
- Egraph.Backtrackable.flush t.solver_state
+ Backtrackable.flush t.solver_state
with Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
conflict_analysis t;
@@ -387,7 +388,7 @@ let rec run_inf_step ~limit ~nodec t =
| true ->
run_inf_step ~limit ~nodec t
| false ->
- Egraph.Backtrackable.delayed_stop t.solver_state
+ Backtrackable.delayed_stop t.solver_state
let run_inf_step ?(limit=(-1)) ?(nodec=false) t =
try
@@ -399,9 +400,9 @@ let run_inf_step ?(limit=(-1)) ?(nodec=false) t =
let init_theories ~theories t =
try
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
- List.iter (fun f -> f d) (Ground.init::Interp.init::theories);
- Egraph.Backtrackable.flush t.solver_state
+ let d = Backtrackable.get_delayed t.solver_state in
+ List.iter (fun f -> f d) (ground_init::interp_init::theories);
+ Backtrackable.flush t.solver_state
with Egraph.Contradiction ->
Debug.dprintf0 debug
"[Scheduler] Contradiction during theory initialization";
@@ -410,7 +411,7 @@ let init_theories ~theories t =
let add_assertion t f =
try
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
+ let d = Backtrackable.get_delayed t.solver_state in
f d;
flush t
with Egraph.Contradiction ->
@@ -422,7 +423,7 @@ let check_sat ?limit t =
try
flush t;
run_inf_step ?limit t;
- `Sat (Egraph.Backtrackable.get_delayed t.solver_state)
+ `Sat (Backtrackable.get_delayed t.solver_state)
with Contradiction ->
`Unsat
@@ -432,7 +433,7 @@ let run_exn ?nodec ?limit ~theories f =
add_assertion t f;
flush t;
run_inf_step ~nodec:(nodec=Some ()) ?limit t;
- let d = Egraph.Backtrackable.get_delayed t.solver_state in
+ let d = Backtrackable.get_delayed t.solver_state in
d
let run ?nodec ?limit ~theories f =
diff --git a/src_colibri2/tests/tests_lib.ml b/src_colibri2/tests/tests_lib.ml
index 227017ec4..965b54a53 100644
--- a/src_colibri2/tests/tests_lib.ml
+++ b/src_colibri2/tests/tests_lib.ml
@@ -31,18 +31,18 @@ let (&:) s l = s >::: (List.map (fun f -> OUnit2.test_case f) l)
let register d cl =
Egraph.register d cl;
- Egraph.flush_internal d
+ ForSchedulers.flush_internal d
let merge d cl1 cl2 =
Egraph.merge d cl1 cl2;
- Egraph.flush_internal d
+ ForSchedulers.flush_internal d
let is_equal = Egraph.is_equal
(** without decisions *)
type t =
{ wakeup_daemons : Events.daemon_key Queue.t;
- solver_state : Egraph.Backtrackable.t;
+ solver_state : ForSchedulers.Backtrackable.t;
context : Colibri2_stdlib.Context.context;
}
@@ -51,7 +51,7 @@ let new_solver () =
let context = Colibri2_stdlib.Context.create () in
{
wakeup_daemons = Queue.create ();
- solver_state = Egraph.Backtrackable.new_t (Colibri2_stdlib.Context.creator context);
+ solver_state = ForSchedulers.Backtrackable.new_t (Colibri2_stdlib.Context.creator context);
context;
}
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index f7b48140a..af77dcd1b 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Colibri2_popop_lib
+module IArray = Colibri2_popop_lib.IArray
open Colibri2_popop_lib.Popop_stdlib
module Case = DInt
module Field = DInt
@@ -117,26 +117,26 @@ let case_of_adt adt =
(** Decide for destructors *)
module Decide = struct
let make_decision n adt cases d =
- Colibri2_popop_lib.Debug.dprintf4 Egraph.print_decision
- "[ADT] decide %a on %a" Case.S.pp cases Node.pp n;
+ Debug.dprintf4 Debug.decision "[ADT] decide %a on %a" Case.S.pp cases
+ Node.pp n;
upd_dom d n (Unk { adt; cases })
let new_decision n adt c =
{
- Egraph.prio = 1;
+ Choice.prio = 1;
choice =
(fun d ->
let decisions s =
- Egraph.DecTodo
+ Choice.DecTodo
[
make_decision n adt (Case.S.singleton c);
make_decision n adt (Case.S.remove c s);
]
in
match Egraph.get_dom d D.key n with
- | Some (One _) -> Egraph.DecNo
- | Some (Unk s) when Case.S.is_num_elt 1 s.cases -> Egraph.DecNo
- | Some (Unk s) when not (Case.S.mem c s.cases) -> Egraph.DecNo
+ | Some (One _) -> Choice.DecNo
+ | Some (Unk s) when Case.S.is_num_elt 1 s.cases -> Choice.DecNo
+ | Some (Unk s) when not (Case.S.mem c s.cases) -> Choice.DecNo
| Some (Unk s) -> decisions s.cases
| None -> decisions (case_of_adt adt));
}
@@ -151,7 +151,7 @@ let converter d (f : Ground.t) =
let setb = setv Boolean.dom in
let getb = getv Boolean.dom in
let set = updd upd_dom in
- let get = getd key in
+ let get = getd D.key in
match Ground.sem f with
| { app = { builtin = Expr.Tester { adt; case; _ }; _ }; args; tyargs; _ } ->
let adt = Option.get_exn (Adt_value.MonoAdt.index adt tyargs) in
@@ -164,7 +164,7 @@ let converter d (f : Ground.t) =
else
let cases = Case.S.remove case (case_of_adt adt) in
if Case.S.is_empty cases then (
- Debug.dprintf4 Egraph.print_contradiction
+ Debug.dprintf4 Debug.contradiction
"[ADT] tester %a removed the only case %a of the type" Node.pp
r Case.pp case;
Egraph.contradiction d)
@@ -199,7 +199,7 @@ let converter d (f : Ground.t) =
let adt = Option.get_exn (Adt_value.MonoAdt.index adt tyargs) in
let e = IArray.extract1_exn args in
reg e;
- Egraph.register_decision d (Decide.new_decision e adt case);
+ Choice.register d (Decide.new_decision e adt case);
attach d
(set e
(let* ve = get e in
@@ -272,4 +272,4 @@ let init env : unit =
Ground.register_converter env converter;
init_node env
-let () = Egraph.add_default_theory init
+let () = Init.add_default_theory init
diff --git a/src_colibri2/theories/ADT/dune b/src_colibri2/theories/ADT/dune
index ecb846e0b..bd987f5ba 100644
--- a/src_colibri2/theories/ADT/dune
+++ b/src_colibri2/theories/ADT/dune
@@ -3,7 +3,7 @@
(public_name colibri2.theories.adt)
(synopsis "theory of algebraic datatype for colibri2")
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.core colibri2.theories.bool
colibri2.theories.quantifiers
)
(preprocess
diff --git a/src_colibri2/theories/FP/dune b/src_colibri2/theories/FP/dune
index f409932f1..dc4d996e9 100644
--- a/src_colibri2/theories/FP/dune
+++ b/src_colibri2/theories/FP/dune
@@ -7,7 +7,6 @@
farith
colibri2.stdlib
colibri2.popop_lib
- colibri2.core.structures
colibri2.core)
(preprocess
(pps ppx_deriving.std ppx_hash))
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 7da6179fb..74b3dfd93 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -31,7 +31,7 @@ include Float32
let init_ty d =
Interp.Register.ty d (fun d ty ->
match ty with
- | {app={builtin = Expr.Float(8, 24);_};_} ->
+ | {app={builtin = Builtin.Float(8, 24);_};_} ->
let seq =
let open Interp.SeqLim in
let+ e = of_seq d posint_sequence in
diff --git a/src_colibri2/theories/FP/float64.ml b/src_colibri2/theories/FP/float64.ml
index eb1d80dce..803b353b0 100644
--- a/src_colibri2/theories/FP/float64.ml
+++ b/src_colibri2/theories/FP/float64.ml
@@ -30,7 +30,7 @@ include Float64
let init_ty d =
Interp.Register.ty d (fun d ty ->
match ty with
- | {app={builtin = Expr.Float(11, 53);_};_} ->
+ | {app={builtin = Builtin.Float(11, 53);_};_} ->
let seq =
let open Interp.SeqLim in
let+ e = of_seq d posint_sequence in
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index b43e48302..aa65f4931 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/src_colibri2/theories/FP/fp.ml
@@ -23,4 +23,4 @@ let th_register env =
(* Add the theory to defaults *)
let () =
- Egraph.add_default_theory th_register
+ Init.add_default_theory th_register
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index b9f35ca93..d92e352e1 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -34,7 +34,7 @@ let th_register env =
Dom_product.init env;
()
-let () = Egraph.add_default_theory th_register
+let () = Init.add_default_theory th_register
(** Helpers to remove *)
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index a727f38c2..0ffb6fd6f 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -73,21 +73,21 @@ let is_integer d n =
module ChoLRA = struct
let make_decision node v env =
- Debug.dprintf4 Egraph.print_decision
+ Debug.dprintf4 Debug.decision
"[LRA] decide %a on %a" D.pp v Node.pp node;
set_dom env node v
let choose_decision node env =
let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
match D.split_heuristic v with
- | Singleton _ -> Egraph.DecNo
+ | Singleton _ -> Choice.DecNo
| Splitted (v1,v2) ->
DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
| NotSplitted ->
DecTodo [make_decision node (D.singleton (D.choose v))]
let choice n = {
- Egraph.prio = 1;
+ Choice.prio = 1;
choice = choose_decision n;
}
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 243272c3b..4ee192231 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -127,7 +127,7 @@ module Th = struct
end
| Cst c ->
(* 0 = cst <> 0 *)
- Debug.dprintf6 Egraph.print_contradiction
+ Debug.dprintf6 Debug.contradiction
"[LRA/Poly] Found 0 = %a when merging %a and %a"
Q.pp c
Node.pp cl1 Node.pp cl2;
@@ -162,7 +162,7 @@ module Th = struct
| Zero -> ()
| Cst c ->
(* 0 = cst <> 0 *)
- Debug.dprintf4 Egraph.print_contradiction
+ Debug.dprintf4 Debug.contradiction
"[LRA/Poly] Found 0 = %a when updating %a"
Q.pp c
Node.pp cl;
@@ -177,7 +177,7 @@ module Th = struct
let key = dom
end
-let () = Egraph.register_dom(module Th)
+let () = Dom.register(module Th)
let norm d (p:Polynome.t) =
let add acc cl c =
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 9ca609428..5d10dbc5e 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -282,7 +282,7 @@ module Th = struct
let pp = pp
end
-let () = Egraph.register_dom(module Th)
+let () = Dom.register(module Th)
let get_repr d n =
let open CCOpt in
@@ -319,7 +319,7 @@ module ChangePos = struct
end
-let () = Egraph.Wait.register_dem (module ChangePos)
+let () = Events.register (module ChangePos)
let factorize res a coef b d _ =
match Egraph.get_dom d dom a, Egraph.get_dom d dom b with
diff --git a/src_colibri2/theories/LRA/dune b/src_colibri2/theories/LRA/dune
index 6fe40e43d..4b7875743 100644
--- a/src_colibri2/theories/LRA/dune
+++ b/src_colibri2/theories/LRA/dune
@@ -3,7 +3,7 @@
(public_name colibri2.theories.LRA)
(synopsis "theories for colibri2")
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.core colibri2.theories.bool
colibri2.theories.quantifiers
colibri2.theories.LRA.stages )
(preprocess
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 2dfec3e4b..ebb907c57 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -138,7 +138,7 @@ let add_eq d eqs p bound origins =
Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
eqs
| Some p, bound ->
- Debug.dprintf4 Egraph.print_contradiction
+ Debug.dprintf4 Debug.contradiction
"[LRA/Fourier] Found %a%a0"
Q.pp p Bound.pp bound;
Egraph.contradiction d
@@ -244,7 +244,7 @@ module Daemon = struct
let run d () = fm d
end
-let () = Egraph.Wait.register_dem (module Daemon)
+let () = Events.register (module Daemon)
(** {2 Initialization} *)
@@ -252,14 +252,14 @@ 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.enqueue;
- Egraph.attach_repr d n Daemon.enqueue;
+ Events.attach_dom d n Dom_polynome.dom Daemon.enqueue;
+ Events.attach_repr d n Daemon.enqueue;
in
IArray.iter ~f:attach args;
- Egraph.attach_value d (Ground.node f) Boolean.dom (fun d n _ -> Daemon.enqueue d n);
+ Events.attach_value d (Ground.node f) Boolean.dom (fun d n _ -> Daemon.enqueue d n);
Datastructure.Push.push comparisons d f;
- Egraph.new_pending_daemon d Daemon.key ();
- Egraph.register_decision d (Boolean.chobool (Ground.node f))
+ Events.new_pending_daemon d Daemon.key ();
+ Choice.register d (Boolean.chobool (Ground.node f))
| _ -> ()
let init env =
diff --git a/src_colibri2/theories/LRA/stages/stage0/dune b/src_colibri2/theories/LRA/stages/stage0/dune
index a84e03e54..f3c33491d 100644
--- a/src_colibri2/theories/LRA/stages/stage0/dune
+++ b/src_colibri2/theories/LRA/stages/stage0/dune
@@ -2,7 +2,7 @@
(name colibri2_theories_LRA_stages_stage0_sign_domain)
(public_name colibri2.theories.LRA.stages.stage0.sign_domain)
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.core colibri2.theories.bool
colibri2.theories.quantifiers colibri2.theories.LRA.stages.def)
(preprocess
(pps ppx_deriving.std ppx_hash))
diff --git a/src_colibri2/theories/LRA/stages/stage1/dune b/src_colibri2/theories/LRA/stages/stage1/dune
index 89ee0c1fb..b5c5dfed1 100644
--- a/src_colibri2/theories/LRA/stages/stage1/dune
+++ b/src_colibri2/theories/LRA/stages/stage1/dune
@@ -2,7 +2,7 @@
(name colibri2_theories_LRA_stages_stage1_interval_domain)
(public_name colibri2.theories.LRA.stages.stage1.interval_domain)
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.core colibri2.theories.bool
colibri2.theories.quantifiers colibri2.theories.LRA.stages.def
colibrics.lib
)
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index ea064fe48..ef869aaf5 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -100,14 +100,14 @@ let _or = _gen Expr.Term._or
module ChoBool = struct
let make_decision env node b =
- Debug.dprintf3 Egraph.print_decision "[Bool] decide %b on %a" b Node.pp node;
+ Debug.dprintf3 Debug.decision "[Bool] decide %b on %a" b Node.pp node;
set_bool env node b
let choose_decision node env =
match is env node with
| Some _ ->
- Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
- Egraph.DecNo
+ Debug.dprintf2 Debug.decision "[Bool] No decision for %a" Node.pp node;
+ Choice.DecNo
| None -> DecTodo
(List.map (fun v env -> make_decision env node v)
(Shuffle.shufflel [true;false]))
@@ -115,7 +115,7 @@ module ChoBool = struct
end
let chobool n = {
- Egraph.prio = 1;
+ Choice.prio = 1;
choice = ChoBool.choose_decision n;
}
@@ -173,9 +173,9 @@ module TwoWatchLiteral = struct
let run d r = r d
let rec attach d r i =
- Egraph.Ro.attach_value d
+ Events.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);
+ Events.Ro.attach_repr d (IArray.get (Ground.sem r.ground).args i) (fun d _ -> enqueue d r);
and enqueue d r =
let o_from_start = Context.Ref.get r.from_start in
@@ -255,7 +255,7 @@ module TwoWatchLiteral = struct
attach (d :> Egraph.Ro.t) r from_end
end
- let () = Egraph.Wait.register_dem (module Daemon)
+ let () = Events.register (module Daemon)
let create = Daemon.create
end
@@ -270,7 +270,7 @@ let converter d (f:Ground.t) =
match Ground.sem f with
| { app = {builtin = Expr.Base; _ }; ty; _ }
when Ground.Ty.equal ty Ground.Ty.bool ->
- Egraph.register_decision d (chobool res)
+ Choice.register d (chobool res)
| { app = {builtin = Expr.Or}; tyargs = []; args; _ } ->
reg_args args;
TwoWatchLiteral.create d values_true f
@@ -347,4 +347,4 @@ let th_register env =
init_check env;
()
-let () = Egraph.add_default_theory th_register
+let () = Init.add_default_theory th_register
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index 44ec950a8..defd19ec0 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -38,7 +38,7 @@ val is_unknown : Egraph.t -> Node.t -> bool
val th_register: Egraph.t -> unit
-val chobool: Node.t -> Egraph.choice
+val chobool: Node.t -> Choice.t
(* val make_dec: Variable.make_dec *)
diff --git a/src_colibri2/theories/bool/dune b/src_colibri2/theories/bool/dune
index 1b294acbe..41ff0647b 100644
--- a/src_colibri2/theories/bool/dune
+++ b/src_colibri2/theories/bool/dune
@@ -4,7 +4,7 @@
(synopsis "theories for colibri2")
(modules Boolean Equality)
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core dolmen.std)
+ colibri2.core dolmen.std)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 0819e5929..b8a6cf32c 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -169,7 +169,7 @@ module D = struct
let s =
Dis.test_disjoint
(fun c ->
- Debug.dprintf6 Egraph.print_contradiction
+ Debug.dprintf6 Debug.contradiction
"[Equality] The currently merged %a and %a are different since \
%a"
Node.pp cl1 Node.pp cl2 Dis.pp_elt c;
@@ -294,7 +294,7 @@ let norm_set d the =
module ChoEquals = struct
let make_equal the (cl1, cl2) d =
- Debug.dprintf6 Egraph.print_decision
+ Debug.dprintf6 Debug.decision
"[Equality] @[decide on merge of %a and %a in %a@]" Node.pp cl1 Node.pp
cl2 ThE.pp the;
Egraph.register d cl1;
@@ -302,7 +302,7 @@ module ChoEquals = struct
Egraph.merge d cl1 cl2
let make_disequal the (cl1, cl2) d =
- Debug.dprintf6 Egraph.print_decision
+ Debug.dprintf6 Debug.decision
"[Equality] @[decide on merge of %a and %a in %a@]" Node.pp cl1 Node.pp
cl2 ThE.pp the;
Egraph.register d cl1;
@@ -315,8 +315,8 @@ module ChoEquals = struct
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
+ if Boolean.is_false d own then Choice.DecNo
+ else if norm_set d the then Choice.DecNo
else
match find_not_disequal d v with
| `AllDiff _ ->
@@ -325,7 +325,7 @@ module ChoEquals = struct
| `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 }
+ let mk_choice the = { Choice.choice = choose_decision the; prio = 1 }
end
let norm_dom d the =
@@ -363,7 +363,7 @@ let norm_dom d the =
(** Propagation *)
-module DaemonPropa = Demon.Key.Register (struct
+module DaemonPropa = DaemonWithKey.Register (struct
module Key = ThE
let delay = Events.Delayed_by 1
@@ -391,7 +391,7 @@ let attach_new_equalities d =
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))
+ Choice.register d (ChoEquals.mk_choice clsem))
| _ -> ())
(** ITE *)
@@ -527,4 +527,4 @@ let th_register env =
init_check env;
()
-let () = Egraph.add_default_theory th_register
+let () = Init.add_default_theory th_register
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 6d5c02821..124dc033c 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -70,7 +70,7 @@ let rec exec d acc substs n ip =
in
let acc =
let match_one_app (ptyl, pargs, pos, t) acc g =
- let { Ground.Term.tyargs = tyl; args; _ } = Ground.sem g in
+ let { Ground.tyargs = tyl; args; _ } = Ground.sem g in
let substs = List.fold_left2 Pattern.match_ty substs tyl ptyl in
let substs =
if Ground.Subst.S.is_empty substs then substs
diff --git a/src_colibri2/theories/quantifier/dune b/src_colibri2/theories/quantifier/dune
index 279a2d266..747afb861 100644
--- a/src_colibri2/theories/quantifier/dune
+++ b/src_colibri2/theories/quantifier/dune
@@ -3,7 +3,7 @@
(public_name colibri2.theories.quantifiers)
(synopsis "theories for colibri2")
(libraries containers base ocamlgraph colibri2.stdlib colibri2.popop_lib
- colibri2.core.structures colibri2.core colibri2.theories.bool)
+ colibri2.core colibri2.theories.bool)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -open Colibri2_stdlib -open Std -open
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index c8e4a7c39..53755873b 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -45,10 +45,7 @@ let congruence_closure d ~other parent0 ~repr parent1 =
let h = Ground.Term.H.create 10 in
let norm g =
let g = Ground.sem g in
- {
- g with
- Ground.Term.args = IArray.map ~f:find_as_if g.Ground.Term.args;
- }
+ { g with Ground.args = IArray.map ~f:find_as_if g.Ground.args }
in
let s = ref (Ground.S.union g1 g2) in
let not_first g = s := Ground.S.remove g !s in
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index dc5d72ea1..ebe4baf21 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -149,7 +149,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
in
Ground.S.fold_left
(fun acc n ->
- let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
+ let { Ground.app = f; tyargs = tyl; args; _ } = Ground.sem n in
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
@@ -192,7 +192,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
in
Ground.S.exists
(fun n ->
- let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
+ let { Ground.app = f; tyargs = tyl; args; _ } = Ground.sem n in
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)
@@ -321,7 +321,7 @@ let match_any_term d subst (p : t) : Ground.Subst.S.t =
| App (pf, ptyl, pargs) ->
Context.Push.fold
(fun acc n ->
- let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
+ let { Ground.app = f; tyargs = tyl; args; _ } = Ground.sem n in
assert (Expr.Term.Const.equal f pf);
let substs = List.fold_left2 match_ty subst tyl ptyl in
let substs =
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 8d0af561b..658f3c4d3 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -155,7 +155,7 @@ module Delayed_find_new_event = struct
let run d (n, ips) = process_inverted_path d n ips
end
-let () = Egraph.Wait.register_dem (module Delayed_find_new_event)
+let () = Events.register (module Delayed_find_new_event)
let () =
Dom.register
@@ -185,10 +185,10 @@ let () =
Egraph.set_dom d Info.dom cl1 info;
let ips = find_new_event d cl0 info0 cl1 info1 in
if not (Base.List.is_empty ips) then
- Egraph.new_pending_daemon d Delayed_find_new_event.key (repr, ips)
+ Events.new_pending_daemon d Delayed_find_new_event.key (repr, ips)
end)
-let skolemize d (e : Ground.ClosedQuantifier.t) =
+let skolemize d (e : Ground.ClosedQuantifier.s) =
if not (Base.List.is_empty e.ty_vars) then
invalid_arg "False type quantification";
let subst_term =
@@ -205,13 +205,13 @@ let skolemize d (e : Ground.ClosedQuantifier.t) =
n
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
+ Daemon.attach_value d (Ground.ClosedQuantifier.node th) Boolean.BoolValue.key
+ (fun d n b ->
+ match (Ground.ClosedQuantifier.sem th, Boolean.BoolValue.value b) with
| ({ binder = Exists; _ } as e), true
| ({ binder = Forall; _ } as e), false ->
- Debug.dprintf2 debug "[Quant] Skolemize %a"
- Ground.ThClosedQuantifier.pp th;
+ Debug.dprintf2 debug "[Quant] Skolemize %a" Ground.ClosedQuantifier.pp
+ th;
Egraph.merge d (skolemize d e) n
| { binder = Exists; _ }, false | { binder = Forall; _ }, true ->
let triggers =
@@ -220,15 +220,15 @@ let attach d th =
| triggers -> triggers
in
Debug.dprintf4 debug "[Quant] For %a adds %a"
- Ground.ThClosedQuantifier.pp th
+ Ground.ClosedQuantifier.pp th
Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp))
triggers;
List.iter (add_trigger d) triggers
(* Todo match with current terms *))
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);
+ let n = Ground.ClosedQuantifier.node th in
+ if Boolean.is_unknown d n then Choice.register d (Boolean.chobool n);
attach d th
(** Verify that this term is congruent closure to another already existing term
@@ -289,8 +289,8 @@ let add_info_on_ground_terms d thg =
let th_register d =
(* let delay = Events.Delayed_by 10 in *)
- Daemon.attach_reg_sem d Ground.ThClosedQuantifier.key quantifier_registered;
+ Daemon.attach_reg_sem d Ground.ClosedQuantifier.key quantifier_registered;
Ground.register_converter d (fun d g ->
if not (application_useless d g) then add_info_on_ground_terms d g)
-let () = Egraph.add_default_theory th_register
+let () = Init.add_default_theory th_register
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index 9d0eadb6c..a160ee268 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -27,7 +27,7 @@ module T = struct
type t = {
pat : Pattern.t;
checks : Pattern.t list;
- form : Ground.ThClosedQuantifier.t;
+ form : Ground.ClosedQuantifier.t;
eager : bool;
}
[@@deriving eq, ord, hash]
@@ -35,14 +35,14 @@ module T = struct
let pp fmt t =
Fmt.pf fmt "[%a, %a -> %a]" Pattern.pp t.pat
Fmt.(list ~sep:comma Pattern.pp)
- t.checks Ground.ThClosedQuantifier.pp t.form
+ t.checks Ground.ClosedQuantifier.pp t.form
end
include T
include Popop_stdlib.MkDatatype (T)
-let compute_top_triggers (cq : Ground.ThClosedQuantifier.t) =
- let cq' = Ground.ThClosedQuantifier.sem cq in
+let compute_top_triggers (cq : Ground.ClosedQuantifier.t) =
+ let cq' = Ground.ClosedQuantifier.sem cq in
let tyvs = cq'.ty_vars in
let tvs = cq'.term_vars in
let t = cq'.body in
@@ -106,8 +106,8 @@ let compute_top_triggers (cq : Ground.ThClosedQuantifier.t) =
multi_pats;
multi_pats
-let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
- let cq' = Ground.ThClosedQuantifier.sem cq in
+let compute_all_triggers (cq : Ground.ClosedQuantifier.t) =
+ let cq' = Ground.ClosedQuantifier.sem cq in
let tyvs = cq'.ty_vars in
let tvs = cq'.term_vars in
let t = cq'.body in
@@ -162,8 +162,8 @@ let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
in
pats
-let get_user_triggers (cq : Ground.ThClosedQuantifier.t) =
- let cq' = Ground.ThClosedQuantifier.sem cq in
+let get_user_triggers (cq : Ground.ClosedQuantifier.t) =
+ let cq' = Ground.ClosedQuantifier.sem cq in
let pats = Expr.Term.get_tag_list cq'.body Expr.Tags.triggers in
let tyvs = Expr.Ty.Var.S.of_list cq'.ty_vars in
let tvs = Expr.Term.Var.S.of_list cq'.term_vars in
@@ -204,14 +204,14 @@ let add_trigger d t =
| Node _ -> ()
let instantiate_aux d tri subst =
- let form = Ground.ThClosedQuantifier.sem tri.form in
+ let form = Ground.ClosedQuantifier.sem tri.form in
Debug.incr nb_instantiation;
let subst = Ground.Subst.distinct_union subst form.subst in
let n = Ground.convert ~subst form.body in
if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
Debug.incr nb_new_instantiation;
Egraph.register d n;
- Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form)
+ Egraph.merge d n (Ground.ClosedQuantifier.node tri.form)
module Delayed_instantiation = struct
let key =
@@ -231,13 +231,13 @@ module Delayed_instantiation = struct
let run d (tri, subst) =
Debug.dprintf8 debug
"[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
- subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp tri.pat
+ subst Ground.ClosedQuantifier.pp tri.form Pattern.pp tri.pat
Fmt.(list ~sep:comma Pattern.pp)
tri.checks;
instantiate_aux d tri subst
end
-let () = Egraph.Wait.register_dem (module Delayed_instantiation)
+let () = Events.register (module Delayed_instantiation)
let instantiate d tri subst =
let subst =
@@ -248,8 +248,7 @@ let instantiate d tri subst =
}
in
Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a"
- Ground.Subst.pp subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp
- tri.pat
+ Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form Pattern.pp tri.pat
Fmt.(list ~sep:comma Pattern.pp)
tri.checks;
if
@@ -261,7 +260,7 @@ let instantiate d tri subst =
then instantiate_aux d tri subst
else (
Debug.dprintf0 debug "[Quant] Delayed";
- Egraph.new_pending_daemon d Delayed_instantiation.key (tri, subst))
+ Events.new_pending_daemon d Delayed_instantiation.key (tri, subst))
let match_ d tri n =
Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index 395c16e7d..df743fb59 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -25,21 +25,21 @@ type t = {
(** The main pattern, the one matched to obtain a complete
substitution *)
checks : Pattern.t list; (** Guards for the existence of terms *)
- form : Ground.ThClosedQuantifier.t; (** the body of the formula *)
+ form : Ground.ClosedQuantifier.t; (** the body of the formula *)
eager : bool;
(** If it should be eagerly applied, otherwise wait for LastEffort *)
}
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
-val compute_top_triggers : Ground.ThClosedQuantifier.t -> t list
+val compute_top_triggers : Ground.ClosedQuantifier.t -> t list
(** Compute triggers, that should only add logical connective or equalities are
new terms *)
-val compute_all_triggers : Ground.ThClosedQuantifier.t -> t list
+val compute_all_triggers : Ground.ClosedQuantifier.t -> t list
(** Compute all the triggers whose patterns contain all the variables of the formula *)
-val get_user_triggers : Ground.ThClosedQuantifier.t -> t list
+val get_user_triggers : Ground.ClosedQuantifier.t -> t list
(** return the triggers given by the user *)
val env_vars : t Datastructure.Push.t
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index 490978b08..1ab005b7a 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -286,11 +286,11 @@ module UFModel = struct
let env =
HConst.create Fmt.nop "Uninterp.UFModel.env" (fun c _ -> Hargs.create c)
- let find d (g : Ground.Term.t) lv =
+ let find d (g : Ground.s) lv =
let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
Hargs.find_opt h lv
- let set d (g : Ground.Term.t) lv v =
+ let set d (g : Ground.s) lv v =
let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
Hargs.set h lv v
@@ -303,14 +303,14 @@ module UFModel = struct
match find d s lv with
| Some v' ->
if not (Value.equal v v') then (
- Debug.dprintf8 Egraph.print_contradiction
+ Debug.dprintf8 Debug.contradiction
"[Uninterp] The model of %a (%a) is %a and not %a" Ground.pp g
- Ground.Term.pp s Value.pp v' Value.pp v;
+ Ground.pp g Value.pp v' Value.pp v;
Egraph.contradiction d)
| None -> set d s lv v
in
let f d g =
- Daemon.FixingModel.attach_any_value d (Ground.node g) (check_or_update g)
+ DaemonFixingModel.attach_any_value d (Ground.node g) (check_or_update g)
in
f d g
@@ -350,4 +350,4 @@ let th_register env =
init_check env;
init_ty env
-let () = Egraph.add_default_theory th_register
+let () = Init.add_default_theory th_register
--
GitLab