package mc2

  1. Overview
  2. Docs

Linear Expressions

type t

Linear expression with rational coefficients and rational-typed terms

type num = Q.t
val equal : t -> t -> bool
val hash : t -> int
val pp_no_paren : t Mc2_core.Fmt.printer
val empty : t

Empty linear expression

val zero : t

Empty linear expression

alias for empty

val is_const : t -> bool

true if the expressions is constant

val is_zero : t -> bool

true if the expressions is constant and equal to zero

val add : t -> t -> t

Sum of linear expressions

val diff : t -> t -> t

Sum of linear expressions

Diff of linear expressions

val const : num -> t
val as_singleton : t -> (num * Mc2_core.term) option

no constant, and exactly one term?

val mem_term : Mc2_core.term -> t -> bool
val add_term : num -> Mc2_core.term -> t -> t
val remove_term : Mc2_core.term -> t -> t
val get_term : Mc2_core.term -> t -> num option
val find_term_exn : Mc2_core.term -> t -> num

Find value for this term, or Not_found

val singleton : num -> Mc2_core.term -> t
val singleton1 : Mc2_core.term -> t
val singleton_term : t -> Mc2_core.term

asserts the given LE is exatly of the form (1 * x) and returns x *

val neg : t -> t

Invert sign

val mult : num -> t -> t

Product by constant

val div : t -> num -> t

div e n is e/n.

  • raises Division_by_zero

    if n=0

val simplify : t -> t

if e is n·x op 0, then rewrite into sign(n)·x op 0 *

val flatten : f:(Mc2_core.term -> t option) -> t -> t

flatten f e traverses all terms, and if they are themselves mapped into expressions by f, replaces them by the corresponding expr

val terms : t -> Mc2_core.term Iter.t
val terms_l : t -> Mc2_core.term list
val as_const : t -> num option
val eval : f:(Mc2_core.term -> num option) -> t -> (num * Mc2_core.term list) option

eval e evaluates the expression if all subterms (returned in a list) have a value according to f

module Infix : sig ... end