diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-20 19:32:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-20 19:32:46 -0500 |
| commit | 75ccf2b4ad3dbcb1a0edfc336db35b45719a09f5 (patch) | |
| tree | 4c3a58acddc52c51f7e2a78e5442e990555247cd /src/options | |
| parent | 54ed57102bbd35241c68d128f88bf2b93dd236cf (diff) | |
Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)
* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms.
* Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent.
* Remove unused NodeList
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/uf_options | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/options/uf_options b/src/options/uf_options index cbac04b18..7e1cbdb17 100644 --- a/src/options/uf_options +++ b/src/options/uf_options @@ -41,4 +41,9 @@ option ufssFairness --uf-ss-fair bool :default true option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false group monotone sorts when enforcing fairness for finite model finding +option ufHo --uf-ho bool :read-write :default false + enable support for higher-order reasoning +option ufHoExt --uf-ho-ext bool :read-write :default true + apply extensionality on function symbols + endmodule |