Add knowledge about floor/ceil bounds #718
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Build failure on macOS is spurious and not related to the PR. |
Halbaroth
approved these changes
Jul 2, 2023
| @@ -56,6 +56,34 @@ theory Real_of_Int extends RIA = | |||
| {i <= real_of_int(x)}. | |||
| k <= x | |||
|
|
|||
| (* floor(x) ≤ i iff x < i + 1 *) | |||
There was a problem hiding this comment.
I guess you meant floor(x) <= i implies x < i+1 instead of floor(x) <= i iff x < i+1.
Besides, I don't understand why you need to use the semantic trigger not_theory_constant here?
There was a problem hiding this comment.
floor(x) <= i iff x < i + 1 is correct, unless I am mistaken? Even though we only implement the implication.
not_theory_constant is here to avoid adding useless axioms, e.g. 3 < 4 if we know that floor(3.5) <= 3
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)
|
Note: waiting on #720 to make sure the test pass :) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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_1andreal_of_int_to_int_2).These state respectively that:
If
real_of_int(i) ≤ yholds in the reals, theni ≤ int_floor(y)holds in the integers.If
y ≤ real_of_int(i)holds in the reals, thenint_ceil(y) ≤ iholds 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) ≤ iholds in the integers,x < real_of_int(i + 1)holds in the realsIf
i ≤ int_floor(x)holds in the integers,real_of_int(i) ≤ xholds in the realsIf
int_ceil(x) ≤ iholds in the integers,x ≤ real_of_int(i)holds in the realsIf
i ≤ int_ceil(x)holds in the integers,real_of_int(i - 1) < xholds in the reals(Note that the test has "unknown" expected but it should be SAT -- this is because the ria prelude is disabled currently)