nx_avatar_encode.nx

nx_avatar_encode.nx -- full AVATAR encoder. Per Vampire-displacement roadmap Phase 2. Generates the hybrid FO-clauses-plus-SAT-problem that the full AVATAR loop consumes. For each multi-component input clause C with components C_1..C_n: Allocate fresh split atoms sp_1, sp_2, ..., sp_n (sequential from a caller-supplied base). Emit one FO clause per component, prefixed with the negation of that component's split atom: {~sp_i, C_i_lits...} (one per i in 1..n) Add one SAT clause to the SatFormula asserting that at least one component is selected: [sp_1, sp_2, ..., sp_n] (DIMACS positive lits) Single-component clauses pass through unchanged: no guard literals added, no SAT clauses contributed. Soundness: the guard literal ~sp_i in the FO clause is true when the SAT solver assigns sp_i=FALSE, making the clause trivially satisfied (no constraint on saturation). When sp_i=TRUE, the guard is false and saturation must close the component. The SAT coordination clause [sp_1..sp_n] forces at least one component per multi-component group to be active. API: nx_avatar_encode_to_sat(input, n_input, sp_base, fo_out, fo_cap, sat_formula, *next_sp_id) -> n_fo_emitted