nx_disctree.nx

nx_disctree.nx -- discrimination tree term index. Per Vampire-displacement roadmap Phase 2. THE biggest perf win for saturation provers: replaces the O(n_processed) iteration in forward subsumption + demodulation candidate lookup with an O(d) trie walk where d is the term depth. Vampire's hot path goes from O(n^2) to O(n * d * branching) per saturation step. Standard "perfect discrimination tree" (Stickel 1989 lineage): - Trie keyed on preorder linearization of terms. - Each token is (sym, n_args); a STAR token marks variables. - Edges from a node match by (sym, n_args). - Insertion: walk the linearization, allocate edges + nodes as needed; mark terminal node with the stored value. - Lookup (find generalizations of Q): at each tree node, follow EITHER the matching (sym, n_args) edge OR a STAR edge. STAR consumes one whole subterm of Q (skip via pending-counter). API: nx_dt_new() -> *DiscTree nx_dt_insert(tree, term, value) -- attach value nx_dt_find_generalizations(tree, query, results, *n) Bits-up nx_int. Variables in queries are not yet handled (TODO): for v1 the caller passes ground queries. Variables in stored terms ARE handled via the STAR edge.