Fix TD3 narrowing non-wpoint #373
Merged
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.
While debugging increased evals in incremental analysis compared to from-scratch analysis (#369 (comment)), I found the following problem.
The TD3 implementation switches to narrowing phase even for non-wpoint variables, which causes extra evaluations. In the TD3 paper, the extra condition
x \in pointis used there.Another question is how this check should be performed:
HM.mem wpoint xorwp(the previous value cached from before evaluating right-hand side). The choice of whether to widen is done based on the latter, so at widening points, the first is always an overwrite (no join or widen). The difference is in the case whenxbecomes a wpoint during the evaluation of its right-hand side.I don't know yet whether this fixes all the excessive evals in the linked cases though, but at least on tiny examples from #363 it does.