mc2 0.1 · OCaml Package

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 : t Mc2_core.Fmt.printer

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

package mc2

Linear Expressions