AltErgoLib.Uf
type r = Shostak.Combine.r
module LX : Xliteral.S with type elt = r
val empty : unit -> t
val find : t -> Expr.t -> r * Explanation.t
val find_r : t -> r -> r * Explanation.t
val union :
t ->
r ->
r ->
Explanation.t ->
t * (r * (r * r * Explanation.t) list * r) list
val distinct : t -> r list -> Explanation.t -> t
val are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answer
val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer
val cl_extract : t -> AltErgoLib.Expr.Set.t list
val print : t -> unit
val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
val output_concrete_model :
Stdlib.Format.formatter ->
prop_model:AltErgoLib.Expr.Set.t ->
t ->
unit
Compute a counterexample using the Uf environment and then print it on the given formatter with the corresponding format setted with Options.get_output_format