Commits on Oct 12, 2023

1. Support delayed computation of partially interpreted functions …

   This patch lifts the existing implementation in `IntervalCalculus` for
   delayed computation of the `pow` function (by "delayed computation" I
   mean that we remember `pow` terms with uninterpreted arguments and
   evaluate them once their arguments become interpreted). This is a
   generic way of integrating functions that we know how to compute but not
   necessarily how to reason about.
   
   The patch is concerned about lifting the implementation for `pow` to a
   generic one and adds `int2bv` and `bv2nat` as delayed functions (with
   corresponding tests), but does not (yet) use it for other partially
   interpreted functions from the arithmetic theory (e.g. `Modulo`,
   `Real_of_int`, and the like); this will be done separately.
   
   The implementation is placed in a new `Rel_utils` module that is
   intended to provide scaffolding for generic behavior (such as delayed
   computation) that can be useful for all relations. An alternative would
   be to support delayed computation in a fully generic way in the
   `Relation` module directly; providing the feature in `Rel_utils` is
   (slightly) simpler and keeps things more decoupled; the implementation
   can easily be moved to `Relation` later if we want to.
   
   Fixes OCamlPro#801

   

   bclement-ocp committed Oct 12, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 797cdf6
   • Browse repository at this point

   Copy the full SHA

   797cdf6 View commit details

   Browse the repository at this point in the history