projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2a5a65f) | patch
Change UF ho to ppRewrite instead of expand definition (#5499)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 Nov 2020 17:49:59 +0000 (11:49 -0600)
committerGitHub <noreply@github.com>
Mon, 23 Nov 2020 17:49:59 +0000 (11:49 -0600)
commita6c001e078767a2de6f36a2fa1333b98e39a6ec8
tree4d3685f39e6e2c0160a7bbcbfa0e07852721db8atree
parent2a5a65feac6ce270732f0a4d672e5838f5cd673acommit | diff
Change UF ho to ppRewrite instead of expand definition (#5499)

UF uses expandDefinitions to convert fully applied HO_APPLY to APPLY_UF. The more appropriate place to do this is in Theory::ppRewrite.
src/theory/uf/ho_extension.cpp diff | blob | history
src/theory/uf/ho_extension.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
test/regress/regress1/ho/NUM925^1.p diff | blob | history
test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 diff | blob | history
test/regress/regress2/ho/involved_parsing_ALG248^3.p diff | blob | history