nx_lia.nx source
↩ module page · 196 lines · 7020 B
1// nx_lia.nx -- Linear Integer Arithmetic decision procedure.
2//
3// Per the comparison commit's named LOSE rows: closes auto_prover
4// gap simultaneously vs Coq (lia/nia), Lean (omega), and HOL Light
5// (ARITH_TAC). Three peers, one engine.
6//
7// PATENT-CLEAN PROVENANCE (Captain Moroni doctrine):
8// - Linear arithmetic decidability: Mojzesz Presburger, 1929.
9// Almost a century in public domain.
10// - Fourier-Motzkin elimination: Joseph Fourier, 1827; Theodore
11// Motzkin, 1936. Fully public domain.
12// - Cooper's algorithm: D.C. Cooper, 1972. Published
13// in academic literature, no patent claims.
14// - Brute-force ground enumeration: textbook decidable SMT method.
15//
16// THIS COMMIT ships a bounded ground-LIA decision procedure suitable
17// for "small constraint systems with explicit variable bounds" --
18// exactly the omega/lia tactic use case. Unbounded Presburger via
19// full Cooper QE is named follow-up.
20//
21// Architecture:
22// - LiaTerm: a + sum(c_i * x_i) -- coefficients + constant
23// - LiaConstraint: term {==, <=, >=, !=} 0
24// - LiaSystem: set of constraints + variable bounds
25// - nx_lia_decide(s) -> SAT / UNSAT / UNKNOWN
26
27// nx_safety_envelope:
28// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
29// sil_target: SIL1
30// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
31// verdict: NOT_YET_EVALUATED
32
33import "nx_kernel_v2.nx"
34
35const NX_LIA_MAX_VARS: nx_int = 8
36const NX_LIA_MAX_CONSTRS: nx_int = 32
37const NX_LIA_BOUND_DEFAULT: nx_int = 16 // default search range [-16, +16]
38
39// Constraint relation
40const NX_LIA_REL_EQ: nx_int = 1 // term == 0
41const NX_LIA_REL_LE: nx_int = 2 // term <= 0
42const NX_LIA_REL_GE: nx_int = 3 // term >= 0
43const NX_LIA_REL_NE: nx_int = 4 // term != 0
44
45// One linear constraint: sum(coefs[i] * x_i) + constant `rel` 0
46struct LiaConstr {
47 coefs: *nx_int, // length NX_LIA_MAX_VARS
48 constant: nx_int,
49 rel: nx_int,
50}
51const NX_LIA_CONSTR_BYTES: nx_int = 24
52
53// Constraint system + bounds
54struct LiaSystem {
55 constrs: *LiaConstr,
56 n_constrs: nx_int,
57 n_vars: nx_int,
58 lo: nx_int,
59 hi: nx_int,
60}
61const NX_LIA_SYS_BYTES: nx_int = 40
62
63func nx_lia_system_new(n_vars: nx_int) -> *LiaSystem {
64 let s: *LiaSystem = (sys_mmap(NX_LIA_SYS_BYTES as i64)) as *LiaSystem
65 s.constrs = (sys_mmap((NX_LIA_MAX_CONSTRS * NX_LIA_CONSTR_BYTES) as i64)) as *LiaConstr
66 s.n_constrs = 0
67 s.n_vars = n_vars
68 s.lo = -NX_LIA_BOUND_DEFAULT
69 s.hi = NX_LIA_BOUND_DEFAULT
70 return s
71}
72
73func nx_lia_constr_at(s: *LiaSystem, i: nx_int) -> *LiaConstr {
74 return ((s.constrs as nx_int) + (i * NX_LIA_CONSTR_BYTES)) as *LiaConstr
75}
76
77// Add a constraint. `coefs` is an array of length s.n_vars.
78// Returns the constraint index, or -1 if full.
79func nx_lia_add(s: *LiaSystem, coefs: *nx_int, constant: nx_int, rel: nx_int) -> nx_int {
80 if s.n_constrs >= NX_LIA_MAX_CONSTRS { return -1 }
81 let c: *LiaConstr = nx_lia_constr_at(s, s.n_constrs)
82 c.coefs = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
83 var i: nx_int = 0
84 while i < s.n_vars {
85 let src: *nx_int = ((coefs as nx_int) + (i * 8)) as *nx_int
86 let dst: *nx_int = ((c.coefs as nx_int) + (i * 8)) as *nx_int
87 dst[0] = src[0]
88 i = i + 1
89 }
90 c.constant = constant
91 c.rel = rel
92 let idx: nx_int = s.n_constrs
93 s.n_constrs = s.n_constrs + 1
94 return idx
95}
96
97// Evaluate one constraint at a given assignment vector.
98// Returns 1 if satisfied, 0 otherwise.
99func nx_lia_eval(c: *LiaConstr, assignment: *nx_int, n_vars: nx_int) -> nx_int {
100 var sum: nx_int = c.constant
101 var i: nx_int = 0
102 while i < n_vars {
103 let pc: *nx_int = ((c.coefs as nx_int) + (i * 8)) as *nx_int
104 let pa: *nx_int = ((assignment as nx_int) + (i * 8)) as *nx_int
105 sum = sum + pc[0] * pa[0]
106 i = i + 1
107 }
108 if c.rel == NX_LIA_REL_EQ {
109 if sum == 0 { return 1 }
110 return 0
111 }
112 if c.rel == NX_LIA_REL_LE {
113 if sum <= 0 { return 1 }
114 return 0
115 }
116 if c.rel == NX_LIA_REL_GE {
117 if sum >= 0 { return 1 }
118 return 0
119 }
120 if c.rel == NX_LIA_REL_NE {
121 if sum != 0 { return 1 }
122 return 0
123 }
124 return 0
125}
126
127// Check whether all constraints are satisfied at a given assignment.
128func nx_lia_all_sat(s: *LiaSystem, assignment: *nx_int) -> nx_int {
129 var i: nx_int = 0
130 while i < s.n_constrs {
131 let c: *LiaConstr = nx_lia_constr_at(s, i)
132 if nx_lia_eval(c, assignment, s.n_vars) == 0 { return 0 }
133 i = i + 1
134 }
135 return 1
136}
137
138// ===== Recursive enumeration over the bounded box ===================
139// Tries every integer assignment in [lo, hi]^n_vars. Returns a
140// satisfying assignment in *out_assignment, or null if none found.
141// Search complexity: O((hi-lo+1)^n_vars * n_constrs) -- exponential
142// in n_vars but exact. Fine for omega-tactic-class problems
143// (typically n_vars <= 4).
144
145func nx_lia_search_inner(s: *LiaSystem, depth: nx_int, current: *nx_int, found: *nx_int) -> nx_int {
146 if depth >= s.n_vars {
147 if nx_lia_all_sat(s, current) == 1 {
148 // Copy current into the found buffer.
149 var k: nx_int = 0
150 while k < s.n_vars {
151 let pc: *nx_int = ((current as nx_int) + (k * 8)) as *nx_int
152 let pf: *nx_int = ((found as nx_int) + (k * 8)) as *nx_int
153 pf[0] = pc[0]
154 k = k + 1
155 }
156 return 1
157 }
158 return 0
159 }
160 var v: nx_int = s.lo
161 while v <= s.hi {
162 let pc: *nx_int = ((current as nx_int) + (depth * 8)) as *nx_int
163 pc[0] = v
164 if nx_lia_search_inner(s, depth + 1, current, found) == 1 { return 1 }
165 v = v + 1
166 }
167 return 0
168}
169
170// Decision verdict
171const NX_LIA_SAT: nx_int = 1
172const NX_LIA_UNSAT: nx_int = 2
173const NX_LIA_UNKNOWN: nx_int = 3 // bounded box exhausted; deeper search needed
174
175// Top-level decide. Returns SAT/UNSAT/UNKNOWN + writes a witness
176// into *witness (only meaningful for SAT verdict).
177func nx_lia_decide(s: *LiaSystem, witness: *nx_int) -> nx_int {
178 if s.n_vars > NX_LIA_MAX_VARS { return NX_LIA_UNKNOWN }
179 let current: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
180 let r: nx_int = nx_lia_search_inner(s, 0, current, witness)
181 if r == 1 { return NX_LIA_SAT }
182 return NX_LIA_UNSAT
183}
184
185// Convenience: build a goal "phi is a tautology" by negating phi and
186// proving the negation UNSAT. Returns 1 if phi is valid (UNSAT
187// negation), 0 if phi has a counterexample (SAT negation).
188//
189// Caller passes the NEGATED system already built; this helper just
190// dispatches to nx_lia_decide and inverts the verdict.
191func nx_lia_validity(neg_phi: *LiaSystem) -> nx_int {
192 let witness: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
193 let v: nx_int = nx_lia_decide(neg_phi, witness)
194 if v == NX_LIA_UNSAT { return 1 }
195 return 0
196}