code wiki / (root) / nx_eqsat.nx

nx_eqsat.nx

buildroot/runtime/nx_eqsat.nx

116362 B2201 linesdepth 6pulls 8 transitivereach 214 importersview sourcekind librarytopic eqsat
docsdependenciesstructsconstsfunctions

about

nx_eqsat.nx -- equality-saturation framework (egg/SpEC family). Foundation for the superoptimization arc per ZERO_TO_ADVANCED.md M2: "the system is the FASTEST possible at every layer". Equality saturation is the 2026-research-grade approach -- developed by Willsey/Tate/Bornholt (egg, 2021) + Tate et al (Equality Saturation for Compiler Optimization, 2009), proven on Souper/Cranelift et al production compilers. Why equality saturation vs traditional peephole: Peephole: apply one rewrite, commit. If the rewrite was bad you lose; if a better cascade existed but required first un-doing a rewrite, you never find it. Phase-ordering tyranny. EqSat: keep ALL equivalent expressions in an e-graph. Apply all rewrites breadth-first to saturation. Extract the lowest-cost representative. Provably optimal under the rule set + cost model. For RV64IM: lets the compiler find non-obvious wins like (add x x) -> (shl x 1) (when shl is faster) (shl (shl x a) b) -> (shl x (add a b)) (kill dependent chain) (mul x 2^k) -> (shl x k) (strength reduction) (and x (not (and ~a y))) -> ... (DeMorgan reroute) AND once silicon-feedback (rv64im_min_hot_report.nx) identifies hot patterns, those become silicon-aware rewrites: (popcount-naive-loop) -> (intrinsic popcount) when silicon has it (gemm-inner-product) -> (vec mac fused) when SIMD lands Status: SEED. 2026-05-26. V1: e-class union-find + rule registry + bounded saturation loop + greedy extractor. ~50 baseline rewrites for RV64IM; extends per silicon-feedback findings.

dependencies 3 imports · 12 importers

nx_syscalls.nx nx_sketch_hash_map.nx nx_nxgate_sim.nx nx_eqsat.nx nx_apex_gcc_bench.nx nx_eqsat_congruence_bench.nx nx_eqsat_congruence_test.nx nx_eqsat_constfold_bench.nx nx_eqsat_dsl_bench.nx nx_eqsat_membership_proof.nx nx_eqsat_race_bench.nx nx_eqsat_test.nx nx_eqsat_vs_gcc_battery_test.nx nx_opt_eqsat_oracle_gate.nx

diagram shows first 10 each side; +0 more imports, +2 more importers in the complete lists below.

imports: nx_syscalls.nxnx_sketch_hash_map.nxnx_nxgate_sim.nx

imported by: nx_apex_gcc_bench.nxnx_eqsat_congruence_bench.nxnx_eqsat_congruence_test.nxnx_eqsat_constfold_bench.nxnx_eqsat_dsl_bench.nxnx_eqsat_membership_proof.nxnx_eqsat_race_bench.nxnx_eqsat_test.nxnx_eqsat_vs_gcc_battery_test.nxnx_opt_eqsat_oracle_gate.nxnx_opt_eqsat_pass.nxnx_superopt.nx

structs

119struct NxENode
134struct NxEClass
219struct NxDslRule
244struct NxEGraph
2164struct NxEmitNode

consts

47const NX_EQSAT_CF_CACHE_SLOTS: i64 = 1024
52const NX_EQSAT_COST_INFINITY: i64 = 1000000000
68const NX_EQSAT_W: i64 = 64
75const NX_EQ_OP_CONST: i64 = 0 // 0 children; payload = i64 value
76const NX_EQ_OP_VAR: i64 = 1 // 0 children; payload = variable id
77const NX_EQ_OP_ADD: i64 = 2 // 2 children
78const NX_EQ_OP_SUB: i64 = 3 // 2 children
79const NX_EQ_OP_MUL: i64 = 4 // 2 children
80const NX_EQ_OP_DIV: i64 = 5 // 2 children
81const NX_EQ_OP_REM: i64 = 6 // 2 children
82const NX_EQ_OP_AND: i64 = 7 // 2 children
83const NX_EQ_OP_OR: i64 = 8 // 2 children
84const NX_EQ_OP_XOR: i64 = 9 // 2 children
85const NX_EQ_OP_NOT: i64 = 10 // 1 child
86const NX_EQ_OP_SHL: i64 = 11 // 2 children
87const NX_EQ_OP_SHR: i64 = 12 // 2 children (logical)
88const NX_EQ_OP_SAR: i64 = 13 // 2 children (arithmetic)
89const NX_EQ_OP_NEG: i64 = 14 // 1 child
90const NX_EQ_OP_EQ: i64 = 15 // 2 children
91const NX_EQ_OP_LT: i64 = 16 // 2 children (signed)
92const NX_EQ_OP_LTU: i64 = 17 // 2 children (unsigned)
93const NX_EQ_OP_SELECT: i64 = 18 // 3 children (mux)
94const NX_EQ_OP_POPCNT: i64 = 19 // 1 child (Zbb-equivalent)
95const NX_EQ_OP_N: i64 = 20
162const NX_CF_NONE: i64 = 0 - 0x7FFFFFFFFFFFFFFF - 1
187const DSL_VAR:i64 = 0
188const DSL_CONST:i64 = 1
189const DSL_SAME_AS_A:i64 = 2
191const RHS_BIND_A:i64 = 0
192const RHS_BIND_B:i64 = 1
193const RHS_CONST:i64 = 2
194const RHS_SHL_A_BY_CONST:i64 = 3
195const RHS_SHL_A_BY_LOG2B:i64 = 4
201const RHS_SHL_A_BY_IADDED_J:i64 = 5
203const SC_NONE:i64 = 0
204const SC_POW2_B_KLTW:i64 = 1
211const SC_SHIFT_MERGE_IJW:i64 = 2
213const CNT_EVERY:i64 = 0 // count every match (the 6 V1 rules' behavior)
214const CNT_REAL_MERGE:i64 = 1 // count only real find!=find merges (mul_pow2)
370const NX_EQSAT_GRAPH_BYTES: i64 = 288
372const NX_EQSAT_OK: i64 = 0
373const NX_EQSAT_BAD_OP: i64 = 1
374const NX_EQSAT_BAD_ARITY: i64 = 2
375const NX_EQSAT_OVERFLOW: i64 = 3
376const NX_EQSAT_SATURATED: i64 = 4
377const NX_EQSAT_STEP_BUDGET: i64 = 5
388const NX_EQSAT_RULE_NONE: i64 = 0
389const NX_EQSAT_RULE_ADD_ZERO: i64 = 1
390const NX_EQSAT_RULE_SUB_SELF: i64 = 2
391const NX_EQSAT_RULE_ADD_SELF: i64 = 3
392const NX_EQSAT_RULE_AND_SELF: i64 = 4
393const NX_EQSAT_RULE_OR_ZERO: i64 = 5
394const NX_EQSAT_RULE_MUL_ONE: i64 = 6
395const NX_EQSAT_RULE_MUL_POW2: i64 = 7
403const NX_EQSAT_RULE_CONGRUENCE: i64 = 8
410const NX_EQSAT_RULE_XOR_SELF: i64 = 9
424const NX_EQSAT_RULE_CONSTFOLD: i64 = 10
435const NX_EQSAT_RULE_SHIFT_MERGE: i64 = 11
436const NX_EQSAT_RULE_N: i64 = 12

functions

97func nx_eqsat_op_is_valid(op: i64) -> i64
called by 1: nx_eqsat_add
103func nx_eqsat_arity_for(op: i64) -> i64
440func nx_eqsat_init(g: *NxEGraph,
500func nx_eqsat_enable_prov(g: *NxEGraph, buf: *i64, cap: i64) -> i64
514func nx_eqsat_log_rule(g: *NxEGraph, rule_id: i64) -> i64
539func nx_eqsat_enable_meet(g: *NxEGraph, hc: *HashMap,
called by 2: _one_itermain
581func nx_eqsat_enable_dsl(g: *NxEGraph, table: *NxDslRule, n: i64, cap: i64) -> i64
600func nx_eqsat_enable_constfold(g: *NxEGraph) -> i64
633func nx_cf_make_const_node(g: *NxEGraph, value: i64) -> i64
656func nx_cf_intern_const(g: *NxEGraph, value: i64) -> i64
694func nx_eqsat_builtin_dsl_table(table: *NxDslRule) -> i64
742func nx_eqsat_dsl_set_row(table: *NxDslRule, i: i64, rule_id: i64, lhs_op: i64,
761func nx_eqsat_mix(h: i64) -> i64
770func nx_eqsat_fingerprint(op: i64, payload: i64, kc0: i64, kc1: i64, kc2: i64) -> i64
784func nx_eqsat_node_matches(g: *NxEGraph, nidx: i64, op: i64, payload: i64,
800func nx_eqsat_add_parent(g: *NxEGraph, nidx: i64, child_cls: i64) -> i64
called by 1: nx_eqsat_add
814func nx_eqsat_push_dirty(g: *NxEGraph, cls: i64) -> i64
824func nx_eqsat_new_class(g: *NxEGraph, node_idx: i64, initial_cost: i64) -> i64
846func nx_eqsat_find(g: *NxEGraph, id: i64) -> i64
862func nx_eqsat_union_cited(g: *NxEGraph, a: i64, b: i64, rule_id: i64) -> i64
914func nx_eqsat_union(g: *NxEGraph, a: i64, b: i64) -> i64
930func nx_eqsat_op_cost(op: i64) -> i64
943func nx_eqsat_class_cost(g: *NxEGraph, class_id: i64) -> i64
981func nx_eqsat_op_to_gate_kind(op: i64) -> i64
1001func nx_eqsat_class_const(g: *NxEGraph, cls: i64, out_v: *i64) -> i64
1017func nx_eqsat_class_cf(g: *NxEGraph, cls: i64, out_v: *i64) -> i64
calls 1: nx_eqsat_find
1034func nx_eqsat_try_constfold(g: *NxEGraph, new_cls: i64, op: i64,
1076func nx_eqsat_fold_value(g: *NxEGraph, op: i64, kc0: i64, kc1: i64, kc2: i64, out_v: *i64) -> i64
1094func nx_eqsat_add(g: *NxEGraph, op: i64, k0: i64, k1: i64, k2: i64, payload: i64) -> i64
1267func nx_eqsat_add_const(g: *NxEGraph, value: i64) -> i64
1270func nx_eqsat_add_var(g: *NxEGraph, var_id: i64) -> i64
1273func nx_eqsat_add_binary(g: *NxEGraph, op: i64, a: i64, b: i64) -> i64
1276func nx_eqsat_add_unary(g: *NxEGraph, op: i64, a: i64) -> i64
called by 1: main calls 1: nx_eqsat_add
1287func nx_eqsat_apply_rule_add_zero(g: *NxEGraph) -> i64
1315func nx_eqsat_apply_rule_sub_self(g: *NxEGraph) -> i64
1334func nx_eqsat_apply_rule_add_self(g: *NxEGraph) -> i64
1354func nx_eqsat_apply_rule_and_self(g: *NxEGraph) -> i64
1372func nx_eqsat_apply_rule_or_zero(g: *NxEGraph) -> i64
1400func nx_eqsat_apply_rule_mul_one(g: *NxEGraph) -> i64
1425func nx_eqsat_apply_rule_mul_pow2(g: *NxEGraph) -> i64
1482func nx_eqsat_match_node_inline(g: *NxEGraph, nidx: i64) -> i64
1616func nx_eqsat_dsl_log2_pow2(c: i64) -> i64
1632func nx_eqsat_dsl_class_is_const(g: *NxEGraph, cls: i64, want: i64) -> i64
1644func nx_eqsat_dsl_const_val(g: *NxEGraph, cls: i64, out_v: *i64) -> i64
1667func nx_eqsat_dsl_shift_merge(g: *NxEGraph, table: *NxDslRule, ri: i64,
1703func nx_eqsat_dsl_instantiate_rhs(g: *NxEGraph, table: *NxDslRule, ri: i64, bindA: i64, shamt: i64) -> i64
1724func nx_eqsat_apply_dsl_rule(g: *NxEGraph, table: *NxDslRule, ri: i64) -> i64
1810func nx_eqsat_apply_dsl_table(g: *NxEGraph) -> i64
1826func nx_eqsat_match_node_dsl(g: *NxEGraph, nidx: i64) -> i64
1895func nx_eqsat_match_node(g: *NxEGraph, nidx: i64) -> i64
1918func nx_eqsat_rebuild(g: *NxEGraph) -> i64
1985func nx_eqsat_saturate(g: *NxEGraph, max_iters: i64) -> i64
2079func nx_eqsat_extract_best_node(g: *NxEGraph, class_id: i64) -> i64
2098func nx_eqsat_recompute_best(g: *NxEGraph) -> i64
2148func nx_eqsat_best_cost(g: *NxEGraph, class_id: i64) -> i64
2172func nx_eqsat_emit(g: *NxEGraph, class_id: i64, out: *NxEmitNode, cap: i64, count: *i64) -> i64