/*
 * ex4_equiv.c -- combinational equivalence checking with EUF.
 *
 * A classical use of SAT modulo EUF: check that two implementations of
 * the same function are equivalent on every input. We model the
 * primitive gates as uninterpreted function symbols `AND`, `OR`, `NOT`,
 * with no semantics other than congruence. Equivalence then reduces to:
 * are there inputs a, b, c such that circuit1(a, b, c) and circuit2(a,
 * b, c) produce different outputs?
 *
 * The two circuits here are different syntactic constructions of a
 * three-input majority gate. The straightforward implementation is
 *
 *     maj(a, b, c) = OR(AND(a, b), OR(AND(b, c), AND(a, c)))
 *
 * A common alternative factorisation is
 *
 *     maj(a, b, c) = OR(AND(a, b), AND(c, OR(a, b)))
 *
 * The two expressions ARE Boolean-equivalent (both compute majority),
 * but they are NOT congruence-equivalent under uninterpreted AND/OR,
 * because AND and OR are opaque function symbols rather than Boolean
 * operators. So EUF says SAT: there exist values of a, b, c (in some
 * abstract sense) for which AND/OR could be implementations that make
 * the two outputs differ.
 *
 * To make the check trivially fail and demonstrate UNSAT, we then add
 * the same construction twice and check that THOSE are equivalent.
 * They are, by congruence alone.
 *
 * The point of the example is to show EUF doing exactly what it
 * promises: structural reasoning about function symbols, with no Boolean
 * semantics built in.
 */
#include "smt.h"
#include <stdio.h>

static int AND(SmtCtx *c, int x, int y) {
    int args[2] = { x, y };
    return smt_mk_app(c, "AND", args, 2);
}
static int OR(SmtCtx *c, int x, int y) {
    int args[2] = { x, y };
    return smt_mk_app(c, "OR", args, 2);
}

static void check_circuits_equivalent(const char *desc, int (*build1)(SmtCtx*, int, int, int),
                                                       int (*build2)(SmtCtx*, int, int, int)) {
    SmtCtx *ctx = smt_new();
    int a = smt_mk_const(ctx, "a");
    int b = smt_mk_const(ctx, "b");
    int c = smt_mk_const(ctx, "c");

    int out1 = build1(ctx, a, b, c);
    int out2 = build2(ctx, a, b, c);

    /* Ask: can the outputs differ? */
    smt_assert_neq(ctx, out1, out2);

    int r = smt_check(ctx);
    printf("  %s\n", desc);
    printf("    terms      : %d\n", smt_n_terms(ctx));
    printf("    result     : %s\n",
        r == SMT_UNSAT ? "EQUIVALENT (UNSAT: no model distinguishing them)"
                       : r == SMT_SAT ? "NOT EQUIVALENT under EUF (a model exists)"
                       : "unknown");
    printf("    decisions  = %ld   conflicts = %ld   theory conf. = %ld   theory props = %ld\n",
        smt_decisions(ctx), smt_conflicts(ctx), smt_theory_conflicts(ctx),
        smt_theory_props(ctx));
    smt_free(ctx);
}

/* maj1: OR(AND(a, b), OR(AND(b, c), AND(a, c))) */
static int maj1(SmtCtx *c, int a, int b, int cc) {
    return OR(c, AND(c, a, b), OR(c, AND(c, b, cc), AND(c, a, cc)));
}
/* maj2: OR(AND(a, b), AND(c, OR(a, b))) -- Boolean-equivalent, not congruence-equivalent. */
static int maj2(SmtCtx *c, int a, int b, int cc) {
    return OR(c, AND(c, a, b), AND(c, cc, OR(c, a, b)));
}
/* Same syntactic construction twice. */
static int maj1_again(SmtCtx *c, int a, int b, int cc) { return maj1(c, a, b, cc); }

int main(void) {
    printf("=== Combinational equivalence with EUF ===\n\n");
    printf("Function symbols AND and OR are uninterpreted (no Boolean\n"
           "semantics); equivalence reduces to syntactic congruence.\n\n");

    check_circuits_equivalent(
        "Two different factorisations of majority (Boolean-equivalent only):",
        maj1, maj2);

    printf("\n");
    check_circuits_equivalent(
        "Same construction twice (congruence-equivalent):",
        maj1, maj1_again);

    return 0;
}
