Skip to content

Conversation

@steve-anunknown
Copy link
Contributor

My attempt at optimizing the W and Wp methods.

The memory taken up by the middle part is reduced by yielding from it in both the first phase and second phase. Turns out that it hurts performance when including middle in product.

Another difference is that the top iteration is performed on the middle part, in order to search in big depths only if no counterexample if found in small depths.

Finally, these ideas can be applied to the W method too, as it suffered from the same problems.

The implementation on the master branch right now is wrong because the oracle does not actually iterate over the middle more than once, because middle is exhausted after the first iteration. It just so happens that all counter examples are found without needing to iterate over the middle more than once.

@emuskardin
Copy link
Member

I will benchmark it agaist my optimization of Wp that is currently on master on Monday.

Same with W.

@emuskardin emuskardin merged commit b55152a into DES-Lab:master Jan 20, 2025
2 checks passed
@emuskardin
Copy link
Member

Merged. It was more efficient. Nicely done :)

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.

2 participants