nx_eq_factor.nx source

1// nx_eq_factor.nx -- equality factoring (Bachmair-Ganzinger 1994). 2// 3// Per Vampire-displacement roadmap Phase 2. Standard inference rule 4// in superposition calculus, paired with paramodulation. Required 5// for completeness when an equational saturation fires. 6// 7// Standard formulation: 8// 9// C ∨ s ≃ t ∨ s' ≃ t' (two positive equality literals) 10// σ = mgu(s, s') 11// -------------------------- 12// (C ∨ s ≃ t ∨ t ≄ t')σ 13// 14// Reading: when two equality literals share a unifiable LHS, ONE of 15// them (here s ≃ t) is kept and the OTHER's RHS is asserted DIFFERENT 16// from the kept RHS (t ≄ t'). Future inference may resolve t≄t' 17// against an equality elsewhere; if t and t' really were equal the 18// resolvent is contradicted, otherwise the disequality survives. 19// 20// Ordering side conditions for full Bachmair-Ganzinger soundness are 21// the caller's responsibility (typically checked via KBO/LPO): 22// - s ≃ t is selected or maximal in C 23// - sσ ⊁ tσ 24// - (s ≃ t)σ ⊁ (s' ≃ t')σ 25// 26// API: caller picks the two equality-literal indices i and j; the 27// primitive validates polarity + equality head, unifies the LHS pair, 28// and emits the residual. 29 30// nx_safety_envelope: 31// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 32// sil_target: SIL1 33// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 34// verdict: NOT_YET_EVALUATED 35 36import "nx_syscalls.nx" 37import "nx_runtime.nx" 38import "nx_tier.nx" 39import "nx_result.nx" 40import "nx_unify.nx" 41import "nx_resolution.nx" 42 43// Build a NEG eq(t, t') literal from two terms. Used to construct 44// the disequality side of the factoring conclusion. 45func nx_eq_factor_make_diseq(t1: *Term, t2: *Term, eq_sym: nx_int) -> *Literal { 46 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term 47 let a0: *Term = args 48 a0.kind = t1.kind; a0.sym = t1.sym; a0.n_args = t1.n_args; a0.args = t1.args 49 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term 50 a1.kind = t2.kind; a1.sym = t2.sym; a1.n_args = t2.n_args; a1.args = t2.args 51 let neq_atom: *Term = nx_term_app(eq_sym, 2, args) 52 return nx_lit_make(NX_LIT_NEG, neq_atom) 53} 54 55// Equality factoring entry. c_out is caller-allocated; populated 56// with the conclusion. Returns Result<n_lits, NX_ERR_*>: 57// NX_ERR_OUT_OF_RANGE -- bad index 58// NX_ERR_TAG_MISMATCH -- chosen literal isn't +eq(_, _) 59// NX_ERR_INVALID_INPUT -- i == j 60// underlying nx_unify err codes if LHS unification fails 61func nx_eq_factor(c: *Clause, i: nx_int, j: nx_int, 62 eq_sym: nx_int, c_out: *Clause) -> *NxResult { 63 if i < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 64 if j < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 65 if i == j { return nx_result_err(NX_ERR_INVALID_INPUT) } 66 if i >= c.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 67 if j >= c.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 68 69 let li: *Literal = nx_clause_lit_at(c, i) 70 let lj: *Literal = nx_clause_lit_at(c, j) 71 72 // Both must be positive equality literals. 73 if li.sign != NX_LIT_POS { return nx_result_err(NX_ERR_TAG_MISMATCH) } 74 if lj.sign != NX_LIT_POS { return nx_result_err(NX_ERR_TAG_MISMATCH) } 75 if li.atom.kind != NX_TERM_APP { return nx_result_err(NX_ERR_TAG_MISMATCH) } 76 if lj.atom.kind != NX_TERM_APP { return nx_result_err(NX_ERR_TAG_MISMATCH) } 77 if li.atom.sym != eq_sym { return nx_result_err(NX_ERR_TAG_MISMATCH) } 78 if lj.atom.sym != eq_sym { return nx_result_err(NX_ERR_TAG_MISMATCH) } 79 if li.atom.n_args != 2 { return nx_result_err(NX_ERR_TAG_MISMATCH) } 80 if lj.atom.n_args != 2 { return nx_result_err(NX_ERR_TAG_MISMATCH) } 81 82 // Pull s, t, s', t'. 83 let s_term: *Term = nx_term_arg(li.atom, 0) 84 let t_term: *Term = nx_term_arg(li.atom, 1) 85 let s2_term: *Term = nx_term_arg(lj.atom, 0) 86 let t2_term: *Term = nx_term_arg(lj.atom, 1) 87 88 // Unify s with s'. 89 let sigma: *Subst = nx_subst_new() 90 let r_un: *NxResult = nx_unify(s_term, s2_term, sigma) 91 if nx_result_is_err(r_un) == 1 { return r_un } 92 93 // Build conclusion: keep all literals of c except j, replace j 94 // with NEG eq(t, t') -- everything under sigma. 95 var k: nx_int = 0 96 while k < c.n_lits { 97 if k != j { 98 let lk: *Literal = nx_clause_lit_at(c, k) 99 let lk_sub: *Literal = nx_lit_apply_subst(lk, sigma) 100 let _r: *NxResult = nx_clause_add(c_out, lk_sub) 101 } 102 k = k + 1 103 } 104 // Append the new disequality t ≄ t' under sigma. 105 let t_sub: *Term = nx_subst_apply(t_term, sigma) 106 let t2_sub: *Term = nx_subst_apply(t2_term, sigma) 107 let diseq: *Literal = nx_eq_factor_make_diseq(t_sub, t2_sub, eq_sym) 108 let _r2: *NxResult = nx_clause_add(c_out, diseq) 109 110 return nx_result_ok(c_out.n_lits) 111}