package yices2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

Arithmetic terms

All functions return arithmetic terms except for comparators.

Only generic arithmetic constructors. For more constructors, see:

val zero : unit -> term

Zero (generic)

val add : term -> term -> term

Binary addition

val addn : term array -> term

N-ary addition

val sub : term -> term -> term

Substract

val neg : term -> term

Negate

val mul : term -> term -> term

Binary multiplication

val muln : term array -> term

N-ary multiplication

val square : term -> term

Power of two

val power : term -> int -> term

Power of fixed integer

val power_int64 : term -> int64 -> term

Power of fixed integer, up to UINT32_MAX

val div : term -> term -> term

Division

val eq : term -> term -> term

val neq : term -> term -> term

val geq : term -> term -> term

val leq : term -> term -> term

val gt : term -> term -> term

val lt : term -> term -> term

val eq0 : term -> term

val neq0 : term -> term

val geq0 : term -> term

val leq0 : term -> term

val gt0 : term -> term

val lt0 : term -> term