package yices2

  1. Overview
  2. Docs
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