nx_tptp_load_test.nx source
↩ module page · 73 lines · 2895 B
1// nx_tptp_load_test.nx -- end-to-end smoke: load real TPTP files
2// from disk and prove UNSAT via the discount-loop saturation.
3//
4// All native NishiLang. No shell preprocessing. No Python.
5
6import "nx_syscalls.nx"
7import "nx_runtime.nx"
8import "nx_tier.nx"
9import "nx_str.nx"
10import "nx_result.nx"
11import "nx_file_result.nx"
12import "nx_unify.nx"
13import "nx_resolution.nx"
14import "nx_subsumption.nx"
15import "nx_tautology.nx"
16import "nx_saturation.nx"
17import "nx_tptp_symtab.nx"
18import "nx_tptp_term.nx"
19import "nx_tptp_formula.nx"
20import "nx_tptp_load.nx"
21
22const SYM_EQ: nx_int = 50
23
24func run_one(path: *u8, expected_verdict: nx_int) -> nx_int {
25 print("---- " as *u8); print(path); println(" ----" as *u8)
26
27 let r: *NxResult = nx_tptp_load_cnf_file(path, SYM_EQ)
28 if nx_result_is_err(r) == 1 {
29 print(" load FAIL err_code=" as *u8); print_i64(nx_result_err_code(r)); println("" as *u8)
30 return 1
31 }
32 let loaded: *TptpLoaded = nx_result_unwrap(r) as *TptpLoaded
33 print(" loaded n_clauses=" as *u8); print_i64(loaded.n); println("" as *u8)
34
35 let s: *Saturation = nx_saturation_new(200)
36 var i: nx_int = 0
37 while i < loaded.n {
38 let c: *Clause = nx_tptp_loaded_at(loaded, i)
39 let _r: *NxResult = nx_sat_add_unproc(s, c)
40 i = i + 1
41 }
42
43 let v: nx_int = nx_sat_run_discount(s, SYM_EQ)
44 print(" verdict=" as *u8); print_i64(v); print(" (expected " as *u8); print_i64(expected_verdict); println(")" as *u8)
45 if v == expected_verdict {
46 println(" PASS" as *u8)
47 return 0
48 }
49 println(" FAIL" as *u8)
50 return 1
51}
52
53func main() -> nx_exit {
54 println("=== TPTP CNF file loader + discount-loop end-to-end smoke ===" as *u8)
55 var fails: nx_int = 0
56 fails = fails + run_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_001.p" as *u8, NX_SAT_VERDICT_UNSAT)
57 fails = fails + run_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_002.p" as *u8, NX_SAT_VERDICT_UNSAT)
58 fails = fails + run_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_003.p" as *u8, NX_SAT_VERDICT_UNSAT)
59 fails = fails + run_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_004.p" as *u8, NX_SAT_VERDICT_UNSAT)
60 fails = fails + run_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_005.p" as *u8, NX_SAT_VERDICT_UNSAT)
61 // easy_006.p needs paramodulation to close the equational chain
62 // {a=b}, {b=c} |- a=c. Now that nx_sat_run_discount fires
63 // paramodulation alongside resolution, this should solve.
64 fails = fails + run_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_006.p" as *u8, NX_SAT_VERDICT_UNSAT)
65
66 println("" as *u8)
67 if fails == 0 {
68 println("=== ALL 6 TPTP-Easy files matched expected verdict PASS ===" as *u8)
69 return 0
70 }
71 print("=== " as *u8); print_i64(fails); println(" file(s) failed ===" as *u8)
72 return 1
73}