nx_avatar_encode.nx source
↩ module page · 171 lines · 6624 B
1// nx_avatar_encode.nx -- full AVATAR encoder.
2//
3// Per Vampire-displacement roadmap Phase 2. Generates the hybrid
4// FO-clauses-plus-SAT-problem that the full AVATAR loop consumes.
5//
6// For each multi-component input clause C with components C_1..C_n:
7// Allocate fresh split atoms sp_1, sp_2, ..., sp_n (sequential
8// from a caller-supplied base).
9//
10// Emit one FO clause per component, prefixed with the negation of
11// that component's split atom:
12// {~sp_i, C_i_lits...} (one per i in 1..n)
13//
14// Add one SAT clause to the SatFormula asserting that at least
15// one component is selected:
16// [sp_1, sp_2, ..., sp_n] (DIMACS positive lits)
17//
18// Single-component clauses pass through unchanged: no guard literals
19// added, no SAT clauses contributed.
20//
21// Soundness: the guard literal ~sp_i in the FO clause is true when
22// the SAT solver assigns sp_i=FALSE, making the clause trivially
23// satisfied (no constraint on saturation). When sp_i=TRUE, the
24// guard is false and saturation must close the component. The SAT
25// coordination clause [sp_1..sp_n] forces at least one component
26// per multi-component group to be active.
27//
28// API:
29// nx_avatar_encode_to_sat(input, n_input, sp_base,
30// fo_out, fo_cap,
31// sat_formula,
32// *next_sp_id)
33// -> n_fo_emitted
34
35// nx_safety_envelope:
36// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
37// sil_target: SIL1
38// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
39// verdict: NOT_YET_EVALUATED
40
41import "nx_syscalls.nx"
42import "nx_runtime.nx"
43import "nx_tier.nx"
44import "nx_result.nx"
45import "nx_unify.nx"
46import "nx_resolution.nx"
47import "nx_clause_components.nx"
48import "nx_avatar_split.nx"
49import "nx_sat_solver.nx"
50
51// Reserve sym ids in this range for AVATAR split atoms. Distinct
52// from user (1000+), Tseitin (800000+), Skolem (900000+), Answer
53// (700000+).
54const NX_AVATAR_SP_BASE_SYM: nx_int = 600000
55
56// Build a 0-arity APP atom representing split atom sp_id. Split
57// atoms are propositional (no arguments) -- the AVATAR coordination
58// is purely at the boolean level.
59func nx_avatar_sp_atom(sp_id: nx_int) -> *Term {
60 let sym: nx_int = NX_AVATAR_SP_BASE_SYM + sp_id
61 return nx_term_app(sym, 0, 0 as *Term)
62}
63
64// Build a NEG sp literal -- the guard literal prepended to a
65// component's FO clause.
66func nx_avatar_neg_sp(sp_id: nx_int) -> *Literal {
67 return nx_lit_make(NX_LIT_NEG, nx_avatar_sp_atom(sp_id))
68}
69
70// Encode the input clause set. Outputs:
71// fo_out: flat array of *Clause; populated with single-
72// component clauses (copied) + guard-prefixed
73// component sub-clauses
74// sat_formula: caller-allocated SatFormula; populated with one
75// disjunction sp_1 ∨ ... ∨ sp_n per multi-component
76// input
77// next_sp_id[0]: updated to the next unused split-atom id
78//
79// Returns total FO clause count emitted, or -1 on overflow.
80func nx_avatar_encode_to_sat(input: *Clause, n_input: nx_int,
81 sp_base: nx_int,
82 fo_out: *Clause, fo_cap: nx_int,
83 sat_formula: *SatFormula,
84 next_sp_id: *nx_int) -> nx_int {
85 next_sp_id[0] = sp_base
86 var n_fo: nx_int = 0
87
88 var i: nx_int = 0
89 while i < n_input {
90 let c: *Clause = ((input as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
91
92 // Single-component clauses (incl. unit + ground): pass through.
93 if c.n_lits <= 1 {
94 if n_fo >= fo_cap { return 0 - 1 }
95 let dest: *Clause = ((fo_out as nx_int) + (n_fo * NX_CLAUSE_BYTES)) as *Clause
96 dest.n_lits = c.n_lits
97 dest.lits = c.lits
98 n_fo = n_fo + 1
99 i = i + 1
100 continue
101 }
102
103 let comp_ids: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
104 let n_comp: nx_int = nx_clause_components_classify(c, comp_ids)
105 if n_comp <= 1 {
106 // Single-component multi-literal: pass through.
107 if n_fo >= fo_cap { return 0 - 1 }
108 let dest: *Clause = ((fo_out as nx_int) + (n_fo * NX_CLAUSE_BYTES)) as *Clause
109 dest.n_lits = c.n_lits
110 dest.lits = c.lits
111 n_fo = n_fo + 1
112 i = i + 1
113 continue
114 }
115
116 // Multi-component: allocate n_comp split atoms; emit guarded
117 // FO clauses + a SAT coordination clause.
118 let sp_lits: *nx_int = (sys_mmap((n_comp * 8) as i64)) as *nx_int
119
120 // Walk literals in input order; for each new component root,
121 // build its guarded clause + record its sp_id.
122 let seen: *nx_int = (sys_mmap((c.n_lits * 8) as i64)) as *nx_int
123 var n_seen: nx_int = 0
124
125 var k: nx_int = 0
126 while k < c.n_lits {
127 let root: nx_int = comp_ids[k]
128 var already: nx_int = 0
129 var s: nx_int = 0
130 while s < n_seen {
131 if seen[s] == root { already = 1 }
132 s = s + 1
133 }
134 if already == 0 {
135 // New component -- assign next sp_id, build guarded clause.
136 seen[n_seen] = root
137 let sp_id: nx_int = next_sp_id[0]
138 next_sp_id[0] = next_sp_id[0] + 1
139 sp_lits[n_seen] = sp_id
140
141 if n_fo >= fo_cap { return 0 - 1 }
142 let dest: *Clause = ((fo_out as nx_int) + (n_fo * NX_CLAUSE_BYTES)) as *Clause
143 dest.n_lits = 0
144 dest.lits = (sys_mmap((NX_CLAUSE_MAX_LITS * NX_LITERAL_BYTES) as i64)) as *Literal
145
146 // Prepend the guard ~sp_id.
147 let _rg: *NxResult = nx_clause_add(dest, nx_avatar_neg_sp(sp_id))
148
149 // Append this component's literals.
150 var m: nx_int = 0
151 while m < c.n_lits {
152 if comp_ids[m] == root {
153 let lm: *Literal = nx_clause_lit_at(c, m)
154 let _r: *NxResult = nx_clause_add(dest, lm)
155 }
156 m = m + 1
157 }
158 n_fo = n_fo + 1
159 n_seen = n_seen + 1
160 }
161 k = k + 1
162 }
163
164 // Add SAT coordination clause: [sp_1, sp_2, ..., sp_n_seen]
165 // -- DIMACS positive literals.
166 let _sat_r: nx_int = nx_sat_add_clause(sat_formula, sp_lits, n_seen)
167
168 i = i + 1
169 }
170 return n_fo
171}