Module Mc2_lra__.Linexp
Linear Expressions
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 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 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 flatten : f:(Mc2_core.term -> t option) -> t -> t
flatten f e
traverses all terms, and if they are themselves mapped into expressions byf
, 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 tof
module Infix : sig ... end