diff options
Diffstat (limited to 'src/options/quantifiers_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 |