Module Smt_sig.S.Type

module Type: sig .. end

Typing

type t = Hstring.t

The type of types in the solver

val type_int : t

The type of integers

val type_real : t

The type of reals

val type_bool : t

The type of booleans

val type_proc : t

The type processes (identifiers)

val declare : Hstring.t -> Hstring.t list -> unit

declare n cstrs declares a new enumerated data-type with name n and constructors cstrs.
declare n [] declares a new abstract type with name n.

val all_constructors : unit -> Hstring.t list

all_constructors () returns a list of all the defined constructors.

val constructors : t -> Hstring.t list

constructors ty returns the list of constructors of ty when type is an enumerated data-type, otherwise returns [].

val declared_types : unit -> t list