| 222 | |
| 223 | template<class Tracer> |
| 224 | forceinline Space* |
| 225 | Path<Tracer>::recompute(unsigned int& d, unsigned int a_d, Worker& stat, |
| 226 | Tracer& t) { |
| 227 | assert(!ds.empty()); |
| 228 | // Recompute space according to path |
| 229 | // Also say distance to copy (d == 0) requires immediate copying |
| 230 | |
| 231 | // Check for LAO |
| 232 | if ((ds.top().space() != nullptr) && ds.top().rightmost()) { |
| 233 | Space* s = ds.top().space(); |
| 234 | s->commit(*ds.top().choice(),ds.top().alt()); |
| 235 | assert(ds.entries()-1 == lc()); |
| 236 | ds.top().space(nullptr); |
| 237 | // Mark as reusable |
| 238 | if (static_cast<unsigned int>(ds.entries()) > ngdl()) |
| 239 | ds.top().next(); |
| 240 | d = 0; |
| 241 | return s; |
| 242 | } |
| 243 | // General case for recomputation |
| 244 | int l = lc(); // Position of last clone |
| 245 | int n = ds.entries(); // Number of stack entries |
| 246 | // New distance, if no adaptive recomputation |
| 247 | d = static_cast<unsigned int>(n - l); |
| 248 | |
| 249 | Space* s = ds[l].space()->clone(); // Last clone |
| 250 | |
| 251 | if (d < a_d) { |
| 252 | // No adaptive recomputation |
| 253 | for (int i=l; i<n; i++) |
| 254 | commit(s,i); |
| 255 | } else { |
| 256 | int m = l + static_cast<int>(d >> 1); // Middle between copy and top |
| 257 | int i = l; // To iterate over all entries |
| 258 | // Recompute up to middle |
| 259 | for (; i<m; i++ ) |
| 260 | commit(s,i); |
| 261 | // Skip over all rightmost branches |
| 262 | for (; (i<n) && ds[i].rightmost(); i++) |
| 263 | commit(s,i); |
| 264 | // Is there any point to make a copy? |
| 265 | if (i<n-1) { |
| 266 | // Propagate to fixpoint |
| 267 | SpaceStatus ss = s->status(stat); |
| 268 | /* |
| 269 | * Again, the space might already propagate to failure (due to |
| 270 | * weakly monotonic propagators). |
| 271 | */ |
| 272 | if (ss == SS_FAILED) { |
| 273 | // s must be deleted as it is not on the stack |
| 274 | delete s; |
| 275 | stat.fail++; |
| 276 | unwind(i,t); |
| 277 | return nullptr; |
| 278 | } |
| 279 | ds[i].space(s->clone()); |
| 280 | d = static_cast<unsigned int>(n-i); |
| 281 | } |