Unify a stack of pairs of unification variables. * If any unification fails, then NULL is returned. * If all unifications are successful, the representative of the equivalence class of the top pair of unified variables * from the stack is returned. * '*bindings_used' is decremented by the number of pairs of (non-trivial) bindings that are successfully unified. * * If 'NULL' is returned, then
| 122 | * NULL != bindings_used |
| 123 | */ |
| 124 | static unification_var* unify_cont(unification_cont* cont, size_t* bindings_used) { |
| 125 | unification_var* result = NULL; |
| 126 | |
| 127 | /* Each time we go through this loop, the stack size of 'cont' either increases by 1 or decreases by 1. |
| 128 | * Whenever the stack size increases by 1, at the same time '*bindings_used' decreases by 1. |
| 129 | * |
| 130 | * For the above reason, the total number of times this loop iterates summed over all calls to 'unify_cont' cannot exceed |
| 131 | * |
| 132 | * (2 * the total number of bindings created + the number of times 'unify_cont' is called). |
| 133 | * |
| 134 | * The total number of bindings created is bounded linearly in the number of nodes in the Simplicity expression's DAG. |
| 135 | * The total number of calls to 'unify_cont' (via 'unify' and 'applyBinding') is bounded |
| 136 | * linearly in the number of nodes in the Simplicity expression's DAG. |
| 137 | * Therefore the total number of times this loop iterates summed over all calls to 'unify_cont' is bounded |
| 138 | * linearly in the number of nodes in the Simplicity DAG. |
| 139 | */ |
| 140 | while (cont) { |
| 141 | unification_var* alpha = findRoot(cont->alpha); |
| 142 | unification_var* beta = findRoot(cont->beta); |
| 143 | |
| 144 | if (alpha == beta) { |
| 145 | /* 'cont->alpha' and 'cont->beta' are already equivalent. */ |
| 146 | cont = cont->next; |
| 147 | } else { |
| 148 | /* We will be making 'alpha' a parent of 'beta', so swap the variables to ensure that 'alpha's rank |
| 149 | * is at least as large as 'beta'. |
| 150 | */ |
| 151 | if (alpha->rank < beta->rank) { |
| 152 | unification_var* tmp = beta; beta = alpha; alpha = tmp; |
| 153 | } |
| 154 | |
| 155 | /* Make 'beta' equivalent to 'alpha'. */ |
| 156 | beta->parent = alpha; |
| 157 | |
| 158 | if (beta->isBound) { |
| 159 | /* Copy/unify 'beta's binding to/with 'alpha'. */ |
| 160 | if (!applyBinding_cont(alpha, &beta->bound, &cont, bindings_used)) return NULL; /* Unification failure */ |
| 161 | } else { |
| 162 | /* 'beta' used to be a free variable. */ |
| 163 | cont = cont->next; |
| 164 | } |
| 165 | |
| 166 | /* Ensure 'alpha's rank exceeds 'beta's rank. |
| 167 | * Note that if 'alpha->rank' == 'beta->rank' then the two variables equivalence classes each had at least |
| 168 | * 2^'alpha->rank' variables in each of them. |
| 169 | * Therefore the unified equivalence classes will now have at least 2^'alpha->rank + 1' variables, |
| 170 | * which will be compatible with 'alpha's increased rank. |
| 171 | */ |
| 172 | if (alpha->rank == beta->rank) alpha->rank++; |
| 173 | } |
| 174 | |
| 175 | /* Return the representative of the unified variable of the two inputs that was on the top of the stack |
| 176 | * (as long as all other unifications are successful). |
| 177 | */ |
| 178 | if (!result) result = alpha; |
| 179 | } |
| 180 | |
| 181 | return result; |
no test coverage detected