wmpy.core.polytope.Polytope

class Polytope(expressions, parser)

Bases: object

Internal class for convex H-polytopes.

inequalities

list of wmpy.core.Inequality

variables

list of pysmt real variables

env

the pysmt environment

inner_box

the largest enclosed axis-aligned box (optional)

outer_box

the smallest enclosing axis-aligned box (optional)

Default constructor for a H-polytope defined on an ordered list of variables (the continuous integration domain).

Parameters:

• expressions (Collection[FNode]) – list of linear inequalities in pysmt format

• parser (PolynomialParser) – a polynomial parser instance

Methods

to_numpy	Converts the polytope to a tuple of numpy arrays.
to_pysmt	Returns a pysmt formula (FNode) encoding the polytope.

Attributes

inner_box
outer_box

to_numpy()

Converts the polytope to a tuple of numpy arrays.

Return type:

tuple[ndarray, ndarray, ndarray]

Returns:

Three numpy arrays A, B, S encoding the polytope

A x {<=/<} B

S is a {0,1} array indicating which rows/entries in A, B correspond to strict inequalities.

to_pysmt()

Returns a pysmt formula (FNode) encoding the polytope.

Return type:

FNode