next up previous contents
Next: General solver options Up: Reference - Command line Previous: Output options   Contents

Preprocessing options

-preset-variables <string> - Variables forced during preprocessing [default=""]
-preprocess-sequence <string>, - The preprocessing sequence
                      -P <string>   [default="{ExDc}{ExSt}{ExPr}{ExSp}{Ff}"]
-All, -All - Enable/Disable All Preprocessing Options (1/0)
-Cl <number>, -Cl <number> - Enable/Disable Clustering (1/0) [default=1]
-Co <number>, -Co <number> - Enable/Disable Cofactoring (1/0) [default=1]
-Pr <number>, -Pr <number> - Enable/Disable Pruning (1/0) [default=1]
-St <number>, -St <number> - Enable/Disable Strengthening (1/0) [default=1]
-In <number>, -In <number> - Enable/Disable Inferences (1/0) [default=1]
-Ex <number>, -Ex <number> - Enable/Disable Existential Quantification (1/0) [default=1]
-Ea <number>, -Ea <number> - Enable/Disable AND-Existential Quantification
    (1/0) [default=1]
-Es <number>, -Es <number> - Enable/Disable AND-Safe Assign + Existential
    Quantification [default=1]
-Sa <number>, -Sa <number> - Enable/Disable Searching for Safe Assignments
    (1/0) [default=1]
-Ss <number>, -Ss <number> - Enable/Disable SafeSearch (1/0) [default=1]
-Pa <number>, -Pa <number> - Enable/Disable clustering to find possible
    values to variables (1/0) [default=1]
-Dc <number>, -Dc <number> - Enable/Disable Dependent Variable
    Clustering (1/0) [default=1]
-Sp <number>, -Sp <number> - Enable/Disable Large Function Splitting (1/0) [default=0]
-Rw <number>, -Rw <number> - Enable/Disable Rewinding of BDDs back to their
    initial state (1/0) [default=1]
-Cf <number>, -Cf <number> - Enable/Disable Clearing the Function Type
    of BDDs (1/0) [default=1]
-Ff <number>, -Ff <number> - Enable/Disable Searching for the Function
    Type of BDDs (1/0) [default=1]
-P3 <number>, -P3 <number> - Enable/Disable Recreating a new set of
    prover3 BDDs (1/0) [default=1]
-max-preproc-time <number> - Set the time limit in seconds (0=no limit) [default=0]
-do-split-max-vars <number> - Threshold above which the Sp splits BDDs [default=10]
-ex-infer <number> - Enable/Disable Ex Quantification trying to safely infer
    variables before they are quantified away (1/0) [default=1]
-gaussian-elimination <char>, - Enable/Disable Gaussian Elimination in the preprocessor (1/0)
                    -gauss <char>   [default='0']


next up previous contents
Next: General solver options Up: Reference - Command line Previous: Output options   Contents
John Franco 2011-09-15