Module `Simplex_Q.Core_Simplex`Source

Sourcetype system = (int * t2) list * t2

Sourcetype i_result = Simplex(AltErgoLib.Numbers.Q).Core_Simplex.i_result =

Sourceexception E_max of system

Sourceexception E_unbound of system

Sourceexception E_unsat of system

Sourceval len : int Stdlib.ref

Sourceval co_opt : t2 option Stdlib.ref

Sourceval v_ghost : string

Sourceval main_simplex : bool Stdlib.ref

Sourceval reset_refs : int -> unit

Sourceval index_of_ghost : int array -> int

Sourceval line_with_min_const : ('a * t2) list -> 'a * t2

Sourceval subst : t2 -> int -> t2 -> unit

Sourceval subst_line : sbt -> (int * t2) -> unit

Sourceval subst_ctx : (int * t2) list -> sbt -> unit

Sourceexception Choose_index of int

Sourceval choose_var : (int * t2) list -> t2 -> (int Stdlib.Queue.t * 'a) -> int

Sourceval choose_eq : (int * t2) list -> t2 -> int -> int * t2

val mult_const : 
  AltErgoLib.Numbers.Q.t array ->
  (AltErgoLib.Numbers.Q.t * AltErgoLib.Numbers.Q.t) ->
  AltErgoLib.Numbers.Q.t ->
  t2

Sourceval change_pivot : int -> (int * t2) -> 'a array -> 'b -> sbt

Sourceval cpt : int Stdlib.ref

Sourceval last_cost : (AltErgoLib.Numbers.Q.t * AltErgoLib.Numbers.Q.t) Stdlib.ref

val loops : 
  'a array ->
  ('b Stdlib.Queue.t * 'c) ->
  (AltErgoLib.Numbers.Q.t * AltErgoLib.Numbers.Q.t) ->
  bool

Sourceval nbloops : int Stdlib.ref

val simplex : 
  (int * t2) list ->
  t2 ->
  int array ->
  (int Stdlib.Queue.t * 'a) ->
  'b

val delete_ghost : 
  int ->
  t2 ->
  (int * t2) list ->
  'a array ->
  'b ->
  (int * t2) list

val report_unsat : 
  int array ->
  'a ->
  (int * t2) list ->
  t2 ->
  (int * t2) list * bool

val report_max : 
  int array ->
  'a ->
  (int * t2) list ->
  t2 ->
  (int * t2) list * bool

val init_simplex : 
  (int * t2) list ->
  (int * t2) ->
  int array ->
  (int Stdlib.Queue.t * 'a) ->
  (int * t2) list * bool

Sourceval retrieve_cost : int array -> t2

val solve : 
  t2 ->
  (int * t2) list ->
  int array ->
  (int Stdlib.Queue.t * 'a) ->
  i_result

val infos_of : 
  int array ->
  int Stdlib.Queue.t ->
  t2 ->
  (int * t2) list ->
  rich_result

Sourceval result_extraction : int array -> int Stdlib.Queue.t -> i_result -> result

Sourceval core_main : t2 -> (int * t2) list -> int array -> result

package alt-ergo