alt-ergo 2.6.0 · OCaml Package

exception Trivial

exception Inconsistent

exception Pivot of int * int * AltErgoLib.Numbers.Q.t

val array_is_null : AltErgoLib.Numbers.Q.t array -> bool

val coefs_have_mem_sign : ('a * AltErgoLib.Numbers.Q.t) array -> int option

val create : 
  int ->
  ((int * AltErgoLib.Numbers.Q.t) list
   * (int * AltErgoLib.Numbers.Q.t) list
   * AltErgoLib.Numbers.Q.t) ->
  'a ->
  t1

val create_strict : int -> (int * AltErgoLib.Numbers.Q.t) list -> 'a -> t1

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

val pivot_in_p : int -> t1 -> (int * int) * t1

val subst_in_p : t1 -> ((int * int) * t1) -> unit

val z_subst_in_p : t1 -> int -> unit

val normalize_poly : 
  t1 ->
  ((int * int) * t1) AltErgoLib.Vec.t ->
  int AltErgoLib.Vec.t ->
  unit

val normalize_sbt : 
  ((int * int) * t1) AltErgoLib.Vec.t ->
  int AltErgoLib.Vec.t ->
  int list * ((int * int) * t1) list

val sbt : ((int * int) * t1) AltErgoLib.Vec.t

val zsbt : int AltErgoLib.Vec.t

val solve_zero_arr : 
  int AltErgoLib.Vec.t ->
  bool array ->
  (int * AltErgoLib.Numbers.Q.t) array ->
  unit

val solve_zero_list : 
  int AltErgoLib.Vec.t ->
  bool array ->
  (int * 'a) list ->
  unit

val substs_from_equalities : 
  ('a
   * ((int * AltErgoLib.Numbers.Q.t) list
      * (int * AltErgoLib.Numbers.Q.t) list
      * AltErgoLib.Numbers.Q.t))
    list ->
  'b ->
  int ->
  int list * ((int * int) * t1) list

val make_problem : 
  (int * AltErgoLib.Numbers.Q.t) list ->
  ('a
   * ((int * AltErgoLib.Numbers.Q.t) list
      * (int * AltErgoLib.Numbers.Q.t) list
      * AltErgoLib.Numbers.Q.t))
    list ->
  (int * AltErgoLib.Numbers.Q.t) list ->
  int ->
  t1 * ((int * int) * t1) list * int list

val compact_poly_2 : 
  t1 ->
  (int, 'a) H.t ->
  int ->
  (int, 'b) H.t ->
  t2 * (int, int) H.t

val compact_poly : t1 -> (int, 'a) H.t -> int -> (int, 'b) H.t -> t2

val compact_problem : 
  t1 ->
  ((int * int) * t1) list ->
  int ->
  int ->
  int list ->
  t2 * (int * t2) list * int array

val norm_main : 
  (int * AltErgoLib.Numbers.Q.t) list ->
  ('a
   * ((int * AltErgoLib.Numbers.Q.t) list
      * (int * AltErgoLib.Numbers.Q.t) list
      * AltErgoLib.Numbers.Q.t))
    list ->
  (int * AltErgoLib.Numbers.Q.t) list ->
  int ->
  t2 * (int * t2) list * int array

package alt-ergo