Command line options

Here are listed the options to qCoral. On the command line, the values for options are specified in the form '--long=value' or '--long value'. The value is mandatory for all options except booleans. Booleans are set to true if no value is specified.

Model Counting

  • --mcSeed num

Seed to be used by the RNG. num is a long "longs", separated by commas. Default value is 99076487270974053l.

  • --mcMaxSamples num

Global sampling budget. num is a long. Default is 100000. Obs: In previous versions, this parameter defined the number of samples taken for every subproblem/partition.

  • --cachePavingResults

Cache RealPaver paving results. Default is false. Enabled by default when using the iterative algorithm (run_qcoral.sh/coral.counters.refactoring.Runner).

  • --mcPartitionAndCache

Partition/cache constraints sent to the selected model counter. Default is false. Enabled by default when using the iterative algorithm (run_qcoral.sh/coral.counters.refactoring.Runner).

  • --mcCallIntSolPartition

Call interval solver for each partition. Default is false. Enabled by default when using the iterative algorithm (run_qcoral.sh/coral.counters.refactoring.Runner).

Iterative sampling

  • --mcIterativeImprovement

Uses the iterative approach described in our FSE'15 paper to estimate probabilities. Default is false.

  • --mcTargetVariance double

qCORAL will stop when the global variance is smaller than double. Default is 1E-16.

  • --mcInitialPartitionBudget num

Number of samples taken in the bootstrap stage. Default is 1000.

  • --mcSamplesPerIncrement num

Number of samples taken in each iteration after the bootstrap. Default is 10000.

  • --mcAllocateBudgetProportionally

Allocate samples to each subproblem proportionally to their derivative. Default is false.

  • --mcProportionalBoxSampleAllocation

Allocate samples to each box proportionally to their respective variance. Default is false.

  • --mcNonRankedIterativeImprovement

Don't rank the partitions and improve all subproblems uniformly. Default is false.

  • --mcDumbRankingHeuristic

Allocate samples to each subproblem proportionally to their variance. Default is false.

Interval Solver

  • --realPaverLocation path

Path to realPaver executable.

  • --intervalSolverPrecision precision

Precision used by the interval solver (1E-precision). precision must be an integer. Default is 3.

  • --intervalSolverTimeout timeout

Max time for the interval solver to answer the query (in ms). timeout must be an integer. Default is 2000.

Deprecated Options

These options may be used by previous implementations of qCORAL (which still may be accessible in the source code - see scripts/runDWCounter.sh and coral.counters.DistributionAwareQCoral, but are not relevant in the current version.

  • --mcMinSamplesPerBox num

Minimum number of sampling points to be used for each box. Default is 0.

  • --mcDistributeSamples

Set distinct amounts of samples for each box based on volume. Default is false.

  • --mcSkipPaving

Don't use an interval solver before running the model counter. Default is false.

  • --mcMergeBoxes

Merge all boxes returned by the interval solver. Default is false.

  • --normalize

Normalize results. Default is true.

  • --mcDisableCache

Disable caching. Default is false.

  • --mcNumExecutions numExecs

Number of times to run the model counter. Default is 1.

  • --mcSeedFile file

File with seeds to use for reseeding the rng at the end of each run - make sure to have enough seeds!. Default is "".

  • --mcResetRngEachSimulation

Reset rng at the end of each simulation. Default is true.

  • --mathematicaGA

Use global adaptive integration with Mathematica (if false, use monte carlo). Default is false.

  • --mcUseMathematica

Use Mathematica to compute the volume. Default is false.

  • --mcDiscretizationRegions num

Number of regions when using discretization. Default is 6.

  • --mcDiscretize

Estimate using discretization. Creates N^n_vars new constraints for each original constraint. Default is false.

  • --mcDiscretizeWithMateusApproach

Estimate using discretization. Splits the domain of each subproblem in N^n_vars regions. Faster than mcDiscretize. Default is false.

  • --rangeLO lo

Default lower bound of input variables. lo must be an integer. Default is -10000.

  • --rangeHI hi

Default upper bound of input variables. hi must be an integer. Default is 10000.

  • --fixed100Domain

Makes the domain of all variables = [[-100,100]]. Default is false.

  • --domainFile

Read the domain of the variables from the input file. Default is false.

After each constraint, qCoral will read the domain for the variables of that constraint. The domain must be in the format [{$LO,$HI},...]. Domains will be attributed to the variables following the order of their IDs. Example: 

DLE(DCONST(45),DVAR(r_1));DLE(DVAR(r_1),DCONST(49));DLE(DCONST(80),DVAR(r_2));DLE(DVAR(r_2),DCONST(160));
[{45.0, 90.0}, {80.0, 200.0}]

In this case, the domain of variable $r_1 is [45,90], and the domain of $r_2 is [80,200].