Module Shostak.Combine

include Sig.X
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 is_constant : r -> bool
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 -> 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 is_solvable_theory_symbol : Symbols.t -> bool
val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
val to_model_term : r -> Expr.t option

to_model_term r creates a model term if r is constant. The function cannot fail if r is a constant (that is statisfied the predicate X.is_constant).

The returned value always satisfies the predicate Expr.is_model_term. See its documentation for more details about model terms.

val src : Logs.src
val top : r
val bot : r