Variables are simply (positive) integers.

The type of vectors or equivalently linear expressions. The current implementation is using association lists. A list (0,c),(x1,ai),...,(xn,an) represents the linear expression c + a1.xn + ... an.xn where ai are rational constants and xi are variables.

Note that the variable 0 has a special meaning and represent a constant. Moreover, the representation is spare and variables with a zero coefficient are not represented.

pp_gen pp_var o v prints the representation of the vector v over the channel o

pp o v prints the representation of the vector v over the channel o

pp_smt o v prints the representation of the vector v over the channel o using SMTLIB conventions

variables v returns the set of variables with non-zero coefficients

get_cst v returns c i.e. the coefficient of the variable zero

decomp_cst v returns the pair (c,a1.x1+...+an.xn)

decomp_at xi v returns the pair (ai, ai+1.xi+...+an.xn)

cst c returns the vector v=c+0.x1+...+0.xn

is_constant v holds if v is a constant vector i.e. v=c+0.x1+...+0.xn

null is the empty vector i.e. 0+0.x1+...+0.xn

is_null v returns whether v is the null vector i.e equal v null

get xi v returns the coefficient ai of the variable xi. get is also defined for the variable 0

set xi ai' v returns the vector c+a1.x1+...ai'.xi+...+an.xn i.e. the coefficient of the variable xi is set to ai'

mkvar xi returns 1.xi

update xi f v returns c+a1.x1+...+f(ai).xi+...+an.xn

fresh v return the fresh variable with index 1+ max (variables v)

choose v decomposes a vector v depending on whether it is null or not.

• returns

  None if v is null

• returns

  Some(x,n,r) where v = r + n.x x is the smallest variable with non-zero coefficient n <> 0.

from_list l returns the vector c+a1.x1...an.xn from the list of coefficient l=c;a1;...;an

to_list v returns the list of all coefficient of the vector v i.e. c;a1;...;an The list representation is (obviously) not sparsed and therefore certain ai may be 0

decr_var i v decrements the variables of the vector v by the amount i. Beware, it is only defined if all the variables of v are greater than i

incr_var i v increments the variables of the vector v by the amount i.

gcd v returns gcd(num(c),num(a1),...,num(an)) where num extracts the numerator of a rational value.

normalise v returns a vector with only integer coefficients

add v1 v2 is vector addition.

• parameter v1

  is of the form c +a1.x1 +...+an.xn

• parameter v2

  is of the form c'+a1'.x1 +...+an'.xn

• returns

  c1+c1'+ (a1+a1').x1 + ... + (an+an').xn

mul a v is vector multiplication of vector v by a scalar a.

• returns

  a.v = a.c+a.a1.x1+...+a.an.xn

mul_add c1 v1 c2 v2 returns the linear combination c1.v1+c2.v2

subst x v v' replaces x by v in vector v'

div c1 v1 returns the mutiplication by the inverse of c1 i.e (1/c1).v1

uminus v

• returns

  -v the opposite vector of v i.e. (-1).v

fold f acc v returns f (f (f acc 0 c ) x1 a1 ) ... xn an

fold_error f acc v is the same as fold (fun acc x i -> match acc with None -> None | Some acc' -> f acc' x i) (Some acc) v but with early exit...

find f v returns the first f xi ai such that f xi ai <> None. If no such xi ai exists, it returns None

for_all p v returns /\_>=0 (f xi ai)

exists2 p v v' returns Some(xi,ai,ai') if p(xi,ai,ai') holds and ai,ai' <> 0. It returns None if no such pair of coefficient exists.

dotproduct v1 v2 is the dot product of v1 and v2.