FM (alt-ergo-lib.AltErgoLib.Inequalities.FM)

Parameters

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

type p = P.t

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

module MP : Stdlib.Map.S with type key = p

type nonrec t = p 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

val reset_age_cpt : unit -> unit

Resets the age counter to zero