Cleanups to handling ml predicates and substitutions #4625
Merged
Conversation
This file contains hidden or 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
This was referenced Sep 5, 2024
ehildenb
force-pushed
the
fix-subst-ml-pred
branch
from
6475931 to
02e8c0f
Compare
ehildenb
changed the title
ehildenb
force-pushed
the
fix-subst-ml-pred
branch
from
34cd321 to
5127f2e
Compare
ehildenb
force-pushed
the
fix-subst-ml-pred
branch
from
5127f2e to
a4a3ae9
Compare
rv-jenkins
added a commit
that referenced
this pull request
Sep 6, 2024
Pulled out of: #4625 This PR improves the substitution extraction machinery in `kast.manip`, and adds tests. This isn't used anywhere at the moment, but #4625 will start using it heavily. - The code for `extract_substs` is simplified. - The cases of circular substitutions are handled slightly more gracefully. --------- Co-authored-by: rv-jenkins <[email protected]>
…e_constraints if needed
…t.ml_pred to CSubst.pred
…pred to tests of CSubst.pred
…er_unique_constraints if needed" This reverts commit 766c539.
ehildenb
force-pushed
the
fix-subst-ml-pred
branch
from
a4a3ae9 to
8757594
Compare
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.
Blocked on: #4631Blocked on: #4630Blocked on: #4633While 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:
CTerm.anti_unifyhas a simplification where it reuses a function fromkast.manipinstead of reimplementing it.CSubst.from_predandCSubst.predare added, as replacements forSubst.ml_pred. This is becauseSubst.ml_preddoesn't have a good way to produce correctly sorted predicates, because it's in modulekast.inner.Subst.ml_predis removed, and tests are updated to use the newCSubstvariant. None of the downstream repositories useSubst.ml_preddirectly.CSubst.predcorrectly sorts the generated#Equalsclauses, defaulting toKsort or if aKDefinitionis 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.CSubst.predcase which caused a bug in the integration tests dealing with identity substitutions.CTermSymbolic.impliesfunction is updated to reuseCSubst.from_predinstead of reimplementing it.