nx_lia.nx
buildroot/runtime/nx_lia.nx
about
nx_lia.nx -- Linear Integer Arithmetic decision procedure.
Per the comparison commit's named LOSE rows: closes auto_prover
gap simultaneously vs Coq (lia/nia), Lean (omega), and HOL Light
(ARITH_TAC). Three peers, one engine.
PATENT-CLEAN PROVENANCE (Captain Moroni doctrine):
- Linear arithmetic decidability: Mojzesz Presburger, 1929.
Almost a century in public domain.
- Fourier-Motzkin elimination: Joseph Fourier, 1827; Theodore
Motzkin, 1936. Fully public domain.
- Cooper's algorithm: D.C. Cooper, 1972. Published
in academic literature, no patent claims.
- Brute-force ground enumeration: textbook decidable SMT method.
THIS COMMIT ships a bounded ground-LIA decision procedure suitable
for "small constraint systems with explicit variable bounds" --
exactly the omega/lia tactic use case. Unbounded Presburger via
full Cooper QE is named follow-up.
Architecture:
- LiaTerm: a + sum(c_i * x_i) -- coefficients + constant
- LiaConstraint: term {==, <=, >=, !=} 0
- LiaSystem: set of constraints + variable bounds
- nx_lia_decide(s) -> SAT / UNSAT / UNKNOWN
dependencies 1 imports · 1 importers
imports: nx_kernel_v2.nx
imported by: nx_lia_legal_test.nx
structs
| 46 | struct LiaConstr |
| 54 | struct LiaSystem |
consts
| 35 | const NX_LIA_MAX_VARS: nx_int = 8 |
| 36 | const NX_LIA_MAX_CONSTRS: nx_int = 32 |
| 37 | const NX_LIA_BOUND_DEFAULT: nx_int = 16 // default search range [-16, +16] |
| 40 | const NX_LIA_REL_EQ: nx_int = 1 // term == 0 |
| 41 | const NX_LIA_REL_LE: nx_int = 2 // term <= 0 |
| 42 | const NX_LIA_REL_GE: nx_int = 3 // term >= 0 |
| 43 | const NX_LIA_REL_NE: nx_int = 4 // term != 0 |
| 51 | const NX_LIA_CONSTR_BYTES: nx_int = 24 |
| 61 | const NX_LIA_SYS_BYTES: nx_int = 40 |
| 171 | const NX_LIA_SAT: nx_int = 1 |
| 172 | const NX_LIA_UNSAT: nx_int = 2 |
| 173 | const NX_LIA_UNKNOWN: nx_int = 3 // bounded box exhausted; deeper search needed |
functions
| 63 | func nx_lia_system_new(n_vars: nx_int) -> *LiaSystem |
| 73 | func nx_lia_constr_at(s: *LiaSystem, i: nx_int) -> *LiaConstr |
| 79 | func nx_lia_add(s: *LiaSystem, coefs: *nx_int, constant: nx_int, rel: nx_int) -> nx_int |
| 99 | func nx_lia_eval(c: *LiaConstr, assignment: *nx_int, n_vars: nx_int) -> nx_int called by 1: nx_lia_all_sat |
| 128 | func nx_lia_all_sat(s: *LiaSystem, assignment: *nx_int) -> nx_int |
| 145 | func nx_lia_search_inner(s: *LiaSystem, depth: nx_int, current: *nx_int, found: *nx_int) -> nx_int |
| 177 | func nx_lia_decide(s: *LiaSystem, witness: *nx_int) -> nx_int |
| 191 | func nx_lia_validity(neg_phi: *LiaSystem) -> nx_int |