projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c430628) | patch
Add new kinds required for higher-order. (#1083)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Sep 2017 02:08:28 +0000 (21:08 -0500)
committerAina Niemetz <aina.niemetz@gmail.com>
Thu, 14 Sep 2017 02:08:28 +0000 (19:08 -0700)
commitdaf1d6bf1176834fa697dd57c6fe28142e715585
tree89c385fa7b5b280531b90a70e505d3c34c8a27c3tree
parentc4306288347e043091628b63797f9f54b0359a7ccommit | diff
Add new kinds required for higher-order. (#1083)

This consists of a binary apply symbol HO_APPLY that returns the result of applying its first argument to its second argument. Update the UF rewriter to ensure that non-standard APPLY_UF applications are rewritten into curried applications of HO_APPLY.
src/theory/uf/kinds diff | blob | history
src/theory/uf/theory_uf_rewriter.h diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history