Exports

The main module of XPORTA.jl provides an interface to the PORTA software. Exported types and methods use historical names from the PORTA software.

Exports

Types

• POI - The vertex representation of a polyhedra.
• IEQ - The intersecting halfspace representation of a polyhedra.

Methods

• traf - Converts a POI -> IEQ or IEQ -> POI.
• dim - Given a POI computes the dimension and constraining equalities of the POI convex hull.
• fmel - Projects the linear system of IEQ onto a subspace using fourier-motzkin elimination.
• vint - Enumerates the integral points which satisfy the linear system specified by an IEQ.
• portsort - Sorts the elements of POI and IEQ structs.
• posie - Enumerates the points and rays of a POI which satisfy the linear system of an IEQ.
• fctp - Determines if inequalities are tight or violated by elements of a POI.

The compiled PORTA binaries are accessed through PORTA_jll.jl

PORTA is a rational solver, its methods accept integer or rational valued matrices. PortaMatrix describes the union of these types to simplify notation.

PortaMatrix = Union{Matrix{Int}, Matrix{Rational{Int}}}

The vertex representation of a polyhedron. This struct is analogous to PORTA files with the .poi extension. Please refer to the PORTA General File Format docs for more information regarding the .poi file format.

Constructor arguments are optional.

POI(;
    vertices::PortaMatrix,
    rays::PortaMatrix,
    valid::PortaMatrix
)

The POI struct can be initialized with either Rational{Int} or Int valued matrices. On construction, all matrix values are standardized. By default matrix elements are Int, if one field has Rational{Int} values then the entire POI struct will be converted to type Rational{Int}.

Fields:

• conv_section - each matrix row is a vertex.
• cone_section - each matrix row is a ray.
• valid - a feasible point for the vertex representation. In the context of a POI, this field has no known use.
• dim - the dimension of vertices and rays. This field is auto-populated on construction.

A DomainError is thrown if the column dimension of rays and vertices is not equal.

The intersecting halfspace representation of a polyhedron. This struct is analogous to PORTA files with the .ieq extension. Please refer to the PORTA General File Format docs for more information refarding the .ieq file format.

Constructor arguments are optional.

IEQ(;
    inequalities :: PortaMatrix,
    equalities :: PortaMatrix,
    lower_bounds :: Matrix{Int},
    upper_bounds :: Matrix{Int},
    elimination_order :: Matrix{Int},
    valid :: PortaMatrix
)

The IEQ struct can be initialized with either Rational{Int} or Int valued matrices. On construction, all matrix values are standardized. By default matrix elements are Int, if one field has Rational{Int} values then the entire IEQ struct will be converted to type Rational{Int}.

Constructor arguments inequalities and equalities each represent a linear system of the following form.

\[\begin{bmatrix} \alpha_{1,1} & \dots & \alpha_{1,M} \\ \vdots & \ddots & \vdots \\ \alpha_{N,1} & \dots & \alpha_{N,M} \end{bmatrix}\begin{bmatrix} x_1 \\ \vdots \\ x_N \end{bmatrix} \leq \text{ or } = \begin{bmatrix} \beta_1 \\ \vdots \\ \beta_N \end{bmatrix}\]

Each matrix row represents a separate linear in/equality. The right-hand-side of each in/equality is described by a vector $\vec{\alpha}_i$ with length $M$ and the right-hand-side is described with a single value $\beta_i$, where $i\in{1,...,N}$.

In the .ieq format, columnn vector $\vec{\beta}$ is concatenated to the right side of the $\alpha$ matrix. In the IEQ struct, inequalities and equalities both have the following form.

\[\begin{bmatrix} \alpha_{1,1} & \dots & \alpha_{1,M} & \beta_1 \\ \vdots & \ddots & \vdots & \vdots \\ \alpha_{N,1} & \dots & \alpha_{N,M} & \beta_N \end{bmatrix}\]

IEQ Fields:

• inequalities: each matrix row is a linear inequality, the first M elements indexed 1:(end-1) are α and the last element indexed end is β.
• equalities: each matrix row is linear equality, the first M elements indexed 1:(end-1) are α and the last element indexed end is β.
• lower_bounds: a row vector which specifies the lower bound on each individual parameter. Used for enumerating integral points with vint.
• upper_bounds: a row vector which specifies the upper bound on each individual parameter. Used for enumerating integral points with vint.
• valid: a feasible point for the linear system.
• dim: the dimension of in/equalities, upper/lower bounds, etc. This field is auto-populated on construction.

A DomainError is thrown if the column dimension of fields is not equal.

The traf method computes an IEQ struct given a POI struct,

traf( poi::POI; kwargs... ) :: IEQ{Rational{Int}}

or computes the POI struct from the IEQ struct.

traf(ieq::IEQ; kwargs... ) :: POI{Rational{Int}}

When converting an IEQ -> POI the valid field of the IEQ must be populated if the origin is not a feasible point of the linear system.

kwargs is shorthand for the following keyword arguments:

• dir::String = "./" - The directory in which to write files.
• filename::String = "traf_tmp"- The name of produced files.
• cleanup::Bool = true - If true, created files are removed after computation.
• opt_flag::String = "" - Optional flags to pass the traf method of the xporta binary.
• verbose::Bool = false- If true, PORTA will print progress to STDOUT.

The following excerpt from the PORTA documentation lists valid optional flags and their behavior:

    -p     Unbuffered redirection of terminal messages into  file filename_'.prt'

    -o     Use  a heuristic to eliminate that variable  next,  for which the number of new
           inequalities is minimal (local criterion). If this option is set, inequalities
           which are  recognized  to  be facet-inducing  for the finite linear system
           are printed into a  file as soon as they are identified.

    -c     Fourier-Motzkin elimination without using the rule  of Chernikov

    -s     Appends a statistical  part  to  each  line  with  the number  of coefficients

    -v     Printing a   table in the  output file which indicates strong validity

    -l     Use  a  special  integer arithmetic allowing the integers to have arbitrary
           lengths. This arithmetic is not as efficient as the system's integer
           arithmetic with respect to time and storage requirements.

           Note: Output values which exceed the 32-bit integer storage size
           are written in hexadecimal format (hex). Such hexadecimal format
           can not be reread as input.

For more details regarding traf please refer to the PORTA traf documentation.

dim( poi::POI; kwargs... ) :: Dict{String, Union{ Int, IEQ{Rational{Int}} } }

Given a POI computes the minimal dimension and constraining equalities for the convex hull of the POI. The returned dictionary has the form

Dict(
    "dim" => <integer number of dimensions>,
    "ieq" => <IEQ struct w/ constraining equalities>
)

kwargs specifies keyword args:

• dir::String = "./" - The directory in which to write files.
• filename::String = "dim_tmp"- The name of produced files.
• cleanup::Bool = true - If true, created files are removed after computation.
• verbose::Bool = false- If true, PORTA will print progress to STDOUT.

For more details regarding dim please refer to the PORTA dim documentation.

fmel( ieq::IEQ; kwargs... ) :: IEQ{Rational{Int}}

Projects the linear system of IEQ onto a subspace using fourier-motzkin elimination. The projected linear system is returned in an IEQ. Note that redundant inequalities may be present in the returned IEQ.

The elimination_order field of the IEQ must be populated and of length dim. A 0 value indicates a parameter which will not be eliminated and 1,2,... specifies the order in which the parameters will be eliminated. Performance may change based on the order of elimination.

kwargs specifies keyword args:

• dir::String = "./" - The directory in which to write files.
• filename::String = "fmel_tmp"- The name of produced files.
• opt_flag::String = "" - optional flags for the fmel subroutine.
• cleanup::Bool = true - If true, created files are removed after computation.
• verbose::Bool = false- If true, PORTA will print progress to STDOUT.

A DomainError is thrown if the elimination_order field is not of length dim. A DomainError is thrown if the opt_flag argument is not a substring of "-pcl" or its permutations.

The valid options for the opt_flag:

-p    Unbuffered redirection of the terminal messages into the file
      input_fname_with_suffix_'prt'

-c    Generation of new inequalities without the rule of Chernikov.

-l    Use  a  special  integer arithmetic allowing the integers to have arbitrary
      lengths.  This arithmetic is not as efficient as the system's integer
      arithmetic with respect to time and storage requirements.

      Note: Output values which exceed the 32-bit integer storage  size  are written
      in hexadecimal format (hex). Such hexadecimal format can not be reread as input.

For more details regarding fmel please refer to the PORTA fmel documentation.

vint( ieq::IEQ; kwargs... ) :: POI{Rational{Int}}

Enumerates all integral (integer) points which satisfy the linear system specified by the IEQ and bounds specified by upper_bounds and lower_bounds fields of the IEQ. These points may lie on the facets, vertices, or interior of the polytope specified by IEQ. If no equalities or inequalities are specified, all integral points within the bounds will be enumerated.

kwargs specifes the keyword args:

• dir::String = "./" - The directory to which files are written.
• filename::String = "vint_tmp"- The name of produced files.
• cleanup::Bool = true - If true, created files are removed after computation.
• verbose::Bool = false- If true, PORTA will print progress to STDOUT.

A DomainError is thrown if the IEQ does not contain upper/lower bounds or if upper/lower bounds contain more than one row.

For more details regarding vint() please refer to the PORTA vint documentation.

portsort( ieq::IEQ; kwargs... ) :: IEQ{Rational{Int}}

Sorts the inequalities and equalities of the provided IEQ.

portsort( poi::POI; kwargs... ) :: POI{Rational{Int}}

Sorts the vertices and rays of the provided POI.

Sorting is performed in the following hierarchy:

1. Right-hand-side of in/equalities from high to low.
2. Scale factors from low to high.
3. Lexicographical order.

kwargs is shorthand for the keyword arguments:

• dir::String = "./" - The directory in which to write files.
• filename::String = "portsort_tmp"- The name of produced files.
• cleanup::Bool = true - If true, created files are removed after computation.
• verbose::Bool = false- If true, PORTA will print progress to STDOUT.

For more details regarding portsort please refer to the PORTA portsort documentation.

posie( ieq::IEQ, poi::POI; kwargs... ) :: POI{Rational{Int}}

Enumerates the points and rays in the POI which satisfy the linear system of the IEQ. A POI containing the valid points and rays is returned.

kwargs is shorthand for the following keyword arguments:

• dir :: String = "./" - The directory to which files are written.
• filename :: String = "posie_tmp"- The name of produced files.
• cleanup :: Bool = true - If true, created files are removed after computation.
• verbose :: Bool = false- If true, PORTA will print progress to STDOUT.

For more details regarding posie() please refer to the PORTA posie documentation.

fctp( inequalities::PortaMatrix, poi::POI; kwargs... ) :: Dict{ String, Dict{Int, POI{Rational{Int}}} }

For the provided inequalities, determines which ones tightly bound the polytope specified by the input POI and which inequalities are violated by the input POI. Tight bounds are labeled "valid" and violations are labeled "invalid". In each case the points which saturate or violate the inequalities are returned in a poi. Inequalities which are loose bounds are not returned.

Each row of the inequalities input corresponds to a distinct inequality in the form specified by the IEQ.inequalites field.

The output has a nested dictionary structure:

Dict(
    "valid" => Dict(
        id => saturating_poi,  # points/rays which saturate inequalities[id]
        ...
    ),
    "invalid" => Dict(
        id => violating_poi,   # points/rays which violate inequalities[id]
        ...
    )
)

where ineq_id corresponds to the row index of the input inequalities. The "valid" and "invalid" dictionaries may include zero or more elements.

kwargs is shorthand for the following keyword arguments:

• dir::String = "./" - The directory to which files are written.
• filename::String = "fctp_tmp"- The name of produced files.
• cleanup::Bool = true - If true, created files are removed after computation.
• verbose::Bool = false- If true, PORTA will print progress to STDOUT.

For more details regarding fctp() please refer to the PORTA fctp documentation.