diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-25 13:50:45 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-25 13:50:45 -0500 |
| commit | dce53c4de6dd7482d9784388cc61753352f241d8 (patch) | |
| tree | d1df5306b02e61cde0cc6d6280fb7cd8efb16494 /src/options/quantifiers_options | |
| parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) | |
Options for counterexample guided instantiation.
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 85355c037..cb4f292c1 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -301,6 +301,10 @@ option cbqiMidpoint --cbqi-midpoint bool :default false choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation option cbqiNopt --cbqi-nopt bool :default true non-optimal bounds for counterexample-based quantifier instantiation +option cbqiLitDepend --cbqi-lit-dep bool :default false + dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation +option cbqiInnermost --cbqi-innermost bool :default false + only process innermost quantified formulas in counterexample-based quantifier instantiation ### local theory extensions options |