code wiki / (root) / nx_prover_eval_test.nx

nx_prover_eval_test.nx

buildroot/runtime/nx_prover_eval_test.nx

4792 B119 linesdepth 6pulls 8 transitivereach 0 importersview sourcekind gate/prooftopic prover
docsdependenciesstructsconstsfunctions

about

nx_prover_eval_test.nx -- realistic prover capability benchmark. 8 test cases of progressively harder proof shapes: case 1 1-axiom-only trivial case 2 2-step MP chain (A, A->B, B->C => C) case 3 5-step MP chain case 4 10-step MP chain case 5 wide branching (axiom A; 10 unrelated impls; target = via_A) case 6 missing premise (target unreachable; expect NO_RULES) case 7 beyond budget (50-step chain, budget 10; expect FAILED_BUDGET) case 8 deep chain inside large budget (50-step chain, budget 200)

dependencies 4 imports · 0 importers

syscalls.nx nx_axioms.nx nx_prover.nx nx_prover_eval.nx nx_prover_eval_test.nx

imports: syscalls.nxnx_axioms.nxnx_prover.nxnx_prover_eval.nx

imported by: nobody (leaf or entry point)

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

main nx_eval_summary_alloc nx_eval_run_case nx_prover_state_alloc nx_prover_add_axiom nx_axiom_is_valid nx_prover_fact_at nx_clock_gettime nx_prover_search nx_prover_has_target nx_prover_fact_at ↻ nx_prover_step_mp nx_prover_has_stmt nx_prover_fact_at ↻ nx_prover_fact_at ↻ nx_prover_add_inferred nx_prover_fact_at ↻ nx_eval_accumulate nx_eval_emit_summary ev_str ev_i64 ev_putc ev_i64 ↻

structs

none

consts

none

functions

18func main() -> i64 {
calls 4: nx_eval_summary_allocnx_eval_run_casenx_eval_accumulatenx_eval_emit_summary