diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e12a7d70f..60f5a171d 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -31,6 +31,9 @@ option varElimQuant --var-elim-quant bool :default false option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas +option clauseSplit --clause-split bool :default false + apply clause splitting to quantified formulas + # Whether to pre-skolemize quantifier bodies. # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to # forall x. P( x ) => f( S( x ) ) = x |