nx_unified_solver_test.nx source
↩ module page · 98 lines · 3985 B
1// nx_unified_solver_test.nx -- smoke for unified dispatcher + UF SMT.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_unified_solver.nx"
8import "nx_congruence_closure.nx"
9
10func main() -> nx_exit {
11 println("=== Unified solver dispatcher + UF congruence closure ===" as *u8)
12
13 // Dispatcher: route a SAT problem
14 let req_sat: *SolveRequest = (sys_mmap(24)) as *SolveRequest
15 req_sat.problem_kind = NX_PROBLEM_SAT
16 req_sat.theory_tag = 0
17 req_sat.payload = 0 as *u8
18 let resp_sat: *SolveResponse = nx_solve(req_sat)
19 print(" routed SAT -> " as *u8); print(resp_sat.subsystem)
20 print(" provenance: " as *u8); print(resp_sat.provenance); println("" as *u8)
21
22 // Dispatcher: SMT-LIA
23 let req_smt: *SolveRequest = (sys_mmap(24)) as *SolveRequest
24 req_smt.problem_kind = NX_PROBLEM_SMT
25 req_smt.theory_tag = NX_SMT_THEORY_LIA
26 req_smt.payload = 0 as *u8
27 let resp_smt: *SolveResponse = nx_solve(req_smt)
28 print(" routed SMT -> theory=" as *u8); print(resp_smt.provenance); println("" as *u8)
29
30 // Dispatcher: FOL
31 let req_fol: *SolveRequest = (sys_mmap(24)) as *SolveRequest
32 req_fol.problem_kind = NX_PROBLEM_FOL
33 req_fol.payload = 0 as *u8
34 let resp_fol: *SolveResponse = nx_solve(req_fol)
35 print(" routed FOL -> " as *u8); print(resp_fol.provenance); println("" as *u8)
36
37 // Dispatcher: QED proof
38 let req_qed: *SolveRequest = (sys_mmap(24)) as *SolveRequest
39 req_qed.problem_kind = NX_PROBLEM_QED_PROOF
40 req_qed.payload = 0 as *u8
41 let resp_qed: *SolveResponse = nx_solve(req_qed)
42 print(" routed QED -> " as *u8); print(resp_qed.provenance); println("" as *u8)
43
44 println("" as *u8)
45 println("=== UF congruence closure decision procedure ===" as *u8)
46
47 // Register terms a, b, c, f_a, f_b
48 let cc: *CongClosure = nx_cc_new()
49 let r_a: *NxResult = nx_cc_add_term(cc)
50 let r_b: *NxResult = nx_cc_add_term(cc)
51 let r_c: *NxResult = nx_cc_add_term(cc)
52 let r_fa: *NxResult = nx_cc_add_term(cc)
53 let r_fb: *NxResult = nx_cc_add_term(cc)
54 let a: nx_int = nx_result_unwrap(r_a)
55 let b: nx_int = nx_result_unwrap(r_b)
56 let c: nx_int = nx_result_unwrap(r_c)
57 let fa: nx_int = nx_result_unwrap(r_fa)
58 let fb: nx_int = nx_result_unwrap(r_fb)
59 print(" registered 5 atomic terms (a=0, b=1, c=2, f(a)=3, f(b)=4); n=" as *u8)
60 print_i64(nx_cc_n_terms(cc)); println("" as *u8)
61
62 // Initially: a and b are not equal
63 let r_eq0: *NxResult = nx_cc_equal(cc, a, b)
64 if nx_result_unwrap(r_eq0) == 1 { return 1 }
65 println(" initial: a = b ? NO (different classes)" as *u8)
66
67 // Assert a = b
68 let _u1: *NxResult = nx_cc_union(cc, a, b)
69 let r_eq1: *NxResult = nx_cc_equal(cc, a, b)
70 if nx_result_unwrap(r_eq1) != 1 { return 2 }
71 println(" after a=b: a = b ? YES (merged)" as *u8)
72
73 // Congruence: a = b implies f(a) = f(b). Initially f(a) != f(b).
74 let r_eq2: *NxResult = nx_cc_equal(cc, fa, fb)
75 if nx_result_unwrap(r_eq2) == 1 { return 3 }
76 println(" before congruence: f(a) = f(b) ? NO" as *u8)
77
78 // Propagate congruence: since a = b, merge f(a) and f(b)
79 let _r_cg: *NxResult = nx_cc_propagate_congruence(cc, fa, a, fb, b)
80 let r_eq3: *NxResult = nx_cc_equal(cc, fa, fb)
81 if nx_result_unwrap(r_eq3) != 1 { return 4 }
82 println(" after propagation: f(a) = f(b) ? YES (congruence)" as *u8)
83
84 // c is still in its own class
85 let r_eq4: *NxResult = nx_cc_equal(cc, a, c)
86 if nx_result_unwrap(r_eq4) == 1 { return 5 }
87 println(" unrelated: a = c ? NO (c is in its own class)" as *u8)
88
89 // Out-of-range
90 let r_oor: *NxResult = nx_cc_equal(cc, 99, 100)
91 if nx_result_is_err(r_oor) != 1 { return 6 }
92 if nx_result_err_code(r_oor) != NX_ERR_OUT_OF_RANGE { return 7 }
93 println(" oor query (99, 100): ERR=OUT_OF_RANGE" as *u8)
94
95 println("" as *u8)
96 println("=== ALL unified + UF tests PASS ===" as *u8)
97 return 0
98}