Module Polyhedron

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.