/*
 * ex2_branching.c -- SAT must enumerate cases that the theory then refutes.
 *
 * We assert a disjunction (a = b) v (c = d), then separately assert
 * facts that make each disjunct theory-inconsistent. The SAT solver
 * must explore both literals; each is killed by the theory; the second
 * theory refutation is what closes the formula.
 *
 * Concretely:
 *
 *   (a = b) v (c = d)
 *   f(a) != f(b)              <-- kills (a = b)  by congruence on f
 *   g(c) = u, g(d) = v, u != v <-- kills (c = d) by congruence on g
 *
 * Without the SAT layer the theory would have no way to know which
 * disjunct to enforce; without the theory the SAT layer would happily
 * pick either and declare victory. Together they refute both.
 *
 * What to look at in the output: the propositional `conflicts` and
 * `theory conflicts` counters. They should both be at least one. Every
 * theory conflict generates a learned clause that the SAT layer then
 * uses to prune future branches.
 */
#include "smt.h"
#include <stdio.h>
#include <stdlib.h>

int main(void) {
    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 d = smt_mk_const(ctx, "d");
    int u = smt_mk_const(ctx, "u");
    int v = smt_mk_const(ctx, "v");

    int fa = smt_mk_app(ctx, "f", &a, 1);
    int fb = smt_mk_app(ctx, "f", &b, 1);
    int gc = smt_mk_app(ctx, "g", &c, 1);
    int gd = smt_mk_app(ctx, "g", &d, 1);

    /* Disjunction: (a = b) v (c = d). */
    int eab = smt_mk_eq_atom(ctx, a, b);
    int ecd = smt_mk_eq_atom(ctx, c, d);
    int cl[2] = { eab, ecd };
    smt_assert_clause(ctx, cl, 2);

    /* Theory refutations of each branch. */
    smt_assert_neq(ctx, fa, fb);    /* kills (a = b) */
    smt_assert_eq (ctx, gc, u);
    smt_assert_eq (ctx, gd, v);
    smt_assert_neq(ctx, u, v);      /* kills (c = d) */

    printf("=== SAT branching, theory refuting ===\n");
    printf("\n  Asserted:\n");
    printf("    (a = b) v (c = d)\n");
    printf("    f(a) != f(b)\n");
    printf("    g(c) = u,  g(d) = v,  u != v\n\n");
    printf("  atoms      : %d\n", smt_n_atoms(ctx));
    printf("  terms      : %d\n", smt_n_terms(ctx));

    int r = smt_check(ctx);
    printf("  result     : %s\n",
        r == SMT_UNSAT ? "UNSAT (as expected -- both branches refuted)"
                       : r == SMT_SAT ? "SAT (BUG!)" : "unknown");
    printf("  decisions     = %ld\n", smt_decisions(ctx));
    printf("  conflicts     = %ld  (propositional + theory)\n", smt_conflicts(ctx));
    printf("  theory conf.  = %ld\n", smt_theory_conflicts(ctx));
    printf("  theory props  = %ld\n", smt_theory_props(ctx));
    printf("  propagations  = %ld\n", smt_propagations(ctx));

    smt_free(ctx);
    return r == SMT_UNSAT ? 0 : 1;
}
