package yices2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Term substitution
Term info and type testing
Term naming
Parsing and 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

val constant : typ -> int -> term

Scalar of given type and index.

val new_uninterpreted : typ -> term

Creates new uninterpreted of type.

module Bool : sig ... end

Boolean terms

module Fun : sig ... end

Function application, update and lambda terms

module Tuple : sig ... end

Tuples

module Arith : sig ... end

Arithmetic terms

module Int : sig ... end

Integer terms

module Ratio : sig ... end

Rational terms

module Poly : sig ... end

Integer polynomial terms

module RatioPoly : sig ... end

Rational polynomial terms

module Bitvector : sig ... end

Bit-vectors

Term substitution

val subst : vars:term array -> repls:term array -> term -> term

val subst_array : vars:term array -> repls:term array -> term array -> unit

Term info and type testing

val type_of : term -> typ

val is_bool : term -> bool

val is_int : term -> bool

val is_real : term -> bool

val is_arithmetic : term -> bool

val is_bitvector : term -> bool

val is_tuple : term -> bool

val is_function : term -> bool

val is_scalar : term -> bool

val bitsize : term -> int

val is_ground : term -> bool

Term naming

val by_name : string -> term

val get_name : term -> string

val set_name : term -> string -> unit

val clear_name : term -> unit

val remove_name : string -> unit

Parsing and pretty printing

val parse : string -> term

Parse a term in Yices format

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

Print a term