Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add method to_axiom to class Rule #4701

Merged
merged 1 commit into from
Dec 5, 2024

Conversation

tothtamas28
Copy link
Contributor

No description provided.

@tothtamas28 tothtamas28 self-assigned this Dec 4, 2024
@tothtamas28 tothtamas28 marked this pull request as ready for review December 4, 2024 12:47
@tothtamas28 tothtamas28 requested a review from jberthold December 4, 2024 12:47
pyk/src/pyk/kore/rule.py Show resolved Hide resolved
pyk/src/pyk/kore/rule.py Show resolved Hide resolved
@jberthold
Copy link
Member

jberthold commented Dec 4, 2024

Your round-tripping from_axiom -> to_axiom test fails on some accidental artefact of simplification priorities:
The simplification attribute takes an optional priority argument, and apparently the compiler inserts an empty string in many cases, but not in the injection rule from BASIC-K.
Booster came to accept both the empty string and the absence of an argument to simplification as priority 50.

@tothtamas28
Copy link
Contributor Author

The simplification attribute takes an optional priority argument, and apparently the compiler inserts an empty string in many cases, but not in the injection rule from BASIC-K.

And for --backend llvm, the "" is not inserted. So I just adjusted the test to normalize the attribute list.

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit c2f9346 into develop Dec 5, 2024
18 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the rule-to-axiom branch December 5, 2024 10:28
@jberthold
Copy link
Member

The simplification attribute takes an optional priority argument, and apparently the compiler inserts an empty string in many cases, but not in the injection rule from BASIC-K.

And for --backend llvm, the "" is not inserted. So I just adjusted the test to normalize the attribute list.

Fun fact: (or rather conjecture, but I am pretty certain after trying to find out more about it this morning...)
The "" is also not inserted for --backend haskell when there is no simplification that has a non-default priority.

Certainly the answer is buried somewhere in the java code... maybe in ModuleToKore.java

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants