nx_tptp_formula_test.nx source
↩ module page · 200 lines · 8151 B
1// nx_tptp_formula_test.nx -- TPTP CNF parser smoke + end-to-end
2// parse-then-saturate verification.
3
4import "nx_syscalls.nx"
5import "nx_runtime.nx"
6import "nx_tier.nx"
7import "nx_str.nx"
8import "nx_result.nx"
9import "nx_unify.nx"
10import "nx_resolution.nx"
11import "nx_subsumption.nx"
12import "nx_tautology.nx"
13import "nx_saturation.nx"
14import "nx_tptp_symtab.nx"
15import "nx_tptp_term.nx"
16import "nx_tptp_formula.nx"
17
18// Reserve eq_sym below NX_TPTP_SYM_BASE so it doesn't clash with
19// parser-allocated symbol ids.
20const SYM_EQ: nx_int = 50
21
22// Allocate a writable buffer holding the literal contents of `s` plus
23// trailing nul. Needed because string literals are read-only and the
24// parsers expect *u8 they can index over a known length.
25func mk_input(s: *u8) -> *u8 {
26 let len: nx_int = nx_str_len(s)
27 let buf: *u8 = sys_mmap((len + 1) as i64)
28 var i: nx_int = 0
29 while i < len {
30 buf[i] = s[i]
31 i = i + 1
32 }
33 buf[len] = 0
34 return buf
35}
36
37func main() -> nx_exit {
38 println("=== TPTP CNF formula parser smoke ===" as *u8)
39 var fails: nx_int = 0
40
41 // ---------- Test 1: parse a single term ---------------------
42 // "f(a, X)" -- APP with sym=interned(f), 2 args [const(a), var(X)]
43 let st1: *TptpSymtab = nx_tptp_symtab_new()
44 let buf1: *u8 = mk_input("f(a, X)" as *u8)
45 let len1: nx_int = nx_str_len("f(a, X)" as *u8)
46 let pos1: *nx_int = sys_mmap(8) as *nx_int
47 pos1[0] = 0
48 let t1: *Term = nx_tptp_parse_term(buf1, len1, pos1, st1)
49 if (t1 as nx_int) == 0 {
50 println("1. parse f(a, X) -> NULL FAIL" as *u8); fails = fails + 1
51 } else {
52 if t1.kind == NX_TERM_APP {
53 if t1.n_args == 2 {
54 let arg0: *Term = nx_term_arg(t1, 0)
55 let arg1: *Term = nx_term_arg(t1, 1)
56 if arg0.kind == NX_TERM_CONST {
57 if arg1.kind == NX_TERM_VAR {
58 println("1. parse f(a, X) -> APP[CONST, VAR] PASS" as *u8)
59 } else {
60 println("1. parse f(a, X) -> arg1 not VAR FAIL" as *u8); fails = fails + 1
61 }
62 } else {
63 println("1. parse f(a, X) -> arg0 not CONST FAIL" as *u8); fails = fails + 1
64 }
65 } else {
66 print("1. parse f(a, X) -> n_args=" as *u8); print_i64(t1.n_args); println(" FAIL" as *u8); fails = fails + 1
67 }
68 } else {
69 println("1. parse f(a, X) -> not APP FAIL" as *u8); fails = fails + 1
70 }
71 }
72
73 // ---------- Test 2: parse a negative literal "~p(X)" ----------
74 let st2: *TptpSymtab = nx_tptp_symtab_new()
75 let buf2: *u8 = mk_input("~p(X)" as *u8)
76 let len2: nx_int = nx_str_len("~p(X)" as *u8)
77 let pos2: *nx_int = sys_mmap(8) as *nx_int
78 pos2[0] = 0
79 let l2: *Literal = nx_tptp_parse_literal(buf2, len2, pos2, st2, SYM_EQ)
80 if (l2 as nx_int) == 0 {
81 println("2. parse ~p(X) -> NULL FAIL" as *u8); fails = fails + 1
82 } else {
83 if l2.sign == NX_LIT_NEG {
84 if l2.atom.kind == NX_TERM_APP {
85 println("2. parse ~p(X) -> NEG APP PASS" as *u8)
86 } else {
87 println("2. parse ~p(X) -> atom not APP FAIL" as *u8); fails = fails + 1
88 }
89 } else {
90 println("2. parse ~p(X) -> sign != NEG FAIL" as *u8); fails = fails + 1
91 }
92 }
93
94 // ---------- Test 3: parse a 2-literal clause ------------------
95 let st3: *TptpSymtab = nx_tptp_symtab_new()
96 let buf3: *u8 = mk_input("p(a) | ~q(b)" as *u8)
97 let len3: nx_int = nx_str_len("p(a) | ~q(b)" as *u8)
98 let pos3: *nx_int = sys_mmap(8) as *nx_int
99 pos3[0] = 0
100 nx_tptp_symtab_reset_vars(st3)
101 let c3: *Clause = nx_tptp_parse_cnf_clause(buf3, len3, pos3, st3, SYM_EQ)
102 if (c3 as nx_int) == 0 {
103 println("3. parse p(a)|~q(b) -> NULL FAIL" as *u8); fails = fails + 1
104 } else {
105 if c3.n_lits == 2 {
106 println("3. parse p(a)|~q(b) -> 2 literals PASS" as *u8)
107 } else {
108 print("3. parse p(a)|~q(b) -> n_lits=" as *u8); print_i64(c3.n_lits); println(" FAIL" as *u8); fails = fails + 1
109 }
110 }
111
112 // ---------- Test 4: parse equality "f(X) = g(Y)" --------------
113 let st4: *TptpSymtab = nx_tptp_symtab_new()
114 let buf4: *u8 = mk_input("f(X) = g(Y)" as *u8)
115 let len4: nx_int = nx_str_len("f(X) = g(Y)" as *u8)
116 let pos4: *nx_int = sys_mmap(8) as *nx_int
117 pos4[0] = 0
118 nx_tptp_symtab_reset_vars(st4)
119 let c4: *Clause = nx_tptp_parse_cnf_clause(buf4, len4, pos4, st4, SYM_EQ)
120 if (c4 as nx_int) == 0 {
121 println("4. parse f(X)=g(Y) -> NULL FAIL" as *u8); fails = fails + 1
122 } else {
123 if c4.n_lits == 1 {
124 let l4: *Literal = nx_clause_lit_at(c4, 0)
125 if l4.sign == NX_LIT_POS {
126 if l4.atom.sym == SYM_EQ {
127 if l4.atom.n_args == 2 {
128 println("4. parse f(X)=g(Y) -> POS eq(., .) PASS" as *u8)
129 } else { println("4. eq arity wrong FAIL" as *u8); fails = fails + 1 }
130 } else { println("4. eq sym wrong FAIL" as *u8); fails = fails + 1 }
131 } else { println("4. eq sign wrong FAIL" as *u8); fails = fails + 1 }
132 } else {
133 print("4. parse f(X)=g(Y) -> n_lits=" as *u8); print_i64(c4.n_lits); println(" FAIL" as *u8); fails = fails + 1
134 }
135 }
136
137 // ---------- Test 5: parse inequality "a != b" -- NEG eq -------
138 let st5: *TptpSymtab = nx_tptp_symtab_new()
139 let buf5: *u8 = mk_input("a != b" as *u8)
140 let len5: nx_int = nx_str_len("a != b" as *u8)
141 let pos5: *nx_int = sys_mmap(8) as *nx_int
142 pos5[0] = 0
143 nx_tptp_symtab_reset_vars(st5)
144 let c5: *Clause = nx_tptp_parse_cnf_clause(buf5, len5, pos5, st5, SYM_EQ)
145 if (c5 as nx_int) == 0 {
146 println("5. parse a != b -> NULL FAIL" as *u8); fails = fails + 1
147 } else {
148 let l5: *Literal = nx_clause_lit_at(c5, 0)
149 if l5.sign == NX_LIT_NEG {
150 if l5.atom.sym == SYM_EQ {
151 println("5. parse a != b -> NEG eq(a, b) PASS" as *u8)
152 } else { println("5. != sym wrong FAIL" as *u8); fails = fails + 1 }
153 } else { println("5. != sign not NEG FAIL" as *u8); fails = fails + 1 }
154 }
155
156 // ---------- Test 6: end-to-end parse + discount UNSAT --------
157 // Two clauses parsed from text, fed to discount loop.
158 // Same symtab across both so 'p' and 'a' get matching sym_ids.
159 let st6: *TptpSymtab = nx_tptp_symtab_new()
160
161 let bufA: *u8 = mk_input("p(a)" as *u8)
162 let lenA: nx_int = nx_str_len("p(a)" as *u8)
163 let posA: *nx_int = sys_mmap(8) as *nx_int
164 posA[0] = 0
165 nx_tptp_symtab_reset_vars(st6)
166 let cA: *Clause = nx_tptp_parse_cnf_clause(bufA, lenA, posA, st6, SYM_EQ)
167
168 let bufB: *u8 = mk_input("~p(a)" as *u8)
169 let lenB: nx_int = nx_str_len("~p(a)" as *u8)
170 let posB: *nx_int = sys_mmap(8) as *nx_int
171 posB[0] = 0
172 nx_tptp_symtab_reset_vars(st6)
173 let cB: *Clause = nx_tptp_parse_cnf_clause(bufB, lenB, posB, st6, SYM_EQ)
174
175 if (cA as nx_int) == 0 {
176 println("6. end-to-end -> parse {p(a)} failed FAIL" as *u8); fails = fails + 1
177 } else {
178 if (cB as nx_int) == 0 {
179 println("6. end-to-end -> parse {~p(a)} failed FAIL" as *u8); fails = fails + 1
180 } else {
181 let s6: *Saturation = nx_saturation_new(50)
182 let _u6a: *NxResult = nx_sat_add_unproc(s6, cA)
183 let _u6b: *NxResult = nx_sat_add_unproc(s6, cB)
184 let v6: nx_int = nx_sat_run_discount(s6, SYM_EQ)
185 if v6 == NX_SAT_VERDICT_UNSAT {
186 println("6. end-to-end parse + discount -> UNSAT PASS" as *u8)
187 } else {
188 print("6. end-to-end -> verdict=" as *u8); print_i64(v6); println(" FAIL" as *u8); fails = fails + 1
189 }
190 }
191 }
192
193 println("" as *u8)
194 if fails == 0 {
195 println("=== ALL 6 TPTP CNF parser tests PASS ===" as *u8)
196 return 0
197 }
198 print("=== " as *u8); print_i64(fails); println(" parser tests FAILED ===" as *u8)
199 return 1
200}