nx_tautology_test.nx source
↩ module page · 108 lines · 5045 B
1// nx_tautology_test.nx -- syntactic-tautology 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_tautology.nx"
10
11const SYM_A: nx_int = 100
12const SYM_B: nx_int = 101
13const SYM_P: nx_int = 200
14const SYM_Q: nx_int = 201
15const SYM_EQ: nx_int = 50 // reserved for "="
16
17// Build atom p(c) for some constant.
18func mk_p_const(p_sym: nx_int, c_sym: nx_int) -> *Term {
19 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
20 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
21 return nx_term_app(p_sym, 1, arg)
22}
23
24// Build eq(t1, t2).
25func mk_eq(t1: *Term, t2: *Term) -> *Term {
26 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
27 let a0: *Term = args
28 a0.kind = t1.kind; a0.sym = t1.sym; a0.n_args = t1.n_args; a0.args = t1.args
29 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
30 a1.kind = t2.kind; a1.sym = t2.sym; a1.n_args = t2.n_args; a1.args = t2.args
31 return nx_term_app(SYM_EQ, 2, args)
32}
33
34func report(name: *u8, expected: nx_int, actual: nx_int) -> nx_int {
35 print(" " as *u8); print(name); print(" -> " as *u8)
36 print(nx_tautology_verdict_name(actual))
37 if actual == expected { println(" PASS" as *u8); return 0 }
38 print(" (expected " as *u8); print(nx_tautology_verdict_name(expected)); println(") FAIL" as *u8)
39 return 1
40}
41
42func main() -> nx_exit {
43 println("=== Tautology detection smoke ===" as *u8)
44 var fails: nx_int = 0
45
46 // ---------- Test 1: ordinary clause, not a tautology --------
47 // {p(a), q(b)}
48 let c1: *Clause = nx_clause_new()
49 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_P, SYM_A)))
50 let _r1b: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_Q, SYM_B)))
51 fails = fails + report("1. {p(a), q(b)}" as *u8, NX_NOT_TAUTOLOGY, nx_is_tautology(c1, SYM_EQ))
52
53 // ---------- Test 2: propositional pair -----------------------
54 // {p(a), ~p(a)}
55 let c2: *Clause = nx_clause_new()
56 let _r2a: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_P, SYM_A)))
57 let _r2b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_NEG, mk_p_const(SYM_P, SYM_A)))
58 fails = fails + report("2. {p(a), ~p(a)}" as *u8, NX_TAUTOLOGY, nx_is_tautology(c2, SYM_EQ))
59
60 // ---------- Test 3: opposite-sign but DIFFERENT atoms ---------
61 // {p(a), ~p(b)} -- not a tautology (atoms differ)
62 let c3: *Clause = nx_clause_new()
63 let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_P, SYM_A)))
64 let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_NEG, mk_p_const(SYM_P, SYM_B)))
65 fails = fails + report("3. {p(a), ~p(b)}" as *u8, NX_NOT_TAUTOLOGY, nx_is_tautology(c3, SYM_EQ))
66
67 // ---------- Test 4: reflexive equality -----------------------
68 // {eq(a, a)}
69 let c4: *Clause = nx_clause_new()
70 let _r4: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS,
71 mk_eq(nx_term_const(SYM_A), nx_term_const(SYM_A))))
72 fails = fails + report("4. {eq(a, a)}" as *u8, NX_TAUTOLOGY, nx_is_tautology(c4, SYM_EQ))
73
74 // ---------- Test 5: non-reflexive equality -------------------
75 // {eq(a, b)} -- not a tautology (a != b syntactically)
76 let c5: *Clause = nx_clause_new()
77 let _r5: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS,
78 mk_eq(nx_term_const(SYM_A), nx_term_const(SYM_B))))
79 fails = fails + report("5. {eq(a, b)}" as *u8, NX_NOT_TAUTOLOGY, nx_is_tautology(c5, SYM_EQ))
80
81 // ---------- Test 6: pair found at non-adjacent positions ------
82 // {p(a), q(b), ~p(a)} -- pair at indices 0 and 2
83 let c6: *Clause = nx_clause_new()
84 let _r6a: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_P, SYM_A)))
85 let _r6b: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_Q, SYM_B)))
86 let _r6c: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_NEG, mk_p_const(SYM_P, SYM_A)))
87 fails = fails + report("6. {p(a), q(b), ~p(a)}" as *u8, NX_TAUTOLOGY, nx_is_tautology(c6, SYM_EQ))
88
89 // ---------- Test 7: empty clause is NOT a tautology -----------
90 // {} -- this is the contradiction (UNSAT witness), not a tautology
91 let c7: *Clause = nx_clause_new()
92 fails = fails + report("7. {} (empty clause)" as *u8, NX_NOT_TAUTOLOGY, nx_is_tautology(c7, SYM_EQ))
93
94 // ---------- Test 8: NEGATIVE eq(t, t) is NOT a tautology ------
95 // {~eq(a, a)} -- contradiction, NOT a tautology
96 let c8: *Clause = nx_clause_new()
97 let _r8: *NxResult = nx_clause_add(c8, nx_lit_make(NX_LIT_NEG,
98 mk_eq(nx_term_const(SYM_A), nx_term_const(SYM_A))))
99 fails = fails + report("8. {~eq(a, a)}" as *u8, NX_NOT_TAUTOLOGY, nx_is_tautology(c8, SYM_EQ))
100
101 println("" as *u8)
102 if fails == 0 {
103 println("=== ALL 8 tautology tests PASS ===" as *u8)
104 return 0
105 }
106 print("=== " as *u8); print_i64(fails); println(" tautology tests FAILED ===" as *u8)
107 return 1
108}