Enum.Shostak
type r = X.r
Type of representants of terms of the theory
return true if the symbol and the type are owned by the theory
val hash : t -> int
solve r1 r2, solve the equality r1=r2 and return the substitution
val solve : r -> r -> r Sig.solve_pb -> r Sig.solve_pb
val print : Stdlib.Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool