/*
 * ex7_lra_branching.c -- LRA inside a Boolean disjunction.
 *
 * Forces the SAT solver to enumerate cases that each get refuted by
 * the LRA theory. This exercises the full pipeline: SAT decisions
 * over LRA atoms, theory conflict on each branch, learned clauses
 * driving backjumps.
 *
 * Setup:
 *
 *   (P)  (x <= 1)  v  (x >= 10)
 *   (Q)  2 <= x <= 9
 *
 * (Q) excludes both options in (P), so the whole is UNSAT. But the
 * exclusion is only visible inside arithmetic, not at the SAT level
 * where x<=1, x>=10, x>=2, x<=9 are just four opaque atoms.
 *
 * The SAT solver decides one literal of (P), the LRA theory refutes
 * it together with (Q), the learned clause forces the other literal,
 * which the theory also refutes, learning the empty (modulo unit)
 * clause that proves UNSAT.
 */
#include "smt.h"
#include <stdio.h>

int main(void) {
    SmtCtx *ctx = smt_new();
    int x = smt_mk_real_var(ctx, "x");
    SmtLinTerm xt = { x, 1, 1 };

    /* atoms */
    int a_le1  = smt_mk_lra_le_atom(ctx, &xt, 1, 1,  1);   /* x <= 1  */
    int a_lt10 = smt_mk_lra_lt_atom(ctx, &xt, 1, 10, 1);   /* x < 10  */
    int a_le9  = smt_mk_lra_le_atom(ctx, &xt, 1, 9,  1);   /* x <= 9  */
    int a_lt2  = smt_mk_lra_lt_atom(ctx, &xt, 1, 2,  1);   /* x < 2   */

    /* (x<=1) v ~(x<10), i.e. (x<=1) v (x>=10) */
    int cl[2] = { a_le1, -a_lt10 };
    smt_assert_clause(ctx, cl, 2);
    /* x <= 9 */
    int u1 =  a_le9;  smt_assert_clause(ctx, &u1, 1);
    /* ~(x<2), i.e. x >= 2 */
    int u2 = -a_lt2;  smt_assert_clause(ctx, &u2, 1);

    int r = smt_check(ctx);

    printf("=== Phase 3: SAT branching over LRA atoms ===\n");
    printf("\n  ((x <= 1) v (x >= 10))  AND  (2 <= x <= 9)\n\n");
    printf("  atoms          = %d   (x<=1, x<10, x<=9, x<2)\n",
           smt_n_atoms(ctx));
    printf("  result         = %s\n",
           r == SMT_UNSAT ? "UNSAT" :
           r == SMT_SAT   ? "SAT (BUG)" : "unknown");
    printf("  decisions      = %ld  (SAT must guess at the disjunction)\n",
           smt_decisions(ctx));
    printf("  theory conf.   = %ld  (LRA refutes each branch)\n",
           smt_theory_conflicts(ctx));
    printf("  conflicts      = %ld\n",  smt_conflicts(ctx));
    printf("  LRA pivots     = %ld\n",  smt_lra_pivots(ctx));
    smt_free(ctx);
    return r == SMT_UNSAT ? 0 : 1;
}
