Module Inequalities.FM

Parameters

module P : Polynome.T with type r = Shostak.Combine.r

Signature

module P = P
module MP : Stdlib.Map.S with type key = P.t
type t = {
ple0 : P.t;
is_le : bool;
dep : (Numbers.Q.t * P.t * bool) AltErgoLib.Util.MI.t;
expl : Explanation.t;
age : Numbers.Z.t;
}
module MINEQS : sig ... end
val current_age : unit -> Numbers.Z.t
val incr_age : unit -> unit
val create_ineq : P.t -> P.t -> bool -> Expr.t option -> Explanation.t -> t
val print_inequation : Stdlib.Format.formatter -> t -> unit
val fourierMotzkin : ( 'are_eq -> 'acc -> P.r option -> t list -> 'acc ) -> 'are_eq -> 'acc -> MINEQS.mp -> 'acc
val fmSimplex : ( 'are_eq -> 'acc -> P.r option -> t list -> 'acc ) -> 'are_eq -> 'acc -> MINEQS.mp -> 'acc
val available : ( 'are_eq -> 'acc -> P.r option -> t list -> 'acc ) -> 'are_eq -> 'acc -> MINEQS.mp -> 'acc