package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Inequalities.FMSource

Parameters

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

Signature

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