Preprocessor options can be applied in any order, as desired, and repeated
by specifying the order and repetitions on the command line in the preprocessor sequence. A preprocessor sequence consists of a list of preprocessor runs, or just runs. Each run may be followed by a
positive integer or another run. A run is a concatenation of preprocessor
options from the above table, wrapped inside matching curly braces. The
preprocessing operations specified by the options of a run are applied in
the order in which they are specified. The run may be repeated if it is
immediately followed by a positive integer . In that case the run is
repeated times or until the internal form is the same before and after
the run (that is, until reaching a fixed point). If the run is not followed
by a number then it will repeat until reaching a fixed point. For
example, the following is a run which applies existential quantification,
followed by dependent variable clustering:
The following is a preprocessor sequence with three runs, the first repeated at most 3 times, the second at most 2 times and the third at most 10 times:
Nesting of runs is allowed as in
There may be times when a preprocessor run should be run the maximum number
of times specified, instead of stopping early once reaching a fixed point.
There may also be times when only certain functions of a preprocessing run
should be considered when determining a stopping condition. All of this can
be controlled by bounding preprocessor runs, or options, inside of square
brackets. A set of square brackets should be followed by either 0 or 1 where
a 0 forces the internal form to be recognized as not altered, and a 1 forces
the internal form to be recognized as altered. For example:
This sequence will causes the preprocessing run to loop 10 times even if the internal form reachs a fixed point prior to 10 iterations. This happens because the square brackets force sbsat to consider the internal form as having been modified, even though it may not have been.
This sequence causes the preprocessing run to loop only when either `Ex' or `Dc' modify the internal form. `St' may modify the internal form, but the looping process ignores this information.