#include <catch2/catch_test_macros.hpp>

#include "fold/symbolic/constraint_slice.hpp"

TEST_CASE("constraint slicing follows symbol-connected fixed points", "[symbolic][slice]") {
    z3::context ctx;
    const z3::expr x = ctx.bv_const("x", 64);
    const z3::expr y = ctx.bv_const("y", 64);
    const z3::expr z = ctx.bv_const("z", 64);
    const z3::expr unrelated = ctx.bv_const("unrelated", 64);
    z3::solver solver(ctx, "QF_BV");
    solver.add(x == y);
    solver.add(y == z);
    solver.add(unrelated == ctx.bv_val(9, 64));

    const z3::expr focus = x == ctx.bv_val(0, 64);
    const z3::expr predicate = focus && z == ctx.bv_val(1, 64);
    const auto slice = fold::symbolic::sliceConstraintsForPredicate(solver, predicate, focus);

    CHECK(slice.input_terms == 5);
    CHECK(slice.selected_terms == 4);
    CHECK(slice.assertions.size() == 2);
    CHECK(slice.assumptions.size() == 2);
    CHECK(slice.reduced());
}

TEST_CASE("constraint slice unsat proves full conjunction", "[symbolic][slice]") {
    z3::context ctx;
    const z3::expr x = ctx.bv_const("x", 64);
    const z3::expr y = ctx.bv_const("y", 64);
    z3::solver full(ctx, "QF_BV");
    full.add(x == ctx.bv_val(1, 64));
    full.add(y == ctx.bv_val(2, 64));
    const z3::expr focus = x == ctx.bv_val(0, 64);
    const auto slice = fold::symbolic::sliceConstraintsForPredicate(full, focus, focus);

    z3::solver reduced(ctx, "QF_BV");
    for (const auto& assertion : slice.assertions)
        reduced.add(assertion);
    z3::expr_vector assumptions(ctx);
    for (const auto& assumption : slice.assumptions)
        assumptions.push_back(assumption);

    CHECK(reduced.check(assumptions) == z3::unsat);
    full.add(focus);
    CHECK(full.check() == z3::unsat);
}

TEST_CASE("slice satisfiability does not prove full feasibility", "[symbolic][slice]") {
    z3::context ctx;
    const z3::expr x = ctx.bv_const("x", 64);
    const z3::expr y = ctx.bv_const("y", 64);
    z3::solver full(ctx, "QF_BV");
    full.add(y == ctx.bv_val(1, 64));
    full.add(y == ctx.bv_val(2, 64));
    const z3::expr focus = x == ctx.bv_val(0, 64);
    const auto slice = fold::symbolic::sliceConstraintsForPredicate(full, focus, focus);

    z3::solver reduced(ctx, "QF_BV");
    for (const auto& assertion : slice.assertions)
        reduced.add(assertion);
    z3::expr_vector assumptions(ctx);
    for (const auto& assumption : slice.assumptions)
        assumptions.push_back(assumption);

    CHECK(reduced.check(assumptions) == z3::sat);
    full.add(focus);
    CHECK(full.check() == z3::unsat);
    CHECK(slice.reduced());
}