Optimization: Share opposite-polarity literals in clause code trees - #880
Optimization: Share opposite-polarity literals in clause code trees#880Synrom wants to merge 16 commits into
Conversation
| inline bool isFun(unsigned num) const { return isFun() && _number()==num; } | ||
| /* Litearl headers encode polarity in their lowest bit, so xor-ing with 1 | ||
| * gives the opposite (negated) predicate. Only meaningful for literal predicates. */ | ||
| inline bool isOppositeFun(unsigned num) const { return isFun() && (_number()^1)==num; } |
There was a problem hiding this comment.
Would it make sense to assert that this actually gives the opposite literal, so if we ever change it, it automatically triggers? Maybe not here, since this is called very often.
There was a problem hiding this comment.
In the method itself, it would be hard. FlatTerm::changeLiteralPolarity uses the same trick, so you could add an assert there.
But as far as I can tell, FlatTerm::changeLiteralPolarity will not be executed anymore.
Maybe, I can just add a unit test that checks the FlatTerm behavior against the Literal implementation?
There was a problem hiding this comment.
Okay, the unit test would be awesome! Please feel free to remove any unused stuff from FlatTerm too.
There was a problem hiding this comment.
I've added a unit test now :) should I also remove the now-unused opposite field and related methods from LitInfo?
The methods are the only remaining callers of FlatTerm::changeLiteralPolarity, so that could go to.
|
Nice work, once the conflict is resolved I will run some more tests to be sure. Do I get it right that this shouldn't affect anything if |
|
Thank you :) Yes with On master and on |
Could you please add an |
|
Alright, I've added an assertion plus TODO now. |
2 participants
This PR optimizes clause code tree subsumption resolution by sharing literal information across polarities. Instead of storing separate positive and negative
LitInfoentries for each literal, matching records whether a result came from the opposite polarity and handles that during matcher execution.The implementation preserves subsumption priority over subsumption resolution by keeping non-opposite matches first in
ILStructand makingClauseMatcher::matchGlobalVarstry non-opposite matches before falling back to opposite-polarity matches.This optimization is currently not compatible with
CHECK_GROUND_TERM=1.