package mc2

  1. Overview
  2. Docs
package mc2
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
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