code wiki / (root) / nx_prover_eval.nx

nx_prover_eval.nx

buildroot/runtime/nx_prover_eval.nx

5529 B174 linesdepth 5pulls 7 transitivereach 1 importersview sourcekind librarytopic prover
docsdependenciesstructsconstsfunctions

about

nx_prover_eval.nx -- honest benchmark of nx_prover capability + timing. Builds realistic test scenarios + measures (a) success rate (b) cycles needed (c) per-theorem wall time. Reports gaps where the current Phase A0 prover (forward chaining + MP) fails. genealogy_id: brodal_okasaki_1996 (data structures) + wos_overbeek_lusk_boyle_1992 (atp benchmarks) lineage_id: theorem_proving_benchmark + timing

dependencies 5 imports · 1 importers

syscalls.nx nx_axioms.nx nx_clock.nx nx_derive.nx nx_prover.nx nx_prover_eval.nx nx_prover_eval_test.nx

imports: syscalls.nxnx_axioms.nxnx_clock.nxnx_derive.nxnx_prover.nx

imported by: nx_prover_eval_test.nx

structs

30struct EvalCase
41struct EvalResult
51struct EvalSummary

consts

25const NX_EVAL_OUTCOME_PROVED: i64 = 0
26const NX_EVAL_OUTCOME_FAILED_BUDGET: i64 = 1
27const NX_EVAL_OUTCOME_NO_RULES: i64 = 2
28const NX_EVAL_OUTCOME_TIMEOUT: i64 = 3
39const NX_EVAL_CASE_BYTES: i64 = 40
49const NX_EVAL_RESULT_BYTES: i64 = 40

functions

62func nx_eval_summary_alloc() -> *EvalSummary
called by 1: main
79func nx_eval_run_case(case_id: i64,
called by 1: main calls 4: nx_prover_state_allocnx_prover_add_axiomnx_clock_gettimenx_prover_search
107func nx_eval_accumulate(summary: *EvalSummary, r: *EvalResult) -> i64
called by 1: main
121func ev_putc(fd: i64, c: i64) -> i64
called by 1: ev_i64
128func ev_str(fd: i64, s: *u8, n: i64) -> i64
called by 1: nx_eval_emit_summary
133func ev_i64(fd: i64, n: i64) -> i64
called by 2: ev_i64nx_eval_emit_summary calls 2: ev_putcev_i64
157func nx_eval_emit_summary(fd: i64, sum: *EvalSummary) -> i64
called by 1: main calls 2: ev_strev_i64