nx_avatar_split.nx source
↩ module page · 137 lines · 5079 B
1// nx_avatar_split.nx -- AVATAR-style clause splitting.
2//
3// Per Vampire-displacement roadmap Phase 2. AVATAR (Voronkov 2014)
4// splits multi-component clauses into independent sub-clauses; full
5// AVATAR uses a SAT solver to coordinate which split combinations
6// to explore.
7//
8// This commit ships the SPLIT-ONLY primitive (trivial AVATAR). For
9// each multi-component input clause, emit one output clause per
10// component containing only that component's literals. Single-
11// component clauses pass through unchanged.
12//
13// Sound when split components are ground or when each split's
14// variables don't escape into the SAT-side coordination -- which is
15// always the case here because we're splitting variable-disjoint
16// components. The components don't share variables by construction
17// (that's what "component" means), so each can be saturated
18// independently and any UNSAT in any sub-clause is UNSAT for the
19// whole clause set.
20//
21// API:
22// nx_avatar_split_clause(c, out, cap) -> n_emitted
23// nx_avatar_split_all(in, n_in, out, cap) -> n_emitted
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"
37import "nx_clause_components.nx"
38
39// Split a single clause into its components. out is a flat array of
40// Clause structs; cap is its size in clauses. Returns count of
41// components emitted (always >= 1; equal to nx_clause_n_components).
42// Returns -1 if cap exceeded.
43func nx_avatar_split_clause(c: *Clause, out: *Clause, cap: nx_int) -> nx_int {
44 if c.n_lits == 0 {
45 // Empty clause: just emit it as-is.
46 if cap < 1 { return 0 - 1 }
47 let dest: *Clause = out
48 dest.n_lits = 0
49 dest.lits = c.lits
50 return 1
51 }
52
53 // Classify literals into components.
54 let comp_ids: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
55 let n_comp: nx_int = nx_clause_components_classify(c, comp_ids)
56
57 if n_comp == 1 {
58 // Single component -- pass through unchanged.
59 if cap < 1 { return 0 - 1 }
60 let dest: *Clause = out
61 dest.n_lits = c.n_lits
62 dest.lits = c.lits
63 return 1
64 }
65 if n_comp > cap { return 0 - 1 }
66
67 // For each distinct component root, build a new clause containing
68 // its literals. Walk in-order so the components are emitted in
69 // first-appearance order.
70 let seen: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
71 var n_seen: nx_int = 0
72
73 var k: nx_int = 0
74 while k < c.n_lits {
75 let root: nx_int = comp_ids[k]
76 // Have we seen this root before?
77 var already: nx_int = 0
78 var s: nx_int = 0
79 while s < n_seen {
80 if seen[s] == root { already = 1 }
81 s = s + 1
82 }
83 if already == 0 {
84 // New component -- build its clause.
85 seen[n_seen] = root
86 let dest: *Clause = ((out as nx_int) + (n_seen * NX_CLAUSE_BYTES)) as *Clause
87 dest.n_lits = 0
88 dest.lits = (sys_mmap((NX_CLAUSE_MAX_LITS * NX_LITERAL_BYTES) as i64)) as *Literal
89 // Walk all literals of c, append those whose comp_id equals root.
90 var m: nx_int = 0
91 while m < c.n_lits {
92 if comp_ids[m] == root {
93 let lm: *Literal = nx_clause_lit_at(c, m)
94 let _r: *NxResult = nx_clause_add(dest, lm)
95 }
96 m = m + 1
97 }
98 n_seen = n_seen + 1
99 }
100 k = k + 1
101 }
102 return n_seen
103}
104
105// Split every clause in the input set; emit all components into out.
106// cap is the output array's clause capacity. Returns total count or
107// -1 on capacity overflow.
108// Number of multi-component clauses in the input set. Diagnostic
109// for "is the AVATAR pre-pass worth running on this problem?"
110func nx_avatar_count_splittable(input: *Clause, n_in: nx_int) -> nx_int {
111 var count: nx_int = 0
112 var i: nx_int = 0
113 while i < n_in {
114 let c: *Clause = ((input as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
115 if c.n_lits >= 2 {
116 if nx_clause_n_components(c) > 1 { count = count + 1 }
117 }
118 i = i + 1
119 }
120 return count
121}
122
123func nx_avatar_split_all(input: *Clause, n_in: nx_int,
124 out: *Clause, cap: nx_int) -> nx_int {
125 var n_out: nx_int = 0
126 var i: nx_int = 0
127 while i < n_in {
128 let c: *Clause = ((input as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
129 let remaining: nx_int = cap - n_out
130 let dest_start: *Clause = ((out as nx_int) + (n_out * NX_CLAUSE_BYTES)) as *Clause
131 let n_emitted: nx_int = nx_avatar_split_clause(c, dest_start, remaining)
132 if n_emitted < 0 { return 0 - 1 }
133 n_out = n_out + n_emitted
134 i = i + 1
135 }
136 return n_out
137}