next up previous contents
Next: Preprocessor sequence Up: Preprocessing Previous: Preprocessing   Contents

Preprocessor options

Most of the many possible preprocessing options available to sbsat users are shown in the table below (options not listed are considered unstable). See Section 10 for an explanation of these options and when an option might pay off and when it might be a liability.

Name Default Option Formats Description
Pattern Matching yes Cl CNF see Section 10.2
Generalized Cofactoring yes Co All see Section 10.3
Branch Pruning yes Pr All see Section 10.4
Strengthening yes St All see Section 10.5
Inferences yes In All see Section 10.6
Existentially Quantify yes Ex All see Section 10.7
Cluster + ExQuant yes Ea All see Section 10.8
Cluster + ExQuant + Safe yes Es All see Section 10.9
Dependent Var. Clustering yes Dc All see Section 10.10
Rewind yes Rw All see Section 10.11
Splitter yes Sp All see Section 10.12


next up previous contents
Next: Preprocessor sequence Up: Preprocessing Previous: Preprocessing   Contents
Sean Weaver 2007-01-08