nx_unified_solver.nx
buildroot/runtime/nx_unified_solver.nx
about
nx_unified_solver.nx -- the "one ring" dispatcher.
Per user 2026-05-14: "i want support for all of this as we do the
casc path and to exceed all of these languages and systems so a
simple notebook ui is usable by all these types of mathmaticians
one ring to rule them all and all that but this time for good".
Routes a query to the appropriate solver subsystem:
PROBLEM_SAT -> nx_sat_solver (DPLL today, CDCL queued)
PROBLEM_SMT -> theory-tagged dispatcher (UF/LIA/LRA/BV/...)
PROBLEM_FOL -> nx_resolution / nx_saturation
PROBLEM_QED_PROOF -> nx_derive_verify
PROBLEM_TPTP -> parse via nx_tptp, then route to FOL or SMT
Result is sealed: SAT / UNSAT / VALID / INVALID / UNKNOWN / TIMEOUT.
Each result carries a provenance row pointing to which subsystem decided.
dependencies 4 imports · 1 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nx
imported by: nx_unified_solver_test.nx
structs
| 110 | struct SolveRequest |
| 116 | struct SolveResponse |
consts
| 30 | const NX_PROBLEM_SAT: nx_int = 1 |
| 31 | const NX_PROBLEM_SMT: nx_int = 2 |
| 32 | const NX_PROBLEM_FOL: nx_int = 3 |
| 33 | const NX_PROBLEM_QED_PROOF: nx_int = 4 |
| 34 | const NX_PROBLEM_TPTP_FOF: nx_int = 5 |
| 35 | const NX_PROBLEM_TPTP_CNF: nx_int = 6 |
| 36 | const NX_PROBLEM_TPTP_TFF: nx_int = 7 |
| 37 | const NX_PROBLEM_TPTP_THF: nx_int = 8 |
| 38 | const NX_PROBLEM_NOTEBOOK: nx_int = 9 // cell evaluation |
| 41 | const NX_SMT_THEORY_UF: nx_int = 101 // uninterpreted functions |
| 42 | const NX_SMT_THEORY_LIA: nx_int = 102 // linear integer arithmetic |
| 43 | const NX_SMT_THEORY_LRA: nx_int = 103 // linear real arithmetic |
| 44 | const NX_SMT_THEORY_BV: nx_int = 104 // bit vectors |
| 45 | const NX_SMT_THEORY_ARRAYS: nx_int = 105 |
| 46 | const NX_SMT_THEORY_STRINGS: nx_int = 106 |
| 47 | const NX_SMT_THEORY_NONLINEAR: nx_int = 107 |
| 48 | const NX_SMT_THEORY_DATATYPES: nx_int = 108 |
| 49 | const NX_SMT_THEORY_PRESBURGER: nx_int = 109 |
| 52 | const NX_VERDICT_SAT_RES: nx_int = 1 // satisfiable |
| 53 | const NX_VERDICT_UNSAT_RES: nx_int = 2 // unsatisfiable |
| 54 | const NX_VERDICT_VALID_RES: nx_int = 3 // logically valid (FOL) |
| 55 | const NX_VERDICT_INVALID_RES: nx_int = 4 // not valid (FOL) |
| 56 | const NX_VERDICT_UNKNOWN_RES: nx_int = 5 // undecidable / incomplete |
| 57 | const NX_VERDICT_TIMEOUT_RES: nx_int = 6 // ran out of resources |
| 58 | const NX_VERDICT_PROOF_OK: nx_int = 7 // QED derivation kernel-verified |
| 59 | const NX_VERDICT_PROOF_FAIL: nx_int = 8 // QED derivation rejected by kernel |
| 60 | const NX_VERDICT_NOTEBOOK_OK: nx_int = 9 // notebook cell evaluated cleanly |
| 122 | const NX_SOLVE_RESPONSE_BYTES: nx_int = 24 |
functions
| 62 | func nx_verdict_name(v: nx_int) -> *u8 |
| 75 | func nx_problem_name(p: nx_int) -> *u8 called by 1: nx_solve |
| 88 | func nx_smt_theory_name(t: nx_int) -> *u8 called by 1: nx_solve |
| 126 | func nx_solve(req: *SolveRequest) -> *SolveResponse |
| 155 | func nx_unified_n_subsystems() -> nx_int { return 9 } |
| 158 | func nx_unified_n_smt_theories() -> nx_int { return 9 } |