Module Micromega_plugin.Vect

type var = int

Variables are simply (positive) integers.

type t

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.

type vector = t

Generic functions

hash equal and compare so that Vect.t can be used as keys for Set Map and Hashtbl

val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int

Basic accessors and utility functions

val pp_gen : (Stdlib.out_channel -> var -> unit) -> Stdlib.out_channel -> t -> unit

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

val pp : Stdlib.out_channel -> t -> unit

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

val pp_smt : Stdlib.out_channel -> t -> unit

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)

val decomp_fst : t -> (var * Micromega_core_plugin.NumCompat.Q.t) * t

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

val is_constant : t -> bool

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

val null : t

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

val is_null : t -> bool

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'

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

val fresh : t -> int

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

val choose : t -> (var * Micromega_core_plugin.NumCompat.Q.t * t) option

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.

val from_list : Micromega_core_plugin.NumCompat.Q.t list -> t

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

val decr_var : int -> t -> t

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

val incr_var : int -> t -> t

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.

val normalise : t -> t

normalise v returns a vector with only integer coefficients

Linear arithmetics

val add : t -> t -> t

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

val subst : int -> t -> t -> t

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

val uminus : t -> t

uminus v

  • returns

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

Iterators

val fold : ('acc -> var -> Micromega_core_plugin.NumCompat.Q.t -> 'acc) -> 'acc -> t -> 'acc

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

val find : (var -> Micromega_core_plugin.NumCompat.Q.t -> 'c option) -> t -> 'c option

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

val for_all : (var -> Micromega_core_plugin.NumCompat.Q.t -> bool) -> t -> bool

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.

val dotproduct : t -> t -> Micromega_core_plugin.NumCompat.Q.t

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

module Bound : sig ... end