package yices2

  1. Overview
  2. Docs

Arithmetic terms

All functions return arithmetic terms except for comparators.

Constructors

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

Comparators

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

Comparators to zero

val eq0 : term -> term
val neq0 : term -> term
val geq0 : term -> term
val leq0 : term -> term
val gt0 : term -> term
val lt0 : term -> term
OCaml

Innovation. Community. Security.