Commits on Jul 3, 2023

1. Add knowledge about floor/ceil bounds …

   In the RIA prelude, we have axioms with semantic triggers to propagate
   bounds on reals to bounds on integers using `real_of_int`
   (`real_of_int_to_int_1` and `real_of_int_to_int_2`).
   
   These state respectively that:
   
    - If `real_of_int(i) ≤ y` holds in the reals, then `i ≤ int_floor(y)`
      holds in the integers.
   
    - If `y ≤ real_of_int(i)` holds in the reals, then `int_ceil(y) ≤ i`
      holds in the integers.
   
   This patch adds the corresponding propagations from bounds on integers
   to bounds on reals. More precisely it adds the propagations:
   
    - If `int_floor(x) ≤ i` holds in the integers, `x < real_of_int(i + 1)`
      holds in the reals
   
    - If `i ≤ int_floor(x)` holds in the integers, `real_of_int(i) ≤ x`
      holds in the reals
   
    - If `int_ceil(x) ≤ i` holds in the integers, `x ≤ real_of_int(i)`
      holds in the reals
   
    - If `i ≤ int_ceil(x)` holds in the integers, `real_of_int(i - 1) < x`
      holds in the reals
   
   (Note that the test has "unknown" expected but it should be SAT -- this
   is because the ria prelude is disabled currently)

   

   bclement-ocp committed Jul 3, 2023
   Configuration menu

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

   Copy the full SHA

   fbedd93 View commit details

   Browse the repository at this point in the history