nx_fof_cnf_test.nx source
↩ module page · 170 lines · 7623 B
1// nx_fof_cnf_test.nx -- FOF -> CNF pipeline smoke + end-to-end
2// FOF -> discount-loop UNSAT.
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_fof.nx"
17import "nx_fof_parse.nx"
18import "nx_fof_cnf.nx"
19
20const SYM_EQ: nx_int = 50
21const NX_FOF_CLAUSE_CAP: nx_int = 16
22
23func mk_input(s: *u8) -> *u8 {
24 let len: nx_int = nx_str_len(s)
25 let buf: *u8 = sys_mmap((len + 1) as i64)
26 var i: nx_int = 0
27 while i < len { buf[i] = s[i]; i = i + 1 }
28 buf[len] = 0
29 return buf
30}
31
32func parse(input: *u8, st: *TptpSymtab) -> *Fof {
33 let len: nx_int = nx_str_len(input)
34 let buf: *u8 = mk_input(input)
35 let pos: *nx_int = sys_mmap(8) as *nx_int
36 pos[0] = 0
37 return nx_fof_parse(buf, len, pos, st, SYM_EQ)
38}
39
40func main() -> nx_exit {
41 println("=== FOF -> CNF pipeline smoke ===" as *u8)
42 var fails: nx_int = 0
43
44 // ---------- Test 1: IFF elimination --------------------------
45 // p <=> q -> (p => q) & (q => p)
46 let st1: *TptpSymtab = nx_tptp_symtab_new()
47 let f1: *Fof = parse("p(a) <=> q(a)" as *u8, st1)
48 let f1e: *Fof = nx_fof_elim_iff(f1)
49 if f1e.kind == NX_FOF_AND {
50 if f1e.left.kind == NX_FOF_IMP {
51 println("1. IFF elim p<=>q -> AND(IMP, IMP) PASS" as *u8)
52 } else { println("1. left not IMP FAIL" as *u8); fails = fails + 1 }
53 } else { println("1. top not AND FAIL" as *u8); fails = fails + 1 }
54
55 // ---------- Test 2: IMP elimination --------------------------
56 // p => q -> ~p | q
57 let st2: *TptpSymtab = nx_tptp_symtab_new()
58 let f2: *Fof = parse("p(a) => q(a)" as *u8, st2)
59 let f2e: *Fof = nx_fof_elim_imp(f2)
60 if f2e.kind == NX_FOF_OR {
61 if f2e.left.kind == NX_FOF_NEG {
62 println("2. IMP elim p=>q -> OR(NEG, q) PASS" as *u8)
63 } else { println("2. left not NEG FAIL" as *u8); fails = fails + 1 }
64 } else { println("2. top not OR FAIL" as *u8); fails = fails + 1 }
65
66 // ---------- Test 3: NNF (De Morgan + double-neg) --------------
67 // ~~p -> p
68 let st3: *TptpSymtab = nx_tptp_symtab_new()
69 let f3: *Fof = parse("~~p(a)" as *u8, st3)
70 let f3n: *Fof = nx_fof_to_nnf(f3)
71 if f3n.kind == NX_FOF_ATOM {
72 println("3. NNF ~~p -> ATOM PASS" as *u8)
73 } else { print("3. kind=" as *u8); print_i64(f3n.kind); println(" FAIL" as *u8); fails = fails + 1 }
74
75 // ---------- Test 4: NNF (push NEG over AND) -------------------
76 // ~(p & q) -> ~p | ~q
77 let st4: *TptpSymtab = nx_tptp_symtab_new()
78 let f4: *Fof = parse("~(p(a) & q(a))" as *u8, st4)
79 let f4n: *Fof = nx_fof_to_nnf(f4)
80 if f4n.kind == NX_FOF_OR {
81 if f4n.left.kind == NX_FOF_NEG {
82 if f4n.right.kind == NX_FOF_NEG {
83 println("4. NNF ~(p&q) -> OR(NEG, NEG) PASS" as *u8)
84 } else { println("4. right not NEG FAIL" as *u8); fails = fails + 1 }
85 } else { println("4. left not NEG FAIL" as *u8); fails = fails + 1 }
86 } else { println("4. top not OR FAIL" as *u8); fails = fails + 1 }
87
88 // ---------- Test 5: Skolemize (no universals -> constant) ----
89 // ?[X]: p(X) -> p(sk_0)
90 let st5: *TptpSymtab = nx_tptp_symtab_new()
91 let f5: *Fof = parse("?[X]: p(X)" as *u8, st5)
92 let f5n: *Fof = nx_fof_to_nnf(f5)
93 let f5s: *Fof = nx_fof_skolemize(f5n)
94 // Result should be ATOM with p as head and a constant arg.
95 if f5s.kind == NX_FOF_ATOM {
96 let arg: *Term = nx_term_arg(f5s.atom, 0)
97 if arg.kind == NX_TERM_CONST {
98 if arg.sym >= NX_TPTP_SK_BASE {
99 println("5. Skolemize ?[X]:p(X) -> p(sk_const) PASS" as *u8)
100 } else { println("5. sk sym not in SK_BASE range FAIL" as *u8); fails = fails + 1 }
101 } else { println("5. Skolem arg not CONST FAIL" as *u8); fails = fails + 1 }
102 } else { print("5. kind=" as *u8); print_i64(f5s.kind); println(" FAIL" as *u8); fails = fails + 1 }
103
104 // ---------- Test 6: Skolemize with universal in scope --------
105 // ![Y]: ?[X]: p(X, Y) -> ![Y]: p(sk_0(Y), Y)
106 let st6: *TptpSymtab = nx_tptp_symtab_new()
107 let f6: *Fof = parse("![Y]: ?[X]: p(X, Y)" as *u8, st6)
108 let f6s: *Fof = nx_fof_skolemize(nx_fof_to_nnf(f6))
109 // Top should be FORALL, body ATOM with p(sk_app(Y), Y).
110 if f6s.kind == NX_FOF_FORALL {
111 if f6s.left.kind == NX_FOF_ATOM {
112 let p_atom: *Term = f6s.left.atom
113 let arg0: *Term = nx_term_arg(p_atom, 0)
114 if arg0.kind == NX_TERM_APP {
115 if arg0.sym >= NX_TPTP_SK_BASE {
116 if arg0.n_args == 1 {
117 println("6. Skolemize ![Y]?[X]:p(X,Y) -> sk_fn(Y) PASS" as *u8)
118 } else { print("6. sk arity=" as *u8); print_i64(arg0.n_args); println(" FAIL" as *u8); fails = fails + 1 }
119 } else { println("6. sk sym not in range FAIL" as *u8); fails = fails + 1 }
120 } else { println("6. arg0 not APP FAIL" as *u8); fails = fails + 1 }
121 } else { println("6. body not ATOM FAIL" as *u8); fails = fails + 1 }
122 } else { print("6. top kind=" as *u8); print_i64(f6s.kind); println(" FAIL" as *u8); fails = fails + 1 }
123
124 // ---------- Test 7: end-to-end FOF -> CNF -> UNSAT -----------
125 // (p & ~p) -- propositional contradiction; CNF should be {p}, {~p}.
126 let st7: *TptpSymtab = nx_tptp_symtab_new()
127 let f7: *Fof = parse("p(a) & ~p(a)" as *u8, st7)
128 let clauses: *Clause = (sys_mmap((NX_FOF_CLAUSE_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
129 let n_out: *nx_int = sys_mmap(8) as *nx_int
130 n_out[0] = 0
131 let rc: nx_int = nx_fof_to_cnf(f7, clauses, n_out, NX_FOF_CLAUSE_CAP)
132 if rc != 0 {
133 println("7. fof_to_cnf rc != 0 FAIL" as *u8); fails = fails + 1
134 } else {
135 if n_out[0] == 2 {
136 // Feed to discount loop.
137 let s: *Saturation = nx_saturation_new(50)
138 var i: nx_int = 0
139 while i < n_out[0] {
140 let c: *Clause = ((clauses as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
141 let _u: *NxResult = nx_sat_add_unproc(s, c)
142 i = i + 1
143 }
144 let v: nx_int = nx_sat_run_discount(s, SYM_EQ)
145 if v == NX_SAT_VERDICT_UNSAT {
146 println("7. (p&~p) -> CNF -> discount -> UNSAT PASS" as *u8)
147 } else { print("7. verdict=" as *u8); print_i64(v); println(" FAIL" as *u8); fails = fails + 1 }
148 } else { print("7. n_clauses=" as *u8); print_i64(n_out[0]); println(" FAIL" as *u8); fails = fails + 1 }
149 }
150
151 // ---------- Test 8: distribute -- (a & b) | c -> (a|c) & (b|c)
152 let st8: *TptpSymtab = nx_tptp_symtab_new()
153 let f8: *Fof = parse("(p(a) & q(a)) | r(a)" as *u8, st8)
154 let f8d: *Fof = nx_fof_distribute_step(nx_fof_to_nnf(nx_fof_elim_imp(nx_fof_elim_iff(f8))))
155 if f8d.kind == NX_FOF_AND {
156 if f8d.left.kind == NX_FOF_OR {
157 if f8d.right.kind == NX_FOF_OR {
158 println("8. distribute (p&q)|r -> AND(OR, OR) PASS" as *u8)
159 } else { println("8. right not OR FAIL" as *u8); fails = fails + 1 }
160 } else { println("8. left not OR FAIL" as *u8); fails = fails + 1 }
161 } else { println("8. top not AND FAIL" as *u8); fails = fails + 1 }
162
163 println("" as *u8)
164 if fails == 0 {
165 println("=== ALL 8 FOF->CNF tests PASS ===" as *u8)
166 return 0
167 }
168 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
169 return 1
170}