nx_avatar_encode_test.nx source
↩ module page · 119 lines · 5086 B
1// nx_avatar_encode_test.nx -- AVATAR encoder 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_clause_components.nx"
10import "nx_avatar_split.nx"
11import "nx_sat_solver.nx"
12import "nx_avatar_encode.nx"
13
14const SYM_A: nx_int = 100
15const SYM_B: nx_int = 101
16const SYM_P: nx_int = 200
17const SYM_Q: nx_int = 201
18const VAR_X: nx_int = 0
19const VAR_Y: nx_int = 1
20
21func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
22 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
23 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
24 return nx_term_app(p_sym, 1, arg)
25}
26
27func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
28 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
29 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
30 return nx_term_app(p_sym, 1, arg)
31}
32
33func place(arr: *Clause, i: nx_int, src: *Clause) {
34 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
35 dest.n_lits = src.n_lits
36 dest.lits = src.lits
37}
38
39func main() -> nx_exit {
40 println("=== AVATAR encoder smoke ===" as *u8)
41 var fails: nx_int = 0
42
43 // Inputs:
44 // c0 = {p(a)} single-component: pass-through
45 // c1 = {p(X), q(Y)} 2-component: encoded with 2 split atoms
46 let in_set: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
47 let c0: *Clause = nx_clause_new()
48 let _r0: *NxResult = nx_clause_add(c0, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
49 place(in_set, 0, c0)
50
51 let c1: *Clause = nx_clause_new()
52 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
53 let _r1b: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_Y)))
54 place(in_set, 1, c1)
55
56 let fo_out: *Clause = (sys_mmap((20 * NX_CLAUSE_BYTES) as i64)) as *Clause
57 let sat_formula: *SatFormula = nx_sat_alloc(64)
58 let next_sp: *nx_int = sys_mmap(8) as *nx_int
59
60 let n_fo: nx_int = nx_avatar_encode_to_sat(in_set, 2, 1,
61 fo_out, 20,
62 sat_formula,
63 next_sp)
64
65 print(" encoded n_fo=" as *u8); print_i64(n_fo)
66 print(" n_sat_clauses=" as *u8); print_i64(sat_formula.n_clauses)
67 print(" next_sp=" as *u8); print_i64(next_sp[0]); println("" as *u8)
68
69 // ---------- Test 1: 3 FO clauses (1 pass-through + 2 components)
70 if n_fo == 3 { println(" 1. n_fo == 3 (1 + 2 components) PASS" as *u8) }
71 else { println(" 1. wrong n_fo FAIL" as *u8); fails = fails + 1 }
72
73 // ---------- Test 2: 1 SAT coordination clause --------------
74 if sat_formula.n_clauses == 1 {
75 println(" 2. 1 SAT coordination clause PASS" as *u8)
76 } else { println(" 2. wrong sat count FAIL" as *u8); fails = fails + 1 }
77
78 // ---------- Test 3: 2 split atoms allocated ----------------
79 if next_sp[0] == 3 {
80 // sp_base = 1, allocated 2 -> next is 3
81 println(" 3. allocated 2 split atoms (sp_1, sp_2) PASS" as *u8)
82 } else { print(" 3. next_sp=" as *u8); print_i64(next_sp[0]); println(" FAIL" as *u8); fails = fails + 1 }
83
84 // ---------- Test 4: pass-through clause unchanged -----------
85 let pt: *Clause = fo_out
86 if pt.n_lits == 1 {
87 let l: *Literal = nx_clause_lit_at(pt, 0)
88 if l.atom.sym == SYM_P {
89 println(" 4. {p(a)} pass-through preserved PASS" as *u8)
90 } else { println(" 4. wrong head FAIL" as *u8); fails = fails + 1 }
91 } else { println(" 4. wrong n_lits FAIL" as *u8); fails = fails + 1 }
92
93 // ---------- Test 5: guarded component clause shape --------
94 // Second emitted FO clause should be {~sp_1, p(X)}.
95 let gc1: *Clause = ((fo_out as nx_int) + NX_CLAUSE_BYTES) as *Clause
96 if gc1.n_lits == 2 {
97 let guard: *Literal = nx_clause_lit_at(gc1, 0)
98 if guard.sign == NX_LIT_NEG {
99 if guard.atom.sym >= NX_AVATAR_SP_BASE_SYM {
100 println(" 5. component clause prefixed with ~sp guard PASS" as *u8)
101 } else { println(" 5. guard sym not in sp range FAIL" as *u8); fails = fails + 1 }
102 } else { println(" 5. guard not NEG FAIL" as *u8); fails = fails + 1 }
103 } else { print(" 5. n_lits=" as *u8); print_i64(gc1.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
104
105 // ---------- Test 6: SAT clause is satisfiable --------------
106 // sat_formula has [sp_1, sp_2] -- simply assign both true; SAT.
107 let sat_v: nx_int = nx_sat_solve(sat_formula)
108 if sat_v == NX_SAT_SAT {
109 println(" 6. SAT clause [sp1, sp2] solves SAT PASS" as *u8)
110 } else { print(" 6. SAT verdict=" as *u8); print_i64(sat_v); println(" FAIL" as *u8); fails = fails + 1 }
111
112 println("" as *u8)
113 if fails == 0 {
114 println("=== ALL 6 AVATAR-encoder tests PASS ===" as *u8)
115 return 0
116 }
117 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
118 return 1
119}