XPORTA.XPORTA
— ModuleThe 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 aPOI
->IEQ
orIEQ
->POI
.dim
- Given aPOI
computes the dimension and constraining equalities of thePOI
convex hull.fmel
- Projects the linear system ofIEQ
onto a subspace using fourier-motzkin elimination.vint
- Enumerates the integral points which satisfy the linear system specified by anIEQ
.portsort
- Sorts the elements ofPOI
andIEQ
structs.posie
- Enumerates the points and rays of aPOI
which satisfy the linear system of anIEQ
.fctp
- Determines if inequalities are tight or violated by elements of aPOI
.
The compiled PORTA binaries are accessed through PORTA_jll.jl
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.
XPORTA.PortaMatrix
— TypePORTA 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.IEQ
— TypeThe 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 indexed1:(end-1)
are α and the last element indexedend
is β.equalities
: each matrix row is linear equality, the first M elements indexed1:(end-1)
are α and the last element indexedend
is β.lower_bounds
: a row vector which specifies the lower bound on each individual parameter. Used for enumerating integral points withvint
.upper_bounds
: a row vector which specifies the upper bound on each individual parameter. Used for enumerating integral points withvint
.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.
XPORTA.POI
— TypeThe 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 aPOI
, 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.
XPORTA.dim
— Methoddim( 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
- Iftrue
, created files are removed after computation.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
For more details regarding dim
please refer to the PORTA dim documentation.
XPORTA.fctp
— Methodfctp( 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
- Iftrue
, created files are removed after computation.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
For more details regarding fctp()
please refer to the PORTA fctp documentation.
XPORTA.fmel
— Methodfmel( 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 thefmel
subroutine.cleanup::Bool = true
- Iftrue
, created files are removed after computation.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
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.
XPORTA.iespo
— Methodiespo( ieq::IEQ, poi::POI; kwargs...) :: IEQ{Rational{Int}}
Enumerates the valid equations and inequalities of the IEQ
which satisfy the points and rays in the POI
. An IEQ
containing valid inequalities and equations is returned.
This method does not work as described by the PORTA iespo documentation. Invalid in/equalities are not filtered out. However, the strong validity check does work.
To run the strong validity check, use arguments cleanup=false
and opt_flag="-v"
. With these arguments, iespo()
will print a table to the output .ieq
file which can manually be read/parsed.
In a future update, a parser may be written for the strong validity table or the PORTA source code may be update to properly execute the in/equality filtering.
kwargs
is shorthand for the following keyword arguments:
dir::String = "./"
- The directory to which files are written.filename::String = "iespo_tmp"
- The name of produced files.strong_validity::Bool = false
- Prints the strong validity table to the outputIEQ
, (requires manual parsing).cleanup::Bool = true
- Iftrue
, created files are removed after computation.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
For more details regarding iespo()
please refer to the PORTA iespo documentation.
XPORTA.make_porta_tmp
— Functionmake_porta_tmp( dir::String = "./") :: String
Creates the porta_tmp/
directory in directory dir
and returns the porta_tmp
path.
XPORTA.portsort
— Methodportsort( 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:
- Right-hand-side of in/equalities from high to low.
- Scale factors from low to high.
- 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
- Iftrue
, created files are removed after computation.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
For more details regarding portsort
please refer to the PORTA portsort documentation.
XPORTA.posie
— Methodposie( 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
- Iftrue
, created files are removed after computation.verbose :: Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
For more details regarding posie()
please refer to the PORTA posie documentation.
XPORTA.read_ieq
— Methodread_ieq( filepath::String ) :: IEQ{Rational{Int}}
Constructs an IEQ
struct by parsing the provided .ieq
file. A DomainError
is thrown if argument filepath
does not end with the .ieq
extension.
XPORTA.read_poi
— Methodread_poi( filepath::String ) :: POI{Rational{Int}}
Constructs a POI
struct by parsing the provided .poi
file. A DomainError
is thrown if argument filepath
does not end with the .poi
extension.
XPORTA.rm_porta_tmp
— Functionrm_porta_tmp( dir::String = "./")
Recursively removes porta_tmp/
from directory dir
.
This method uses rm("<dir/>porta_tmp/", force=true, recursive=true)
. Make sure not to delete important data.
XPORTA.run_valid
— Methodrun_valid( method_flag::String, args::Array{String,1}; verbose::Bool=false ) :: String
This method is intended for advanced use of the valid
binary. User knowledge of flags and arguments is required for successful execution. Users must explicitly handle file IO for the valid
binary.
Runs the valid
binary through PORTA_jll
and returns a string containing STDOUT
. The method_flag
specifies which valid
subroutine to call.
Valid options for method_flag
are:
"-C"
runs thefctp
subroutine"-I"
runs theiespo
subroutine"-P"
runs theposie
subroutine"-V"
runs thevint
subroutine
The args
parameter is uniquely specified by method_flag
, for more information regarding methods and arguments see the valid
documentation.
If verbose=true
the valid
binary prints to STDOUT
.
XPORTA.run_xporta
— Methodrun_xporta( method_flag::String, args::Array{String,1}; verbose::Bool = false) :: String
This method is intended for advanced use of the xporta binary. User knowledge of flags and arguments is required for successful execution. Furthermore, users must explicitly handle file IO for the xporta
binary.
Runs the xporta
binary through PORTA_jll
and returns a string containing STDOUT
. The method_flag
argument specifies which xporta
subroutine to call.
Valid options for method_flag
are:
"-D"
runs thedim
subroutine"-F"
runs thefmel
subroutine"-S"
runs theportsort
subroutine"-T"
runs thetraf
subroutine
The args
parameter is uniquely specified by method_flag
, for more information regarding methods and arguments see the xporta
documentation.
If verbose=true
the xporta
prints to STDOUT
.
XPORTA.traf
— MethodThe 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
- Iftrue
, created files are removed after computation.opt_flag::String = ""
- Optional flags to pass thetraf
method of the xporta binary.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
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.
XPORTA.vint
— Methodvint( 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
- Iftrue
, created files are removed after computation.verbose::Bool = false
- Iftrue
, PORTA will print progress toSTDOUT
.
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.
XPORTA.write_ieq
— Methodwrite_ieq( filename::String, ieq::IEQ; dir::String="./") :: String
Writes an .ieq
file, dir/filename.ieq
, from the provided IEQ
struct. If filename
does not explicitly contain the .ieq
extension, it will be added automatically. The method returns the complete file path for the created file, dir/filename.ieq
.
XPORTA.write_poi
— Methodwrite_poi(filename::String, poi::POI; dir::String="./") :: String
Writes a .poi
file, dir/filename.poi
, from the provided POI
. If filename
does not explicitly have the .poi
extension, it will automatically be added. The method returns the complete file path for the created file, dir/filename.poi
.
XPORTA.@matrepelem
— MacroThe representation rep
contain the elements elem
inside a vector in the field field
.