SMTArithmetic

SMT-LIB Euclidean integer arithmetic for invariant specifications. Division by zero is unspecified by SMT-LIB. The concrete evaluator chooses zero, which is only one interpretation; universal validation uses the SMT file.
Table of Contents

Types

Rational

(type)
type Rational

Functions

smt_div

SMT-LIB Euclidean integer arithmetic for invariant specifications. Division by zero is unspecified by SMT-LIB. The concrete evaluator chooses zero, which is only one interpretation; universal validation uses the SMT file.
def smt_div (x : Int) (y : Int) : Int

smt_mod

def smt_mod (x : Int) (y : Int) : Int

fractions

The source templates also contain `/` on integer-valued expressions. SMT-LIB interprets this as real division: keep an exact rational at runtime.
def fractions : Unit

rational

def rational (x : Int) : Rational

rationalAdd

def rationalAdd (x : Rational) (y : Rational) : Rational

rationalSub

def rationalSub (x : Rational) (y : Rational) : Rational

rationalMul

def rationalMul (x : Rational) (y : Rational) : Rational

rationalDiv

def rationalDiv (x : Rational) (y : Rational) : Rational

rationalFloor

def rationalFloor (x : Rational) : Int

rationalEq

def rationalEq (x : Rational) (y : Rational) : Bool

rationalLt

def rationalLt (x : Rational) (y : Rational) : Bool

rationalLe

def rationalLe (x : Rational) (y : Rational) : Bool

rationalGt

def rationalGt (x : Rational) (y : Rational) : Bool

rationalGe

def rationalGe (x : Rational) (y : Rational) : Bool