diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-30 14:06:27 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-30 14:06:34 -0500 |
| commit | 2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df (patch) | |
| tree | 6c72c3145cef49e76b1f8e5577947d441e14f938 /src/options | |
| parent | f7c6707fa38a850d6798c747b3c45ef10769fa7c (diff) | |
Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index d001684a0..04b6e6813 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -37,11 +37,6 @@ option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false aggressive split quantified formulas that lead to variable eliminations option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false split ites with dt testers as conditions -# Whether to CNF quantifier bodies -# option cnfQuant --cnf-quant bool :default false -# apply CNF conversion to quantified formulas -option nnfQuant --nnf-quant bool :default true - apply NNF conversion 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 |