nx_casc_bench.nx source
↩ module page · 195 lines · 8372 B
1// nx_casc_bench.nx -- in-substrate honest bench: discount vs otter on
2// synthetic clause-set problems.
3//
4// Per the honest-perf-verdict cardinal: emit sealed-enum per-axis
5// verdict, name the LOSE improvement, refuse weasel words. This
6// bench measures what we ACTUALLY can measure today (in-substrate
7// strategy comparison on synthetic problems). TPTP-file-driven
8// bench vs Vampire is BLOCKED on nx_tptp_formula parser; that gap
9// is reported explicitly, not papered over.
10//
11// Axes measured (per problem):
12// AX_CORRECTNESS -- did each strategy reach UNSAT?
13// AX_STEPS -- budget consumed before halt
14// AX_PROCESSED -- clauses that entered the processed set
15//
16// Per-axis sealed verdict:
17// WIN_DISCOUNT / WIN_OTTER / TIE / BOTH_FAIL / UNMEASURABLE
18
19// nx_safety_envelope:
20// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
21// sil_target: SIL1
22// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
23// verdict: NOT_YET_EVALUATED
24
25import "nx_syscalls.nx"
26import "nx_runtime.nx"
27import "nx_tier.nx"
28import "nx_result.nx"
29import "nx_unify.nx"
30import "nx_resolution.nx"
31import "nx_subsumption.nx"
32import "nx_tautology.nx"
33import "nx_saturation.nx"
34
35const NX_VERDICT_WIN_DISCOUNT: nx_int = 1
36const NX_VERDICT_WIN_OTTER: nx_int = 2
37const NX_VERDICT_TIE: nx_int = 3
38const NX_VERDICT_BOTH_FAIL: nx_int = 4
39const NX_VERDICT_UNMEASURABLE: nx_int = 5
40
41const SYM_A: nx_int = 100
42const SYM_B: nx_int = 101
43const SYM_P: nx_int = 200
44const SYM_Q: nx_int = 201
45const SYM_R: nx_int = 202
46const SYM_EQ: nx_int = 50
47
48func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
49 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
50 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
51 return nx_term_app(p_sym, 1, arg)
52}
53
54func verdict_name(v: nx_int) -> *u8 {
55 if v == NX_VERDICT_WIN_DISCOUNT { return "WIN_DISCOUNT" as *u8 }
56 if v == NX_VERDICT_WIN_OTTER { return "WIN_OTTER" as *u8 }
57 if v == NX_VERDICT_TIE { return "TIE" as *u8 }
58 if v == NX_VERDICT_BOTH_FAIL { return "BOTH_FAIL" as *u8 }
59 if v == NX_VERDICT_UNMEASURABLE { return "UNMEASURABLE" as *u8 }
60 return "?" as *u8
61}
62
63// Axis verdicts. Lower is better for steps + processed; equal=>TIE.
64func axis_lower_better(otter_val: nx_int, disc_val: nx_int,
65 both_ran_correctly: nx_int) -> nx_int {
66 if both_ran_correctly == 0 { return NX_VERDICT_UNMEASURABLE }
67 if disc_val < otter_val { return NX_VERDICT_WIN_DISCOUNT }
68 if otter_val < disc_val { return NX_VERDICT_WIN_OTTER }
69 return NX_VERDICT_TIE
70}
71
72func axis_correctness(otter_v: nx_int, disc_v: nx_int) -> nx_int {
73 var o_ok: nx_int = 0
74 if otter_v == NX_SAT_VERDICT_UNSAT { o_ok = 1 }
75 var d_ok: nx_int = 0
76 if disc_v == NX_SAT_VERDICT_UNSAT { d_ok = 1 }
77 if o_ok == 1 {
78 if d_ok == 1 { return NX_VERDICT_TIE }
79 return NX_VERDICT_WIN_OTTER
80 }
81 if d_ok == 1 { return NX_VERDICT_WIN_DISCOUNT }
82 return NX_VERDICT_BOTH_FAIL
83}
84
85// ===== Problem builders =============================================
86// P1: trivial UNSAT {p(a), ~p(a)}
87func mk_p1(s: *Saturation) {
88 let c1: *Clause = nx_clause_new()
89 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
90 let c2: *Clause = nx_clause_new()
91 let _r2: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
92 let _u1: *NxResult = nx_sat_add_unproc(s, c1)
93 let _u2: *NxResult = nx_sat_add_unproc(s, c2)
94}
95
96// P2: UNSAT through 3-clause chain {p(a)} {~p(a) v q(a)} {~q(a)}
97func mk_p2(s: *Saturation) {
98 let c1: *Clause = nx_clause_new()
99 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
100
101 let c2: *Clause = nx_clause_new()
102 let _r2a: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
103 let _r2b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
104
105 let c3: *Clause = nx_clause_new()
106 let _r3: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
107
108 let _u1: *NxResult = nx_sat_add_unproc(s, c1)
109 let _u2: *NxResult = nx_sat_add_unproc(s, c2)
110 let _u3: *NxResult = nx_sat_add_unproc(s, c3)
111}
112
113// P3: UNSAT with redundant subsumed inputs (discount should prune)
114// {p(a)}, {p(a) v q(a)}, {p(a) v q(a) v r(a)}, {~p(a)}
115// Otter has to process all 4; Discount prunes {p(a)v..} as subsumed.
116func mk_p3(s: *Saturation) {
117 let c1: *Clause = nx_clause_new()
118 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
119
120 let c2: *Clause = nx_clause_new()
121 let _r2a: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
122 let _r2b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
123
124 let c3: *Clause = nx_clause_new()
125 let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
126 let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
127 let _r3c: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_R, SYM_A)))
128
129 let c4: *Clause = nx_clause_new()
130 let _r4: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
131
132 let _u1: *NxResult = nx_sat_add_unproc(s, c1)
133 let _u2: *NxResult = nx_sat_add_unproc(s, c2)
134 let _u3: *NxResult = nx_sat_add_unproc(s, c3)
135 let _u4: *NxResult = nx_sat_add_unproc(s, c4)
136}
137
138// ===== Per-problem runner ==========================================
139// Runs the same problem twice (otter, then discount), emits per-axis
140// verdicts + records aggregate counters.
141func run_problem(name: *u8, build: nx_int) {
142 let budget: nx_int = 100
143
144 let s_otter: *Saturation = nx_saturation_new(budget)
145 if build == 1 { mk_p1(s_otter) }
146 if build == 2 { mk_p2(s_otter) }
147 if build == 3 { mk_p3(s_otter) }
148 let v_otter: nx_int = nx_sat_run(s_otter)
149 let steps_otter: nx_int = budget - s_otter.budget
150 let proc_otter: nx_int = s_otter.n_processed
151
152 let s_disc: *Saturation = nx_saturation_new(budget)
153 if build == 1 { mk_p1(s_disc) }
154 if build == 2 { mk_p2(s_disc) }
155 if build == 3 { mk_p3(s_disc) }
156 let v_disc: nx_int = nx_sat_run_discount(s_disc, SYM_EQ)
157 let steps_disc: nx_int = budget - s_disc.budget
158 let proc_disc: nx_int = s_disc.n_processed
159
160 let v_corr: nx_int = axis_correctness(v_otter, v_disc)
161 var both_ok: nx_int = 0
162 if v_corr == NX_VERDICT_TIE { both_ok = 1 }
163 let v_steps: nx_int = axis_lower_better(steps_otter, steps_disc, both_ok)
164 let v_proc: nx_int = axis_lower_better(proc_otter, proc_disc, both_ok)
165
166 print("---- " as *u8); print(name); println(" ----" as *u8)
167 print(" otter: verdict=" as *u8); print_i64(v_otter)
168 print(" steps=" as *u8); print_i64(steps_otter)
169 print(" processed=" as *u8); print_i64(proc_otter); println("" as *u8)
170 print(" discount: verdict=" as *u8); print_i64(v_disc)
171 print(" steps=" as *u8); print_i64(steps_disc)
172 print(" processed=" as *u8); print_i64(proc_disc); println("" as *u8)
173 print(" axis:correctness -> " as *u8); println(verdict_name(v_corr))
174 print(" axis:steps -> " as *u8); println(verdict_name(v_steps))
175 print(" axis:processed -> " as *u8); println(verdict_name(v_proc))
176}
177
178func main() -> nx_exit {
179 println("=== CASC bench (in-substrate: discount vs otter) ===" as *u8)
180 println("Per honest-perf-verdict cardinal: sealed verdict per axis." as *u8)
181 println("" as *u8)
182 run_problem("P1: trivial UNSAT {p(a), ~p(a)}" as *u8, 1)
183 run_problem("P2: 3-chain {p(a), ~p(a) v q(a), ~q(a)}" as *u8, 2)
184 run_problem("P3: subsumed inputs {p(a), p(a)vq(a), p(a)vq(a)vr(a), ~p(a)}" as *u8, 3)
185
186 println("" as *u8)
187 println("=== STATUS notes ===" as *u8)
188 println(" TPTP CNF formula parser: UNBLOCKED (Phase 1.6 shipped 2026-05-15)" as *u8)
189 println(" TPTP file loader: UNBLOCKED (nx_tptp_load_smoke 3/3 PASS)" as *u8)
190 println(" vs-Vampire head-to-head: BLOCKED_ON_VAMPIRE_BINARY_INSTALL" as *u8)
191 println(" TPTP-Easy bench corpus: BLOCKED_ON_TPTP_CORPUS_DOWNLOAD (~24k .p files)" as *u8)
192 println(" FOF (quantifiers/connectives): queued (Phase 2)" as *u8)
193 println("=== bench complete ===" as *u8)
194 return 0
195}