/*
 * sanity.c -- smoke tests for the SAT solver.
 */
#include "sat.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

static int test_count = 0, pass_count = 0;

static void check(int cond, const char *name, const char *msg) {
    test_count++;
    if (cond) {
        pass_count++;
        printf("  [ok ]  %s\n", name);
    } else {
        printf("  [FAIL] %s: %s\n", name, msg);
    }
}

/* ------ Test 1: trivial SAT */
static void test_trivial_sat(void) {
    Sat *s = sat_new(3);
    sat_add_clause(s, (int[]){ 1, 2 }, 2);
    sat_add_clause(s, (int[]){ -1, 3 }, 2);
    int r = sat_solve(s);
    check(r == SAT_SATISFIABLE, "trivial SAT", "expected SAT");
    sat_free(s);
}

/* ------ Test 2: trivial UNSAT */
static void test_trivial_unsat(void) {
    Sat *s = sat_new(1);
    sat_add_clause(s, (int[]){  1 }, 1);
    sat_add_clause(s, (int[]){ -1 }, 1);
    int r = sat_solve(s);
    check(r == SAT_UNSATISFIABLE, "trivial UNSAT", "expected UNSAT");
    sat_free(s);
}

/* ------ Test 3: empty clause */
static void test_empty(void) {
    Sat *s = sat_new(1);
    sat_add_clause(s, NULL, 0);
    int r = sat_solve(s);
    check(r == SAT_UNSATISFIABLE, "empty clause = UNSAT", "");
    sat_free(s);
}

/* ------ Test 4: implication chain */
static void test_chain(void) {
    /* x1 => x2 => x3 => x4, x1, ~x4 => UNSAT */
    Sat *s = sat_new(4);
    sat_add_clause(s, (int[]){ -1,  2 }, 2);
    sat_add_clause(s, (int[]){ -2,  3 }, 2);
    sat_add_clause(s, (int[]){ -3,  4 }, 2);
    sat_add_clause(s, (int[]){  1 }, 1);
    sat_add_clause(s, (int[]){ -4 }, 1);
    int r = sat_solve(s);
    check(r == SAT_UNSATISFIABLE, "implication chain UNSAT", "");
    sat_free(s);
}

/* ------ Test 5: xor circuit */
static void test_xor(void) {
    /* (x1 XOR x2) = (x1 OR x2) AND (~x1 OR ~x2) -- both ways */
    Sat *s = sat_new(2);
    sat_add_clause(s, (int[]){  1,  2 }, 2);
    sat_add_clause(s, (int[]){ -1, -2 }, 2);
    int r = sat_solve(s);
    int sat = (r == SAT_SATISFIABLE);
    int v1 = sat_value(s, 1), v2 = sat_value(s, 2);
    check(sat && (v1 != v2), "xor SAT, x1 != x2", "");
    sat_free(s);
}

/* ------ Test 6: tautology dropped, no extra constraints */
static void test_tautology(void) {
    Sat *s = sat_new(1);
    sat_add_clause(s, (int[]){ 1, -1 }, 2);   /* tautology, dropped */
    int r = sat_solve(s);
    check(r == SAT_SATISFIABLE, "tautology dropped", "");
    sat_free(s);
}

/* ------ Test 7: medium random 3-SAT (handcrafted, SAT) */
static void test_random_sat(void) {
    Sat *s = sat_new(5);
    /* A small 3-SAT formula known to be SAT. x1=T,x2=F,x3=T,x4=T,x5=F works. */
    int cls[][3] = {
        { 1, -2,  3},
        { 2,  3, -4},
        {-1,  4,  5},
        { 1, -3, -5},
        { 2, -4, -5},
        {-2,  3,  4},
        { 1,  2, -3},
    };
    for (int i = 0; i < 7; i++) sat_add_clause(s, cls[i], 3);
    int r = sat_solve(s);
    /* Verify every clause is satisfied. */
    int ok = (r == SAT_SATISFIABLE);
    if (ok) {
        for (int i = 0; i < 7 && ok; i++) {
            int sat_cl = 0;
            for (int j = 0; j < 3; j++) {
                int lit = cls[i][j];
                int v = sat_value(s, lit > 0 ? lit : -lit);
                if ((lit > 0 && v == SAT_TRUE) || (lit < 0 && v == SAT_FALSE))
                    sat_cl = 1;
            }
            if (!sat_cl) ok = 0;
        }
    }
    check(ok, "small 3-SAT", "model didn't satisfy all clauses");
    sat_free(s);
}

int main(void) {
    test_trivial_sat();
    test_trivial_unsat();
    test_empty();
    test_chain();
    test_xor();
    test_tautology();
    test_random_sat();

    printf("\n%d / %d passed\n", pass_count, test_count);
    return pass_count == test_count ? 0 : 1;
}
