Repository navigation
Conversation
|
Could you add tests covering backtracking, equality orientations and subsumption resolution, plus a before/after benchmark? It would help to check whether the saved matching work outweighs the cost of computing occupied positions. |
|
|
||
| inline bool isExclusive() const | ||
| { | ||
| return std::has_single_bit(bitmask); |
There was a problem hiding this comment.
Shouldn't we save an overflow bit so that we know when there are "unsaved" overflown bits and therefore this function would return the wrong value?
| struct LitInfoOccupation { | ||
| static constexpr unsigned CAPACITY = 64; | ||
|
|
||
| static LitInfoOccupation createEmptyOccupation() |
| CodeTree::LitInfoOccupation ClauseCodeTree::ClauseMatcher::occupiedPositions() | ||
| { | ||
| LitInfoOccupation occupied; | ||
| // A truncated domain could falsely appear to contain just one position. |
There was a problem hiding this comment.
Ah okay I see the case I asked about below is handled here.
| return occupied; | ||
| } | ||
|
|
||
| for(auto& lm : lms) { |
There was a problem hiding this comment.
This should be const if possible, I don't see any reason why not (apart from having to add a const getILS?).
| eagerResults.reset(); | ||
|
|
||
| RSTAT_CTR_INC("LiteralMatcher::init"); | ||
| if (!seekOnlySuccess && !prepareLiteral()) { |
There was a problem hiding this comment.
Can you write a comment why this is needed now?
There was a problem hiding this comment.
I've added a comment
| { | ||
| void init(const CodeTree& tree, FlatTerm* ft_) { | ||
| CodeTree::Matcher</*removing*/false,/*checkRange=*/false>::init(tree,tree.getEntryPoint(), 0, 0); | ||
| CodeTree::Matcher</*removing*/false,/*checkRange=*/false>::init(tree,tree.getEntryPoint(), LitInfoOccupation(), 0, 0); |
There was a problem hiding this comment.
This could be made a default value, similarly here. Is a default LitInfoOccupation() value a correct one in all cases?
There was a problem hiding this comment.
I've made LitInfoOccupation() the default now, but kept it here to maintain the following arguments from before.
|
TPTP FOL Discount: run 0 unsat: 9168 (0) sat: 1042 (0) cputime: 60786.71 s instructions: 223481241 Mi memory: 1803241.82 MB TPTP FOL Otter: run 0 unsat: 9304 (0) sat: 1026 (0) cputime: 66220.80 s instructions: 223238846 Mi memory: 2069794.32 MB |
…thub.com/Synrom/vampire into optimization/code-tree-literal-occupancy
|
@shalashaska117 I think most of these cases are already covered by the existing code tree tests. |
Optimizes Code trees by ignoring occupied query literals.
That is when an earlier indexed literal only matches a single query literal, that query literal can be ignored moving forward inside the tree.