Parameter Pmap.Key

include Soteria.Data.S_map.Key(CSYMEX).S
include Stdlib.Map.OrderedType
type t
val compare : t -> t -> int
include Soteria.Data.S_map.Key(CSYMEX).Abstr.Sem_eq with type t := t
include Soteria.Data.S_map.Key(CSYMEX).Abstr.Simplifiable with type t := t
val simplify : t -> t CSYMEX.t
val distinct : t list -> CSYMEX.Value.sbool CSYMEX.Value.t
include Soteria.Data.Abstr.M(CSYMEX).S_with_syn with type t := t
include Soteria.Data.Abstr.M(CSYMEX).S with type t := t
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val fresh : unit -> t CSYMEX.t
type syn

Syntactic representation of the abstraction (that can be serialized). Basically, everywhere a symbolic value exists, it must be cast to an Expr.t

val pp_syn : Ppx_deriving_runtime.Format.formatter -> syn -> Ppx_deriving_runtime.unit
val show_syn : syn -> Ppx_deriving_runtime.string
val to_syn : t -> syn
val subst : (CSYMEX.Value.Expr.t -> 'a CSYMEX.Value.t) -> syn -> t

Given a substitution, casts a syntactic object to a semantic object.

val learn_eq : syn -> t -> (unit, 'a) CSYMEX.Consumer.t

learn_eq s t extends the substitution θ of the consumer monad such that all variables of s are bound and θ(s) = t (or fails to do so).

val exprs_syn : syn -> CSYMEX.Value.Expr.t list

Returns the list of expressions contained by the abstraction.

val to_int : t -> int