diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-04 18:54:45 -0500 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-04 16:54:45 -0700 |
| commit | 01c540202392fad77ee32c65e065257890c8d07e (patch) | |
| tree | 476d5e0bc2a1cac056a7904e381750b9b4f50f8e /src/options | |
| parent | f2bd626d6337ca4df70c0bf541d7d9bec4ef5be5 (diff) | |
Ho quant util (#1119)
Quantifiers utilities for higher-order.
This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.
Also adds required options and a minor utility for implementing app completion.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 44fbc4ee7..2e765ce6b 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -368,6 +368,16 @@ option quantAntiSkolem --quant-anti-skolem bool :read-write :default false option quantEqualityEngine --quant-ee bool :default false maintain congrunce closure over universal equalities +### higher-order options + +option hoMatching --ho-matching bool :default true + do higher-order matching algorithm for triggers with variable operators +option hoMatchingVarArgPriority --ho-matching-var-priority bool :default true + give priority to variable arguments over constant arguments + +option hoMergeTermDb --ho-merge-term-db bool :default true + merge term indices modulo equality + ### proof options option trackInstLemmas --track-inst-lemmas bool :read-write :default false |