diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-06 08:20:23 +0100 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-06 00:20:23 -0700 |
| commit | a3a3c6f56ef1593076379e39ec478013d8a01ab8 (patch) | |
| tree | 10e6a51dfdaeacd340be27eae425ad128f5e0052 /src/api/cvc4cpp.cpp | |
| parent | ceba90a89f878cda01067042ca9a0dfee555b7cd (diff) | |
sygusComp2018: simplify beta reduction in uf rewriter. (#2106)
This is PR 8/18 from the sygus comp 2018 branch (https://github.com/ajreynol/CVC4/tree/sygusComp2018-2).
I am not sure how it is possible in any circumstance that the complication in the comment I am deleting would ever happen, without doing something very strange. I think it is referring to some sort of inter-dependence between macro expansion + beta-reductions. This should not concern the rewriter. Here is the commit that introduced it: bdaa304.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
0 files changed, 0 insertions, 0 deletions