Module Smt_sig.S.Symbol

module Symbol: sig .. end

Function symbols

type t = Hstring.t

The type of function symbols

val declare : Hstring.t -> Smt_sig.S.Type.t list -> Smt_sig.S.Type.t -> unit

declare s [arg_1; ... ; arg_n] out declares a new function symbol with type (arg_1, ... , arg_n) -> out

val type_of : t -> Smt_sig.S.Type.t list * Smt_sig.S.Type.t

type_of x returns the type of x.

val has_abstract_type : t -> bool

has_abstract_type x is true if the type of x is abstract.

val has_infinite_type : t -> bool

has_infinite_type x is true if the type of x is not finite.

val has_type_proc : t -> bool

has_type_proc x is true if x has the type of a process identifier.

val declared : t -> bool

declared x is true if x is already declared.