module Polyhedron: sig
.. end
Convex polyhedra.
type
t
module V: Linear.QQVector
val enum : t ->
[ `EqZero of V.t | `LeqZero of V.t | `LtZero of V.t ] BatEnum.t
val pp : 'a CoordinateSystem.t -> Format.formatter -> t -> unit
val conjoin : t -> t -> t
val top : t
val of_formula : ?admit:bool -> 'a CoordinateSystem.t -> 'a Syntax.formula -> t
Convert formula that contains only conjunction and linear equalities and
disequalities into a polyhedron.
val to_formula : 'a CoordinateSystem.t -> t -> 'a Syntax.formula
Inverse of of_formula
val to_apron : 'a CoordinateSystem.t ->
'a SrkApron.Env.t ->
'abs Apron.Manager.t -> t -> ('a, 'abs) SrkApron.property
val mem : (int -> QQ.t) -> t -> bool
Test whether a point, representing as a map from symbols to rationals, is
inside a polyhedron.
val of_implicant : ?admit:bool ->
'a CoordinateSystem.t -> 'a Syntax.formula list -> t
Convert a conjunction of atomic formulas (as returned by
Interpretation.select_implicant
) to a polyhedron.
val implicant_of : 'a CoordinateSystem.t -> t -> 'a Syntax.formula list
Convert a polyhedron to a conjunction of atomic formulas (as returned by
Interpretation.select_implicant
).
val local_project : (int -> QQ.t) -> int list -> t -> t
Model-guided projection of a polyhedron. Given a point m within a
polyhedron p and a set of dimension xs, compute a polyhedron q such that
m|_xs is within q, and q is a subset of p|_xs (using |_xs to denote
projection of dimensions xs)
val project : int list -> t -> t
Fourier-Motzkin elimination.
val try_fourier_motzkin : 'a CoordinateSystem.t ->
(Syntax.symbol -> bool) -> t -> t
Apply Fourier-Motzkin elimination to the subset of symbols that appear
linearly. Symbols that do not appear linearly are not projected.