fix(Shostak): names must return false for X.is_constant
#1031
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
The `X.is_constant` function is intended to determine whether a semantic value is a constant value (it is documented to be equivalent to having an empty `X.leaves`). This invariant is relied upon by the code for delayed computation in `Rel_utils` that it was introduced for in OCamlPro#869. While the change only makes the delayed computation code less efficient, it makes the `X.is_constant` function worthless for its original purpose in planned patches. The invariant was broken in OCamlPro#925 which causes `X.is_constant` to now consider some terms (specifically, names, i.e. uninterpreted constants) as constants, which is incorrect for the intended and documented purpose of `X.is_constant` (uninterpreted constants have different values in different context, they are thus not constant values). This patch restores the original semantic of `X.is_constant` with improved documentation, and removes the assertion introduced in OCamlPro#925 which seems to be the only incorrect use.
Halbaroth
approved these changes
Jan 23, 2024
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.
The
X.is_constantfunction is intended to determine whether a semantic value is a constant value (it is documented to be equivalent to having an emptyX.leaves). This invariant is relied upon by the code for delayed computation inRel_utilsthat it was introduced for in #869. While the change only makes the delayed computation code less efficient, it makes theX.is_constantfunction worthless for its original purpose in planned patches.The invariant was broken in #925 which causes
X.is_constantto now consider some terms (specifically, names, i.e. uninterpreted constants) as constants, which is incorrect for the intended and documented purpose ofX.is_constant(uninterpreted constants have different values in different context, they are thus not constant values).This patch restores the original semantic of
X.is_constantwith improved documentation, and removes the assertion introduced in #925 which seems to be the only incorrect use.