alt-ergo
alt-ergo copied to clipboard
Generalize handling of partially interpreted functions
Following #869 we should move most of the partially interpreted functions (float, div, mod, ...) to the Delayed implementation so that they work with substitutions.
Note that * is a tricky one — need to check that the implementation in #869 behaves properly for AC symbols.
Note that most of the functions mentioned above are handled by the FPA preludes. Notable exceptions are the BV functions bvand and bvor.
- For the arith related stuff, would be in favor of waiting for #917 first. If we ship #917 in 2.6.0, there is nothing to do (doing something specific for those functions would even slightly hurt performance I guess because of duplicated work)
- For the bv stuff, need to see how it would fit with #903 but might we worth still
Note that all these functions are handled using more generic propagators elsewhere. We might still want to consider specialized constant propagators for redundancy.