/*
 * ex3_arrays.c -- modelling memory accesses through uninterpreted
 *                 read / write functions.
 *
 * This is the classical pattern from program verification: arrays are
 * modelled as values, and "reading from memory at address p" is a
 * function symbol `read(mem, p)`. Two reads from the same memory at the
 * same address must give the same result, by congruence on read. This
 * is the entire story before you bring in the array axioms for writes,
 * so this example stops one step short of the McCarthy array theory --
 * but it already does interesting verification-flavoured work.
 *
 * We pose the question: if pointers p and q happen to be equal, can
 * the values at those addresses differ?
 *
 *     p = q
 *     read(mem, p) != read(mem, q)
 *
 * The theory unifies read(mem, p) and read(mem, q) by congruence on
 * `read` (its two arguments mem, p match mem, q via p = q), which
 * clashes with the asserted disequality.
 *
 * Then we add a second, harder case: a chain of pointer aliases.
 *
 *     p = q,  q = r,  read(mem, p) != read(mem, r)
 *
 * Transitivity on equality plus congruence on read both have to fire.
 */
#include "smt.h"
#include <stdio.h>

static void demo1(void) {
    SmtCtx *ctx = smt_new();
    int mem = smt_mk_const(ctx, "mem");
    int p   = smt_mk_const(ctx, "p");
    int q   = smt_mk_const(ctx, "q");

    int rp_args[] = { mem, p };
    int rq_args[] = { mem, q };
    int rp = smt_mk_app(ctx, "read", rp_args, 2);
    int rq = smt_mk_app(ctx, "read", rq_args, 2);

    smt_assert_eq (ctx, p,  q);
    smt_assert_neq(ctx, rp, rq);

    printf("  Case A:  p = q,  read(mem, p) != read(mem, q)\n");
    int r = smt_check(ctx);
    printf("    %s   (theory conflicts = %ld)\n",
        r == SMT_UNSAT ? "UNSAT" : "SAT??",
        smt_theory_conflicts(ctx));
    smt_free(ctx);
}

static void demo2(void) {
    SmtCtx *ctx = smt_new();
    int mem = smt_mk_const(ctx, "mem");
    int p   = smt_mk_const(ctx, "p");
    int q   = smt_mk_const(ctx, "q");
    int r   = smt_mk_const(ctx, "r");

    int rp_args[] = { mem, p };
    int rr_args[] = { mem, r };
    int rp = smt_mk_app(ctx, "read", rp_args, 2);
    int rr = smt_mk_app(ctx, "read", rr_args, 2);

    smt_assert_eq (ctx, p, q);
    smt_assert_eq (ctx, q, r);
    smt_assert_neq(ctx, rp, rr);

    printf("  Case B:  p = q,  q = r,  read(mem, p) != read(mem, r)\n");
    int rc = smt_check(ctx);
    printf("    %s   (theory conflicts = %ld)\n",
        rc == SMT_UNSAT ? "UNSAT" : "SAT??",
        smt_theory_conflicts(ctx));
    smt_free(ctx);
}

/* A satisfiable variant: different addresses, distinct reads allowed. */
static void demo3(void) {
    SmtCtx *ctx = smt_new();
    int mem = smt_mk_const(ctx, "mem");
    int p   = smt_mk_const(ctx, "p");
    int q   = smt_mk_const(ctx, "q");

    int rp_args[] = { mem, p };
    int rq_args[] = { mem, q };
    int rp = smt_mk_app(ctx, "read", rp_args, 2);
    int rq = smt_mk_app(ctx, "read", rq_args, 2);

    smt_assert_neq(ctx, p,  q);
    smt_assert_neq(ctx, rp, rq);

    printf("  Case C:  p != q,  read(mem, p) != read(mem, q)\n");
    int r = smt_check(ctx);
    printf("    %s   (no conflicts -- nothing to refute)\n",
        r == SMT_SAT ? "SAT" : "UNSAT??");
    smt_free(ctx);
}

int main(void) {
    printf("=== read/write as uninterpreted functions ===\n\n");
    demo1();
    printf("\n");
    demo2();
    printf("\n");
    demo3();
    return 0;
}
