nx_tstp_emit_test.nx source
↩ module page · 99 lines · 3832 B
1// nx_tstp_emit_test.nx -- TSTP proof serializer smoke.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_str.nx"
7import "nx_result.nx"
8import "nx_unify.nx"
9import "nx_resolution.nx"
10import "nx_tptp_symtab.nx"
11import "nx_tptp_emit.nx"
12import "nx_proof_log.nx"
13import "nx_tstp_emit.nx"
14
15const SYM_EQ: nx_int = 50
16
17func mk_unary(p_sym: nx_int, c_sym: nx_int) -> *Term {
18 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
19 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
20 return nx_term_app(p_sym, 1, arg)
21}
22
23func place(arr: *Clause, i: nx_int, src: *Clause) {
24 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
25 dest.n_lits = src.n_lits
26 dest.lits = src.lits
27}
28
29func main() -> nx_exit {
30 println("=== TSTP proof serializer smoke ===" as *u8)
31 var fails: nx_int = 0
32
33 // Build a 3-clause proof:
34 // c0 = {p(a)} input
35 // c1 = {~p(a)} input
36 // c2 = {} inference(resolution, [], [c0, c1])
37 let st: *TptpSymtab = nx_tptp_symtab_new()
38 let p_sym: nx_int = nx_tptp_symtab_intern(st, "p" as *u8)
39 let a_sym: nx_int = nx_tptp_symtab_intern(st, "a" as *u8)
40
41 let c0: *Clause = nx_clause_new()
42 let _r0: *NxResult = nx_clause_add(c0, nx_lit_make(NX_LIT_POS, mk_unary(p_sym, a_sym)))
43 let c1: *Clause = nx_clause_new()
44 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_NEG, mk_unary(p_sym, a_sym)))
45 let c2: *Clause = nx_clause_new() // empty
46
47 let clauses: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
48 place(clauses, 0, c0)
49 place(clauses, 1, c1)
50 place(clauses, 2, c2)
51
52 let log: *ProofLog = nx_proof_log_new(16)
53 let _i0: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
54 let _i1: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
55 let _i2: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_RES, 0, 1)
56
57 let buf: *u8 = sys_mmap(2048)
58 let pos: *nx_int = sys_mmap(8) as *nx_int
59 pos[0] = 0
60 let rc: nx_int = nx_tstp_emit_proof(clauses, 3, log, st, SYM_EQ, buf, pos, 2048)
61 buf[pos[0]] = 0 // null-terminate
62
63 print(" rc=" as *u8); print_i64(rc); print(" bytes=" as *u8); print_i64(pos[0]); println("" as *u8)
64 println(" output:" as *u8)
65 print(buf)
66
67 // ---------- Test 1: rc OK + nonzero bytes ------------------
68 if rc == 1 {
69 if pos[0] > 0 {
70 println(" 1. proof serialized OK PASS" as *u8)
71 } else { println(" 1. zero bytes FAIL" as *u8); fails = fails + 1 }
72 } else { println(" 1. rc != 1 FAIL" as *u8); fails = fails + 1 }
73
74 // ---------- Test 2: output contains "cnf(c0, axiom" ---------
75 let p_axiom: nx_int = nx_str_str(buf, "cnf(c0, axiom" as *u8)
76 if p_axiom >= 0 {
77 println(" 2. first clause emitted as axiom PASS" as *u8)
78 } else { println(" 2. missing axiom annotation FAIL" as *u8); fails = fails + 1 }
79
80 // ---------- Test 3: output contains inference(resolution, [], [c0, c1])
81 let p_inf: nx_int = nx_str_str(buf, "inference(resolution, [], [c0, c1])" as *u8)
82 if p_inf >= 0 {
83 println(" 3. inference annotation correct PASS" as *u8)
84 } else { println(" 3. inference missing/malformed FAIL" as *u8); fails = fails + 1 }
85
86 // ---------- Test 4: empty clause emitted as $false ----------
87 let p_false: nx_int = nx_str_str(buf, "$false" as *u8)
88 if p_false >= 0 {
89 println(" 4. empty clause -> $false PASS" as *u8)
90 } else { println(" 4. empty not emitted as $false FAIL" as *u8); fails = fails + 1 }
91
92 println("" as *u8)
93 if fails == 0 {
94 println("=== ALL 4 TSTP-emit tests PASS ===" as *u8)
95 return 0
96 }
97 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
98 return 1
99}