nx_disctree.nx source

1// nx_disctree.nx -- discrimination tree term index. 2// 3// Per Vampire-displacement roadmap Phase 2. THE biggest perf win 4// for saturation provers: replaces the O(n_processed) iteration in 5// forward subsumption + demodulation candidate lookup with an O(d) 6// trie walk where d is the term depth. Vampire's hot path goes 7// from O(n^2) to O(n * d * branching) per saturation step. 8// 9// Standard "perfect discrimination tree" (Stickel 1989 lineage): 10// - Trie keyed on preorder linearization of terms. 11// - Each token is (sym, n_args); a STAR token marks variables. 12// - Edges from a node match by (sym, n_args). 13// - Insertion: walk the linearization, allocate edges + nodes 14// as needed; mark terminal node with the stored value. 15// - Lookup (find generalizations of Q): at each tree node, follow 16// EITHER the matching (sym, n_args) edge OR a STAR edge. STAR 17// consumes one whole subterm of Q (skip via pending-counter). 18// 19// API: 20// nx_dt_new() -> *DiscTree 21// nx_dt_insert(tree, term, value) -- attach value 22// nx_dt_find_generalizations(tree, query, results, *n) 23// 24// Bits-up nx_int. Variables in queries are not yet handled (TODO): 25// for v1 the caller passes ground queries. Variables in stored 26// terms ARE handled via the STAR edge. 27 28// nx_safety_envelope: 29// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 30// sil_target: SIL1 31// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 32// verdict: NOT_YET_EVALUATED 33 34import "nx_syscalls.nx" 35import "nx_runtime.nx" 36import "nx_tier.nx" 37import "nx_result.nx" 38import "nx_unify.nx" 39 40// 0 is reserved as wildcard -- real sym_ids start at NX_TPTP_SYM_BASE 41// (1000), so 0 is safe to use as the STAR sentinel. 42const NX_DT_STAR: nx_int = 0 43const NX_DT_MAX_TOKENS: nx_int = 256 44const NX_DT_MAX_RESULTS: nx_int = 64 45 46struct DTToken { 47 sym: nx_int, 48 n_args: nx_int, 49} 50const NX_DT_TOKEN_BYTES: nx_int = 16 51 52struct DTEdge { 53 sym: nx_int, // NX_DT_STAR for wildcard 54 n_args: nx_int, 55 child: *DTNode, 56 next: *DTEdge, 57} 58const NX_DT_EDGE_BYTES: nx_int = 32 59 60struct DTNode { 61 edges: *DTEdge, 62 has_value: nx_int, 63 value: nx_int, 64} 65const NX_DT_NODE_BYTES: nx_int = 24 66 67struct DiscTree { 68 root: *DTNode, 69} 70const NX_DT_BYTES: nx_int = 8 71 72// ===== Constructors ================================================= 73func nx_dt_node_new() -> *DTNode { 74 let n: *DTNode = (sys_mmap(NX_DT_NODE_BYTES as i64)) as *DTNode 75 n.edges = 0 as *DTEdge 76 n.has_value = 0 77 n.value = 0 78 return n 79} 80 81func nx_dt_new() -> *DiscTree { 82 let t: *DiscTree = (sys_mmap(NX_DT_BYTES as i64)) as *DiscTree 83 t.root = nx_dt_node_new() 84 return t 85} 86 87// Find or create the child node reached by the (sym, n_args) edge. 88func nx_dt_node_descend(node: *DTNode, sym: nx_int, n_args: nx_int) -> *DTNode { 89 var e: *DTEdge = node.edges 90 while ((e as nx_int) != 0) { 91 if e.sym == sym { 92 if e.n_args == n_args { return e.child } 93 } 94 e = e.next 95 } 96 // Not found -- allocate. 97 let new_child: *DTNode = nx_dt_node_new() 98 let new_edge: *DTEdge = (sys_mmap(NX_DT_EDGE_BYTES as i64)) as *DTEdge 99 new_edge.sym = sym 100 new_edge.n_args = n_args 101 new_edge.child = new_child 102 new_edge.next = node.edges 103 node.edges = new_edge 104 return new_child 105} 106 107// ===== Linearization =============================================== 108// Emit preorder tokens for term t into out_tokens; advance *out_n. 109func nx_dt_linearize(t: *Term, out_tokens: *DTToken, out_n: *nx_int) { 110 if out_n[0] >= NX_DT_MAX_TOKENS { return } 111 let slot: *DTToken = ((out_tokens as nx_int) + (out_n[0] * NX_DT_TOKEN_BYTES)) as *DTToken 112 if t.kind == NX_TERM_VAR { 113 slot.sym = NX_DT_STAR 114 slot.n_args = 0 115 out_n[0] = out_n[0] + 1 116 return 117 } 118 slot.sym = t.sym 119 slot.n_args = t.n_args 120 out_n[0] = out_n[0] + 1 121 if t.kind == NX_TERM_CONST { return } 122 var i: nx_int = 0 123 while i < t.n_args { 124 nx_dt_linearize(nx_term_arg(t, i), out_tokens, out_n) 125 i = i + 1 126 } 127} 128 129// ===== Insert ===================================================== 130func nx_dt_insert(tree: *DiscTree, t: *Term, value: nx_int) { 131 let tokens: *DTToken = (sys_mmap((NX_DT_MAX_TOKENS * NX_DT_TOKEN_BYTES) as i64)) as *DTToken 132 let n_p: *nx_int = (sys_mmap(8)) as *nx_int 133 n_p[0] = 0 134 nx_dt_linearize(t, tokens, n_p) 135 136 var cur: *DTNode = tree.root 137 var i: nx_int = 0 138 while i < n_p[0] { 139 let tok: *DTToken = ((tokens as nx_int) + (i * NX_DT_TOKEN_BYTES)) as *DTToken 140 cur = nx_dt_node_descend(cur, tok.sym, tok.n_args) 141 i = i + 1 142 } 143 cur.has_value = 1 144 cur.value = value 145} 146 147// ===== Skip a subterm in the linearized stream ===================== 148// Starting at `cursor`, consume tokens until exactly one whole subterm 149// has been consumed. Each token "takes 1, gives n_args" -- start with 150// pending=1, decrement per token + add token's arity. When pending 151// hits 0, return the position past the consumed subterm. 152func nx_dt_skip_subterm(tokens: *DTToken, n: nx_int, cursor: nx_int) -> nx_int { 153 var pending: nx_int = 1 154 var pos: nx_int = cursor 155 while pos < n { 156 if pending == 0 { return pos } 157 let tok: *DTToken = ((tokens as nx_int) + (pos * NX_DT_TOKEN_BYTES)) as *DTToken 158 pending = pending - 1 159 pending = pending + tok.n_args 160 pos = pos + 1 161 } 162 return pos 163} 164 165// ===== Find generalizations ======================================= 166func nx_dt_walk(node: *DTNode, tokens: *DTToken, n_tokens: nx_int, 167 cursor: nx_int, results: *nx_int, n_results: *nx_int) { 168 if cursor >= n_tokens { 169 if node.has_value == 1 { 170 if n_results[0] < NX_DT_MAX_RESULTS { 171 results[n_results[0]] = node.value 172 n_results[0] = n_results[0] + 1 173 } 174 } 175 return 176 } 177 let qtok: *DTToken = ((tokens as nx_int) + (cursor * NX_DT_TOKEN_BYTES)) as *DTToken 178 179 var e: *DTEdge = node.edges 180 while ((e as nx_int) != 0) { 181 if e.sym == NX_DT_STAR { 182 // Wildcard edge: consume one whole subterm of the query. 183 let skip_to: nx_int = nx_dt_skip_subterm(tokens, n_tokens, cursor) 184 nx_dt_walk(e.child, tokens, n_tokens, skip_to, results, n_results) 185 } 186 if e.sym != NX_DT_STAR { 187 if e.sym == qtok.sym { 188 if e.n_args == qtok.n_args { 189 nx_dt_walk(e.child, tokens, n_tokens, cursor + 1, results, n_results) 190 } 191 } 192 } 193 e = e.next 194 } 195} 196 197func nx_dt_find_generalizations(tree: *DiscTree, query: *Term, 198 results: *nx_int, n_results: *nx_int) { 199 let tokens: *DTToken = (sys_mmap((NX_DT_MAX_TOKENS * NX_DT_TOKEN_BYTES) as i64)) as *DTToken 200 let n_q_p: *nx_int = (sys_mmap(8)) as *nx_int 201 n_q_p[0] = 0 202 nx_dt_linearize(query, tokens, n_q_p) 203 n_results[0] = 0 204 nx_dt_walk(tree.root, tokens, n_q_p[0], 0, results, n_results) 205} 206 207// Delete every leaf with stored value == `target` -- recursively 208// walks the entire tree. Used by saturation backward subsumption to 209// clean up entries pointing at tombstoned clauses, preventing the 210// monotonic memory growth that would otherwise OOM on long-running 211// problems (e.g. pel012's 118-clause Tseitin output). 212// 213// Implementation: the leaves don't get physically removed (that would 214// require parent-pointer bookkeeping); instead has_value is set to 0 215// so the lookup walker ignores them. Memory footprint stays the 216// same per individual deletion, but the search-time cost of those 217// branches drops to "follow edge, check has_value, skip". 218func nx_dt_delete_value_node(node: *DTNode, target: nx_int) { 219 if node.has_value == 1 { 220 if node.value == target { node.has_value = 0 } 221 } 222 var e: *DTEdge = node.edges 223 while ((e as nx_int) != 0) { 224 nx_dt_delete_value_node(e.child, target) 225 e = e.next 226 } 227} 228 229func nx_dt_delete_value(tree: *DiscTree, target: nx_int) { 230 nx_dt_delete_value_node(tree.root, target) 231}