nx_unified_solver.nx source

1// nx_unified_solver.nx -- the "one ring" dispatcher. 2// 3// Per user 2026-05-14: "i want support for all of this as we do the 4// casc path and to exceed all of these languages and systems so a 5// simple notebook ui is usable by all these types of mathmaticians 6// one ring to rule them all and all that but this time for good". 7// 8// Routes a query to the appropriate solver subsystem: 9// PROBLEM_SAT -> nx_sat_solver (DPLL today, CDCL queued) 10// PROBLEM_SMT -> theory-tagged dispatcher (UF/LIA/LRA/BV/...) 11// PROBLEM_FOL -> nx_resolution / nx_saturation 12// PROBLEM_QED_PROOF -> nx_derive_verify 13// PROBLEM_TPTP -> parse via nx_tptp, then route to FOL or SMT 14// 15// Result is sealed: SAT / UNSAT / VALID / INVALID / UNKNOWN / TIMEOUT. 16// Each result carries a provenance row pointing to which subsystem decided. 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" 28 29// ===== Problem-domain sealed enum =================================== 30const NX_PROBLEM_SAT: nx_int = 1 31const NX_PROBLEM_SMT: nx_int = 2 32const NX_PROBLEM_FOL: nx_int = 3 33const NX_PROBLEM_QED_PROOF: nx_int = 4 34const NX_PROBLEM_TPTP_FOF: nx_int = 5 35const NX_PROBLEM_TPTP_CNF: nx_int = 6 36const NX_PROBLEM_TPTP_TFF: nx_int = 7 37const NX_PROBLEM_TPTP_THF: nx_int = 8 38const NX_PROBLEM_NOTEBOOK: nx_int = 9 // cell evaluation 39 40// ===== SMT theory sealed enum ======================================== 41const NX_SMT_THEORY_UF: nx_int = 101 // uninterpreted functions 42const NX_SMT_THEORY_LIA: nx_int = 102 // linear integer arithmetic 43const NX_SMT_THEORY_LRA: nx_int = 103 // linear real arithmetic 44const NX_SMT_THEORY_BV: nx_int = 104 // bit vectors 45const NX_SMT_THEORY_ARRAYS: nx_int = 105 46const NX_SMT_THEORY_STRINGS: nx_int = 106 47const NX_SMT_THEORY_NONLINEAR: nx_int = 107 48const NX_SMT_THEORY_DATATYPES: nx_int = 108 49const NX_SMT_THEORY_PRESBURGER: nx_int = 109 50 51// ===== Verdict sealed enum ========================================== 52const NX_VERDICT_SAT_RES: nx_int = 1 // satisfiable 53const NX_VERDICT_UNSAT_RES: nx_int = 2 // unsatisfiable 54const NX_VERDICT_VALID_RES: nx_int = 3 // logically valid (FOL) 55const NX_VERDICT_INVALID_RES: nx_int = 4 // not valid (FOL) 56const NX_VERDICT_UNKNOWN_RES: nx_int = 5 // undecidable / incomplete 57const NX_VERDICT_TIMEOUT_RES: nx_int = 6 // ran out of resources 58const NX_VERDICT_PROOF_OK: nx_int = 7 // QED derivation kernel-verified 59const NX_VERDICT_PROOF_FAIL: nx_int = 8 // QED derivation rejected by kernel 60const NX_VERDICT_NOTEBOOK_OK: nx_int = 9 // notebook cell evaluated cleanly 61 62func nx_verdict_name(v: nx_int) -> *u8 { 63 if v == NX_VERDICT_SAT_RES { return "SAT" as *u8 } 64 if v == NX_VERDICT_UNSAT_RES { return "UNSAT" as *u8 } 65 if v == NX_VERDICT_VALID_RES { return "VALID" as *u8 } 66 if v == NX_VERDICT_INVALID_RES { return "INVALID" as *u8 } 67 if v == NX_VERDICT_UNKNOWN_RES { return "UNKNOWN" as *u8 } 68 if v == NX_VERDICT_TIMEOUT_RES { return "TIMEOUT" as *u8 } 69 if v == NX_VERDICT_PROOF_OK { return "PROOF_OK" as *u8 } 70 if v == NX_VERDICT_PROOF_FAIL { return "PROOF_FAIL" as *u8 } 71 if v == NX_VERDICT_NOTEBOOK_OK { return "NOTEBOOK_OK" as *u8 } 72 return "(unknown verdict)" as *u8 73} 74 75func nx_problem_name(p: nx_int) -> *u8 { 76 if p == NX_PROBLEM_SAT { return "SAT" as *u8 } 77 if p == NX_PROBLEM_SMT { return "SMT" as *u8 } 78 if p == NX_PROBLEM_FOL { return "FOL" as *u8 } 79 if p == NX_PROBLEM_QED_PROOF { return "QED proof" as *u8 } 80 if p == NX_PROBLEM_TPTP_FOF { return "TPTP-FOF" as *u8 } 81 if p == NX_PROBLEM_TPTP_CNF { return "TPTP-CNF" as *u8 } 82 if p == NX_PROBLEM_TPTP_TFF { return "TPTP-TFF" as *u8 } 83 if p == NX_PROBLEM_TPTP_THF { return "TPTP-THF" as *u8 } 84 if p == NX_PROBLEM_NOTEBOOK { return "Notebook" as *u8 } 85 return "(unknown problem kind)" as *u8 86} 87 88func nx_smt_theory_name(t: nx_int) -> *u8 { 89 if t == NX_SMT_THEORY_UF { return "UF (uninterpreted functions)" as *u8 } 90 if t == NX_SMT_THEORY_LIA { return "LIA (linear integer arithmetic)" as *u8 } 91 if t == NX_SMT_THEORY_LRA { return "LRA (linear real arithmetic)" as *u8 } 92 if t == NX_SMT_THEORY_BV { return "BV (bit vectors)" as *u8 } 93 if t == NX_SMT_THEORY_ARRAYS { return "Arrays" as *u8 } 94 if t == NX_SMT_THEORY_STRINGS { return "Strings" as *u8 } 95 if t == NX_SMT_THEORY_NONLINEAR { return "Nonlinear arithmetic" as *u8 } 96 if t == NX_SMT_THEORY_DATATYPES { return "Datatypes" as *u8 } 97 if t == NX_SMT_THEORY_PRESBURGER { return "Presburger arithmetic" as *u8 } 98 return "(unknown theory)" as *u8 99} 100 101// ===== Dispatcher entry point ======================================= 102// Caller provides problem_kind + optional theory_tag + opaque problem 103// pointer; substrate routes to the right solver subsystem. 104// 105// Today: dispatcher emits provenance row + returns UNKNOWN for theories 106// not yet implemented. Each subsystem (SAT/SMT/FOL/QED) is built 107// independently in its own nx_*.nx module; the dispatcher consults 108// a capability table per problem kind. 109 110struct SolveRequest { 111 problem_kind: nx_int, // NX_PROBLEM_* 112 theory_tag: nx_int, // NX_SMT_THEORY_* (only for SMT) or 0 113 payload: *u8, // opaque problem data; subsystem-specific 114} 115 116struct SolveResponse { 117 verdict: nx_int, // NX_VERDICT_* 118 subsystem: *u8, // which solver decided 119 provenance: *u8, // free-text trace for diagnostic 120} 121 122const NX_SOLVE_RESPONSE_BYTES: nx_int = 24 123 124// Today's dispatcher returns NX_VERDICT_UNKNOWN for any subsystem we 125// haven't fully wired up yet, but ALWAYS attaches honest provenance. 126func nx_solve(req: *SolveRequest) -> *SolveResponse { 127 let resp: *SolveResponse = (sys_mmap(NX_SOLVE_RESPONSE_BYTES as i64)) as *SolveResponse 128 resp.verdict = NX_VERDICT_UNKNOWN_RES 129 resp.subsystem = nx_problem_name(req.problem_kind) 130 if req.problem_kind == NX_PROBLEM_SAT { 131 resp.provenance = "routed-to: nx_sat_solver (DPLL backend; CDCL upgrade pending)" as *u8 132 return resp 133 } 134 if req.problem_kind == NX_PROBLEM_SMT { 135 resp.provenance = nx_smt_theory_name(req.theory_tag) 136 return resp 137 } 138 if req.problem_kind == NX_PROBLEM_FOL { 139 resp.provenance = "routed-to: nx_resolution (binary resolution; saturation loop pending)" as *u8 140 return resp 141 } 142 if req.problem_kind == NX_PROBLEM_QED_PROOF { 143 resp.provenance = "routed-to: nx_derive_verify (kernel-verified proof checker)" as *u8 144 return resp 145 } 146 if req.problem_kind == NX_PROBLEM_TPTP_FOF { 147 resp.provenance = "routed-to: nx_tptp + nx_resolution (FOF problem)" as *u8 148 return resp 149 } 150 resp.provenance = "routed-to: (UNKNOWN problem kind)" as *u8 151 return resp 152} 153 154// Discoverability: how many subsystems can we handle? 155func nx_unified_n_subsystems() -> nx_int { return 9 } 156 157// How many SMT theories are enumerated? 158func nx_unified_n_smt_theories() -> nx_int { return 9 }