nx_clause_components.nx source
↩ module page · 169 lines · 5683 B
1// nx_clause_components.nx -- variable-disjoint clause components.
2//
3// Per Vampire-displacement roadmap Phase 2. Foundational analysis
4// for AVATAR-style splitting: a clause whose literals partition into
5// variable-disjoint groups can be solved component-by-component, with
6// the SAT solver coordinating which combinations are consistent.
7//
8// Definition: two literals are in the same COMPONENT iff they share
9// at least one variable. Constants and matching predicates without
10// shared variables are independent.
11//
12// Algorithm: union-find over literals, where literal i and literal j
13// are unioned iff they share any variable. Output: for each literal,
14// the component id (canonical root) it belongs to.
15//
16// Single-component clause: the standard case; AVATAR doesn't split
17// it. Multi-component clause: AVATAR introduces a fresh propositional
18// var for each component and asks the SAT solver to coordinate.
19//
20// API:
21// nx_clause_n_components(c) -> int (# distinct components)
22// nx_clause_component_of(c, lit_idx) -> int (component id 0..n-1)
23// nx_clause_components_classify(c, out_ids) -- fills out_ids[lit_idx] = comp_id
24
25// nx_safety_envelope:
26// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
27// sil_target: SIL1
28// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
29// verdict: NOT_YET_EVALUATED
30
31import "nx_syscalls.nx"
32import "nx_runtime.nx"
33import "nx_tier.nx"
34import "nx_result.nx"
35import "nx_unify.nx"
36import "nx_resolution.nx"
37
38const NX_COMP_MAX_VARS_PER_LIT: nx_int = 32
39
40// Walk a term, append every distinct variable id encountered to out.
41// Returns updated count.
42func nx_comp_collect_vars(t: *Term, out: *nx_int, n_out: nx_int) -> nx_int {
43 if t.kind == NX_TERM_VAR {
44 // Dedup against existing entries.
45 var i: nx_int = 0
46 while i < n_out {
47 if out[i] == t.sym { return n_out }
48 i = i + 1
49 }
50 if n_out < NX_COMP_MAX_VARS_PER_LIT {
51 out[n_out] = t.sym
52 return n_out + 1
53 }
54 return n_out
55 }
56 if t.kind == NX_TERM_CONST { return n_out }
57 var n: nx_int = n_out
58 var k: nx_int = 0
59 while k < t.n_args {
60 n = nx_comp_collect_vars(nx_term_arg(t, k), out, n)
61 k = k + 1
62 }
63 return n
64}
65
66// True iff vars_a and vars_b share at least one variable id.
67func nx_comp_vars_share(a: *nx_int, na: nx_int, b: *nx_int, nb: nx_int) -> nx_int {
68 var i: nx_int = 0
69 while i < na {
70 var j: nx_int = 0
71 while j < nb {
72 if a[i] == b[j] { return 1 }
73 j = j + 1
74 }
75 i = i + 1
76 }
77 return 0
78}
79
80// Union-find find (path-compressed).
81func nx_comp_uf_find(parent: *nx_int, x: nx_int) -> nx_int {
82 var cur: nx_int = x
83 while parent[cur] != cur {
84 cur = parent[cur]
85 }
86 // Path compression
87 var p: nx_int = x
88 while parent[p] != cur {
89 let next: nx_int = parent[p]
90 parent[p] = cur
91 p = next
92 }
93 return cur
94}
95
96// Union two roots.
97func nx_comp_uf_union(parent: *nx_int, a: nx_int, b: nx_int) {
98 let ra: nx_int = nx_comp_uf_find(parent, a)
99 let rb: nx_int = nx_comp_uf_find(parent, b)
100 if ra != rb { parent[ra] = rb }
101}
102
103// Classify each literal of c into a component. out_ids[i] gets the
104// canonical root (an arbitrary literal index in the same component).
105// Returns the number of distinct components.
106func nx_clause_components_classify(c: *Clause, out_ids: *nx_int) -> nx_int {
107 if c.n_lits == 0 { return 0 }
108
109 // Collect var sets per literal (fresh buffers to avoid sharing).
110 let var_buf: *nx_int = (sys_mmap((c.n_lits * NX_COMP_MAX_VARS_PER_LIT * 8) as i64)) as *nx_int
111 let n_vars_per_lit: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
112 var i: nx_int = 0
113 while i < c.n_lits {
114 let lit: *Literal = nx_clause_lit_at(c, i)
115 let slot: *nx_int = ((var_buf as nx_int) + (i * NX_COMP_MAX_VARS_PER_LIT * 8)) as *nx_int
116 n_vars_per_lit[i] = nx_comp_collect_vars(lit.atom, slot, 0)
117 i = i + 1
118 }
119
120 // Initialize union-find: each literal is its own root.
121 let parent: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
122 var k: nx_int = 0
123 while k < c.n_lits {
124 parent[k] = k
125 k = k + 1
126 }
127
128 // Union literals that share variables.
129 var p: nx_int = 0
130 while p < c.n_lits {
131 var q: nx_int = p + 1
132 while q < c.n_lits {
133 let pa: *nx_int = ((var_buf as nx_int) + (p * NX_COMP_MAX_VARS_PER_LIT * 8)) as *nx_int
134 let qa: *nx_int = ((var_buf as nx_int) + (q * NX_COMP_MAX_VARS_PER_LIT * 8)) as *nx_int
135 if nx_comp_vars_share(pa, n_vars_per_lit[p], qa, n_vars_per_lit[q]) == 1 {
136 nx_comp_uf_union(parent, p, q)
137 }
138 q = q + 1
139 }
140 p = p + 1
141 }
142
143 // Read out roots into out_ids; count distinct.
144 let seen: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
145 var n_seen: nx_int = 0
146 var m: nx_int = 0
147 while m < c.n_lits {
148 let root: nx_int = nx_comp_uf_find(parent, m)
149 out_ids[m] = root
150 var found: nx_int = 0
151 var s: nx_int = 0
152 while s < n_seen {
153 if seen[s] == root { found = 1 }
154 s = s + 1
155 }
156 if found == 0 {
157 seen[n_seen] = root
158 n_seen = n_seen + 1
159 }
160 m = m + 1
161 }
162 return n_seen
163}
164
165// Convenience: number of components.
166func nx_clause_n_components(c: *Clause) -> nx_int {
167 let buf: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
168 return nx_clause_components_classify(c, buf)
169}