Module Mc2_lra.LESource

Linear Expressions

Sourcetype t

Linear expression with rational coefficients and rational-typed terms

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

Empty linear expression

Sourceval zero : t

Empty linear expression

alias for empty

Sourceval is_const : t -> bool

true if the expressions is constant

Sourceval is_zero : t -> bool

true if the expressions is constant and equal to zero

Sourceval add : t -> t -> t

Sum of linear expressions

Sourceval diff : t -> t -> t

Sum of linear expressions

Diff of linear expressions

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

no constant, and exactly one term?

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

Find value for this term, or Not_found

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

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

Sourceval neg : t -> t

Invert sign

Sourceval mult : num -> t -> t

Product by constant

Sourceval div : t -> num -> t

div e n is e/n.

Sourceval simplify : t -> t

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

Sourceval 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

Sourceval terms : t -> Mc2_core.term Iter.t
Sourceval terms_l : t -> Mc2_core.term list
Sourceval as_const : t -> num option
Sourceval 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

Sourcemodule Infix : sig ... end