package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 : (out_channel -> var -> unit) -> out_channel -> t -> unit

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

val pp : out_channel -> t -> unit

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

val pp_smt : 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct