Exports

XPORTA.XPORTA — Module

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

  • POI - Type, The vertex representation of a polyhedra.
  • IEQ - Type, The intersecting halfspace representation of a polyhedra.
  • traf - Method, Converts a POI -> IEQ or IEQ -> POI.

The compiled PORTA binaries are accessed through PORTA_jll.jl

File IO and Temp Files

The PORTA binaries use files to read and write data. XPORTA.jl writes the input to a temp file, runs the PORTA binary, and reads the output from a file created by PORTA.

By default, all intermediate files are written to a porta_tmp/ directory. At the end of computation, data is returned to the user and porta_tmp/ is deleted. This functionality is intended to prevent the local filesystem from becoming polluted with temp files.

Please note that in the case of failure porta_tmp/ may not get deleted.

Types

XPORTA.PortaMatrix — Constant

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}}}
XPORTA.POI — Type

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.
  • 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.

XPORTA.IEQ — Type

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: each matrix row is a lower bound for enumerating integral points with vint.
  • upper_bounds: each matrix row is an upper bound 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.

Methods

XPORTA.traf — Function

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

traf( poi::POI; kwargs... ) :: IEQ

or computes the POI struct from the IEQ struct.

traf(ieq::IEQ; kwargs... ) :: POI

where kwargs is shorthand for the following keyword arguments:

  • cleanup :: Bool = true - Remove created files after computation.
  • dir :: String = "./" - The directory in which to write files.
  • filename :: String = "traf_tmp"- The name of produced files
  • 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.
Temp Files

By default files created by the PORTA binaries are deleted. When performing longer computations with PORTA, it may be desirable to keep intermediate files. Passing the argument cleanup = false will cause the traf method to write all files to directroy dir.

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.