Inequalities (p.alt-ergo-lib.2.4.0.doc.alt-ergo-lib.AltErgoLib.Inequalities)

Sourcemodule type S = sig ... end

module FM
  (P : Polynome.T with type r = Shostak.Combine.r) : 
  S with module P = P

Sourcemodule type Container_SIG = sig ... end

Sourceval get_current : unit -> (module Container_SIG)

returns the current activated 'inequalities reasoner'. The default value is the Fourier-Motzkin module. When the selected reasoner is an external plugin, the first call of this function will attemp to dynamically load it *

Sourceval set_current : (module Container_SIG) -> unit

sets a new 'inequalities reasoner'. This function is intended to be used by dynamically loaded plugins *