alt-ergo 2.6.0 · OCaml Package

type system = (int * t2) list * t2

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

exception E_max of system

exception E_unbound of system

exception E_unsat of system

val len : int ref

val co_opt : t2 option ref

val v_ghost : string

val main_simplex : bool ref

val reset_refs : int -> unit

val index_of_ghost : int array -> int

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

val subst : t2 -> int -> t2 -> unit

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

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

exception Choose_index of int

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

val 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

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

val cpt : int ref

val last_cost : (AltErgoLib.Numbers.Q.t * AltErgoLib.Numbers.Q.t) ref

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

val nbloops : int ref

val simplex : (int * t2) list -> t2 -> int array -> (int 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 Queue.t * 'a) ->
  (int * t2) list * bool

val retrieve_cost : int array -> t2

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

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

val result_extraction : int array -> int Queue.t -> i_result -> result

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

package alt-ergo