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 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 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.

The comparison function is based on hashes, not structural

include Container_types.S_plus_stdlib with type t := r
module T : Container_types_intf.Thing with type t = r
include Container_types_intf.Thing with type t := T.t
include Stdlib.Hashtbl.HashedType with type t := T.t
val equal : T.t -> T.t -> bool
val hash : T.t -> int
include Stdlib.Map.OrderedType with type t := T.t
val compare : T.t -> T.t -> int
val print : T.t Fmt.t
module Map : Container_types_intf.Map_plus_stdlib with type key = r and module Set = Set
val src : Logs.src
val top : r
val bot : r