Module Omega.MakeOmegaSolver

Parameters

Signature

type bigint = I.bigint
val (=?) : I.bigint -> I.bigint -> bool
val (<?) : I.bigint -> I.bigint -> bool
val (<=?) : I.bigint -> I.bigint -> bool
val (>?) : I.bigint -> I.bigint -> bool
val (>=?) : I.bigint -> I.bigint -> bool
val (+) : I.bigint -> I.bigint -> I.bigint
val (-) : I.bigint -> I.bigint -> I.bigint
val (*) : I.bigint -> I.bigint -> I.bigint
val (/) : I.bigint -> I.bigint -> I.bigint
val (mod) : I.bigint -> I.bigint -> I.bigint
val zero : I.bigint
val one : I.bigint
val two : I.bigint
val negone : I.bigint
val abs : I.bigint -> I.bigint
val string_of_bigint : I.bigint -> string
val neg : I.bigint -> I.bigint
val (<) : int -> int -> bool
val (>) : int -> int -> bool
val (<=) : int -> int -> bool
val (>=) : int -> int -> bool
val pp : int -> unit
val push : 'a -> 'a list Stdlib.ref -> unit
val pgcd : I.bigint -> I.bigint -> I.bigint
val pgcd_l : I.bigint list -> I.bigint
val floor_div : I.bigint -> I.bigint -> I.bigint
type coeff = {
c : bigint;
v : int;
}
type linear = coeff list
type eqn_kind =
| EQUA
| INEQ
| DISE
type afine = {
id : int;
kind : eqn_kind;
body : coeff list;
constant : bigint;
}
type state_action = {
st_new_eq : afine;
st_def : afine;
st_orig : afine;
st_coef : bigint;
st_var : int;
}
type action =
| DIVIDE_AND_APPROX of afine * afine * bigint * bigint
| NOT_EXACT_DIVIDE of afine * bigint
| FORGET_C of int
| EXACT_DIVIDE of afine * bigint
| SUM of int * bigint * afine * bigint * afine
| STATE of state_action
| HYP of afine
| FORGET of int * int
| FORGET_I of int * int
| CONTRADICTION of afine * afine
| NEGATE_CONTRADICT of afine * afine * bool
| MERGE_EQ of int * afine * int
| CONSTANT_NOT_NUL of int * bigint
| CONSTANT_NUL of int
| CONSTANT_NEG of int * bigint
| SPLIT_INEQ of afine * int * action list * int * action list
| WEAKEN of int * bigint
exception UNSOLVABLE
exception NO_CONTRADICTION
val display_eq : (int -> string) -> (coeff list * I.bigint) -> unit
val trace_length : action list -> I.bigint
val operator_of_eq : eqn_kind -> string
val kind_of : eqn_kind -> string
val display_system : (int -> string) -> afine list -> unit
val display_inequations : (int -> string) -> (coeff list * I.bigint) list -> unit
val sbi : I.bigint -> string
val display_action : (int -> string) -> action list -> unit
val default_print_var : int -> string
val add_event : action -> unit
val history : unit -> action list
val clear_history : unit -> unit
val nf_linear : coeff list -> coeff list
val nf : (bool * (coeff list * int)) -> bool * (coeff list * int)
val map_eq_linear : (bigint -> bigint) -> coeff list -> coeff list
val map_eq_afine : (bigint -> bigint) -> afine -> afine
val negate_eq : afine -> afine
val sum : coeff list -> coeff list -> coeff list
val sum_afine : (unit -> int) -> afine -> afine -> afine
exception FACTOR1
val chop_factor_1 : coeff list -> coeff * coeff list
exception CHOPVAR
val chop_var : int -> coeff list -> coeff * coeff list
val normalize : afine -> afine list
val eliminate_with_in : (unit -> int) -> coeff -> afine -> afine -> afine
val omega_mod : I.bigint -> I.bigint -> I.bigint
val banerjee_step : ((unit -> int) * (unit -> int) * (int -> string)) -> afine -> afine list -> afine list -> afine * afine list * afine list
val eliminate_one_equation : ((unit -> int) * (unit -> int) * (int -> string)) -> (afine * afine list * afine list) -> afine list * afine list
val banerjee : ((unit -> int) * (unit -> int) * (int -> string)) -> (afine list * afine list) -> afine list
type kind =
| INVERTED
| NORMAL
val redundancy_elimination : (unit -> int) -> afine list -> afine list * afine list
exception SOLVED_SYSTEM
val select_variable : afine list -> int
val classify : int -> afine list -> afine list * (bigint * afine) list * (I.bigint * afine) list
val product : (unit -> int) -> bool -> (bigint * afine) list -> (bigint * afine) list -> afine list
val fourier_motzkin : ((unit -> int) * 'a * (int -> string)) -> bool -> afine list -> afine list
val simplify : ((unit -> int) * (unit -> int) * (int -> string)) -> bool -> afine list -> afine list
val depend : int list -> action list -> action list -> int list * action list
val negation : (afine list * afine list) -> unit
exception FULL_SOLUTION of action list * int list
val simplify_strong : ((unit -> int) * (unit -> int) * (int -> string)) -> afine list -> action list