Encode floating point operations as uninterpreted functions#1095
Encode floating point operations as uninterpreted functions#1095can-leh-emmtrix wants to merge 7 commits into
Conversation
|
(not forgotten, but review delayed for a few weeks, sorry. PLDI deadline approaching) |
| if (get_uf_float()) | ||
| doesApproximation("uf-float"); |
There was a problem hiding this comment.
I am not sure what the best way to handle doesApproximation is with this approach. One option would be to call it in fm_poison in instr.cpp, however we don't have direct access to the UFs anymore. From what I can tell from the source code, the second argument to doesApproximation needs to be the APP node of the UF. However we do not have access to that anymore at this point. It may be possible to obtain the UFs by traversing the AST though. Another option might be to register a callback function with expr.h which is called for each created UF.
|
Thanks for letting me know and no worries about the delay. |
|
@can-leh-emmtrix I have a local branch that catches these changes up to 28bb8c6, but wanted to run it by you before I push anything to your branch in case you have other work on your end that hasn't been broadcast yet. Certainly #1095 (comment) still hasn't been resolved, but these changes overall seem pretty reasonable to me. |
3 participants
Approach based on modifying expr.cpp. Please let me know what you think.
Previous PR: #1057