| 345 | |
| 346 | |
| 347 | static void instantiate_undef(const Input *in, map<expr, expr> &instances, |
| 348 | const Type &ty, unsigned child) { |
| 349 | if (auto agg = ty.getAsAggregateType()) { |
| 350 | for (unsigned i = 0, e = agg->numElementsConst(); i < e; ++i) { |
| 351 | if (!agg->isPadding(i)) |
| 352 | instantiate_undef(in, instances, agg->getChild(i), child + i); |
| 353 | } |
| 354 | return; |
| 355 | } |
| 356 | |
| 357 | // Bail out if it gets too big. It's unlikely we can solve it anyway. |
| 358 | if (instances.size() >= 128 || hit_half_memory_limit()) |
| 359 | return; |
| 360 | |
| 361 | auto var = in->getUndefVar(ty, child); |
| 362 | if (!var.isValid()) |
| 363 | return; |
| 364 | |
| 365 | // TODO: add support for per-bit input undef |
| 366 | assert(var.bits() == 1); |
| 367 | |
| 368 | map<expr, expr> instances2; |
| 369 | expr nums[2] = { expr::mkUInt(0, 1), expr::mkUInt(1, 1) }; |
| 370 | |
| 371 | for (auto I = instances.begin(); I != instances.end(); |
| 372 | I = instances.erase(I)) { |
| 373 | |
| 374 | if (hit_half_memory_limit()) { |
| 375 | instances2.insert(instances.begin(), instances.end()); |
| 376 | break; |
| 377 | } |
| 378 | |
| 379 | auto &[e, v] = *I; |
| 380 | for (unsigned i = 0; i < 2; ++i) { |
| 381 | expr newexpr = e.subst(var, nums[i]); |
| 382 | if (newexpr.eq(e)) { |
| 383 | instances2[std::move(newexpr)] = std::move(v); |
| 384 | break; |
| 385 | } |
| 386 | |
| 387 | newexpr = newexpr.simplify(); |
| 388 | if (newexpr.isFalse()) |
| 389 | continue; |
| 390 | |
| 391 | // keep 'var' variables for counterexample printing |
| 392 | instances2.try_emplace(std::move(newexpr), v && var == nums[i]); |
| 393 | } |
| 394 | } |
| 395 | instances = std::move(instances2); |
| 396 | } |
| 397 | |
| 398 | static expr preprocess(const Transform &t, const set<expr> &qvars0, |
| 399 | const set<expr> &undef_qvars, expr &&e) { |
no test coverage detected