Merge CTerm #4621
Closed
Merge CTerm #4621
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
Stevengre
commented
Sep 3, 2024
| consequent = mlAnd(t.constraints) if t.constraints else TRUE | ||
| new_constraints.append(mlImplies(antecedent, consequent)) | ||
|
|
||
| return CTerm(new_config, new_constraints) |
There was a problem hiding this comment.
Main implementation of merge_cterms.
- Return
Noneif the configuration structures are different. - Replace cell content into a new free variable if there are free variables or different between them.
- The constraints will be
CELL_NAME == SUBST /\ ... -> source.constraint /\ ...
Stevengre
commented
Sep 3, 2024
Stevengre
commented
Sep 3, 2024
tothtamas28
approved these changes
Sep 3, 2024
ehildenb
reviewed
Sep 3, 2024
Stevengre
added a commit
that referenced
this pull request
Sep 4, 2024
ehildenb
reviewed
Sep 4, 2024
pyk/src/pyk/cterm/cterm.py
Outdated
| new_constraints: list[KInner] = [] | ||
| for new_subst, t in [(new_t1_subst, t1), (new_t2_subst, t2)]: | ||
| if new_subst: | ||
| antecedent = mlAnd([mlEquals(KVariable(cell), new_subst[cell]) for cell in new_subst]) |
There was a problem hiding this comment.
I think this can be simplified as well? See https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/kast/inner.py#L753
Suggested change
| antecedent = mlAnd([mlEquals(KVariable(cell), new_subst[cell]) for cell in new_subst]) | |
| antecedent = new_subst.ml_pred |
There was a problem hiding this comment.
Thank you for point it out! I've changed that!
ehildenb
reviewed
Sep 4, 2024
ehildenb
reviewed
Sep 5, 2024
Comment on lines
+261
to
+298
| def merge_cterms(t1: CTerm, t2: CTerm) -> CTerm | None: | ||
| """Return a `CTerm` which is the merge of the two input `CTerm` instances. | ||
|
|
||
| Args: | ||
| t1: First `CTerm` to merge. | ||
| t2: Second `CTerm` to merge. | ||
|
|
||
| Returns: | ||
| A `CTerm` which is the merge of the two input `CTerm` instances. | ||
| """ | ||
| # check all cells in t1 and t1, if they are the same, keep them, otherwise, create a new free variable for them | ||
| t1_config, t1_subst = split_config_from(t1.config) | ||
| t2_config, t2_subst = split_config_from(t2.config) | ||
|
|
||
| if t1_config != t2_config: | ||
| # cannot merge two configurations with different structure | ||
| return None | ||
|
|
||
| new_subst = Subst({}) | ||
| new_t1_subst = Subst({}) | ||
| new_t2_subst = Subst({}) | ||
|
|
||
| for cell in t1_subst: | ||
| if t1_subst[cell] == t2_subst[cell]: | ||
| # keep the cell if it is the same | ||
| new_subst = new_subst * Subst({cell: t1_subst[cell]}) | ||
| else: | ||
| # create a new free variable for the cell | ||
| new_t1_subst = new_t1_subst * Subst({cell: t1_subst[cell]}) | ||
| new_t2_subst = new_t2_subst * Subst({cell: t2_subst[cell]}) | ||
| new_config = new_subst(t1_config) | ||
|
|
||
| new_constraints: list[KInner] = [] | ||
| for new_subst, t in [(new_t1_subst, t1), (new_t2_subst, t2)]: | ||
| if new_subst: | ||
| new_constraints.append(mlImplies(new_subst.ml_pred, t.constraint)) | ||
|
|
||
| return CTerm(new_config, new_constraints) |
There was a problem hiding this comment.
This seems like a less powerful version of CTerm.anti_unify. Basically, instead of merge_cterms(cterm1, cterm2), you can do:
cterm, csubst1, csubst2 = cterm1.anti_unify(cterm2)
You'll have that csubst1(cterm) == cterm1, and csubst2(cterm) == cterm2, and you can use the data returned there to compute what you need for the merged nodes.
There was a problem hiding this comment.
Here are some tests of antiunification:
k/pyk/src/tests/integration/proof/test_imp.py
Line 1296 in 42e0354
k/pyk/src/tests/integration/proof/test_imp.py
Line 1247 in 42e0354
There was a problem hiding this comment.
Thank you! I looked at the code and tests of anti_unify and feel that anti_unify can indeed be directly used. It's just that the generated csubst I can't use. Perhaps I can close this PR.
Stevengre
added a commit
that referenced
this pull request
Sep 9, 2024
rv-jenkins
pushed a commit
that referenced
this pull request
Sep 9, 2024
~Blocked on: #4631 ~Blocked on: #4630 ~Blocked on: #4633 While reviewing and going over #4621 with @Stevengre , it became somewhat clear that how we handle turning substitions into ML predicates is a bit dirty. This attempts to clean this up a bit. Where potentially breaking changes to API are introduced here, I've checked if it affects the following repos when I mention "downstream" below: `evm-semantics kontrol wasm-semantics riscv-semantics mir-semantics`. In particular: - The function `CTerm.anti_unify` has a simplification where it reuses a function from `kast.manip` instead of reimplementing it. - The functions `CSubst.from_pred` and `CSubst.pred` are added, as replacements for `Subst.ml_pred`. This is because `Subst.ml_pred` doesn't have a good way to produce correctly sorted predicates, because it's in module `kast.inner`. - `Subst.ml_pred` is removed, and tests are updated to use the new `CSubst` variant. None of the downstream repositories use `Subst.ml_pred` directly. - The new `CSubst.pred` correctly sorts the generated `#Equals` clauses, defaulting to `K` sort or if a `KDefinition` is supplied using it to do sort inference. It also provides options for controlling whether we include the substitution or the constraints in the generated predicate. - A test is added for a `CSubst.pred` case which caused a bug in the integration tests dealing with identity substitutions. - The `CTermSymbolic.implies` function is updated to reuse `CSubst.from_pred` instead of reimplementing it. - On the case of duplicate entries, the first is kept and the latter are made as predicates.
Closed
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.
Merge two cterms into one for merging node functionality #4425.