nx_avatar_solve_test.nx source
↩ module page · 82 lines · 2935 B
1// nx_avatar_solve_test.nx -- AVATAR composite smoke.
2// Loads a multi-component TPTP problem, splits, solves, verifies UNSAT.
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_disctree.nx"
15import "nx_paramodulation.nx"
16import "nx_saturation.nx"
17import "nx_pre_sat.nx"
18import "nx_sine.nx"
19import "nx_tptp_symtab.nx"
20import "nx_tptp_term.nx"
21import "nx_tptp_formula.nx"
22import "nx_tptp_load.nx"
23import "nx_clause_components.nx"
24import "nx_avatar_split.nx"
25import "nx_solve.nx"
26
27const SYM_EQ: nx_int = 50
28
29func main() -> nx_exit {
30 println("=== AVATAR composite solve smoke ===" as *u8)
31 var fails: nx_int = 0
32
33 // Load the multi-component test file.
34 let r_load: *NxResult = nx_tptp_load_cnf_file(
35 "/mnt/c/Users/elder/nishi-core/nxc2/tests/tptp/easy_007_avatar.p" as *u8, SYM_EQ)
36 if nx_result_is_err(r_load) == 1 {
37 println(" load FAIL" as *u8); return 1
38 }
39 let loaded: *TptpLoaded = nx_result_unwrap(r_load) as *TptpLoaded
40 print(" loaded: n_clauses=" as *u8); print_i64(loaded.n); println("" as *u8)
41
42 // Diagnostic: how many input clauses are splittable?
43 let n_splittable: nx_int = nx_avatar_count_splittable(loaded.clauses, loaded.n)
44 print(" splittable input clauses: " as *u8); print_i64(n_splittable); println("" as *u8)
45 if n_splittable < 1 {
46 println(" WARNING: no multi-component clauses -- AVATAR path won't engage" as *u8)
47 }
48
49 // Solve via the AVATAR composite.
50 let v_avatar: nx_int = nx_avatar_solve_simple(loaded.clauses, loaded.n, SYM_EQ, 200)
51 print(" AVATAR-solve verdict: " as *u8); print_i64(v_avatar); println("" as *u8)
52 if v_avatar == NX_SAT_VERDICT_UNSAT {
53 println(" AVATAR composite -> UNSAT PASS" as *u8)
54 } else {
55 println(" expected UNSAT FAIL" as *u8); fails = fails + 1
56 }
57
58 // Also verify the standard discount loop solves it (sanity check
59 // that the answer doesn't depend on AVATAR).
60 let s: *Saturation = nx_saturation_new(200)
61 var i: nx_int = 0
62 while i < loaded.n {
63 let c: *Clause = nx_tptp_loaded_at(loaded, i)
64 let _u: *NxResult = nx_sat_add_unproc(s, c)
65 i = i + 1
66 }
67 let v_std: nx_int = nx_sat_run_discount(s, SYM_EQ)
68 print(" standard discount verdict: " as *u8); print_i64(v_std); println("" as *u8)
69 if v_std == NX_SAT_VERDICT_UNSAT {
70 println(" standard discount -> UNSAT PASS (cross-check)" as *u8)
71 } else {
72 println(" standard discount mismatch FAIL" as *u8); fails = fails + 1
73 }
74
75 println("" as *u8)
76 if fails == 0 {
77 println("=== AVATAR composite + cross-check PASS ===" as *u8)
78 return 0
79 }
80 print("=== " as *u8); print_i64(fails); println(" failures ===" as *u8)
81 return 1
82}