The qCORAL input file format

The input file format is quite simple. Here is an example: 

 
;; This is a comment!
 
:Variables:
1 NORMAL -100 100 0 33.3
2 NORMAL -100 100 0 33.3
 
:Constraints:
 
DLT(ADD(DVAR(ID_1),DVAR(ID_2)),DCONST(50.0));DGE(DVAR(ID_1),DVAR(ID_2))

The first section, ":Variables:", contain the input variables used in the constraints plus their characteristics. Each line define a single input variable. The input format is as follows: 

 
$ID $VARTYPE $LOWER_BOUND $UPPER_BOUND $[VARTYPE_PARAMS]
  • $ID is an unique integer identifier for the variable.
  • $VARTYPE is the distribution of the variable. Allowed values are NORMAL,EXPONENTIAL,BINOMIAL,POISSON,GEOMETRIC,UNIFORM_INT and UNIFORM_REAL.
  • $LOWER_BOUND and $UPPER_BOUND are, respectively, the lower and upper bound of the variable.
  • $[VARTYPE_PARAMS] is a list of the distribution parameters for the variable. In our example above, both variables are NORMAL, so we have two extra parameters: the mean (0) and the standard deviation (33.3). Other types have the following parameters:
    1. EXPONENTIAL: $MEAN
    2. BINOMIAL: $NUMBER_OF_TRIALS $PROBABILITY
    3. POISSON: $LAMBDA
    4. GEOMETRIC: $PROBABILITY
    5. UNIFORM_INT/REAL: none

For more details on how the parsing of variables is done, see the method coral.counters.DistributionAwareQCoral.parseVariable(...)

The second section, ":Constraints:", contain the constraints to be analyzed by qCORAL. The complete grammar of the input language for symbolic expressions can be found in docs/QCORAL_INPUT_LANGUAGE.txt, or here.

One example expression: 

 
DLT(SIN_(MUL(DVAR(ID_1),DVAR(ID_2))),DCONST(0.0));DGT(COS_(MUL(DVAR(ID_1),DCONST(2.0))),DCONST(0.25))
// pretty-prints as: sin(id_1 * id_2) < 0 && cos(2x) > 0.25

You can also define a "truncated" domain for a single constraint. Example: 

 
[{-1,1},{-2,2}]#DEQ(DVAR(V_2),DVAR(V_1))
// in this case, the domain of V1 is [-1,1], and V_2 is [-2,2]

In this specific constraint, V1 and V2 are handled as variables following a truncated distribution (see this link for more information).