nx_paramodulation.nx source
↩ module page · 211 lines · 9383 B
1// nx_paramodulation.nx -- paramodulation rule for equational reasoning.
2//
3// Per Vampire-displacement roadmap Phase 2. The third corner of the
4// equational-reasoning triangle (resolution + demodulation +
5// paramodulation). Where demodulation rewrites with already-oriented
6// equations, paramodulation derives new clauses by unifying a positive
7// equality literal in one clause with a non-variable subterm in another
8// clause, then rewriting under the unifier.
9//
10// Robinson + Wos 1969 standard formulation:
11//
12// Given: C ∨ s = t (clause with positive equality literal)
13// D ∨ L[s'] (clause with subterm s' inside literal L)
14// unify(s, s') = σ
15//
16// Derive: (C ∨ D ∨ L[t])σ
17//
18// where L[s' := t] is L with the chosen subterm position replaced by t,
19// and everything is closed under σ.
20//
21// API: caller picks the equation literal (in eq_clause) and the target
22// literal (in target_clause) by index; this primitive walks the target
23// atom outermost-first looking for the first unifiable subterm. Returns
24// null if no paramodulant exists for that literal pair.
25//
26// Bits-up nx_int. Variables shared across the two input clauses
27// require renaming by the caller for soundness in saturation; this
28// primitive trusts its inputs are appropriately renamed (matches
29// nx_resolve's contract).
30//
31// nx_safety_envelope:
32// intended_use: "Paramodulation inference rule -- equality
33// reasoning in first-order theorem prover"
34// sil_target: SIL2
35// asil_target: QM
36// dal_target: DAL B
37// evidence: [Robinson_Wos_1969_canonical_basis,
38// composes_nx_unify_Result_typed,
39// no_FP]
40// hazard_register: [bug-tape-paramod-into-variable-position,
41// bug-tape-orientation-bias-loss-of-completeness]
42// residual_risk: "Substrate enforces non-variable LHS; full
43// ordering-aware paramodulation (LPO/KBO)
44// queued."
45// verdict: NOT_YET_EVALUATED
46
47import "nx_syscalls.nx"
48import "nx_runtime.nx"
49import "nx_tier.nx"
50import "nx_result.nx"
51import "nx_unify.nx"
52import "nx_resolution.nx"
53
54// Walk `t` outermost-first looking for a non-variable subterm that
55// unifies with `pattern`. On success, fills `out_subst` with the
56// unifier, fills `*out_replaced` with the rewritten target term
57// (pattern-position replaced by `replacement`, all under the unifier),
58// and returns 1. Returns 0 if no unifiable subterm found.
59//
60// `out_subst` must already be initialised by the caller via
61// nx_subst_new() -- bindings discovered during the walk persist.
62func nx_paramod_walk(pattern: *Term, replacement: *Term, t: *Term,
63 out_subst: *Subst, out_replaced: **Term) -> nx_int {
64 // Don't paramodulate at variable positions -- standard rule.
65 if t.kind == NX_TERM_VAR { return 0 }
66
67 // Try root match first.
68 let snapshot: nx_int = out_subst.n
69 let r: *NxResult = nx_unify(pattern, t, out_subst)
70 if nx_result_is_err(r) == 0 {
71 // Unification succeeded -- the rewritten term IS the replacement
72 // under the unifier.
73 out_replaced[0] = nx_subst_apply(replacement, out_subst)
74 return 1
75 }
76 // Rollback and try children.
77 out_subst.n = snapshot
78
79 if t.kind == NX_TERM_CONST { return 0 }
80 if t.n_args == 0 { return 0 }
81
82 // Walk each child; on first success, build a new term with that
83 // child replaced and the unifier applied to all sibling positions
84 // (since the unifier may bind variables that appear in siblings too).
85 var i: nx_int = 0
86 while i < t.n_args {
87 let child: *Term = nx_term_arg(t, i)
88 let inner_replaced: **Term = (sys_mmap(8)) as **Term
89 if nx_paramod_walk(pattern, replacement, child, out_subst, inner_replaced) == 1 {
90 // Found a hit in this subtree. Build new args array.
91 let new_args: *Term = (sys_mmap((t.n_args * NX_TERM_BYTES) as i64)) as *Term
92 var j: nx_int = 0
93 while j < t.n_args {
94 let dest: *Term = ((new_args as nx_int) + (j * NX_TERM_BYTES)) as *Term
95 if j == i {
96 let r_child: *Term = inner_replaced[0]
97 dest.kind = r_child.kind
98 dest.sym = r_child.sym
99 dest.n_args = r_child.n_args
100 dest.args = r_child.args
101 } else {
102 // Apply unifier to sibling.
103 let sib: *Term = nx_term_arg(t, j)
104 let sib_sub: *Term = nx_subst_apply(sib, out_subst)
105 dest.kind = sib_sub.kind
106 dest.sym = sib_sub.sym
107 dest.n_args = sib_sub.n_args
108 dest.args = sib_sub.args
109 }
110 j = j + 1
111 }
112 // Apply unifier to head as well (head is a sym_id, no
113 // substitution needed there -- only term args carry vars).
114 out_replaced[0] = nx_term_app(t.sym, t.n_args, new_args)
115 return 1
116 }
117 i = i + 1
118 }
119 return 0
120}
121
122// Paramodulate eq_clause's literal at eq_idx (must be a positive
123// equality with the supplied eq_sym) into target_clause's literal at
124// target_idx. Builds the paramodulant in c_out (caller allocated).
125//
126// Returns Result<n_lits_in_paramodulant, NX_ERR_*> where errors:
127// NX_ERR_OUT_OF_RANGE -- bad index
128// NX_ERR_TAG_MISMATCH -- eq literal isn't +eq(s, t)
129// NX_ERR_NOT_FOUND -- no unifiable subterm in target literal
130func nx_paramodulate(eq_clause: *Clause, eq_idx: nx_int,
131 target_clause: *Clause, target_idx: nx_int,
132 eq_sym: nx_int, c_out: *Clause) -> *NxResult {
133 if eq_idx < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
134 if eq_idx >= eq_clause.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
135 if target_idx < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
136 if target_idx >= target_clause.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
137
138 let eq_lit: *Literal = nx_clause_lit_at(eq_clause, eq_idx)
139 if eq_lit.sign != NX_LIT_POS { return nx_result_err(NX_ERR_TAG_MISMATCH) }
140 if eq_lit.atom.kind != NX_TERM_APP { return nx_result_err(NX_ERR_TAG_MISMATCH) }
141 if eq_lit.atom.sym != eq_sym { return nx_result_err(NX_ERR_TAG_MISMATCH) }
142 if eq_lit.atom.n_args != 2 { return nx_result_err(NX_ERR_TAG_MISMATCH) }
143
144 let s: *Term = nx_term_arg(eq_lit.atom, 0)
145 let t: *Term = nx_term_arg(eq_lit.atom, 1)
146
147 let target_lit: *Literal = nx_clause_lit_at(target_clause, target_idx)
148
149 // Try paramodulating s -> t into the target atom. If that fails,
150 // try the symmetric direction (t -> s) since equality is symmetric
151 // and the literal as written may be either way around.
152 let subst: *Subst = nx_subst_new()
153 let new_atom_p: **Term = (sys_mmap(8)) as **Term
154 var ok: nx_int = nx_paramod_walk(s, t, target_lit.atom, subst, new_atom_p)
155 if ok == 0 {
156 // Fresh subst for the symmetric attempt -- previous one may have
157 // partial bindings from a failed root unify.
158 let subst2: *Subst = nx_subst_new()
159 ok = nx_paramod_walk(t, s, target_lit.atom, subst2, new_atom_p)
160 if ok == 0 { return nx_result_err(NX_ERR_NOT_FOUND) }
161 // Use subst2 going forward.
162 let new_target_atom: *Term = new_atom_p[0]
163 let new_target_lit: *Literal = nx_lit_make(target_lit.sign, new_target_atom)
164 let _r1: *NxResult = nx_clause_add(c_out, new_target_lit)
165 // Append remaining literals from C (eq_clause minus the equation).
166 var k: nx_int = 0
167 while k < eq_clause.n_lits {
168 if k != eq_idx {
169 let lk: *Literal = nx_clause_lit_at(eq_clause, k)
170 let lk_sub: *Literal = nx_lit_apply_subst(lk, subst2)
171 let _r2: *NxResult = nx_clause_add(c_out, lk_sub)
172 }
173 k = k + 1
174 }
175 // Append remaining literals from D (target minus the target lit).
176 k = 0
177 while k < target_clause.n_lits {
178 if k != target_idx {
179 let lk: *Literal = nx_clause_lit_at(target_clause, k)
180 let lk_sub: *Literal = nx_lit_apply_subst(lk, subst2)
181 let _r3: *NxResult = nx_clause_add(c_out, lk_sub)
182 }
183 k = k + 1
184 }
185 return nx_result_ok(c_out.n_lits)
186 }
187
188 // Forward direction succeeded.
189 let new_target_atom: *Term = new_atom_p[0]
190 let new_target_lit: *Literal = nx_lit_make(target_lit.sign, new_target_atom)
191 let _r4: *NxResult = nx_clause_add(c_out, new_target_lit)
192 var k: nx_int = 0
193 while k < eq_clause.n_lits {
194 if k != eq_idx {
195 let lk: *Literal = nx_clause_lit_at(eq_clause, k)
196 let lk_sub: *Literal = nx_lit_apply_subst(lk, subst)
197 let _r5: *NxResult = nx_clause_add(c_out, lk_sub)
198 }
199 k = k + 1
200 }
201 k = 0
202 while k < target_clause.n_lits {
203 if k != target_idx {
204 let lk: *Literal = nx_clause_lit_at(target_clause, k)
205 let lk_sub: *Literal = nx_lit_apply_subst(lk, subst)
206 let _r6: *NxResult = nx_clause_add(c_out, lk_sub)
207 }
208 k = k + 1
209 }
210 return nx_result_ok(c_out.n_lits)
211}