type r = Shostak.Combine.rExtensible type for global domains identifiers, see GlobalDomains.
val src : Logs.srcmodule type GlobalDomain = sig ... endModule signature for global domains used by the union-find module.
type 'a global_domain = (module GlobalDomain with type t = 'a)The type of global domain modules with a given storage type (see GlobalDomain).
module GlobalDomains : sig ... endThis module provides a registry type to access and update a single "current" instance associated with multiple global domain types.
module LX = Shostak.Lval empty : tval find : t -> Expr.t -> r * Explanation.tval find_r : t -> r -> r * Explanation.tval domains : t -> GlobalDomains.tval set_domains : t -> GlobalDomains.t -> tval union :
t ->
r ->
r ->
Explanation.t ->
t * (r * (r * r * Explanation.t) list * r) listval distinct : t -> r list -> Explanation.t -> tval are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answerval are_distinct : t -> Expr.t -> Expr.t -> Th_util.answerval class_of : t -> Expr.t -> Expr.Set.tval rclass_of : t -> r -> Expr.Set.tval cl_extract : t -> Expr.Set.t listval print : t -> unitval assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * tval extract_concrete_model :
prop_model:Expr.Set.t ->
declared_ids:Id.typed list ->
t ->
Models.tCompute a counterexample using the Uf environment