alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Generalize handling of partially interpreted functions

Open bclement-ocp opened this issue 2 years ago • 2 comments

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.

bclement-ocp avatar Oct 12 '23 14:10 bclement-ocp

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

bclement-ocp avatar Nov 13 '23 09:11 bclement-ocp

Note that all these functions are handled using more generic propagators elsewhere. We might still want to consider specialized constant propagators for redundancy.

bclement-ocp avatar Jul 11 '24 07:07 bclement-ocp