# MINTS Input file structure

PRIORITY
┣━ BATCH_1
┣━ BATCH_2
┃ :
┃ :
┗━ BATCH_n
In a PRIORITY file, we define the minimization policy used by MINTS. Each line in PRIORITY is the file name of a BATCH file.
Each BATCH file defines weighted policy selection criteria of a certain priority in our hybrid selection policy scheme.
In PRIORITY, BATCH files are listed in the order of their respective priority.
BATCH
┣━ t: # of variables
┣━ RELATIVE_CRITERIA
┣━ m: # of absolute criteria
┗━ ABSOLUTE_CRITERIA
In a BATCH file, we define selection criteria of weighted policy
The first line indicates the number of test cases in the test suite. This value should be consistent across all BATCH files.
The second line, RELATIVE_CRITERIA, is the file name of the file that actually stores the of relative criteria.
The third line is the number of absolute criteria to be considered in current BATCH file.
The fourth line, ABSOLUTE_CRITERIA, is the file name of the file that stores the absolute criteria.
RELATIVE_CRITERIA
┣━ RELATIVE_CRITERION_1
┣━ RELATIVE_CRITERION_2
┃ :
┗━ RELATIVE_CRITERION_n
Each line in RELATIVE_CRITERIA represents RELATIVE_CRITERION_i, the path/file name of *i*th relative criterion for current RELATIVE_CRITERIA.
RELATIVE_CRITERION
┣━ weight of relative criterion
┗━ coefficients of criterion
RELATIVE_CRITERION stores the weights and coefficients of a relative criterion.
The first line represents the linear weight on this criterion.
The second line stores a list of coefficients of the linear criterion. Each coefficient is separated with a ASCII white space ('\ '). Given t variables, there should be t coefficients.
ABSOLUTE_CRITERIA
┣━ criterion type of criterion_1
┣━ RHS of criterion_1
┣━ coefficients of criterion_1
┣━ criterion type of criterion_2
┣━ RHS of criterion_2
┣━ coefficients of criterion_2
┃ :
┃ :
┣━ criterion type of criterion_m
┣━ RHS of criterion_m
┗━ coefficients of criterion_m
ABSOLUTE_CRITERIA stores the absolute criteria in one BATCH file
Each absolute criterion consists of three lines: The first line consists of a single character, ranging from 'a' to 'e', which represents the type of binary operator in the absolute criterion.
type:
a: >
b: >=
c: =
d: <=
e: <
The second line stores the value at the right hand side of the absolute criterion.
The third line stores a list of coefficients of the left hand side of the absolute criterion, in the same format of the second line in a RELATIVE_CRITERION file.