code wiki / (root) / nx_casc_bench.nx

nx_casc_bench.nx

buildroot/runtime/nx_casc_bench.nx

8372 B195 linesdepth 8pulls 11 transitivereach 0 importersview sourcekind bench
docsdependenciesstructsconstsfunctions

about

nx_casc_bench.nx -- in-substrate honest bench: discount vs otter on synthetic clause-set problems. Per the honest-perf-verdict cardinal: emit sealed-enum per-axis verdict, name the LOSE improvement, refuse weasel words. This bench measures what we ACTUALLY can measure today (in-substrate strategy comparison on synthetic problems). TPTP-file-driven bench vs Vampire is BLOCKED on nx_tptp_formula parser; that gap is reported explicitly, not papered over. Axes measured (per problem): AX_CORRECTNESS -- did each strategy reach UNSAT? AX_STEPS -- budget consumed before halt AX_PROCESSED -- clauses that entered the processed set Per-axis sealed verdict: WIN_DISCOUNT / WIN_OTTER / TIE / BOTH_FAIL / UNMEASURABLE

dependencies 9 imports · 0 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_result.nx nx_unify.nx nx_resolution.nx nx_subsumption.nx nx_tautology.nx nx_saturation.nx nx_casc_bench.nx

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nxnx_resolution.nxnx_subsumption.nxnx_tautology.nxnx_saturation.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main println sys_write strlen sys_mmap run_problem nx_saturation_new sys_mmap ↻ nx_dt_new sys_mmap ↻ nx_dt_node_new sys_mmap ↻ mk_p1 nx_clause_new sys_mmap ↻ nx_clause_add nx_result_err sys_mmap ↻ nx_clause_lit_at nx_result_ok sys_mmap ↻ nx_lit_make sys_mmap ↻ mk_p sys_mmap ↻ nx_term_app sys_mmap ↻ nx_sat_add_unproc nx_result_err ↻ nx_sat_unproc_at nx_result_ok ↻ mk_p2 nx_clause_new ↻ nx_clause_add ↻ nx_lit_make ↻ mk_p ↻ nx_sat_add_unproc ↻ mk_p3 nx_clause_new ↻ nx_clause_add ↻

structs

none

consts

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
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

functions

48func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term
called by 3: mk_p1mk_p2mk_p3 calls 2: sys_mmapnx_term_app
54func verdict_name(v: nx_int) -> *u8
called by 1: run_problem
64func axis_lower_better(otter_val: nx_int, disc_val: nx_int,
called by 1: run_problem
72func axis_correctness(otter_v: nx_int, disc_v: nx_int) -> nx_int
called by 1: run_problem
87func mk_p1(s: *Saturation)
called by 1: run_problem calls 5: nx_clause_newnx_clause_addnx_lit_makemk_pnx_sat_add_unproc
97func mk_p2(s: *Saturation)
called by 1: run_problem calls 5: nx_clause_newnx_clause_addnx_lit_makemk_pnx_sat_add_unproc
116func mk_p3(s: *Saturation)
called by 1: run_problem calls 5: nx_clause_newnx_clause_addnx_lit_makemk_pnx_sat_add_unproc
141func run_problem(name: *u8, build: nx_int)
called by 1: main calls 12: nx_saturation_newmk_p1mk_p2mk_p3nx_sat_runnx_sat_run_discount+6
178func main() -> nx_exit
calls 2: printlnrun_problem