`nx_fmb_test.nx` source

↩ module page · 103 lines · 4558 B
1// nx_fmb_test.nx -- Finite Model Building smoke.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_unify.nx"
8import "nx_resolution.nx"
9import "nx_sat_solver.nx"
10import "nx_fmb.nx"
11
12const SYM_P: nx_int = 200
13const SYM_Q: nx_int = 201
14const VAR_X: nx_int = 0
15
16func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
17    let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
18    arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
19    return nx_term_app(p_sym, 1, arg)
20}
21
22func place(arr: *Clause, i: nx_int, src: *Clause) {
23    let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
24    dest.n_lits = src.n_lits
25    dest.lits = src.lits
26}
27
28func main() -> nx_exit {
29    println("=== Finite Model Building smoke ===" as *u8)
30    var fails: nx_int = 0
31
32    // ---------- Test 1: satisfiable single-clause set --------------
33    // {p(X)} -- this is satisfiable: any model where p(d) is true for
34    // each domain element d.  Domain size 1 should suffice.
35    let c1: *Clause = nx_clause_new()
36    let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
37
38    let in1: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
39    place(in1, 0, c1)
40
41    let size1: *nx_int = sys_mmap(8) as *nx_int
42    let v1: nx_int = nx_fmb_search(in1, 1, 5, size1)
43    print("  1. {p(X)} -> verdict=" as *u8); print(nx_fmb_verdict_name(v1)); print(" size=" as *u8); print_i64(size1[0]); println("" as *u8)
44    if v1 == NX_FMB_MODEL_FOUND {
45        if size1[0] == 1 { println("     model at domain size 1  PASS" as *u8) }
46        else { println("     unexpected size  FAIL" as *u8); fails = fails + 1 }
47    } else { println("     expected MODEL_FOUND  FAIL" as *u8); fails = fails + 1 }
48
49    // ---------- Test 2: unsat clause set  ------------------------
50    // {p(X)}, {~p(X)} -- ground at any size produces propositional
51    // p(d) and ~p(d), which is UNSAT.
52    let c2a: *Clause = nx_clause_new()
53    let _r2a: *NxResult = nx_clause_add(c2a, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
54    let c2b: *Clause = nx_clause_new()
55    let _r2b: *NxResult = nx_clause_add(c2b, nx_lit_make(NX_LIT_NEG, mk_p_var(SYM_P, VAR_X)))
56
57    let in2: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
58    place(in2, 0, c2a)
59    place(in2, 1, c2b)
60
61    let size2: *nx_int = sys_mmap(8) as *nx_int
62    let v2: nx_int = nx_fmb_search(in2, 2, 5, size2)
63    print("  2. {p(X)}, {~p(X)} -> " as *u8); print(nx_fmb_verdict_name(v2)); println("" as *u8)
64    if v2 == NX_FMB_NO_MODEL {
65        println("     correctly identified as unsatisfiable  PASS" as *u8)
66    } else { println("     expected NO_MODEL  FAIL" as *u8); fails = fails + 1 }
67
68    // ---------- Test 3: requires domain size >= 2 ----------------
69    // {p(X) | q(X)}, {~p(X)}, {~q(X)} but with fresh vars per clause
70    // is unsat at size 1.  Skip -- our subst mechanism uses one
71    // var-id space across clauses, so this would behave differently.
72    // Test 3 instead: model exists trivially.
73    let c3: *Clause = nx_clause_new()
74    let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
75    let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
76
77    let in3: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
78    place(in3, 0, c3)
79
80    let size3: *nx_int = sys_mmap(8) as *nx_int
81    let v3: nx_int = nx_fmb_search(in3, 1, 3, size3)
82    print("  3. {p(X) | q(X)} -> " as *u8); print(nx_fmb_verdict_name(v3)); print(" size=" as *u8); print_i64(size3[0]); println("" as *u8)
83    if v3 == NX_FMB_MODEL_FOUND {
84        println("     disjunction satisfiable  PASS" as *u8)
85    } else { println("     expected MODEL_FOUND  FAIL" as *u8); fails = fails + 1 }
86
87    // ---------- Test 4: empty clause set is trivially SAT --------
88    let in4: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
89    let size4: *nx_int = sys_mmap(8) as *nx_int
90    let v4: nx_int = nx_fmb_search(in4, 0, 3, size4)
91    print("  4. {} (empty input) -> " as *u8); print(nx_fmb_verdict_name(v4)); println("" as *u8)
92    if v4 == NX_FMB_MODEL_FOUND {
93        println("     trivially satisfiable  PASS" as *u8)
94    } else { println("     expected MODEL_FOUND  FAIL" as *u8); fails = fails + 1 }
95
96    println("" as *u8)
97    if fails == 0 {
98        println("=== ALL 4 FMB tests PASS ===" as *u8)
99        return 0
100    }
101    print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
102    return 1
103}
nx_fmb_test.nx source

`nx_fmb_test.nx` source
