nx_fof_cnf.nx source

1// nx_fof_cnf.nx -- FOF -> CNF conversion pipeline. 2// 3// Per Vampire-displacement roadmap Phase 2. Closes the FOF axis end- 4// to-end: a parsed *Fof tree (from nx_fof_parse) becomes an array of 5// *Clause that the saturation loop can consume. Required for the 6// CASC FOF division -- competition problems are stated in FOF and 7// must be CNF-converted before resolution + paramodulation can fire. 8// 9// Standard pipeline: 10// 1. eliminate IFF A<=>B => (A=>B) & (B=>A) 11// 2. eliminate IMP A=>B => ~A | B 12// 3. NNF (push NEG) ~~A=>A; De Morgan; swap quantifiers 13// 4. Skolemize ?[X]:F => F[X := sk_N(U_1..U_k)] where U_i 14// are the universal vars in scope 15// 5. drop FORALL all remaining vars become implicitly free 16// 6. distribute & / | A|(B&C) => (A|B)&(A|C) (may iterate) 17// 7. extract clauses AND-of-OR-of-literals -> array of *Clause 18// 19// Each pipeline stage is a pure function -- callers can inspect 20// intermediate forms. Top-level entry nx_fof_to_cnf chains them. 21 22// nx_safety_envelope: 23// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 24// sil_target: SIL1 25// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 26// verdict: NOT_YET_EVALUATED 27 28import "nx_syscalls.nx" 29import "nx_runtime.nx" 30import "nx_tier.nx" 31import "nx_result.nx" 32import "nx_unify.nx" 33import "nx_resolution.nx" 34import "nx_tptp_symtab.nx" 35import "nx_fof.nx" 36 37// Skolem functions get sym_ids in this range -- we assume user 38// symbols stay below NX_TPTP_SK_BASE. 256 capacity (NX_TPTP_SYM_MAX) 39// gives plenty of headroom in practice. 40const NX_TPTP_SK_BASE: nx_int = 900000 41 42// ===== Stage 1: eliminate IFF ====================================== 43// A <=> B => (A => B) & (B => A) 44func nx_fof_elim_iff(f: *Fof) -> *Fof { 45 if f.kind == NX_FOF_ATOM { return f } 46 if f.kind == NX_FOF_NEG { 47 return nx_fof_neg(nx_fof_elim_iff(f.left)) 48 } 49 if f.kind == NX_FOF_FORALL { 50 return nx_fof_quantified(NX_FOF_FORALL, f.var_id, nx_fof_elim_iff(f.left)) 51 } 52 if f.kind == NX_FOF_EXISTS { 53 return nx_fof_quantified(NX_FOF_EXISTS, f.var_id, nx_fof_elim_iff(f.left)) 54 } 55 let l: *Fof = nx_fof_elim_iff(f.left) 56 let r: *Fof = nx_fof_elim_iff(f.right) 57 if f.kind == NX_FOF_IFF { 58 // Build (l => r) & (r => l) -- use elim_iff result, no need to 59 // re-eliminate since the rewrite produces only AND/IMP nodes. 60 let l_imp_r: *Fof = nx_fof_binary(NX_FOF_IMP, l, r) 61 let r_imp_l: *Fof = nx_fof_binary(NX_FOF_IMP, r, l) 62 return nx_fof_binary(NX_FOF_AND, l_imp_r, r_imp_l) 63 } 64 return nx_fof_binary(f.kind, l, r) 65} 66 67// ===== Stage 2: eliminate IMP ====================================== 68// A => B => ~A | B 69func nx_fof_elim_imp(f: *Fof) -> *Fof { 70 if f.kind == NX_FOF_ATOM { return f } 71 if f.kind == NX_FOF_NEG { 72 return nx_fof_neg(nx_fof_elim_imp(f.left)) 73 } 74 if f.kind == NX_FOF_FORALL { 75 return nx_fof_quantified(NX_FOF_FORALL, f.var_id, nx_fof_elim_imp(f.left)) 76 } 77 if f.kind == NX_FOF_EXISTS { 78 return nx_fof_quantified(NX_FOF_EXISTS, f.var_id, nx_fof_elim_imp(f.left)) 79 } 80 let l: *Fof = nx_fof_elim_imp(f.left) 81 let r: *Fof = nx_fof_elim_imp(f.right) 82 if f.kind == NX_FOF_IMP { 83 return nx_fof_binary(NX_FOF_OR, nx_fof_neg(l), r) 84 } 85 return nx_fof_binary(f.kind, l, r) 86} 87 88// ===== Stage 3: NNF (push negations inward) ======================= 89// ~~A => A 90// ~(A & B) => ~A | ~B 91// ~(A | B) => ~A & ~B 92// ~∀x.A => ∃x.~A 93// ~∃x.A => ∀x.~A 94// ~atom => ~atom (literal; cannot push further) 95// 96// Pre: input has no IFF or IMP (run elim_iff + elim_imp first). 97func nx_fof_to_nnf(f: *Fof) -> *Fof { 98 if f.kind == NX_FOF_ATOM { return f } 99 if f.kind == NX_FOF_AND { 100 return nx_fof_binary(NX_FOF_AND, nx_fof_to_nnf(f.left), nx_fof_to_nnf(f.right)) 101 } 102 if f.kind == NX_FOF_OR { 103 return nx_fof_binary(NX_FOF_OR, nx_fof_to_nnf(f.left), nx_fof_to_nnf(f.right)) 104 } 105 if f.kind == NX_FOF_FORALL { 106 return nx_fof_quantified(NX_FOF_FORALL, f.var_id, nx_fof_to_nnf(f.left)) 107 } 108 if f.kind == NX_FOF_EXISTS { 109 return nx_fof_quantified(NX_FOF_EXISTS, f.var_id, nx_fof_to_nnf(f.left)) 110 } 111 // f.kind == NEG -- look at the child to apply the right rule. 112 let inner: *Fof = f.left 113 if inner.kind == NX_FOF_NEG { 114 // ~~A -> A 115 return nx_fof_to_nnf(inner.left) 116 } 117 if inner.kind == NX_FOF_AND { 118 // ~(A & B) -> ~A | ~B 119 return nx_fof_binary(NX_FOF_OR, 120 nx_fof_to_nnf(nx_fof_neg(inner.left)), 121 nx_fof_to_nnf(nx_fof_neg(inner.right))) 122 } 123 if inner.kind == NX_FOF_OR { 124 // ~(A | B) -> ~A & ~B 125 return nx_fof_binary(NX_FOF_AND, 126 nx_fof_to_nnf(nx_fof_neg(inner.left)), 127 nx_fof_to_nnf(nx_fof_neg(inner.right))) 128 } 129 if inner.kind == NX_FOF_FORALL { 130 // ~∀x.A -> ∃x.~A 131 return nx_fof_quantified(NX_FOF_EXISTS, inner.var_id, 132 nx_fof_to_nnf(nx_fof_neg(inner.left))) 133 } 134 if inner.kind == NX_FOF_EXISTS { 135 // ~∃x.A -> ∀x.~A 136 return nx_fof_quantified(NX_FOF_FORALL, inner.var_id, 137 nx_fof_to_nnf(nx_fof_neg(inner.left))) 138 } 139 // ~atom -- leave as NEG of ATOM. 140 return f 141} 142 143// ===== Term-level variable substitution ============================ 144// Returns a new Term with every occurrence of var `var_id` replaced by 145// `replacement`. Recursive; doesn't modify the input. 146func nx_term_subst_var(t: *Term, var_id: nx_int, replacement: *Term) -> *Term { 147 if t.kind == NX_TERM_VAR { 148 if t.sym == var_id { return replacement } 149 return t 150 } 151 if t.kind == NX_TERM_CONST { return t } 152 // APP: rebuild with substituted children. 153 if t.n_args == 0 { return t } 154 let new_args: *Term = (sys_mmap((t.n_args * NX_TERM_BYTES) as i64)) as *Term 155 var any_changed: nx_int = 0 156 var i: nx_int = 0 157 while i < t.n_args { 158 let child: *Term = nx_term_arg(t, i) 159 let new_child: *Term = nx_term_subst_var(child, var_id, replacement) 160 let dest: *Term = ((new_args as nx_int) + (i * NX_TERM_BYTES)) as *Term 161 dest.kind = new_child.kind 162 dest.sym = new_child.sym 163 dest.n_args = new_child.n_args 164 dest.args = new_child.args 165 if (new_child as nx_int) != (child as nx_int) { any_changed = 1 } 166 i = i + 1 167 } 168 if any_changed == 1 { return nx_term_app(t.sym, t.n_args, new_args) } 169 return t 170} 171 172// ===== Fof-level variable substitution ============================= 173// Walk the formula tree replacing var_id in every embedded atom. 174// Skips occurrences inside a quantifier that re-binds var_id (variable 175// shadowing -- though in proper NNF after skolemize this shouldn't 176// arise, the safety check keeps us correct under future restructure). 177func nx_fof_subst_var(f: *Fof, var_id: nx_int, replacement: *Term) -> *Fof { 178 if f.kind == NX_FOF_ATOM { 179 return nx_fof_atom(nx_term_subst_var(f.atom, var_id, replacement)) 180 } 181 if f.kind == NX_FOF_NEG { 182 return nx_fof_neg(nx_fof_subst_var(f.left, var_id, replacement)) 183 } 184 if f.kind == NX_FOF_FORALL { 185 if f.var_id == var_id { return f } // shadowed 186 return nx_fof_quantified(NX_FOF_FORALL, f.var_id, 187 nx_fof_subst_var(f.left, var_id, replacement)) 188 } 189 if f.kind == NX_FOF_EXISTS { 190 if f.var_id == var_id { return f } 191 return nx_fof_quantified(NX_FOF_EXISTS, f.var_id, 192 nx_fof_subst_var(f.left, var_id, replacement)) 193 } 194 return nx_fof_binary(f.kind, 195 nx_fof_subst_var(f.left, var_id, replacement), 196 nx_fof_subst_var(f.right, var_id, replacement)) 197} 198 199// ===== Stage 4: Skolemization ===================================== 200// Walk the NNF formula; track universal vars in scope. At each 201// existential, build a Skolem-function term applied to the universals 202// in scope, substitute it for the existential's bound var, drop the 203// quantifier. 204// 205// Universal-vars-in-scope passed as a flat array + count; capped at 206// NX_TPTP_VAR_MAX (already 64). *next_sk_id is the running Skolem 207// function counter -- shared across the recursive walk. 208const NX_FOF_SK_MAX_UNIV: nx_int = 64 209 210func nx_fof_skolem_walk(f: *Fof, univ_vars: *nx_int, n_univ: nx_int, 211 next_sk_id: *nx_int) -> *Fof { 212 if f.kind == NX_FOF_ATOM { return f } 213 if f.kind == NX_FOF_NEG { 214 return nx_fof_neg(nx_fof_skolem_walk(f.left, univ_vars, n_univ, next_sk_id)) 215 } 216 if f.kind == NX_FOF_AND { 217 return nx_fof_binary(NX_FOF_AND, 218 nx_fof_skolem_walk(f.left, univ_vars, n_univ, next_sk_id), 219 nx_fof_skolem_walk(f.right, univ_vars, n_univ, next_sk_id)) 220 } 221 if f.kind == NX_FOF_OR { 222 return nx_fof_binary(NX_FOF_OR, 223 nx_fof_skolem_walk(f.left, univ_vars, n_univ, next_sk_id), 224 nx_fof_skolem_walk(f.right, univ_vars, n_univ, next_sk_id)) 225 } 226 if f.kind == NX_FOF_FORALL { 227 // Push f.var_id onto the universal stack, recurse on body. 228 if n_univ >= NX_FOF_SK_MAX_UNIV { return f } // cap; treat as opaque 229 univ_vars[n_univ] = f.var_id 230 let body: *Fof = nx_fof_skolem_walk(f.left, univ_vars, n_univ + 1, next_sk_id) 231 return nx_fof_quantified(NX_FOF_FORALL, f.var_id, body) 232 } 233 if f.kind == NX_FOF_EXISTS { 234 // Build sk_N(U_1, ..., U_k) and substitute for f.var_id. 235 let sk_id: nx_int = NX_TPTP_SK_BASE + next_sk_id[0] 236 next_sk_id[0] = next_sk_id[0] + 1 237 var sk_term: *Term = 0 as *Term 238 if n_univ == 0 { 239 // No universals in scope -- Skolem is a constant. 240 sk_term = nx_term_const(sk_id) 241 } else { 242 let args: *Term = (sys_mmap((n_univ * NX_TERM_BYTES) as i64)) as *Term 243 var i: nx_int = 0 244 while i < n_univ { 245 let dest: *Term = ((args as nx_int) + (i * NX_TERM_BYTES)) as *Term 246 dest.kind = NX_TERM_VAR 247 dest.sym = univ_vars[i] 248 dest.n_args = 0 249 dest.args = 0 as *Term 250 i = i + 1 251 } 252 sk_term = nx_term_app(sk_id, n_univ, args) 253 } 254 // Substitute and continue skolemizing the body (which may have 255 // nested existentials). 256 let body_sub: *Fof = nx_fof_subst_var(f.left, f.var_id, sk_term) 257 return nx_fof_skolem_walk(body_sub, univ_vars, n_univ, next_sk_id) 258 } 259 return f // defensive 260} 261 262func nx_fof_skolemize(f: *Fof) -> *Fof { 263 let univ_vars: *nx_int = (sys_mmap((NX_FOF_SK_MAX_UNIV * 8) as i64)) as *nx_int 264 let next_sk_id: *nx_int = (sys_mmap(8)) as *nx_int 265 next_sk_id[0] = 0 266 return nx_fof_skolem_walk(f, univ_vars, 0, next_sk_id) 267} 268 269// ===== Stage 5: drop universal quantifiers ========================= 270// After skolemize, only FORALL nodes remain (no EXISTS). Drop each -- 271// the bound var becomes implicitly universally quantified at the 272// clause level (standard CNF convention). 273func nx_fof_drop_forall(f: *Fof) -> *Fof { 274 if f.kind == NX_FOF_FORALL { return nx_fof_drop_forall(f.left) } 275 if f.kind == NX_FOF_ATOM { return f } 276 if f.kind == NX_FOF_NEG { return nx_fof_neg(nx_fof_drop_forall(f.left)) } 277 if f.kind == NX_FOF_AND { 278 return nx_fof_binary(NX_FOF_AND, nx_fof_drop_forall(f.left), nx_fof_drop_forall(f.right)) 279 } 280 if f.kind == NX_FOF_OR { 281 return nx_fof_binary(NX_FOF_OR, nx_fof_drop_forall(f.left), nx_fof_drop_forall(f.right)) 282 } 283 return f 284} 285 286// ===== Stage 6: distribute & over | ================================ 287// A | (B & C) => (A | B) & (A | C) 288// (A & B) | C => (A | C) & (B | C) 289// Iterate to fixpoint. Worst case 2^n size blowup but acceptable for 290// CASC-Easy problems; Tseitin transformation would avoid it but 291// requires fresh propositional vars and is queued. 292func nx_fof_distribute_step(f: *Fof) -> *Fof { 293 if f.kind == NX_FOF_ATOM { return f } 294 if f.kind == NX_FOF_NEG { return nx_fof_neg(nx_fof_distribute_step(f.left)) } 295 let l: *Fof = nx_fof_distribute_step(f.left) 296 let r: *Fof = nx_fof_distribute_step(f.right) 297 if f.kind == NX_FOF_AND { return nx_fof_binary(NX_FOF_AND, l, r) } 298 if f.kind == NX_FOF_OR { 299 // (A & B) | C -> (A|C) & (B|C) 300 if l.kind == NX_FOF_AND { 301 return nx_fof_binary(NX_FOF_AND, 302 nx_fof_distribute_step(nx_fof_binary(NX_FOF_OR, l.left, r)), 303 nx_fof_distribute_step(nx_fof_binary(NX_FOF_OR, l.right, r))) 304 } 305 // A | (B & C) -> (A|B) & (A|C) 306 if r.kind == NX_FOF_AND { 307 return nx_fof_binary(NX_FOF_AND, 308 nx_fof_distribute_step(nx_fof_binary(NX_FOF_OR, l, r.left)), 309 nx_fof_distribute_step(nx_fof_binary(NX_FOF_OR, l, r.right))) 310 } 311 return nx_fof_binary(NX_FOF_OR, l, r) 312 } 313 return f 314} 315 316// ===== Stage 7: extract clauses ==================================== 317// After distribution, formula is AND of (OR of literals). Walk: 318// AND(L, R) -> emit clauses from L and R 319// OR or atom -> flatten into one clause 320// 321// `out_clauses` is a caller-allocated array; `out_n` is updated. 322func nx_fof_collect_lits(f: *Fof, c: *Clause) -> nx_int { 323 if f.kind == NX_FOF_OR { 324 let lc: nx_int = nx_fof_collect_lits(f.left, c) 325 if lc != 0 { return lc } 326 return nx_fof_collect_lits(f.right, c) 327 } 328 if f.kind == NX_FOF_ATOM { 329 let _r: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, f.atom)) 330 return 0 331 } 332 if f.kind == NX_FOF_NEG { 333 if f.left.kind == NX_FOF_ATOM { 334 let _r: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_NEG, f.left.atom)) 335 return 0 336 } 337 return 0 - 1 // ill-formed: NEG of non-atom past NNF 338 } 339 return 0 - 1 340} 341 342func nx_fof_extract_clauses(f: *Fof, out_clauses: *Clause, out_n: *nx_int, 343 cap: nx_int) -> nx_int { 344 if f.kind == NX_FOF_AND { 345 if nx_fof_extract_clauses(f.left, out_clauses, out_n, cap) != 0 { return 0 - 1 } 346 return nx_fof_extract_clauses(f.right, out_clauses, out_n, cap) 347 } 348 // Leaf: this whole subformula is one clause (OR or atom or NEG-atom). 349 if out_n[0] >= cap { return 0 - 1 } 350 let c: *Clause = nx_clause_new() 351 let cr: nx_int = nx_fof_collect_lits(f, c) 352 if cr != 0 { return cr } 353 let dest: *Clause = ((out_clauses as nx_int) + (out_n[0] * NX_CLAUSE_BYTES)) as *Clause 354 dest.n_lits = c.n_lits 355 dest.lits = c.lits 356 out_n[0] = out_n[0] + 1 357 return 0 358} 359 360// ===== Top-level pipeline ========================================== 361// Returns 0 on success, negative on failure. out_clauses is a 362// caller-allocated array of *Clause; out_n is the count populated. 363func nx_fof_to_cnf(f: *Fof, out_clauses: *Clause, out_n: *nx_int, 364 cap: nx_int) -> nx_int { 365 let f1: *Fof = nx_fof_elim_iff(f) 366 let f2: *Fof = nx_fof_elim_imp(f1) 367 let f3: *Fof = nx_fof_to_nnf(f2) 368 let f4: *Fof = nx_fof_skolemize(f3) 369 let f5: *Fof = nx_fof_drop_forall(f4) 370 let f6: *Fof = nx_fof_distribute_step(f5) 371 out_n[0] = 0 372 return nx_fof_extract_clauses(f6, out_clauses, out_n, cap) 373} 374 375// Tseitin-based pipeline: linear-size CNF instead of exponential 376// distribution. Useful for formulas with deeply nested <=> or 377// alternating &/| that would blow up exponentially under naive 378// distribution. Requires nx_fof_tseitin which lives in 379// nx_fof_tseitin.nx -- caller imports that module + calls this 380// wrapper which composes the elim/NNF/skolem stages with Tseitin. 381// 382// Caller imports nx_fof_tseitin.nx for nx_fof_to_cnf_tseitin(). 383// This wrapper just composes the pre-Tseitin stages here. 384func nx_fof_to_nnf_quantifier_free(f: *Fof) -> *Fof { 385 let f1: *Fof = nx_fof_elim_iff(f) 386 let f2: *Fof = nx_fof_elim_imp(f1) 387 let f3: *Fof = nx_fof_to_nnf(f2) 388 let f4: *Fof = nx_fof_skolemize(f3) 389 return nx_fof_drop_forall(f4) 390} 391 392// Count IFF + IMP nodes in a Fof tree. Used by the CNF strategy 393// chooser: many of these means the distribute pipeline will explode 394// exponentially, so Tseitin (linear-size) is preferable. 395func nx_fof_count_iff_imp(f: *Fof) -> nx_int { 396 if f.kind == NX_FOF_ATOM { return 0 } 397 if f.kind == NX_FOF_NEG { return nx_fof_count_iff_imp(f.left) } 398 if f.kind == NX_FOF_FORALL { return nx_fof_count_iff_imp(f.left) } 399 if f.kind == NX_FOF_EXISTS { return nx_fof_count_iff_imp(f.left) } 400 var n: nx_int = 0 401 if f.kind == NX_FOF_IFF { n = 1 } 402 if f.kind == NX_FOF_IMP { n = 1 } 403 return n + nx_fof_count_iff_imp(f.left) + nx_fof_count_iff_imp(f.right) 404}