nx_demodulation.nx source
↩ module page · 130 lines · 5402 B
1// nx_demodulation.nx -- term rewriting via oriented equations.
2//
3// Per Vampire-displacement roadmap Phase 1 step 3.
4//
5// An oriented equation l = r (with l >_KBO r) is a rewrite rule.
6// Demodulation rewrites every subterm of a target that matches l
7// to the corresponding instance of r, normalizing terms before they
8// re-enter the saturation loop. Together with subsumption, this is
9// the second-largest pruner in Vampire-class provers.
10//
11// Match direction: l is the pattern, target subterm is the term.
12// We walk the target outermost-first; on any successful match we
13// substitute and recurse into the result. Single-pass per call --
14// callers run it to a fixpoint when full normal form is required.
15//
16// Bits-up nx_int. Result-typed for orientation.
17
18// nx_safety_envelope:
19// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
20// sil_target: SIL1
21// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
22// verdict: NOT_YET_EVALUATED
23
24import "nx_syscalls.nx"
25import "nx_runtime.nx"
26import "nx_tier.nx"
27import "nx_result.nx"
28import "nx_unify.nx"
29import "nx_resolution.nx"
30import "nx_term_order.nx"
31
32// ===== Oriented equation ============================================
33struct Equation {
34 lhs: *Term, // strictly KBO-greater (the rewrite-from side)
35 rhs: *Term, // strictly KBO-smaller (the rewrite-to side)
36}
37
38const NX_EQUATION_BYTES: nx_int = 16
39
40func nx_eqn_make(lhs: *Term, rhs: *Term) -> *Equation {
41 let e: *Equation = (sys_mmap(NX_EQUATION_BYTES as i64)) as *Equation
42 e.lhs = lhs
43 e.rhs = rhs
44 return e
45}
46
47// Orient an unoriented equation pair using KBO. Returns the oriented
48// Equation wrapped in a Result; if KBO can't compare the sides
49// (NX_KBO_EQ or NX_KBO_INCOMP), returns NX_ERR_INVALID_STATE because
50// the equation cannot be safely used as a rewrite rule.
51func nx_eqn_orient(st: *KboState, lhs: *Term, rhs: *Term,
52 max_var_id: nx_int) -> *NxResult {
53 let cmp: nx_int = nx_kbo_compare(st, lhs, rhs, max_var_id)
54 if cmp == NX_KBO_GT { return nx_result_ok((nx_eqn_make(lhs, rhs)) as nx_int) }
55 if cmp == NX_KBO_LT { return nx_result_ok((nx_eqn_make(rhs, lhs)) as nx_int) }
56 return nx_result_err(NX_ERR_INVALID_STATE)
57}
58
59// ===== Subterm demodulation =========================================
60// Rewrite every outermost subterm of t that matches eqn.lhs to the
61// corresponding instance of eqn.rhs. Returns the rewritten term.
62// Pointer-identical to t when no rewrite happened (small optimization
63// callers use to detect "nothing changed").
64func nx_demodulate_term(eqn: *Equation, t: *Term) -> *Term {
65 // Try a root match first (outermost-first strategy).
66 let s: *Subst = nx_subst_new()
67 let r: *NxResult = nx_match(eqn.lhs, t, s)
68 if nx_result_is_err(r) == 0 {
69 // Match succeeded -- rewrite to rhs[sigma]. Recurse to keep
70 // rewriting (in case the rhs itself contains a redex).
71 let rewritten: *Term = nx_subst_apply(eqn.rhs, s)
72 return nx_demodulate_term(eqn, rewritten)
73 }
74 // No root match -- try each child.
75 if t.kind != NX_TERM_APP { return t }
76 if t.n_args == 0 { return t }
77
78 let new_args: *Term = (sys_mmap((t.n_args * NX_TERM_BYTES) as i64)) as *Term
79 var any_changed: nx_int = 0
80 var i: nx_int = 0
81 while i < t.n_args {
82 let child: *Term = nx_term_arg(t, i)
83 let new_child: *Term = nx_demodulate_term(eqn, child)
84 let dest: *Term = ((new_args as nx_int) + (i * NX_TERM_BYTES)) as *Term
85 dest.kind = new_child.kind
86 dest.sym = new_child.sym
87 dest.n_args = new_child.n_args
88 dest.args = new_child.args
89 if (new_child as nx_int) != (child as nx_int) { any_changed = 1 }
90 i = i + 1
91 }
92 if any_changed == 1 { return nx_term_app(t.sym, t.n_args, new_args) }
93 return t
94}
95
96// ===== Clause-level demodulation ====================================
97// Rewrite every literal's atom in clause c using eqn; emit results
98// into c_out (caller-allocated). Returns the number of literals that
99// were actually changed.
100func nx_demodulate_clause(eqn: *Equation, c: *Clause, c_out: *Clause) -> nx_int {
101 var n_changed: nx_int = 0
102 var i: nx_int = 0
103 while i < c.n_lits {
104 let l: *Literal = nx_clause_lit_at(c, i)
105 let new_atom: *Term = nx_demodulate_term(eqn, l.atom)
106 let new_lit: *Literal = nx_lit_make(l.sign, new_atom)
107 let _r: *NxResult = nx_clause_add(c_out, new_lit)
108 if (new_atom as nx_int) != (l.atom as nx_int) { n_changed = n_changed + 1 }
109 i = i + 1
110 }
111 return n_changed
112}
113
114// ===== Fixpoint demodulation ========================================
115// Rewrite term t to KBO-normal form by applying eqn repeatedly until
116// no further rewrite is possible. Bounded by max_steps to guard
117// against pathological non-terminating cases (a well-oriented eqn
118// with KBO-decreasing rhs guarantees termination, but defensive cap
119// stays cheap and bounds qemu test runtime).
120func nx_demodulate_fixpoint(eqn: *Equation, t: *Term, max_steps: nx_int) -> *Term {
121 var current: *Term = t
122 var step: nx_int = 0
123 while step < max_steps {
124 let next: *Term = nx_demodulate_term(eqn, current)
125 if (next as nx_int) == (current as nx_int) { return current }
126 current = next
127 step = step + 1
128 }
129 return current
130}