nx_solve.nx source
↩ module page · 147 lines · 6131 B
1// nx_solve.nx -- composite CASC solver entry point.
2//
3// One call that does the full pipeline:
4// 1. Load TPTP CNF file via native sys_read_file
5// 2. (optional) Pre-saturation simplify (drop tautologies + subsumed)
6// 3. (optional) Sine selection (drop irrelevant axioms)
7// 4. Discount-loop saturation with paramodulation + indexed
8// forward subsumption + backward simp
9// 5. Return verdict
10//
11// Used as the substrate's main entry point for CASC-style submissions:
12// caller passes a path and gets back "UNSAT" / "UNKNOWN" / file error.
13// All native NishiLang -- no shell wrapper, no Python.
14
15// nx_safety_envelope:
16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
17// sil_target: SIL1
18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
19// verdict: NOT_YET_EVALUATED
20
21import "nx_syscalls.nx"
22import "nx_runtime.nx"
23import "nx_tier.nx"
24import "nx_result.nx"
25import "nx_unify.nx"
26import "nx_resolution.nx"
27import "nx_subsumption.nx"
28import "nx_tautology.nx"
29import "nx_disctree.nx"
30import "nx_paramodulation.nx"
31import "nx_saturation.nx"
32import "nx_pre_sat.nx"
33import "nx_sine.nx"
34import "nx_tptp_symtab.nx"
35import "nx_tptp_term.nx"
36import "nx_tptp_formula.nx"
37import "nx_tptp_load.nx"
38import "nx_clause_components.nx"
39import "nx_avatar_split.nx"
40const NX_MAGIC_1024: i64 = 1024
41
42const NX_SOLVE_MAX_CLAUSES: nx_int = 256
43
44// Options struct. All defaults conservative -- caller turns features
45// on as desired.
46struct SolveOpts {
47 pre_sat_simp: nx_int, // 1 to enable nx_pre_sat_simplify
48 sine_select: nx_int, // 1 to enable nx_sine_select
49 sine_tolerance: nx_int, // Q10 tolerance for sine (NX_MAGIC_1024 = 1.0)
50 sine_conj_idx: nx_int, // index of the conjecture clause in the loaded set
51 budget: nx_int, // saturation step budget
52}
53const NX_SOLVE_OPTS_BYTES: nx_int = 40
54
55func nx_solve_opts_default() -> *SolveOpts {
56 let o: *SolveOpts = (sys_mmap(NX_SOLVE_OPTS_BYTES as i64)) as *SolveOpts
57 o.pre_sat_simp = 1
58 o.sine_select = 0 // off by default; needs conjecture to be useful
59 o.sine_tolerance = NX_MAGIC_1024 // 1.0
60 o.sine_conj_idx = 0 - 1 // unset
61 o.budget = 200
62 return o
63}
64
65// Solve. Returns Result<verdict_code, NX_ERR_*> where verdict_code is
66// one of NX_SAT_VERDICT_UNSAT / NX_SAT_VERDICT_UNKNOWN.
67func nx_solve_tptp_file(path: *u8, eq_sym: nx_int, opts: *SolveOpts) -> *NxResult {
68 let r_load: *NxResult = nx_tptp_load_cnf_file(path, eq_sym)
69 if nx_result_is_err(r_load) == 1 { return r_load }
70 let loaded: *TptpLoaded = nx_result_unwrap(r_load) as *TptpLoaded
71
72 // The "current" clause set; starts as loaded.clauses + loaded.n.
73 var working: *Clause = loaded.clauses
74 var n_working: nx_int = loaded.n
75
76 // Stage: pre-saturation simplification.
77 if opts.pre_sat_simp == 1 {
78 let preout: *Clause = (sys_mmap((NX_SOLVE_MAX_CLAUSES * NX_CLAUSE_BYTES) as i64)) as *Clause
79 // nx_pre_sat_simplify RETURNS the kept count -- there's no
80 // out_n parameter. Bug-fixed 2026-05-15: initial version
81 // read from a separate *n_pre[0] that stayed 0, dropping
82 // every clause before saturation.
83 let kept: nx_int = nx_pre_sat_simplify(working, n_working, eq_sym, preout)
84 working = preout
85 n_working = kept
86 }
87
88 // Stage: Sine selection.
89 if opts.sine_select == 1 {
90 if opts.sine_conj_idx >= 0 {
91 if opts.sine_conj_idx < n_working {
92 let conj: *Clause = ((working as nx_int) + (opts.sine_conj_idx * NX_CLAUSE_BYTES)) as *Clause
93 let sel: *nx_int = (sys_mmap((NX_SOLVE_MAX_CLAUSES * 8) as i64)) as *nx_int
94 let _n_sel: nx_int = nx_sine_select(working, n_working, conj, opts.sine_tolerance, sel)
95 // Rebuild working as the selected subset.
96 let sineout: *Clause = (sys_mmap((NX_SOLVE_MAX_CLAUSES * NX_CLAUSE_BYTES) as i64)) as *Clause
97 var n_sineout: nx_int = 0
98 var i: nx_int = 0
99 while i < n_working {
100 if sel[i] == 1 {
101 let src: *Clause = ((working as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
102 let dst: *Clause = ((sineout as nx_int) + (n_sineout * NX_CLAUSE_BYTES)) as *Clause
103 dst.n_lits = src.n_lits
104 dst.lits = src.lits
105 n_sineout = n_sineout + 1
106 }
107 i = i + 1
108 }
109 working = sineout
110 n_working = n_sineout
111 }
112 }
113 }
114
115 // Stage: saturate.
116 let s: *Saturation = nx_saturation_new(opts.budget)
117 var k: nx_int = 0
118 while k < n_working {
119 let c: *Clause = ((working as nx_int) + (k * NX_CLAUSE_BYTES)) as *Clause
120 let _u: *NxResult = nx_sat_add_unproc(s, c)
121 k = k + 1
122 }
123 let v: nx_int = nx_sat_run_discount(s, eq_sym)
124 return nx_result_ok(v)
125}
126
127// ===== AVATAR-style splitting wrapper =============================
128// Trivial AVATAR: split each multi-component clause into independent
129// sub-clauses BEFORE saturation. Sound (variable-disjoint
130// components have disjoint refutation worlds) and faster on
131// splittable problems. Full SAT-coordinated AVATAR is the next
132// integration step; this primitive ships the standalone benefit.
133func nx_avatar_solve_simple(input: *Clause, n_input: nx_int,
134 eq_sym: nx_int, budget: nx_int) -> nx_int {
135 let split_out: *Clause = (sys_mmap((NX_SOLVE_MAX_CLAUSES * NX_CLAUSE_BYTES) as i64)) as *Clause
136 let n_split: nx_int = nx_avatar_split_all(input, n_input, split_out, NX_SOLVE_MAX_CLAUSES)
137 if n_split < 0 { return NX_SAT_VERDICT_UNKNOWN }
138
139 let s: *Saturation = nx_saturation_new(budget)
140 var i: nx_int = 0
141 while i < n_split {
142 let c: *Clause = ((split_out as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
143 let _u: *NxResult = nx_sat_add_unproc(s, c)
144 i = i + 1
145 }
146 return nx_sat_run_discount(s, eq_sym)
147}