nx_lpo.nx source
↩ module page · 163 lines · 6147 B
1// nx_lpo.nx -- Lexicographic Path Ordering (LPO).
2//
3// Per Vampire-displacement roadmap Phase 2. Sibling to KBO -- both
4// well-founded simplification orders on first-order terms. LPO is
5// purely structural: no symbol weights, just a total precedence on
6// symbols. Useful when KBO can't be admissibly weighted (e.g.
7// theories with many constants where all weights tied to w_0).
8//
9// Kamin-Levy 1980 standard formulation:
10//
11// s >_LPO t iff one of:
12// (LPO1) t is a proper subterm of s
13// (LPO2) s = f(s_1..s_n), t = g(t_1..t_m), f > g in precedence,
14// and s >_LPO t_j for every j in 1..m
15// (LPO3) s = f(s_1..s_n), t = f(t_1..t_n) (same head, same arity),
16// (s_1..s_n) >_LPO_lex (t_1..t_n) at the first differing
17// pair, and s >_LPO t_j for every j after that index
18//
19// Sealed verdict {GT, EQ, LT, INCOMP}.
20//
21// Reuses KboState's precedence + arity fields -- the precedence
22// concept is identical across KBO and LPO, so two stores would just
23// be redundant. weights field is ignored by LPO.
24
25// nx_safety_envelope:
26// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
27// sil_target: SIL1
28// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
29// verdict: NOT_YET_EVALUATED
30
31import "nx_syscalls.nx"
32import "nx_runtime.nx"
33import "nx_tier.nx"
34import "nx_result.nx"
35import "nx_unify.nx"
36import "nx_term_order.nx"
37
38const NX_LPO_GT: nx_int = 1
39const NX_LPO_EQ: nx_int = 2
40const NX_LPO_LT: nx_int = 3
41const NX_LPO_INCOMP: nx_int = 4
42
43// Returns 1 iff `inner` appears as a proper (strict) subterm of `outer`.
44// Structural equality at the root does NOT count -- "proper" excludes
45// outer == inner.
46func nx_lpo_is_proper_subterm(outer: *Term, inner: *Term) -> nx_int {
47 if outer.kind == NX_TERM_VAR { return 0 } // vars have no subterms
48 if outer.kind == NX_TERM_CONST { return 0 }
49 var i: nx_int = 0
50 while i < outer.n_args {
51 let child: *Term = nx_term_arg(outer, i)
52 if nx_term_eq(child, inner) == 1 { return 1 }
53 if nx_lpo_is_proper_subterm(child, inner) == 1 { return 1 }
54 i = i + 1
55 }
56 return 0
57}
58
59// Precedence comparison helper. Variables are not in the precedence
60// table; this helper assumes both inputs are non-variable. Returns
61// +1 if a > b, 0 if equal, -1 if a < b.
62func nx_lpo_prec_cmp(st: *KboState, a_sym: nx_int, b_sym: nx_int) -> nx_int {
63 let pa: nx_int = st.precedences[a_sym]
64 let pb: nx_int = st.precedences[b_sym]
65 if pa > pb { return 1 }
66 if pa < pb { return -1 }
67 return 0
68}
69
70// Forward decl: needed by the helper that checks "s > t_j for all j".
71func nx_lpo_compare(st: *KboState, s: *Term, t: *Term) -> nx_int {
72 // (case-EQ) structural equality
73 if nx_term_eq(s, t) == 1 { return NX_LPO_EQ }
74
75 // Variable handling. LPO is undefined as a strict order between
76 // a variable and a non-variable that doesn't contain it; the safe
77 // conservative answer is INCOMP. When the variable is contained
78 // in the non-variable side, the larger-side wins by the subterm
79 // property (LPO1 / its mirror).
80 if s.kind == NX_TERM_VAR {
81 if t.kind == NX_TERM_VAR { return NX_LPO_INCOMP }
82 // s is var, t is non-var. If s occurs in t, then t > s.
83 if nx_term_contains_var(t, s.sym) == 1 { return NX_LPO_LT }
84 return NX_LPO_INCOMP
85 }
86 if t.kind == NX_TERM_VAR {
87 // t is var, s is non-var. Mirror.
88 if nx_term_contains_var(s, t.sym) == 1 { return NX_LPO_GT }
89 return NX_LPO_INCOMP
90 }
91
92 // Both s and t are non-variable.
93
94 // (LPO1) t a proper subterm of s -> s > t
95 if nx_lpo_is_proper_subterm(s, t) == 1 { return NX_LPO_GT }
96 // mirror: s a proper subterm of t -> s < t
97 if nx_lpo_is_proper_subterm(t, s) == 1 { return NX_LPO_LT }
98
99 let pc: nx_int = nx_lpo_prec_cmp(st, s.sym, t.sym)
100
101 // (LPO2) f > g in precedence -> s > t iff s > t_j for all j
102 if pc > 0 {
103 var j: nx_int = 0
104 while j < t.n_args {
105 let sub: nx_int = nx_lpo_compare(st, s, nx_term_arg(t, j))
106 if sub != NX_LPO_GT { return NX_LPO_INCOMP }
107 j = j + 1
108 }
109 return NX_LPO_GT
110 }
111 // mirror: f < g in precedence
112 if pc < 0 {
113 var j2: nx_int = 0
114 while j2 < s.n_args {
115 let sub2: nx_int = nx_lpo_compare(st, t, nx_term_arg(s, j2))
116 if sub2 != NX_LPO_GT { return NX_LPO_INCOMP }
117 j2 = j2 + 1
118 }
119 return NX_LPO_LT
120 }
121
122 // (LPO3) heads equal -- need lex compare on args, plus the winning
123 // side must dominate the remaining args.
124 if s.n_args != t.n_args { return NX_LPO_INCOMP }
125 var i: nx_int = 0
126 while i < s.n_args {
127 let sub3: nx_int = nx_lpo_compare(st, nx_term_arg(s, i), nx_term_arg(t, i))
128 if sub3 == NX_LPO_GT {
129 // Remaining args: s must dominate every t_k for k > i.
130 var k: nx_int = i + 1
131 while k < t.n_args {
132 let extra: nx_int = nx_lpo_compare(st, s, nx_term_arg(t, k))
133 if extra != NX_LPO_GT { return NX_LPO_INCOMP }
134 k = k + 1
135 }
136 return NX_LPO_GT
137 }
138 if sub3 == NX_LPO_LT {
139 var k2: nx_int = i + 1
140 while k2 < s.n_args {
141 let extra2: nx_int = nx_lpo_compare(st, t, nx_term_arg(s, k2))
142 if extra2 != NX_LPO_GT { return NX_LPO_INCOMP }
143 k2 = k2 + 1
144 }
145 return NX_LPO_LT
146 }
147 if sub3 == NX_LPO_INCOMP { return NX_LPO_INCOMP }
148 // sub3 == EQ: continue to next arg
149 i = i + 1
150 }
151 // All argument pairs reported EQ but the up-front nx_term_eq said
152 // s != t. Defensive fallback (should be unreachable for well-formed
153 // input).
154 return NX_LPO_INCOMP
155}
156
157func nx_lpo_verdict_name(v: nx_int) -> *u8 {
158 if v == NX_LPO_GT { return "GT" as *u8 }
159 if v == NX_LPO_EQ { return "EQ" as *u8 }
160 if v == NX_LPO_LT { return "LT" as *u8 }
161 if v == NX_LPO_INCOMP { return "INCOMP" as *u8 }
162 return "?" as *u8
163}