nx_proof_log.nx
buildroot/runtime/nx_proof_log.nx
about
nx_proof_log.nx -- inference history tracking.
Side table recording, per derived clause, the inference rule + parent
clause indices. Foundation for TSTP-format proof certificate
emission required by CASC submissions (LOSE -> WIN on the
"proof certificate output" axis of the honest CASC verdict).
API:
nx_proof_log_new(cap) -> *ProofLog
nx_proof_log_add(log, rule, parent_a, parent_b) -> entry_idx
nx_proof_log_walk_unsat(log, empty_idx, visited[]) -> count
(transitive parent walk from the empty clause back to inputs --
the "minimal proof support" set)
Caller threading is the saturation loop's responsibility. A clause
index in `log` corresponds 1:1 to its index in the clause set the
loop manages. Input clauses get NX_PROOF_RULE_INPUT with parents -1.
dependencies 4 imports · 5 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nx
imported by: nx_atp_to_derive.nxnx_atp_to_derive_test.nxnx_proof_log_test.nxnx_tstp_emit.nxnx_tstp_emit_test.nx
structs
| 56 | struct ProofEntry |
| 63 | struct ProofLog |
consts
| 31 | const NX_PROOF_RULE_INPUT: nx_int = 0 |
| 32 | const NX_PROOF_RULE_RES: nx_int = 1 // binary resolution |
| 33 | const NX_PROOF_RULE_FACTOR: nx_int = 2 |
| 34 | const NX_PROOF_RULE_PARAMOD: nx_int = 3 |
| 35 | const NX_PROOF_RULE_DEMOD: nx_int = 4 |
| 36 | const NX_PROOF_RULE_HYPERRES: nx_int = 5 // N-electron hyperresolution |
| 37 | const NX_PROOF_RULE_EQ_FACTOR: nx_int = 6 |
| 38 | const NX_PROOF_RULE_INST_GEN: nx_int = 7 |
| 39 | const NX_PROOF_RULE_DEDUP: nx_int = 8 // literal dedup (preprocessing) |
| 40 | const NX_PROOF_RULE_AVATAR_SPLIT: nx_int = 9 |
| 61 | const NX_PROOF_ENTRY_BYTES: nx_int = 24 |
| 68 | const NX_PROOF_LOG_BYTES: nx_int = 24 |
functions
| 42 | func nx_proof_rule_name(r: nx_int) -> *u8 |
| 70 | func nx_proof_log_new(cap: nx_int) -> *ProofLog |
| 79 | func nx_proof_log_add(log: *ProofLog, rule: nx_int, |
| 91 | func nx_proof_log_get(log: *ProofLog, i: nx_int) -> *ProofEntry |
| 103 | func nx_proof_walk_ancestors(log: *ProofLog, start_idx: nx_int, |