Module Libabsolute.Expr

This module defines the numerical language and some basic operations over it

type binop =
  1. | ADD
  2. | SUB
  3. | MUL
  4. | DIV
  5. | POW

binary arithmetic operators

type t =
  1. | Funcall of string * t list
  2. | Neg of t
  3. | Binary of binop * t * t
  4. | Var of string
  5. | Cst of Q.t

numeric expressions (function call, unary negation, binary operations, variables and constants)

type 'a annot =
  1. | AFuncall of string * 'a annot_t list
  2. | ANeg of 'a annot_t
  3. | ABinary of binop * 'a annot_t * 'a annot_t
  4. | AVar of string
  5. | ACst of Q.t

generic type for annotated expressions

and 'a annot_t = 'a annot * 'a
val compare : t -> t -> int

Errors

exception Division_by_zero

raised by evaluation functions

exception Non_integer_exposant

raised by evaluation functions

Constructors

Constants

val one : t
val zero : t
val two : t

Expression Constructors

val of_int : int -> t

builds an expression from an integer

val of_float : float -> t

builds an expression from an float

val of_mpqf : Q.t -> t

builds an expression from an Mpqf.t

val var : string -> t

variables constructor

val add : t -> t -> t

addition

val sub : t -> t -> t

substraction

val mul : t -> t -> t

multiplication

val div : t -> t -> t

multiplication

val pow : t -> t -> t

given an expression e builds the expresspion for e1^e2

val square : t -> t

given an expression e builds the expresspion for e*e

Predicates

val has_variable : t -> bool

checks if an expression contains a variable

val is_linear : t -> bool

checks if an expression is linear:

  • is_linear (2*x + 4*y) = true
  • is_linear (2*x*z + y) = false

Operations

val op_to_fun : binop -> Q.t -> Q.t -> Q.t

convert a binary operator to a rational function. The resulting function may raise Division_by_zero or Non_integer_exposant when the binary operator is respectivelly DIV or POW

val constant_propagation : t -> t

bottom-up partial evaluation of expressions when operations involving only constants are involved:

  • constant_propagation (x+2) = (x+2)
  • constant_propagation (2+2)*x = (4*x)
val collect_vars : t -> int Tools.VarMap.t

Returns all the variables appearing in an expression as a map where to each variable is associated the integer number of its occurences

val replace : ?simplify:bool -> t -> string -> t -> t

replace expr var value builds a new expression identical to expr where all the occurences of the variable var are replaced by the expression value.

if simplify is true (default behaviour), a round of constant propagation is applied on the resulting expression

val fix_var : ?simplify:bool -> t -> string -> Q.t -> t

fix_var expr var cst builds a new expression identical to expr where all the occurences of the variable var are replaced by the constant cst

if simplify is true (default behaviour), a round of constant propagation is applied on the resulting expression

val eval : t -> Instance.t -> Q.t

Evaluates the expression at the given point.

  • raises [Invalid_arg]

    if a division by zero occurs of if an exponentitation by a non integer exposant is made.

val deannot : 'a annot_t -> t

removes annotations from an annotated expression

Printing

val pp_var : Stdlib.Format.formatter -> string -> unit

variables printing

val pp_binop : Stdlib.Format.formatter -> binop -> unit

binary operators printing

val print : Stdlib.Format.formatter -> t -> unit

expression printer

val to_string : t -> string

Conversion to a string

module Operators : sig ... end

Classic infix operators are redefined on t.