code wiki / (root) / nx_congruence_closure.nx

nx_congruence_closure.nx

buildroot/runtime/nx_congruence_closure.nx

4482 B118 linesdepth 4pulls 4 transitivereach 1 importersview sourcekind library

docs dependencies structs consts functions

about

nx_congruence_closure.nx -- UF (uninterpreted functions) decision procedure -- the foundational SMT theory. Per user 2026-05-14 unified-system request. This is the canonical SMT-LIB QF_UF decision procedure: given a set of equalities + a query equality, decide whether the query is implied. Algorithm: union-find over terms, with congruence propagation: if f(x) = f(y) needs to be added but x and y are in different classes, no congruence; if x and y are in same class, merge f(x) and f(y). Iterate until fixpoint. Simplified scalar form: caller supplies ground equalities between atomic IDs (treating function applications as distinct atoms); substrate's union-find decides equivalence.

dependencies 4 imports · 1 importers

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nx

imported by: nx_unified_solver_test.nx

structs

30	struct CongClosure

consts

28	const NX_CC_MAX_TERMS: nx_int = 1024
36	const NX_CC_BYTES: nx_int = 24

functions

38	func nx_cc_new() -> *CongClosure called by 1: main calls 1: sys_mmap
47	func nx_cc_add_term(c: CongClosure) -> NxResult called by 1: main calls 2: nx_result_err nx_result_ok
57	func nx_cc_find(c: *CongClosure, x: nx_int) -> nx_int called by 2: nx_cc_union nx_cc_equal
71	func nx_cc_union(c: CongClosure, x: nx_int, y: nx_int) -> NxResult called by 2: nx_cc_propagate_congruence main calls 3: nx_result_err nx_cc_find nx_result_ok
91	func nx_cc_equal(c: CongClosure, x: nx_int, y: nx_int) -> NxResult called by 2: nx_cc_propagate_congruence main calls 3: nx_result_err nx_cc_find nx_result_ok
106	func nx_cc_propagate_congruence(c: *CongClosure, called by 1: main calls 5: nx_cc_equal nx_result_is_err nx_result_unwrap nx_cc_union nx_result_ok
118	func nx_cc_n_terms(c: *CongClosure) -> nx_int { return c.n } called by 1: main