Module Smt_sig.S.Type

module Type: sig .. end

Typing


type t = Hstring.t 

The type of types in the solver

Builtin types

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)

Declaring new types

val declare : Hstring.t -> Hstring.t list -> unit
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