colibri2_core.mli 42.76 KiB
(*************************************************************************)
(* 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
type 'a t
type rw
type wt = rw t
(** Egraph where its structure can be modified *)
type ro
type rt = ro t
(** Egraph where its structure can not be modified *)
val is_equal : _ t -> Node.t -> Node.t -> bool
(** Tests if two nodes are equal *)
val find_def : _ t -> Node.t -> Node.t
(** [find_def d n] finds the representative of the equivalence class of [n] *)
val find : _ t -> Node.t -> Node.t
val is_repr : _ t -> Node.t -> bool
val get_dom : _ t -> 'a Dom.Kind.t -> Node.t -> 'a option
(** [get_dom d dom n] returns the domain [dom] of the node [n] if it is set *)
val get_value : _ t -> Node.t -> Value.t option
(** [get_value d n] returns the value of the node [n] if set *)
(** {4 The classes must have been registered} *)
val is_registered : _ t -> Node.t -> bool
(** [is_registered n] tests if [n] is registered *)
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 *)
(** {3 Immediate modifications} *)
val set_dom : rw t -> 'a Dom.Kind.t -> Node.t -> 'a -> unit
(** change the dom of the equivalence class *)
val unset_dom : rw t -> 'a Dom.Kind.t -> Node.t -> unit
(** remove the dom of the equivalence class *)
(** {3 Delayed modifications} *)
val set_thterm : rw t -> Node.t -> ThTerm.t -> unit
(** attach a theory term to an equivalence class *)
val set_value : rw t -> Node.t -> Value.t -> unit
(** attach value to an equivalence class *)
val merge : rw t -> Node.t -> Node.t -> unit
(** [merge n1 n2] Asks to merge the equivalence class of [n1] and [n2] *)
val contradiction : _ t -> 'a
(** raises {!Contradiction} *)
exception Contradiction
exception NotRegistered
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.NotTotallyApplied.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
val map_repr : _ Egraph.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 array : t -> t -> t
(** The type of strings *)
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 -> _ Egraph.t -> Expr.Term.t -> Node.t
val apply :
_ Egraph.t ->
Expr.Term.Const.t ->
Ty.t list ->
Node.t Colibri2_popop_lib.IArray.t ->
s
val init : Egraph.wt -> unit
val register_converter : Egraph.wt -> (Egraph.wt -> t -> unit) -> unit
(** register callback called for each new ground term registered *)
val tys : _ Egraph.t -> Node.t -> Ty.S.t
val add_ty : Egraph.wt -> Node.t -> Ground.Ty.t -> unit
module Defs : sig
val add :
Egraph.wt ->
Dolmen_std.Expr.term_cst ->
Dolmen_std.Expr.ty_var list ->
Dolmen_std.Expr.term_var list ->
Expr.term ->
unit
(** [add d sym tys vars def] add the definition [def] for the symbol [sym] *)
val add_handler :
Egraph.wt ->
(Egraph.wt ->
Dolmen_std.Expr.Term.Const.t ->
Dolmen_std.Expr.Ty.Var.t list ->
Dolmen_std.Expr.Term.Var.t list ->
Expr.Term.t ->
unit) ->
unit
(** Called every time a definition is registered *)
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 NotTotallyApplied : 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
val convert_one_app :
Subst.t ->
'a Egraph.t ->
Expr.term ->
Expr.ty list ->
Node.t Colibri2_popop_lib.IArray.t ->
Expr.ty ->
Node.t
val convert_one_cst :
Subst.t -> 'a Egraph.t -> Dolmen_std.Expr.term_cst -> Node.t
val convert_one_binder :
Subst.t -> 'a Egraph.t -> Expr.binder -> Expr.term -> Expr.ty -> Node.t
val convert_let_seq :
Subst.t ->
'a ->
(Dolmen_std.Expr.term_var * Expr.term) list ->
Expr.term ->
('a -> Subst.t -> Expr.term -> Node.t) ->
Node.t
val convert_let_par :
Subst.t ->
'a ->
(Dolmen_std.Expr.term_var * Expr.term) list ->
Expr.term ->
('a -> Subst.t -> Expr.term -> Node.t) ->
Node.t
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.NotTotallyApplied.s} is {!Ground.NotTotallyApplied.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
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 of_value : s -> Value.t
val coerce_nodevalue : Value.t -> t
val coerce_value : Value.t -> s
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.wt -> t option * Node.t -> t option * Node.t -> bool -> unit
(** [merge d (dom1,cl1) (dom2,cl2) inv] called when [cl1] and [cl2] are
going to be merged in the same equivalence class. - if inv is false, cl2 will
be the new representative - if inv is true, cl1 will be the new
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.wt -> t -> t -> t option
(** [inter d d1 d2] compute the intersection of [d1] and [d2] return [None]
if it is empty. In this last case a contradiction is reported *)
val is_singleton : Egraph.wt -> 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.wt -> Node.t -> L.t -> unit
(** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
(** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
[l] with the current value of the domain. *)
end
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 filter_map : 'a t -> f:('a -> 'b option) -> 'b t
val unfold_with :
'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Base.Sequence.Step.t) -> 'c t
val hd_exn : 'a t -> 'a
end
type check =
| Right
(** The current model verify the interpretation of the constraint *)
| Wrong
(** The current model do not verify the interpretation of the constraint *)
| NA (** I don't know the interpretation of the constraint *)
| Unknown
(** I know the interpretation of the constraint but I can't check it *)
val check_of_bool : bool -> check
(** {!Right} for {!true}, {!Wrong} for {!false} *)
type compute = Value of Value.t | NA
module Register : sig
val check : Egraph.wt -> (Egraph.rt -> Ground.t -> check) -> unit
(** Check the value of the arguments corresponds to the the one of the of
the ground term according to its interpretation *)
val check_closed_quantifier :
Egraph.wt -> (Egraph.rt -> Ground.ClosedQuantifier.t -> check) -> unit
(** Check the interpretation of the closed quantifier in the current model *)
val check_not_totally_applied :
Egraph.wt -> (Egraph.rt -> Ground.NotTotallyApplied.t -> check) -> unit
(** Check the interpretation for this partial application or lambdas *)
val compute : Egraph.wt -> (Egraph.rt -> Ground.t -> compute) -> unit
val compute_closed_quantifier :
Egraph.wt -> (Egraph.rt -> Ground.ClosedQuantifier.t -> compute) -> unit
val compute_not_totally_applied :
Egraph.wt -> (Egraph.rt -> Ground.NotTotallyApplied.t -> compute) -> unit
val node :
Egraph.wt ->
((Egraph.wt -> Node.t -> Value.t SeqLim.t) ->
Egraph.wt ->
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.wt -> (Egraph.rt -> Ground.Ty.t -> Value.t SeqLim.t option) -> unit
(** Register iterators on all the possible value of some types, all the values
must be reached eventually *)
val print_value_smt :
(_, 'a) Value.Kind.t -> (Egraph.rt -> 'a Fmt.t) -> unit
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 *)
val print_value_smt : _ Egraph.t -> Value.t Fmt.t
val interp : Egraph.wt -> Expr.Term.t -> Value.t
(** [interp d e] Should be used when the model has been computed. Compute the
value of [e] in the current model. The value of [e] and the intermediary
expression are also stored in the [d] *)
module WatchArgs : sig
val create :
Egraph.wt -> (Egraph.wt -> Ground.t -> unit) -> Ground.t -> unit
(** call the given function when all the arguments of the ground term have a value *)
end
end
(** {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
val iter : f:(key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
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
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 type Memo2 = sig
type ('a, 'b) t
type key
val create :
'a Format.printer -> string -> ('b Egraph.t -> key -> 'a) -> ('a, 'b) t
val find : ('a, 'b) t -> 'b Egraph.t -> key -> 'a
val iter : (key -> 'a -> unit) -> ('a, 'b) t -> 'b Egraph.t -> unit
val fold :
(key -> 'a -> 'acc -> 'acc) -> ('a, 'b) t -> 'b Egraph.t -> 'acc -> 'acc
end
module Memo2 (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
Memo2 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 exists : f:('a -> bool) -> 'a t -> _ Egraph.t -> bool
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
end
end
(** {3 Events } *)
(**
The modification of the Egraph (events) can be monitored through daemons.
*)
module type 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 ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
(Egraph.wt -> Node.t -> unit) ->
unit
(** [attach_dom d ?direct n dom callback] The callback is scheduled when the
domain [dom] of the equivalence class of [n] is modified. If direct is true
(default) the callback is scheduled immediately if the domain is already
set. *)
val attach_any_dom :
_ Egraph.t ->
?thterm:ThTerm.t ->
'a Dom.Kind.t ->
(Egraph.wt -> Node.t -> unit) ->
unit
val attach_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
(Egraph.wt -> Node.t -> 'b -> unit) ->
unit
val attach_any_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
(Egraph.wt -> Node.t -> Value.t -> unit) ->
unit
val attach_reg_any :
_ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.wt -> Node.t -> unit) -> unit
val attach_reg_node :
_ Egraph.t ->
?thterm:ThTerm.t ->
Node.t ->
(Egraph.wt -> Node.t -> unit) ->
unit
val attach_reg_sem :
_ Egraph.t ->
?thterm:ThTerm.t ->
('a, 'b) ThTerm.Kind.t ->
(Egraph.wt -> 'b -> unit) ->
unit
val attach_reg_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
('a, 'b) Value.Kind.t ->
(Egraph.wt -> 'b -> unit) ->
unit
val attach_repr :
_ Egraph.t ->
?thterm:ThTerm.t ->
Node.t ->
(Egraph.wt -> Node.t -> unit) ->
unit
val attach_any_repr :
_ Egraph.t -> ?thterm:ThTerm.t -> (Egraph.wt -> Node.t -> unit) -> unit
val schedule_immediately :
_ Egraph.t -> ?thterm:Nodes.ThTerm.t -> (Egraph.wt -> unit) -> unit
end
module Daemon : Daemon
module DaemonFixingModel : Daemon
(** Same as {!Daemon} but they are scheduled to run as soon as possible during
the FixingModel phase *)
module DaemonLastEffort : Daemon
module DaemonLastEffortUncontextual : Daemon
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.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
(Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
(** [attach_dom d ?direct n dom callback] The callback is *)
val attach_any_dom :
_ Egraph.t ->
?thterm:ThTerm.t ->
'a Dom.Kind.t ->
(Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
(Egraph.rt -> Node.t -> 'b -> (Egraph.wt -> unit) option) ->
unit
val attach_any_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
(Egraph.rt -> Node.t -> Value.t -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_any :
_ Egraph.t ->
?thterm:ThTerm.t ->
(Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_node :
_ Egraph.t ->
?thterm:ThTerm.t ->
Node.t ->
(Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_sem :
_ Egraph.t ->
?thterm:ThTerm.t ->
('a, 'b) ThTerm.Kind.t ->
(Egraph.rt -> 'b -> (Egraph.wt -> unit) option) ->
unit
val attach_reg_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
('a, 'b) Value.Kind.t ->
(Egraph.rt -> 'b -> (Egraph.wt -> unit) option) ->
unit
val attach_repr :
_ Egraph.t ->
?thterm:ThTerm.t ->
Node.t ->
(Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
val attach_any_repr :
_ Egraph.t ->
?thterm:ThTerm.t ->
(Egraph.rt -> Node.t -> (Egraph.wt -> unit) option) ->
unit
end
module Monad : sig
type 'a monad
type sequence
val getd : ?def:'a -> 'a Dom.Kind.t -> Node.t -> 'a option monad
val setd : 'a Dom.Kind.t -> Node.t -> 'a option monad -> sequence
val exec : (Egraph.wt -> unit) -> bool option monad -> sequence
val updd :
(Egraph.wt -> 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 exec_ro : (Egraph.rt -> unit) -> 'a monad -> 'a monad
(** An hook in the middle, for printing debug message for example *)
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 -> ?thterm:ThTerm.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.wt -> Key.t -> state
val name : string
end
module Register (S : S) : sig
val attach_dom :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
'a Dom.Kind.t ->
S.Key.t ->
unit
val attach_any_dom :
_ Egraph.t -> ?thterm:ThTerm.t -> 'a Dom.Kind.t -> S.Key.t -> unit
val attach_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
('a, 'b) Value.Kind.t ->
S.Key.t ->
unit
val attach_any_value :
_ Egraph.t ->
?thterm:ThTerm.t ->
?direct:bool ->
Node.t ->
S.Key.t ->
unit
val attach_reg_any : _ Egraph.t -> ?thterm:ThTerm.t -> S.Key.t -> unit
val attach_reg_node :
_ Egraph.t -> ?thterm:ThTerm.t -> Node.t -> S.Key.t -> unit
val attach_reg_sem :
_ Egraph.t ->
?thterm:ThTerm.t ->
('a, 'b) ThTerm.Kind.t ->
S.Key.t ->
unit
val attach_reg_value :
_ Egraph.t -> ?thterm:ThTerm.t -> ('a, 'b) Value.Kind.t -> S.Key.t -> unit
val attach_repr :
_ Egraph.t -> ?thterm:ThTerm.t -> Node.t -> S.Key.t -> unit
val attach_any_repr : _ Egraph.t -> ?thterm:ThTerm.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
(** After no propagation and decisions remains to be done *)
| LastEffortUncontextual of int
(** Same as before but could be moved as propagation before the time it is
added *)
| FixingModel
type enqueue =
| EnqRun : 'r Dem.t * 'r * ThTerm.t option -> enqueue
(** Schedule a daemon run *)
| EnqLast : 'r Dem.t * 'r * ThTerm.t option -> 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 * ThTerm.t option -> daemon_key
val pp_daemon_key : daemon_key Fmt.t
(** {3 Basic daemons} *)
module type T = sig
type runable
val print_runable : runable Format.printer
val run : Egraph.wt -> 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.rt -> Node.t -> enqueue) ->
unit
(** wakeup when the dom of the node change *)
val attach_any_dom :
_ Egraph.t -> 'a Dom.Kind.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when the dom of any node change *)
val attach_value :
_ Egraph.t ->
?direct:bool -> Node.t ->
('a, 'b) Value.Kind.t ->
(Egraph.rt -> 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.rt -> Node.t -> Value.t -> enqueue) ->
unit
(** wakeup when any kind of value is attached to this equivalence class *)
val attach_reg_any : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when any node is registered *)
val attach_reg_node :
_ Egraph.t -> Node.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when this node is registered *)
val attach_reg_sem :
_ Egraph.t -> ('a, 'b) ThTerm.Kind.t -> (Egraph.rt -> 'b -> enqueue) -> unit
(** wakeup when a new semantical class is registered *)
val attach_reg_value :
_ Egraph.t -> ('a, 'b) Value.Kind.t -> (Egraph.rt -> 'b -> enqueue) -> unit
(** wakeup when a new value is registered *)
val attach_repr :
_ Egraph.t -> Node.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when it is not anymore the representative class *)
val attach_any_repr : _ Egraph.t -> (Egraph.rt -> Node.t -> enqueue) -> unit
(** wakeup when a node is not its representative class anymore *)
val new_pending_daemon :
_ Egraph.t -> ?thterm:ThTerm.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.wt -> unit) list
and t = { choice : Egraph.wt -> choice_state; prio : int; print_cho : string }
val register : _ Egraph.t -> Ground.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. The decision will not be scheduled if the ground term is part of a
group not activated.If no group have been specified at that point, the
default is for the decision to be directly activated *)
val register_thterm : _ Egraph.t -> ThTerm.t -> t -> unit
(** Same as {!register} but for {!ThTerm.t} *)
module Group : sig
type t
(** A scope for decision, allows to wait before adding decisions for terms.
Used for propagating into a term without decisions *)
val create : _ Egraph.t -> t
(** Create a new group *)
val activate : _ Egraph.t -> t -> unit
val add_to_group : _ Egraph.t -> ThTerm.t -> t -> unit
(** Add a {!ThTerm.t} to a group *)
val make_choosable : _ Egraph.t -> ThTerm.t -> unit
(** Register the decisions attached to the node, and will not delay them in the
future *)
val add_to_group_of : _ Egraph.t -> ThTerm.t -> ThTerm.t -> unit
(** [add_to_group_of d t1 t2] add t1 in the group of t2 *)
end
end
(** {3 Helpers } *)
module Init : sig
val add_default_theory : (Egraph.wt -> unit) -> unit
end
module Debug : sig
type flag = Colibri2_stdlib.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 ->
?ct:unit ->
flag ->
(unit, Format.formatter, unit) format ->
unit
(** Print only if the flag is set *)
val dprintf1 :
?nobox:unit ->
?ct:unit ->
flag ->
('a -> unit, Format.formatter, unit) format ->
'a ->
unit
(** Print only if the flag is set *)
val dprintf2 :
?nobox:unit ->
?ct:unit ->
flag ->
('b -> 'a -> unit, Format.formatter, unit) format ->
'b ->
'a ->
unit
(** Print only if the flag is set *)
val dprintf3 :
?nobox:unit ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 ->
?ct: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 : string -> int stat
val register_stats_time : string -> float stat
val add_time_during : float stat -> (unit -> 'a) -> 'a
val incr : int stat -> unit
val decr : int stat -> unit
val real_dprintf :
?nobox:unit -> ?ct:unit -> ('a, Format.formatter, unit) format -> 'a
end
module Options : sig
type 'a t
val register : ?pp:'a Fmt.t -> string -> 'a Cmdliner.Term.t -> 'a t
(** Register a new option *)
val get : _ Egraph.t -> 'a t -> 'a
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.wt
val run_daemon : Egraph.wt -> 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
val get_unknown : t -> bool
(** Indicate if the current status can't be sat but only unknown *)
end
val default_theories : unit -> (Egraph.wt -> unit) list
val ground_init : Egraph.wt -> unit
(** Initialize the module ground for later use *)
val interp_init : Egraph.wt -> unit
(** Initialize the module interp for later use *)
val get_event_priority : Events.daemon_key -> Events.delay
val flush_internal : Egraph.wt -> unit
module Fix_model : sig
(** The model is search using iterative deepening depth-first search for
ensuring optimality even in presence of infinite choice *)
val next_dec : Egraph.wt -> (Egraph.wt -> unit) Base.Sequence.t
(** Add a level of decision for fixing the model, another level could be
needed. Could raise unsatisfiable if all the model have been tried *)
end
module Options : sig
type options
val set_egraph : _ Egraph.t -> options -> unit
val parser : unit -> options Cmdliner.Term.t
val default_options : unit -> options
end
end