Implement variable ordering optimization#181
Implement variable ordering optimization#181ProgMiner wants to merge 1 commit intoPLTools:masterfrom
Conversation
I don't really understand how it is related. |
| 11: { 0: [| 11 =/= _.10 |] } | ||
|
|
||
| 11: { 0: [| 11 =/= boxed 0 <_.12, _.13> |] } | ||
| 11: { 0: [| 11 =/= _.10 |] } |
There was a problem hiding this comment.
I've added explanation in the commit message
Since we allocate variable numbers linearly, we may assume that variables with greater number was allocated after variables with less number. So, if we have two variables |
Since variables allocated linearly of allocation time, this optimization must increase [Var.subst] optimization hit rate and shorten [Subst.walk] recursion paths In "regression_ppx/test015.t" we have change from term to variable because of swapping sides of disequality in constraint store. As a result, we doesn't simplify the constraint when variable "10" is unified. Signed-off-by: Eridan Domoratskiy <eridan200@mail.ru>
2 participants
Since variables allocated linearly of allocation time, this optimization must increase
Var.substoptimization hit rate and shortenSubst.walkrecursion paths