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

Custom rewrites #74

Merged
merged 21 commits into from
Aug 10, 2023
Merged

Custom rewrites #74

merged 21 commits into from
Aug 10, 2023

Conversation

RazinShaikh
Copy link
Collaborator

@RazinShaikh RazinShaikh commented Aug 8, 2023

This PR contains preliminary implementation of custom rewrites. Currently, the rewrites only work with exact phases but we can add support for more general types of phases in the future.

@RazinShaikh RazinShaikh requested a review from akissinger August 9, 2023 09:47
Copy link
Collaborator

@jvdwetering jvdwetering left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good! I have some small comments, and there's definitely room for enhancements in the future.
Maybe something to consider as well is to do a check for the semantics of the lhs and rhs when you build the new rule. Since we are not considering bang-boxes or any fancy logic we just have to calculate the matrix of the lhs and of the rhs and see if they are equal, and we can warn the user if they are trying to create a rewrite rule that doesn't preserve semantics.
We could even use this to automatically find the right scalar factor to scale the graph by when you do the graph replacement.

zxlive/edit_panel.py Outdated Show resolved Hide resolved
zxlive/mainwindow.py Outdated Show resolved Hide resolved
zxlive/mainwindow.py Outdated Show resolved Hide resolved
zxlive/proof_actions.py Show resolved Hide resolved
zxlive/proof_actions.py Show resolved Hide resolved
zxlive/mainwindow.py Outdated Show resolved Hide resolved
@RazinShaikh
Copy link
Collaborator Author

@jvdwetering I believe I have addressed all of your comments now. Let me know if there is anything else to do for this PR.

@jvdwetering
Copy link
Collaborator

Yes this all looks good, and in any case we can still add stuff to it later of course.

@jvdwetering jvdwetering merged commit 9e16d80 into master Aug 10, 2023
@RazinShaikh RazinShaikh deleted the custom_rewrites branch August 10, 2023 21:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Support custom rewrites / lemmas Implement bialgebra in the other direction
3 participants