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 [*] 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 [*]
Generalized Cofactoring yes Co All see Section [*]
Branch Pruning yes Pr All see Section [*]
Strengthening yes St All see Section [*]
Inferences yes In All see Section [*]
Existentially Quantify yes Ex All see Section [*]
Cluster + ExQuant yes Ea All see Section [*]
Cluster + ExQuant + Safe yes Es All see Section [*]
Dependent Var. Clustering yes Dc All see Section [*]
Rewind yes Rw All see Section [*]
Splitter yes Sp All see Section [*]


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