package yices2

  1. Overview
  2. Docs

Module Yices2.Type

Types

Type constructors and type testing.

val int : unit -> typ

Get built-in type for whole numbers

val bool : unit -> typ

Get built-in type for Booleans

val real : unit -> typ

Get build-in type for real numbers

val bitvector : int -> typ

Get type for bitvector of given size (in bits)

val new_scalar : int -> typ

Create new type for scalar of given cardinality

val new_uninterpreted : unit -> typ

Create new uninterpreted type

val tuple : typ array -> typ

Get tuple type of provided types

val tuple1 : typ -> typ
val tuple2 : typ -> typ -> typ
val tuple3 : typ -> typ -> typ -> typ
val func : typ array -> typ -> typ

Get function type

val func1 : typ -> typ -> typ
val func2 : typ -> typ -> typ -> typ
val func3 : typ -> typ -> typ -> typ -> typ
val parse : string -> typ

Parse type

val of_term : term -> typ

Get type of term

Type naming

val by_name : string -> typ

Get type by name

val get_name : typ -> string

Get name of type

val set_name : typ -> string -> unit

Set name of type

val clear_name : typ -> unit

Unbind type of its associated name, if any

val remove_name : string -> unit

Unbind name of its associated type, if any

Type testing

val bitsize : typ -> int

Get size of bit-vector type in bits

val is_bool : typ -> bool

Check if type is boolean

val is_int : typ -> bool

Check if type is integer

val is_real : typ -> bool

Check if type is real

val is_arithmetic : typ -> bool

Check if type is arithmetic

val is_bitvector : typ -> bool

Check if type is bit-vector

val is_tuple : typ -> bool

Check if type is tuple

val is_function : typ -> bool

Check if type is function

val is_scalar : typ -> bool

Check if type is scalar

val is_uninterpreted : typ -> bool

Check if type is uninterpreted

val is_subtype : typ -> typ -> bool

Check if first type is subtype of the second

Pretty printing

val print : ?width:int -> ?height:int -> ?offset:int -> (string -> unit) -> typ -> unit

Print type