Shostak.Combine
type r
val save_cache : unit -> unit
saves the module's current cache
val reinit_cache : unit -> unit
restores the module's cache
val make : Expr.t -> r * Expr.t list
val type_info : r -> Ty.t
val str_cmp : r -> r -> int
val hash_cmp : r -> r -> int
val equal : r -> r -> bool
val hash : r -> int
val leaves : r -> r list
val subst : r -> r -> r -> r
val solve : r -> r -> (r * r) list
val term_embed : Expr.t -> r
val term_extract : r -> Expr.t option * bool
val ac_embed : r Sig.ac -> r
val ac_extract : r -> r Sig.ac option
val color : r Sig.ac -> r
val fully_interpreted : Symbols.t -> Ty.t -> bool
val is_a_leaf : r -> bool
val print : Stdlib.Format.formatter -> r -> unit
val abstract_selectors : r -> (r * r) list -> r * (r * r) list
val top : unit -> r
val bot : unit -> r
val is_solvable_theory_symbol : Symbols.t -> Ty.t -> bool
val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string