#include <catch2/catch_test_macros.hpp>
#include <vector>

#include "fold/symbolic/encoder.hpp"
#include "fold/symbolic/theory.hpp"

TEST_CASE("instantiateSummaryPredicateInContext substitutes positional args",
          "[encoder][summary]") {
    z3::context ctx;
    std::vector<z3::expr> args;
    args.push_back(ctx.bv_val(7, fold::kBitvecWidth));
    args.push_back(ctx.bv_val(3, fold::kBitvecWidth));

    // The body uses the formal argument naming the summary parser expects.
    auto result = fold::instantiateSummaryPredicateInContext("(bvuge arg0 arg1)", args, ctx);
    REQUIRE(result.has_value());
    REQUIRE(result->simplify().is_true());
}

TEST_CASE("instantiateSummaryPredicateInContext returns false when predicate fails",
          "[encoder][summary]") {
    z3::context ctx;
    std::vector<z3::expr> args;
    args.push_back(ctx.bv_val(1, fold::kBitvecWidth));
    args.push_back(ctx.bv_val(2, fold::kBitvecWidth));

    auto result = fold::instantiateSummaryPredicateInContext("(bvuge arg0 arg1)", args, ctx);
    REQUIRE(result.has_value());
    REQUIRE(result->simplify().is_false());
}

TEST_CASE("instantiateSummaryPredicateInContext returns nullopt on empty body",
          "[encoder][summary]") {
    z3::context ctx;
    std::vector<z3::expr> args;
    args.push_back(ctx.bv_val(0, fold::kBitvecWidth));

    auto result = fold::instantiateSummaryPredicateInContext("", args, ctx);
    REQUIRE_FALSE(result.has_value());
}

TEST_CASE("instantiateSummaryPredicateInContext returns nullopt on syntactically invalid body",
          "[encoder][summary]") {
    z3::context ctx;
    std::vector<z3::expr> args;
    args.push_back(ctx.bv_val(0, fold::kBitvecWidth));

    auto result = fold::instantiateSummaryPredicateInContext("(((not smtlib", args, ctx);
    REQUIRE_FALSE(result.has_value());
}

TEST_CASE("instantiateSummaryPredicateInContext widens narrow bv args to BV-64",
          "[encoder][summary]") {
    z3::context ctx;
    std::vector<z3::expr> args;
    // 8-bit -1 (0xFF) should sign-extend to 0xFFFF'FFFF'FFFF'FFFF when widened
    // to BV-64 by normalizeSummaryArg.
    args.push_back(ctx.bv_val(-1, 8));

    auto result =
        fold::instantiateSummaryPredicateInContext("(= arg0 #xFFFFFFFFFFFFFFFF)", args, ctx);
    REQUIRE(result.has_value());
    REQUIRE(result->simplify().is_true());
}

TEST_CASE("instantiateSummaryExpr substitutes into a value expression", "[encoder][summary]") {
    auto env = fold::SymbolicEnv::create();
    std::vector<z3::expr> args;
    args.push_back(env.ctx().bv_val(10, fold::kBitvecWidth));
    args.push_back(env.ctx().bv_val(5, fold::kBitvecWidth));

    auto result = fold::instantiateSummaryExpr("(bvadd arg0 arg1)", args, env);
    REQUIRE(result.has_value());
    REQUIRE(result->is_bv());
    z3::expr expected = env.ctx().bv_val(15, fold::kBitvecWidth);
    REQUIRE((result.value() == expected).simplify().is_true());
}

TEST_CASE("instantiateSummaryExpr returns nullopt on empty body", "[encoder][summary]") {
    auto env = fold::SymbolicEnv::create();
    std::vector<z3::expr> args;
    auto result = fold::instantiateSummaryExpr("", args, env);
    REQUIRE_FALSE(result.has_value());
}

TEST_CASE("instantiateSummaryPredicate evaluates an equality predicate over args",
          "[encoder][summary]") {
    auto env = fold::SymbolicEnv::create();
    std::vector<z3::expr> args;
    args.push_back(env.ctx().bv_val(42, fold::kBitvecWidth));
    args.push_back(env.ctx().bv_val(42, fold::kBitvecWidth));

    auto result = fold::instantiateSummaryPredicate("(= arg0 arg1)", args, env);
    REQUIRE(result.has_value());
    REQUIRE(result->simplify().is_true());
}