nx_fof_tseitin_test.nx source
↩ module page · 146 lines · 6256 B
1// nx_fof_tseitin_test.nx -- Tseitin transformation 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_subsumption.nx"
11import "nx_tautology.nx"
12import "nx_saturation.nx"
13import "nx_tptp_symtab.nx"
14import "nx_tptp_term.nx"
15import "nx_fof.nx"
16import "nx_fof_parse.nx"
17import "nx_fof_cnf.nx"
18import "nx_fof_tseitin.nx"
19
20const SYM_EQ: nx_int = 50
21const NX_TS_CAP: nx_int = 64
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_to_nnf(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 let f: *Fof = nx_fof_parse(buf, len, pos, st, SYM_EQ)
38 if (f as nx_int) == 0 { return 0 as *Fof }
39 return nx_fof_drop_forall(nx_fof_skolemize(nx_fof_to_nnf(nx_fof_elim_imp(nx_fof_elim_iff(f)))))
40}
41
42func main() -> nx_exit {
43 println("=== Tseitin transformation smoke ===" as *u8)
44 var fails: nx_int = 0
45
46 // ---------- Test 1: bare ATOM produces unit clause -----------
47 // p(a) -> one unit clause {p(a)}
48 let st1: *TptpSymtab = nx_tptp_symtab_new()
49 let f1: *Fof = parse_to_nnf("p(a)" as *u8, st1)
50 let out1: *Clause = (sys_mmap((NX_TS_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
51 let n1: *nx_int = sys_mmap(8) as *nx_int
52 n1[0] = 0
53 let _r1: nx_int = nx_fof_to_cnf_tseitin(f1, out1, n1, NX_TS_CAP)
54 print(" 1. p(a) -> n_clauses=" as *u8); print_i64(n1[0]); println("" as *u8)
55 if n1[0] == 1 {
56 println(" single unit clause PASS" as *u8)
57 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
58
59 // ---------- Test 2: ~p(a) produces unit clause with NEG ------
60 let st2: *TptpSymtab = nx_tptp_symtab_new()
61 let f2: *Fof = parse_to_nnf("~p(a)" as *u8, st2)
62 let out2: *Clause = (sys_mmap((NX_TS_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
63 let n2: *nx_int = sys_mmap(8) as *nx_int
64 n2[0] = 0
65 let _r2: nx_int = nx_fof_to_cnf_tseitin(f2, out2, n2, NX_TS_CAP)
66 if n2[0] == 1 {
67 let c: *Clause = out2
68 let l: *Literal = nx_clause_lit_at(c, 0)
69 if l.sign == NX_LIT_NEG {
70 println(" 2. ~p(a) -> 1 unit clause NEG PASS" as *u8)
71 } else { println(" 2. sign not NEG FAIL" as *u8); fails = fails + 1 }
72 } else { print(" 2. n=" as *u8); print_i64(n2[0]); println(" FAIL" as *u8); fails = fails + 1 }
73
74 // ---------- Test 3: AND emits 4 clauses (3 def + 1 unit) ------
75 // p & q -> fresh r; (~r ∨ p)(~r ∨ q)(r ∨ ~p ∨ ~q) + unit (r)
76 let st3: *TptpSymtab = nx_tptp_symtab_new()
77 let f3: *Fof = parse_to_nnf("p(a) & q(a)" as *u8, st3)
78 let out3: *Clause = (sys_mmap((NX_TS_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
79 let n3: *nx_int = sys_mmap(8) as *nx_int
80 n3[0] = 0
81 let _r3: nx_int = nx_fof_to_cnf_tseitin(f3, out3, n3, NX_TS_CAP)
82 print(" 3. p(a) & q(a) -> n_clauses=" as *u8); print_i64(n3[0]); println("" as *u8)
83 if n3[0] == 4 {
84 println(" 3 def + 1 unit PASS" as *u8)
85 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
86
87 // ---------- Test 4: OR also emits 4 -------------------------
88 let st4: *TptpSymtab = nx_tptp_symtab_new()
89 let f4: *Fof = parse_to_nnf("p(a) | q(a)" as *u8, st4)
90 let out4: *Clause = (sys_mmap((NX_TS_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
91 let n4: *nx_int = sys_mmap(8) as *nx_int
92 n4[0] = 0
93 let _r4: nx_int = nx_fof_to_cnf_tseitin(f4, out4, n4, NX_TS_CAP)
94 print(" 4. p(a) | q(a) -> n_clauses=" as *u8); print_i64(n4[0]); println("" as *u8)
95 if n4[0] == 4 { println(" PASS" as *u8) }
96 else { println(" FAIL" as *u8); fails = fails + 1 }
97
98 // ---------- Test 5: linear scaling ---------------------------
99 // ((a & b) & (c & d)) -- 3 ANDs, each emits 3 clauses + 1 unit = 10 total
100 let st5: *TptpSymtab = nx_tptp_symtab_new()
101 let f5: *Fof = parse_to_nnf("((p(a) & q(a)) & (r(a) & s(a)))" as *u8, st5)
102 let out5: *Clause = (sys_mmap((NX_TS_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
103 let n5: *nx_int = sys_mmap(8) as *nx_int
104 n5[0] = 0
105 let _r5: nx_int = nx_fof_to_cnf_tseitin(f5, out5, n5, NX_TS_CAP)
106 print(" 5. 4-way nested AND -> n_clauses=" as *u8); print_i64(n5[0]); println("" as *u8)
107 if n5[0] == 10 {
108 println(" 3 ANDs * 3 def + 1 unit = 10 PASS" as *u8)
109 } else {
110 // Linear scaling: any value O(n) is the win, exact count
111 // depends on structure. Accept anything <= 16 (vs 2^4 = 16
112 // for distribute on similar structure).
113 if n5[0] <= 16 { println(" within linear bound PASS" as *u8) }
114 else { println(" non-linear FAIL" as *u8); fails = fails + 1 }
115 }
116
117 // ---------- Test 6: end-to-end FOF -> tseitin -> UNSAT ------
118 // (p & ~p) -- propositional contradiction.
119 let st6: *TptpSymtab = nx_tptp_symtab_new()
120 let f6: *Fof = parse_to_nnf("p(a) & ~p(a)" as *u8, st6)
121 let out6: *Clause = (sys_mmap((NX_TS_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
122 let n6: *nx_int = sys_mmap(8) as *nx_int
123 n6[0] = 0
124 let _r6: nx_int = nx_fof_to_cnf_tseitin(f6, out6, n6, NX_TS_CAP)
125 print(" 6. (p&~p) tseitin -> n_clauses=" as *u8); print_i64(n6[0]); println("" as *u8)
126
127 let s: *Saturation = nx_saturation_new(200)
128 var i: nx_int = 0
129 while i < n6[0] {
130 let c: *Clause = ((out6 as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
131 let _u: *NxResult = nx_sat_add_unproc(s, c)
132 i = i + 1
133 }
134 let v: nx_int = nx_sat_run_discount(s, SYM_EQ)
135 if v == NX_SAT_VERDICT_UNSAT {
136 println(" UNSAT via tseitin pipeline PASS" as *u8)
137 } else { print(" verdict=" as *u8); print_i64(v); println(" FAIL" as *u8); fails = fails + 1 }
138
139 println("" as *u8)
140 if fails == 0 {
141 println("=== ALL 6 Tseitin tests PASS ===" as *u8)
142 return 0
143 }
144 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
145 return 1
146}