Module Micromega_plugin.Vect
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
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 vectorv
over the channelo
val pp : Stdlib.out_channel -> t -> unit
pp o v
prints the representation of the vectorv
over the channelo
val pp_smt : Stdlib.out_channel -> t -> unit
pp_smt o v
prints the representation of the vectorv
over the channelo
using SMTLIB conventions
val variables : t -> Micromega_plugin.Mutils.ISet.t
variables v
returns the set of variables with non-zero coefficients
val get_cst : t -> NumCompat.Q.t
get_cst v
returns c i.e. the coefficient of the variable zero
val decomp_cst : t -> NumCompat.Q.t * t
decomp_cst v
returns the pair (c,a1.x1+...+an.xn)
val decomp_at : int -> t -> NumCompat.Q.t * t
decomp_cst v
returns the pair (ai, ai+1.xi+...+an.xn)
val decomp_fst : t -> (var * NumCompat.Q.t) * t
val cst : NumCompat.Q.t -> t
cst c
returns the vector v=c+0.x1+...+0.xn
val is_constant : t -> bool
is_constant v
holds ifv
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 whetherv
is thenull
vector i.eequal v null
val get : var -> t -> NumCompat.Q.t
get xi v
returns the coefficient ai of the variablexi
.get
is also defined for the variable 0
val set : var -> NumCompat.Q.t -> t -> t
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'
val update : var -> (NumCompat.Q.t -> NumCompat.Q.t) -> t -> t
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 * NumCompat.Q.t * t) option
choose v
decomposes a vectorv
depending on whether it isnull
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 : NumCompat.Q.t list -> t
from_list l
returns the vector c+a1.x1...an.xn from the list of coefficientl=c;a1;...;an
val to_list : t -> NumCompat.Q.t list
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
val decr_var : int -> t -> t
decr_var i v
decrements the variables of the vectorv
by the amounti
. Beware, it is only defined if all the variables of v are greater than i
val gcd : t -> NumCompat.Z.t
gcd v
returns gcd(num(c),num(a1),...,num(an)) where num extracts the numerator of a rational value.
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
val mul : NumCompat.Q.t -> t -> t
mul a v
is vector multiplication of vectorv
by a scalara
.- returns
a.v = a.c+a.a1.x1+...+a.an.xn
val mul_add : NumCompat.Q.t -> t -> NumCompat.Q.t -> t -> t
mul_add c1 v1 c2 v2
returns the linear combination c1.v1+c2.v2
val div : NumCompat.Q.t -> t -> t
div c1 v1
returns the mutiplication by the inverse of c1 i.e (1/c1).v1
Iterators
val fold : ('acc -> var -> NumCompat.Q.t -> 'acc) -> 'acc -> t -> 'acc
fold f acc v
returns f (f (f acc 0 c ) x1 a1 ) ... xn an
val fold_error : ('acc -> var -> NumCompat.Q.t -> 'acc option) -> 'acc -> t -> 'acc option
fold_error f acc v
is the same asfold (fun acc x i -> match acc with None -> None | Some acc' -> f acc' x i) (Some acc) v
but with early exit...
val find : (var -> NumCompat.Q.t -> 'c option) -> t -> 'c option
find f v
returns the firstf xi ai
such thatf xi ai <> None
. If no such xi ai exists, it returns None
val for_all : (var -> NumCompat.Q.t -> bool) -> t -> bool
for_all p v
returns /\_>=0 (f xi ai)
val exists2 : (NumCompat.Q.t -> NumCompat.Q.t -> bool) -> t -> t -> (var * NumCompat.Q.t * NumCompat.Q.t) option
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 -> NumCompat.Q.t
dotproduct v1 v2
is the dot product of v1 and v2.
val map : (var -> NumCompat.Q.t -> 'a) -> t -> 'a list
val abs_min_elt : t -> (var * NumCompat.Q.t) option
val partition : (var -> NumCompat.Q.t -> bool) -> t -> t * t
module Bound : sig ... end