Canonicalize all commutative operators in Expr #684
+68
−39
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
msooseth
changed the title
msooseth
force-pushed
the
more-simplifications
branch
from
fc8433e to
08b313e
Compare
msooseth
changed the title
msooseth
force-pushed
the
more-simplifications
branch
from
08b313e to
e32c08b
Compare
Update MOre te Also order all commutative Improve Update Changelog More simp Fixing Update changelog Cleanup No need to check
msooseth
force-pushed
the
more-simplifications
branch
from
e32c08b to
41825cd
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.
Description
Canonicalize all commutative operators in Expr. Much more powerful than some of the rewrite rules we had before.
This helps us with Eq x1 x1. In cases when x1 == x2 modulo commutativity, the Eq x1 x2 could actually be dispatched to the SMT solver. However, if we canonicalize x1 and x2, then this will not happen. This significantly improves solving. Note that this canonicalization is 100% compatible with us wanting Lit as the 1st argument. Lit is the lowest in the order, and so will always be the 1st.
This also means that some old rewrite rules need to change. The Add (Add ((Lit x) y) (Lit z)) can no longer stay that way, as Lit is smaller than Add, so it becomes Add (Lit x) (Add (Lit z) y. This is a good thing, because it brings all Lit-s to the LHS. This is now done for all commutative operators. The new setup is cleaner and also more principled than before. I adjusted the tests, and they showcase quite well that we are doing good indeed.
This change necessitated one small, logical change in our array decomposition. However, this thankfully helped us pass one more test that I have been meaning to pass! Yay.
Checklist