nx_congruence_closure.nx source
↩ module page · 118 lines · 4482 B
1// nx_congruence_closure.nx -- UF (uninterpreted functions) decision
2// procedure -- the foundational SMT theory.
3//
4// Per user 2026-05-14 unified-system request. This is the canonical
5// SMT-LIB QF_UF decision procedure: given a set of equalities + a
6// query equality, decide whether the query is implied.
7//
8// Algorithm: union-find over terms, with congruence propagation:
9// if f(x) = f(y) needs to be added but x and y are in different
10// classes, no congruence; if x and y are in same class, merge
11// f(x) and f(y). Iterate until fixpoint.
12//
13// Simplified scalar form: caller supplies ground equalities between
14// atomic IDs (treating function applications as distinct atoms);
15// substrate's union-find decides equivalence.
16
17// nx_safety_envelope:
18// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
19// sil_target: SIL1
20// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
21// verdict: NOT_YET_EVALUATED
22
23import "nx_syscalls.nx"
24import "nx_runtime.nx"
25import "nx_tier.nx"
26import "nx_result.nx"
27
28const NX_CC_MAX_TERMS: nx_int = 1024
29
30struct CongClosure {
31 n: nx_int, // number of registered terms
32 parent: *nx_int, // union-find parent array
33 rank: *nx_int, // union-find rank
34}
35
36const NX_CC_BYTES: nx_int = 24
37
38func nx_cc_new() -> *CongClosure {
39 let c: *CongClosure = (sys_mmap(NX_CC_BYTES as i64)) as *CongClosure
40 c.n = 0
41 c.parent = (sys_mmap((NX_CC_MAX_TERMS * 8) as i64)) as *nx_int
42 c.rank = (sys_mmap((NX_CC_MAX_TERMS * 8) as i64)) as *nx_int
43 return c
44}
45
46// Register a new atomic term; returns its id (returns Result).
47func nx_cc_add_term(c: *CongClosure) -> *NxResult {
48 if c.n >= NX_CC_MAX_TERMS { return nx_result_err(NX_ERR_OVERFLOW) }
49 let id: nx_int = c.n
50 c.parent[id] = id // self-parent: own class
51 c.rank[id] = 0
52 c.n = c.n + 1
53 return nx_result_ok(id)
54}
55
56// Find root with path compression.
57func nx_cc_find(c: *CongClosure, x: nx_int) -> nx_int {
58 var root: nx_int = x
59 while c.parent[root] != root { root = c.parent[root] }
60 // Path compression: walk again, set each ancestor's parent to root
61 var cur: nx_int = x
62 while c.parent[cur] != root {
63 let nxt: nx_int = c.parent[cur]
64 c.parent[cur] = root
65 cur = nxt
66 }
67 return root
68}
69
70// Union by rank. Returns Result<n_classes_after, NX_ERR_*>.
71func nx_cc_union(c: *CongClosure, x: nx_int, y: nx_int) -> *NxResult {
72 if x < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
73 if y < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
74 if x >= c.n { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
75 if y >= c.n { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
76 let rx: nx_int = nx_cc_find(c, x)
77 let ry: nx_int = nx_cc_find(c, y)
78 if rx == ry { return nx_result_ok(0) } // already same class
79 let rkx: nx_int = c.rank[rx]
80 let rky: nx_int = c.rank[ry]
81 if rkx < rky { c.parent[rx] = ry }
82 if rkx > rky { c.parent[ry] = rx }
83 if rkx == rky {
84 c.parent[ry] = rx
85 c.rank[rx] = rkx + 1
86 }
87 return nx_result_ok(1)
88}
89
90// Decide: is x = y under the current equality set?
91func nx_cc_equal(c: *CongClosure, x: nx_int, y: nx_int) -> *NxResult {
92 if x < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
93 if y < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
94 if x >= c.n { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
95 if y >= c.n { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
96 let rx: nx_int = nx_cc_find(c, x)
97 let ry: nx_int = nx_cc_find(c, y)
98 if rx == ry { return nx_result_ok(1) } // equal
99 return nx_result_ok(0) // not provably equal
100}
101
102// Congruence step: if f(a) and f(b) are registered and a = b under
103// current closure, then f(a) = f(b) must also be merged. This
104// simplified API takes paired-up application terms via caller-supplied
105// mapping; full congruence-aware closure is queued.
106func nx_cc_propagate_congruence(c: *CongClosure,
107 fa: nx_int, a: nx_int,
108 fb: nx_int, b: nx_int) -> *NxResult {
109 // If a == b under closure, merge fa and fb
110 let r_eq: *NxResult = nx_cc_equal(c, a, b)
111 if nx_result_is_err(r_eq) == 1 { return r_eq }
112 if nx_result_unwrap(r_eq) == 1 {
113 return nx_cc_union(c, fa, fb)
114 }
115 return nx_result_ok(0) // no propagation
116}
117
118func nx_cc_n_terms(c: *CongClosure) -> nx_int { return c.n }