nx_tptp_write_test.nx source
↩ module page · 87 lines · 3382 B
1// nx_tptp_write_test.nx -- write a clause set to disk, read it back,
2// verify the round-trip preserves the clause count + verdict.
3
4import "nx_syscalls.nx"
5import "nx_runtime.nx"
6import "nx_tier.nx"
7import "nx_str.nx"
8import "nx_result.nx"
9import "nx_file_result.nx"
10import "nx_unify.nx"
11import "nx_resolution.nx"
12import "nx_subsumption.nx"
13import "nx_tautology.nx"
14import "nx_saturation.nx"
15import "nx_tptp_symtab.nx"
16import "nx_tptp_term.nx"
17import "nx_tptp_formula.nx"
18import "nx_tptp_load.nx"
19import "nx_tptp_emit.nx"
20import "nx_disctree.nx"
21
22const SYM_EQ: nx_int = 50
23
24func main() -> nx_exit {
25 println("=== TPTP file-write + round-trip smoke ===" as *u8)
26 var fails: nx_int = 0
27
28 // Load easy_001.p (the trivial UNSAT) -- 2 clauses.
29 let r_in: *NxResult = nx_tptp_load_cnf_file(
30 "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_001.p" as *u8, SYM_EQ)
31 if nx_result_is_err(r_in) == 1 {
32 println(" load failed FAIL" as *u8); return 1
33 }
34 let loaded_in: *TptpLoaded = nx_result_unwrap(r_in) as *TptpLoaded
35 print(" loaded in: n_clauses=" as *u8); print_i64(loaded_in.n); println("" as *u8)
36
37 // Write to /tmp/nxc2_easy_001_roundtrip.p
38 let outpath: *u8 = "/tmp/nxc2_easy_001_roundtrip.p" as *u8
39 let r_w: *NxResult = nx_tptp_write_cnf_file(outpath, loaded_in.clauses,
40 loaded_in.n, loaded_in.symtab, SYM_EQ)
41 if nx_result_is_err(r_w) == 1 {
42 print(" write failed err_code=" as *u8); print_i64(nx_result_err_code(r_w)); println("" as *u8)
43 fails = fails + 1
44 } else {
45 let bytes_written: nx_int = nx_result_unwrap(r_w)
46 print(" wrote " as *u8); print_i64(bytes_written); print(" bytes to " as *u8); println(outpath)
47
48 // Read back.
49 let r_back: *NxResult = nx_tptp_load_cnf_file(outpath, SYM_EQ)
50 if nx_result_is_err(r_back) == 1 {
51 print(" re-load failed err_code=" as *u8); print_i64(nx_result_err_code(r_back)); println("" as *u8)
52 fails = fails + 1
53 } else {
54 let loaded_back: *TptpLoaded = nx_result_unwrap(r_back) as *TptpLoaded
55 print(" loaded back: n_clauses=" as *u8); print_i64(loaded_back.n); println("" as *u8)
56
57 if loaded_back.n != loaded_in.n {
58 println(" clause count mismatch FAIL" as *u8)
59 fails = fails + 1
60 } else {
61 // Run discount loop on the round-tripped clauses; expect UNSAT.
62 let s: *Saturation = nx_saturation_new(50)
63 var i: nx_int = 0
64 while i < loaded_back.n {
65 let c: *Clause = nx_tptp_loaded_at(loaded_back, i)
66 let _u: *NxResult = nx_sat_add_unproc(s, c)
67 i = i + 1
68 }
69 let v: nx_int = nx_sat_run_discount(s, SYM_EQ)
70 if v == NX_SAT_VERDICT_UNSAT {
71 println(" round-tripped clauses solve UNSAT PASS" as *u8)
72 } else {
73 print(" unexpected verdict=" as *u8); print_i64(v); println(" FAIL" as *u8)
74 fails = fails + 1
75 }
76 }
77 }
78 }
79
80 println("" as *u8)
81 if fails == 0 {
82 println("=== file-write round-trip PASS ===" as *u8)
83 return 0
84 }
85 print("=== " as *u8); print_i64(fails); println(" failures ===" as *u8)
86 return 1
87}