nx_casc_runner_test.nx source
↩ module page · 215 lines · 8590 B
1// nx_casc_runner_test.nx -- run the substrate against the TPTP-Easy
2// corpus in tests/tptp/casc/ and emit per-problem honest verdict
3// + aggregate scoreboard.
4//
5// Per honest-perf-verdict cardinal: sealed-enum verdict per axis,
6// named blockers for unmeasurable axes (no Vampire binary, no full
7// CASC corpus download).
8//
9// CASC-style scoreboard: problems_solved_in_budget / total.
10
11import "nx_syscalls.nx"
12import "nx_runtime.nx"
13import "nx_tier.nx"
14import "nx_str.nx"
15import "nx_result.nx"
16import "nx_file_result.nx"
17import "nx_unify.nx"
18import "nx_resolution.nx"
19import "nx_subsumption.nx"
20import "nx_tautology.nx"
21import "nx_disctree.nx"
22import "nx_paramodulation.nx"
23import "nx_saturation.nx"
24import "nx_pre_sat.nx"
25import "nx_sine.nx"
26import "nx_tptp_symtab.nx"
27import "nx_tptp_term.nx"
28import "nx_tptp_formula.nx"
29import "nx_tptp_load.nx"
30import "nx_fof.nx"
31import "nx_fof_parse.nx"
32import "nx_fof_cnf.nx"
33import "nx_tptp_load_any.nx"
34
35const SYM_EQ: nx_int = 50
36const RUNNER_BUDGET: nx_int = 5000
37
38// Run one problem; return 1 if SOLVED (UNSAT verdict matches expectation),
39// 0 if not solved, -1 on load/parse error.
40//
41// Strategy: try standard discount loop first. If UNKNOWN, retry with
42// LRS picker (Vampire's signature alternating age/weight strategy).
43// LRS finds proofs faster on problems where naive FIFO gets stuck on
44// deep search branches.
45func run_problem(path: *u8) -> nx_int {
46 let r_load: *NxResult = nx_tptp_load_any_file(path, SYM_EQ)
47 if nx_result_is_err(r_load) == 1 {
48 print(" " as *u8); print(path); print(" -> load ERR (code " as *u8); print_i64(nx_result_err_code(r_load)); println(")" as *u8)
49 return 0 - 1
50 }
51 let loaded: *TptpLoaded = nx_result_unwrap(r_load) as *TptpLoaded
52
53 // First attempt: standard discount loop (FIFO picker).
54 let s1: *Saturation = nx_saturation_new(RUNNER_BUDGET)
55 var i: nx_int = 0
56 while i < loaded.n {
57 let c: *Clause = nx_tptp_loaded_at(loaded, i)
58 let _u: *NxResult = nx_sat_add_unproc(s1, c)
59 i = i + 1
60 }
61 let v1: nx_int = nx_sat_run_discount(s1, SYM_EQ)
62 let steps1: nx_int = RUNNER_BUDGET - s1.budget
63
64 if v1 == NX_SAT_VERDICT_UNSAT {
65 print(" " as *u8); print(path)
66 print(" : n_clauses=" as *u8); print_i64(loaded.n)
67 print(" steps=" as *u8); print_i64(steps1)
68 print(" strategy=DISCOUNT verdict=UNSAT" as *u8); println("" as *u8)
69 return 1
70 }
71
72 // LRS retry skipped on large clause sets. Even with tombstones
73 // (no rebuild), the second Saturation struct + its own discrim
74 // tree alloc doubles memory consumption -- pel012's 118 input
75 // clauses + saturation expansion exceed qemu-tracked memory
76 // budget. Cap = 50 chosen empirically from runner observations.
77 if loaded.n > 50 {
78 print(" " as *u8); print(path)
79 print(" : n_clauses=" as *u8); print_i64(loaded.n)
80 print(" steps=" as *u8); print_i64(steps1)
81 print(" strategy=DISCOUNT verdict=UNKNOWN (LRS retry SKIPPED -- exceeds 50-clause cap)" as *u8); println("" as *u8)
82 return 0
83 }
84
85 // Fallback: LRS strategy with 1:5 weight:age ratio. Lighter clauses
86 // first, occasional FIFO injection for fairness.
87 let s2: *Saturation = nx_saturation_new(RUNNER_BUDGET)
88 var j: nx_int = 0
89 while j < loaded.n {
90 let c2: *Clause = nx_tptp_loaded_at(loaded, j)
91 let _u2: *NxResult = nx_sat_add_unproc(s2, c2)
92 j = j + 1
93 }
94 let v2: nx_int = nx_sat_run_discount_lrs(s2, SYM_EQ, 5)
95 let steps2: nx_int = RUNNER_BUDGET - s2.budget
96
97 print(" " as *u8); print(path)
98 print(" : n_clauses=" as *u8); print_i64(loaded.n)
99 print(" steps_disc=" as *u8); print_i64(steps1)
100 print(" steps_lrs=" as *u8); print_i64(steps2)
101 print(" verdict=" as *u8); print_i64(v2); println("" as *u8)
102 if v2 == NX_SAT_VERDICT_UNSAT { return 1 }
103 return 0
104}
105
106func main() -> nx_exit {
107 println("=== CASC runner: substrate vs TPTP-Easy corpus ===" as *u8)
108 println("" as *u8)
109
110 var n_total: nx_int = 0
111 var n_solved: nx_int = 0
112 var n_load_err: nx_int = 0
113
114 let paths: *u8 = sys_mmap(2048)
115 // Hard-code the corpus list -- a directory walker is queued.
116 // 7 problems: 5 Pelletier + 1 group + 1 steamroller-mini.
117 let problems: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/" as *u8
118
119 let p1: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel001.p" as *u8
120 let p2: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel002.p" as *u8
121 let p3: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel003.p" as *u8
122 let p4: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel005.p" as *u8
123 let p5: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel009.p" as *u8
124 let p6: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/group_id.p" as *u8
125 let p7: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/steamroller_mini.p" as *u8
126 let p8: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel006.p" as *u8
127 let p9: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel007.p" as *u8
128 let p10: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel012.p" as *u8
129 let p11: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel013.p" as *u8
130 let p12: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel016.p" as *u8
131 let p13: *u8 = "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/casc/pel020.p" as *u8
132
133 let r1: nx_int = run_problem(p1)
134 n_total = n_total + 1
135 if r1 == 1 { n_solved = n_solved + 1 }
136 if r1 < 0 { n_load_err = n_load_err + 1 }
137
138 let r2: nx_int = run_problem(p2)
139 n_total = n_total + 1
140 if r2 == 1 { n_solved = n_solved + 1 }
141 if r2 < 0 { n_load_err = n_load_err + 1 }
142
143 let r3: nx_int = run_problem(p3)
144 n_total = n_total + 1
145 if r3 == 1 { n_solved = n_solved + 1 }
146 if r3 < 0 { n_load_err = n_load_err + 1 }
147
148 let r4: nx_int = run_problem(p4)
149 n_total = n_total + 1
150 if r4 == 1 { n_solved = n_solved + 1 }
151 if r4 < 0 { n_load_err = n_load_err + 1 }
152
153 let r5: nx_int = run_problem(p5)
154 n_total = n_total + 1
155 if r5 == 1 { n_solved = n_solved + 1 }
156 if r5 < 0 { n_load_err = n_load_err + 1 }
157
158 let r6: nx_int = run_problem(p6)
159 n_total = n_total + 1
160 if r6 == 1 { n_solved = n_solved + 1 }
161 if r6 < 0 { n_load_err = n_load_err + 1 }
162
163 let r7: nx_int = run_problem(p7)
164 n_total = n_total + 1
165 if r7 == 1 { n_solved = n_solved + 1 }
166 if r7 < 0 { n_load_err = n_load_err + 1 }
167
168 let r8: nx_int = run_problem(p8)
169 n_total = n_total + 1
170 if r8 == 1 { n_solved = n_solved + 1 }
171 if r8 < 0 { n_load_err = n_load_err + 1 }
172
173 let r9: nx_int = run_problem(p9)
174 n_total = n_total + 1
175 if r9 == 1 { n_solved = n_solved + 1 }
176 if r9 < 0 { n_load_err = n_load_err + 1 }
177
178 let r10: nx_int = run_problem(p10)
179 n_total = n_total + 1
180 if r10 == 1 { n_solved = n_solved + 1 }
181 if r10 < 0 { n_load_err = n_load_err + 1 }
182
183 let r11: nx_int = run_problem(p11)
184 n_total = n_total + 1
185 if r11 == 1 { n_solved = n_solved + 1 }
186 if r11 < 0 { n_load_err = n_load_err + 1 }
187
188 let r12: nx_int = run_problem(p12)
189 n_total = n_total + 1
190 if r12 == 1 { n_solved = n_solved + 1 }
191 if r12 < 0 { n_load_err = n_load_err + 1 }
192
193 let r13: nx_int = run_problem(p13)
194 n_total = n_total + 1
195 if r13 == 1 { n_solved = n_solved + 1 }
196 if r13 < 0 { n_load_err = n_load_err + 1 }
197
198 println("" as *u8)
199 println("=== CASC scoreboard ===" as *u8)
200 print(" total problems: " as *u8); print_i64(n_total); println("" as *u8)
201 print(" SOLVED (UNSAT): " as *u8); print_i64(n_solved); println("" as *u8)
202 print(" load errors: " as *u8); print_i64(n_load_err); println("" as *u8)
203 print(" UNKNOWN/timeout: " as *u8); print_i64(n_total - n_solved - n_load_err); println("" as *u8)
204
205 println("" as *u8)
206 println("=== Honest BLOCKED axes (per cardinal) ===" as *u8)
207 println(" vs-Vampire head-to-head: BLOCKED_ON_VAMPIRE_BINARY_INSTALL" as *u8)
208 println(" full TPTP-24k corpus: BLOCKED_ON_TPTP_CORPUS_DOWNLOAD" as *u8)
209 println(" proof certificate output: BLOCKED_ON_PROOF_HISTORY_TRACKING" as *u8)
210 println(" HOL division: BLOCKED_ON_HIGHER_ORDER_EXTENSION" as *u8)
211 println("" as *u8)
212 print("=== Substrate result: " as *u8); print_i64(n_solved); print(" / " as *u8); print_i64(n_total)
213 println(" TPTP-Easy problems solved within budget ===" as *u8)
214 return 0
215}