| 428 | } |
| 429 | |
| 430 | void Solver::block(const Model &m, Solver *sneg) { |
| 431 | set<expr> assignments; |
| 432 | for (const auto &[var, val] : m) { |
| 433 | assignments.insert(var == val); |
| 434 | } |
| 435 | |
| 436 | if (sneg) { |
| 437 | // simple left-to-right variable discard algorithm |
| 438 | for (auto I = assignments.begin(); I != assignments.end(); ) { |
| 439 | SolverPush push(*sneg); |
| 440 | expr val = *I; |
| 441 | I = assignments.erase(I); |
| 442 | |
| 443 | sneg->add(expr::mk_and(assignments)); |
| 444 | if (!sneg->check("block model").isUnsat()) |
| 445 | assignments.insert(std::move(val)); |
| 446 | } |
| 447 | } |
| 448 | |
| 449 | add(!expr::mk_and(assignments)); |
| 450 | } |
| 451 | |
| 452 | void Solver::reset() { |
| 453 | Z3_solver_reset(ctx(), s); |