projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3cb6e28) | patch
Support AND/OR definitions in lambda to array rewriting (#4615)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Mon, 15 Jun 2020 21:00:08 +0000 (18:00 -0300)
committerGitHub <noreply@github.com>
Mon, 15 Jun 2020 21:00:08 +0000 (18:00 -0300)
commit545bdeebf38e7212dc161567ec16ddc6bd36d708
treef35c4ffdca509abf3a1f8581fcc9a08d330fb367tree
parent3cb6e28c13a2c3ff42d68d5b5025e4b56cb2054bcommit | diff
Support AND/OR definitions in lambda to array rewriting (#4615)

This makes the conversion between lambdas and arrays, done in the theory builtin rewriter and used in higher-order model construction, robust to function definitions in terms of AND/OR.

This also improves tracing and makes a few parts of the code adhere to code guidelines.
src/theory/builtin/theory_builtin_rewriter.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history