nx_solve_test.nx source
↩ module page · 57 lines · 2349 B
1// nx_solve_test.nx -- composite CASC solver smoke.
2// Runs all 6 TPTP-Easy files through the one-call entry point and
3// confirms each gets the expected verdict.
4
5import "nx_syscalls.nx"
6import "nx_runtime.nx"
7import "nx_tier.nx"
8import "nx_result.nx"
9import "nx_unify.nx"
10import "nx_resolution.nx"
11import "nx_subsumption.nx"
12import "nx_tautology.nx"
13import "nx_disctree.nx"
14import "nx_paramodulation.nx"
15import "nx_saturation.nx"
16import "nx_pre_sat.nx"
17import "nx_sine.nx"
18import "nx_tptp_symtab.nx"
19import "nx_tptp_term.nx"
20import "nx_tptp_formula.nx"
21import "nx_tptp_load.nx"
22import "nx_solve.nx"
23
24const SYM_EQ: nx_int = 50
25
26func solve_one(path: *u8, expected: nx_int) -> nx_int {
27 let opts: *SolveOpts = nx_solve_opts_default()
28 let r: *NxResult = nx_solve_tptp_file(path, SYM_EQ, opts)
29 if nx_result_is_err(r) == 1 {
30 print(" " as *u8); print(path); print(" -> load/parse ERR code=" as *u8); print_i64(nx_result_err_code(r)); println(" FAIL" as *u8)
31 return 1
32 }
33 let v: nx_int = nx_result_unwrap(r)
34 print(" " as *u8); print(path); print(" -> verdict=" as *u8); print_i64(v); print(" expected=" as *u8); print_i64(expected); println("" as *u8)
35 if v == expected { return 0 }
36 println(" verdict mismatch FAIL" as *u8)
37 return 1
38}
39
40func main() -> nx_exit {
41 println("=== Composite CASC solver smoke ===" as *u8)
42 var fails: nx_int = 0
43 fails = fails + solve_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_001.p" as *u8, NX_SAT_VERDICT_UNSAT)
44 fails = fails + solve_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_002.p" as *u8, NX_SAT_VERDICT_UNSAT)
45 fails = fails + solve_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_003.p" as *u8, NX_SAT_VERDICT_UNSAT)
46 fails = fails + solve_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_004.p" as *u8, NX_SAT_VERDICT_UNSAT)
47 fails = fails + solve_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_005.p" as *u8, NX_SAT_VERDICT_UNSAT)
48 fails = fails + solve_one("/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_006.p" as *u8, NX_SAT_VERDICT_UNSAT)
49
50 println("" as *u8)
51 if fails == 0 {
52 println("=== ALL 6 files solved via composite entry point PASS ===" as *u8)
53 return 0
54 }
55 print("=== " as *u8); print_i64(fails); println(" failed ===" as *u8)
56 return 1
57}