package alt-ergo-lib

  1. Overview
  2. Docs

Parameters

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

Signature

module P = P
module MP : Map.S with type key = P.t
type 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;
}
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 : 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