Sig.SHOSTAK
type t
Type of terms of the theory
type r
Type of representants of terms of the theory
val name : string
Name of the theory
val is_mine_symb : Symbols.t -> Ty.t -> bool
return true if the symbol and the type are owned by the theory
val make : Expr.t -> r * Expr.t list
Give a representant of a term of the theory
val term_extract : r -> Expr.t option * bool
val color : r ac -> r
val type_info : t -> Ty.t
val embed : r -> t
val is_mine : t -> r
val leaves : t -> r list
Give the leaves of a term of the theory
val subst : r -> r -> t -> r
val compare : r -> r -> int
val equal : t -> t -> bool
val hash : t -> int
solve r1 r2, solve the equality r1=r2 and return the substitution
val solve : r -> r -> r solve_pb -> r solve_pb
val print : Stdlib.Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool
val abstract_selectors : t -> (r * r) list -> r * (r * r) list
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