projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 54ed571) | patch
Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 21 Sep 2017 00:32:46 +0000 (19:32 -0500)
committerGitHub <noreply@github.com>
Thu, 21 Sep 2017 00:32:46 +0000 (19:32 -0500)
commit75ccf2b4ad3dbcb1a0edfc336db35b45719a09f5
tree4c3a58acddc52c51f7e2a78e5442e990555247cdtree
parent54ed57102bbd35241c68d128f88bf2b93dd236cfcommit | 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
src/options/uf_options diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history