next up previous contents
Next: Preprocessor command Up: Preprocessing Previous: Preprocessor options   Contents


Preprocessor sequence

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 $R$. In that case the run is repeated $R$ 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:


{ExDc}


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:


{ExDc}3{ExSt}2{ExPr}10


Nesting of runs is allowed as in


{{StDc{Pr{ExDc}3}{Ex}10}Ex}

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:


{[ExDc]1}10


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.


{Ex[St]0Dc}


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.


next up previous contents
Next: Preprocessor command Up: Preprocessing Previous: Preprocessor options   Contents
John Franco 2011-09-15