diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-20 16:02:14 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-20 16:02:22 -0500 |
| commit | 374fc2396a4f4338ade7ea0fb958e26c9e3bb982 (patch) | |
| tree | 841f9b1727ded2a82e15389c279e23e9ab024280 /src/options | |
| parent | e61e9853656d0a0d1c16cb095b9173dc2f732b21 (diff) | |
More refactoring of cbqi. Add a few regressions. Add option for qcf.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 3fc589b5c..3269b7574 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -182,8 +182,6 @@ option qcfNestedConflict --qcf-nested-conflict bool :default false consider conflicts for nested quantifiers option qcfVoExp --qcf-vo-exp bool :default false qcf experimental variable ordering - - option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -193,8 +191,11 @@ option instPropagate --inst-prop bool :read-write :default false option qcfEagerTest --qcf-eager-test bool :default true optimization, test qcf instances eagerly +option qcfEagerCheckRd --qcf-eager-check-rd bool :default true + optimization, eagerly check relevant domain of matched position option qcfSkipRd --qcf-skip-rd bool :default false optimization, skip instances based on possibly irrelevant portions of quantified formulas + ### rewrite rules options option quantRewriteRules --rewrite-rules bool :default false |