Module Funarith_zarith__Simplex_zarith.Make_full

Parameters

L : sig ... end
V : Funarith__Simplex.VAR_GEN

Signature

module Q : sig ... end
type var = V.t
module Var_map : sig ... end
type t = Funarith__Simplex.Make_full(Funarith_zarith__.Rat_zarith)(V)(L).t
type cert = Funarith__Simplex.Make_full(Funarith_zarith__.Rat_zarith)(V)(L).cert = {
cert_var : var;
cert_expr : (Q.t * var) list;
}
type res = Funarith__Simplex.Make_full(Funarith_zarith__.Rat_zarith)(V)(L).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
module L : sig ... end
type op = [
| `Eq
| `Geq
| `Gt
| `Leq
| `Lt
]
type 'a constr = 'a L.Constr.t constraint 'a = [< op ]
module Problem : sig ... end
val add_constr : t ‑> [< op ] constr ‑> unit
val add_problem : t ‑> [< op ] Problem.t ‑> unit