package yices2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Type naming
Type testing
Pretty printing

package yices2

yices2
- Yices2
  - Context
    
    Config
    
    Params
  - Error
  - Experimental
  - Model
  - Term
    
    Arith
    
    Bitvector
    
    Bool
    
    Fun
    
    Int
    
    Poly
    
    Ratio
    
    RatioPoly
    
    Tuple
  - Type

Legend:
Library
Module
Module type
Parameter
Class
Class 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