Parking, Google CTF 2021

parking.cpp

#include <iostream>
#include <fstream>
#include <vector>
#include <unordered_map>
#include <forward_list>

#include <z3++.h>

int width, height;
std::vector<bool> walls;

inline bool intersecting(int x, int y, int w, int h) {
    for (int i = x; i < x + w; ++i)
        for (int j = y; j < y + h; ++j)
            if (walls[i * height + j])
                return true;
    return false;
}

struct block {
    int index;
    int x, y, w, h, t;

    std::forward_list<int> movable() const {
        std::forward_list<int> can;
        if (t != -2) can.push_front(0);

        if (w == 1) {
            for (int i = y + 1; i + h < height; ++i) {
                if (intersecting(x, i, w, h))
                    break;
                can.push_front(i - y);
            }

            for (int i = y - 1; i > 0; --i) {
                if (intersecting(x, i, w, h))
                    break;
                can.push_front(i - y);
            }
        } else {
            for (int i = x + 1; i + w < width; ++i) {
                if (intersecting(i, y, w, h))
                    break;
                can.push_front(i - x);
            }

            for (int i = x - 1; i > 0; --i) {
                if (intersecting(i, y, w, h))
                    break;
                can.push_front(i - x);
            }
        }

        return can;
    }
};

std::unordered_map<int, z3::expr> symbols;

inline const z3::expr &get_expr(z3::context &ctx, int index) {
    auto it = symbols.find(index);
    if (it == symbols.end()) {
        it = symbols.emplace(index, ctx.constant(ctx.int_symbol(index), ctx.bool_sort())).first;
    }
    return it->second;
}

int main() {
    std::ifstream file("level2");
    file >> width >> height;
    walls.resize(width * height, false);

    std::vector<block> blocks;
    block in;

    while (file >> in.x >> in.y >> in.w >> in.h >> in.t) {
        if (in.t != 0 && in.w != 1 && in.h != 1) {
            std::cerr << "not elongated";
            return 1;
        }
        if (in.t == 0) {
            for (int i = in.x; i < in.x + in.w; ++i) {
                for (int j = in.y; j < in.y + in.h; ++j) {
                    walls[i * height + j] = true;
                }
            }
        } else {
            in.index = blocks.size();
            blocks.push_back(in);
        }
    }


    z3::context ctx;
    z3::solver solver(ctx);

    {
        std::unordered_map<int, std::vector<int>> occupy;
        for (const block &b : blocks) {
            z3::expr_vector vec(ctx);
            for (int step : b.movable()) {
                const int index = b.index * 20 + step;
                if (b.w == 1) {
                    for (int i = b.y; i < b.y + b.h; ++i) {
                        occupy[b.x * height + (i + step)].push_back(index);
                    }
                } else {
                    for (int i = b.x; i < b.x + b.w; ++i) {
                        occupy[(i + step) * height + b.y].push_back(index);
                    }
                }
                vec.push_back(get_expr(ctx, index));
            }
            solver.add(z3::mk_or(vec));
        }

        for (const auto &o : occupy) {
            for (auto it = o.second.begin(); it < o.second.end(); ++it) {
                for (auto jt = it + 1; jt < o.second.end(); ++jt) {
                    solver.add(z3::implies(get_expr(ctx, *it), !get_expr(ctx, *jt)));
                }
            }
        }
    }

    std::cerr << "solving..." << std::endl;
    if (solver.check() == z3::unsat) {
        std::cerr << "unsatisfied" << std::endl;
        return 1;
    }
    std::cerr << "solved" << std::endl;

    char c = 0;
    int count = 0;
    const z3::model &model = solver.get_model();

    std::cout << "CTF{";
    for (block &b : blocks) {
        if (b.t != -1) continue;
        const z3::expr &expr = model.eval(get_expr(ctx, b.index * 20));
        switch (expr.bool_value()) {
            case Z3_L_FALSE:
                c |= (1 << count);
                break;
            case Z3_L_TRUE:
                break;
            default:
                std::cerr << "undefined" << std::endl;
                return 1;
        }
        if (++count == 8) {
            std::cout << c;
            count = c = 0;
        }
    }
    std::cout << '}' << std::endl;

    return 0;
}