nx_fof_tseitin.nx source
↩ module page · 204 lines · 7700 B
1// nx_fof_tseitin.nx -- linear-size FOF -> CNF via Tseitin encoding.
2//
3// Per Vampire-displacement roadmap Phase 2. The naive distribution
4// step in nx_fof_cnf can produce 2^n clauses for n-deep alternations
5// of & and |. Tseitin 1968 introduces a fresh propositional variable
6// p_G for each non-atomic subformula G and asserts the equivalence
7// p_G <-> G as 2-3 clauses. Result: O(n) clauses.
8//
9// Pre-condition: input formula is in NNF and quantifier-free (i.e.
10// post-Skolemize + post-drop_forall). Tseitin doesn't handle IFF or
11// IMP directly -- caller must run elim_iff + elim_imp first (those
12// are also pre-conditions of the existing distribute step).
13//
14// Algorithm:
15//
16// ts_walk(F) returns a Literal that is "true iff F is true".
17//
18// ATOM -> POS atom
19// NEG ATOM-> NEG atom (no fresh var needed)
20// NEG G -> introduce p; emit p <-> ~ts_walk(G)
21// AND L R -> introduce p; recurse on L,R; emit p <-> l_lit & r_lit
22// OR L R -> introduce p; recurse on L,R; emit p <-> l_lit | r_lit
23//
24// Top-level: emit a unit clause asserting ts_walk(F) is true.
25//
26// Equivalence clauses (each ↔ becomes 2-3 clauses):
27//
28// p ↔ ~q : (p ∨ q) ∧ (~p ∨ ~q)
29// p ↔ q ∧ r : (~p ∨ q) ∧ (~p ∨ r) ∧ (p ∨ ~q ∨ ~r)
30// p ↔ q ∨ r : (~p ∨ q ∨ r) ∧ (p ∨ ~q) ∧ (p ∨ ~r)
31//
32// Bits-up nx_int. Tseitin variables get sym_ids in their own range.
33
34// nx_safety_envelope:
35// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
36// sil_target: SIL1
37// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
38// verdict: NOT_YET_EVALUATED
39
40import "nx_syscalls.nx"
41import "nx_runtime.nx"
42import "nx_tier.nx"
43import "nx_result.nx"
44import "nx_unify.nx"
45import "nx_resolution.nx"
46import "nx_fof.nx"
47
48// Tseitin propositional vars get sym_ids in this range -- well above
49// user symbols (NX_TPTP_SYM_BASE = 1000) and Skolem fns
50// (NX_TPTP_SK_BASE = 900_000).
51const NX_TPTP_TS_BASE: nx_int = 800000
52
53struct TseitinCtx {
54 next_id: nx_int, // counter for fresh propositional vars
55 out: *Clause, // flat array of NX_CLAUSE_BYTES
56 n_out: nx_int,
57 cap: nx_int,
58 overflow: nx_int, // 1 if cap exceeded; caller checks
59}
60
61const NX_TS_CTX_BYTES: nx_int = 40
62
63func nx_ts_ctx_new(out: *Clause, cap: nx_int) -> *TseitinCtx {
64 let ctx: *TseitinCtx = (sys_mmap(NX_TS_CTX_BYTES as i64)) as *TseitinCtx
65 ctx.next_id = 0
66 ctx.out = out
67 ctx.n_out = 0
68 ctx.cap = cap
69 ctx.overflow = 0
70 return ctx
71}
72
73// Emit a clause built from a flat array of literals.
74func nx_ts_emit(ctx: *TseitinCtx, lits: *Literal, n_lits: nx_int) {
75 if ctx.n_out >= ctx.cap { ctx.overflow = 1; return }
76 let dest: *Clause = ((ctx.out as nx_int) + (ctx.n_out * NX_CLAUSE_BYTES)) as *Clause
77 let c: *Clause = nx_clause_new()
78 var i: nx_int = 0
79 while i < n_lits {
80 let l: *Literal = ((lits as nx_int) + (i * NX_LITERAL_BYTES)) as *Literal
81 let _r: *NxResult = nx_clause_add(c, l)
82 i = i + 1
83 }
84 dest.n_lits = c.n_lits
85 dest.lits = c.lits
86 ctx.n_out = ctx.n_out + 1
87}
88
89// Allocate a fresh propositional variable atom (0-arity APP).
90func nx_ts_fresh(ctx: *TseitinCtx) -> *Term {
91 let sym: nx_int = NX_TPTP_TS_BASE + ctx.next_id
92 ctx.next_id = ctx.next_id + 1
93 return nx_term_app(sym, 0, 0 as *Term)
94}
95
96// Build a Literal pair (POS / NEG of the same atom).
97func nx_ts_pos(atom: *Term) -> *Literal { return nx_lit_make(NX_LIT_POS, atom) }
98func nx_ts_neg(atom: *Term) -> *Literal { return nx_lit_make(NX_LIT_NEG, atom) }
99
100// Flip the sign of a literal (POS <-> NEG).
101func nx_ts_flip(l: *Literal) -> *Literal {
102 var s: nx_int = NX_LIT_POS
103 if l.sign == NX_LIT_POS { s = NX_LIT_NEG }
104 return nx_lit_make(s, l.atom)
105}
106
107// Pack two literals into a 2-element flat buffer.
108func nx_ts_pair(a: *Literal, b: *Literal) -> *Literal {
109 let buf: *Literal = (sys_mmap((2 * NX_LITERAL_BYTES) as i64)) as *Literal
110 let s0: *Literal = buf
111 s0.sign = a.sign; s0.atom = a.atom
112 let s1: *Literal = ((buf as nx_int) + NX_LITERAL_BYTES) as *Literal
113 s1.sign = b.sign; s1.atom = b.atom
114 return buf
115}
116
117// Pack three literals into a 3-element flat buffer.
118func nx_ts_triple(a: *Literal, b: *Literal, c: *Literal) -> *Literal {
119 let buf: *Literal = (sys_mmap((3 * NX_LITERAL_BYTES) as i64)) as *Literal
120 let s0: *Literal = buf
121 s0.sign = a.sign; s0.atom = a.atom
122 let s1: *Literal = ((buf as nx_int) + NX_LITERAL_BYTES) as *Literal
123 s1.sign = b.sign; s1.atom = b.atom
124 let s2: *Literal = ((buf as nx_int) + (2 * NX_LITERAL_BYTES)) as *Literal
125 s2.sign = c.sign; s2.atom = c.atom
126 return buf
127}
128
129// One-element buffer (for unit clause emission).
130func nx_ts_single(a: *Literal) -> *Literal {
131 let buf: *Literal = (sys_mmap(NX_LITERAL_BYTES as i64)) as *Literal
132 buf.sign = a.sign; buf.atom = a.atom
133 return buf
134}
135
136// Walk the formula, emit definitional clauses, return the literal
137// representing F's truth value.
138func nx_ts_walk(ctx: *TseitinCtx, f: *Fof) -> *Literal {
139 if f.kind == NX_FOF_ATOM {
140 return nx_ts_pos(f.atom)
141 }
142 if f.kind == NX_FOF_NEG {
143 // Special-case ~ATOM for cleaner output (no fresh var needed).
144 if f.left.kind == NX_FOF_ATOM {
145 return nx_ts_neg(f.left.atom)
146 }
147 // ~complex: introduce p, emit p ↔ ~q
148 let q: *Literal = nx_ts_walk(ctx, f.left)
149 let p_atom: *Term = nx_ts_fresh(ctx)
150 let p_pos: *Literal = nx_ts_pos(p_atom)
151 let p_neg: *Literal = nx_ts_neg(p_atom)
152 let nq: *Literal = nx_ts_flip(q)
153 // (p ∨ q)
154 nx_ts_emit(ctx, nx_ts_pair(p_pos, q), 2)
155 // (~p ∨ ~q)
156 nx_ts_emit(ctx, nx_ts_pair(p_neg, nq), 2)
157 return p_pos
158 }
159 if f.kind == NX_FOF_AND {
160 let l: *Literal = nx_ts_walk(ctx, f.left)
161 let r: *Literal = nx_ts_walk(ctx, f.right)
162 let p_atom: *Term = nx_ts_fresh(ctx)
163 let p_pos: *Literal = nx_ts_pos(p_atom)
164 let p_neg: *Literal = nx_ts_neg(p_atom)
165 // (~p ∨ l)
166 nx_ts_emit(ctx, nx_ts_pair(p_neg, l), 2)
167 // (~p ∨ r)
168 nx_ts_emit(ctx, nx_ts_pair(p_neg, r), 2)
169 // (p ∨ ~l ∨ ~r)
170 nx_ts_emit(ctx, nx_ts_triple(p_pos, nx_ts_flip(l), nx_ts_flip(r)), 3)
171 return p_pos
172 }
173 if f.kind == NX_FOF_OR {
174 let l: *Literal = nx_ts_walk(ctx, f.left)
175 let r: *Literal = nx_ts_walk(ctx, f.right)
176 let p_atom: *Term = nx_ts_fresh(ctx)
177 let p_pos: *Literal = nx_ts_pos(p_atom)
178 let p_neg: *Literal = nx_ts_neg(p_atom)
179 // (~p ∨ l ∨ r)
180 nx_ts_emit(ctx, nx_ts_triple(p_neg, l, r), 3)
181 // (p ∨ ~l)
182 nx_ts_emit(ctx, nx_ts_pair(p_pos, nx_ts_flip(l)), 2)
183 // (p ∨ ~r)
184 nx_ts_emit(ctx, nx_ts_pair(p_pos, nx_ts_flip(r)), 2)
185 return p_pos
186 }
187 // Defensive: IFF/IMP/quantifiers should not reach here (caller
188 // ran elim_iff + elim_imp + skolemize + drop_forall first).
189 return nx_ts_pos(f.atom)
190}
191
192// Top-level entry: convert NNF + quantifier-free formula F to CNF.
193// out_clauses is caller-allocated; out_n is updated. Returns 0 on
194// success, negative on capacity overflow.
195func nx_fof_to_cnf_tseitin(f: *Fof, out_clauses: *Clause, out_n: *nx_int,
196 cap: nx_int) -> nx_int {
197 let ctx: *TseitinCtx = nx_ts_ctx_new(out_clauses, cap)
198 let top: *Literal = nx_ts_walk(ctx, f)
199 // Unit clause asserting the top is true.
200 nx_ts_emit(ctx, nx_ts_single(top), 1)
201 out_n[0] = ctx.n_out
202 if ctx.overflow == 1 { return 0 - 1 }
203 return 0
204}