diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-12 10:13:17 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-12 10:13:17 -0500 |
| commit | 411ced2c475e5ccb4c114ce2c77a39bf93d139f4 (patch) | |
| tree | 633033193faf75556ca16772efc8730f1893f04a /src/options | |
| parent | b78f4be5dac08916e0b189ba99f608a44fa08d5d (diff) | |
Add casc scripts. Improvements to qcf related to nested quantifiers and variable ordering.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 5dc6071ba..19d6885b7 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -171,6 +171,12 @@ option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm option qcfAllConflict --qcf-all-conflict bool :read-write :default false add all available conflicting instances during conflict-based instantiation +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 @@ -182,7 +188,6 @@ option qcfEagerTest --qcf-eager-test bool :default true optimization, test qcf instances eagerly 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 |