nx_solve.nx
buildroot/runtime/nx_solve.nx
about
nx_solve.nx -- composite CASC solver entry point.
One call that does the full pipeline:
1. Load TPTP CNF file via native sys_read_file
2. (optional) Pre-saturation simplify (drop tautologies + subsumed)
3. (optional) Sine selection (drop irrelevant axioms)
4. Discount-loop saturation with paramodulation + indexed
forward subsumption + backward simp
5. Return verdict
Used as the substrate's main entry point for CASC-style submissions:
caller passes a path and gets back "UNSAT" / "UNKNOWN" / file error.
All native NishiLang -- no shell wrapper, no Python.
dependencies 19 imports · 2 importers
diagram shows first 10 each side; +9 more imports, +0 more importers in the complete lists below.
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nxnx_resolution.nxnx_subsumption.nxnx_tautology.nxnx_disctree.nxnx_paramodulation.nxnx_saturation.nxnx_pre_sat.nxnx_sine.nxnx_tptp_symtab.nxnx_tptp_term.nxnx_tptp_formula.nxnx_tptp_load.nxnx_clause_components.nxnx_avatar_split.nx
imported by: nx_avatar_solve_test.nxnx_solve_test.nx
structs
| 46 | struct SolveOpts |
consts
| 40 | const NX_MAGIC_1024: i64 = 1024 |
| 42 | const NX_SOLVE_MAX_CLAUSES: nx_int = 256 |
| 53 | const NX_SOLVE_OPTS_BYTES: nx_int = 40 |
functions
| 55 | func nx_solve_opts_default() -> *SolveOpts |
| 67 | func nx_solve_tptp_file(path: *u8, eq_sym: nx_int, opts: *SolveOpts) -> *NxResult called by 1: solve_one calls 10: nx_tptp_load_cnf_filenx_result_is_errnx_result_unwrapsys_mmapnx_pre_sat_simplifynx_sine_select+4 |
| 133 | func nx_avatar_solve_simple(input: *Clause, n_input: nx_int, called by 1: main calls 5: sys_mmapnx_avatar_split_allnx_saturation_newnx_sat_add_unprocnx_sat_run_discount |