Module Funarith_zarith__.Simplex_zarith.Make

Parameters

V : Funarith__Simplex.VAR

Signature

module Q : sig ... end
type var = V.t
module Var_map : sig ... end
type t = Funarith__Simplex.Make(Funarith_zarith__.Rat_zarith)(V).t
type cert = Funarith__Simplex.Make(Funarith_zarith__.Rat_zarith)(V).cert = {
cert_var : var;
cert_expr : (Q.t * var) list;
}
type res = Funarith__Simplex.Make(Funarith_zarith__.Rat_zarith)(V).res =
| Solution of Q.t Var_map.t
| Unsatisfiable of cert
val create : unit ‑> t
val copy : t ‑> t
val add_eq : t ‑> (var * (Q.t * var) list) ‑> unit
val add_bounds : t ‑> ?⁠strict_lower:bool ‑> ?⁠strict_upper:bool ‑> (var * Q.t * Q.t) ‑> unit
val add_lower_bound : t ‑> ?⁠strict:bool ‑> var ‑> Q.t ‑> unit
val add_upper_bound : t ‑> ?⁠strict:bool ‑> var ‑> Q.t ‑> unit
val solve : t ‑> res
val check_cert : t ‑> cert ‑> [ `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t | `Ok ]
val pp_cert : cert CCFormat.printer
val pp_full_state : t CCFormat.printer
val check_invariants : t ‑> bool
val matrix_pp_width : int Pervasives.ref