nx_saturation_test.nx source
↩ module page · 83 lines · 3390 B
1// nx_saturation_test.nx -- saturation loop + factoring smoke.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_unify.nx"
8import "nx_resolution.nx"
9import "nx_saturation.nx"
10
11const SYM_P: nx_int = 200
12const SYM_A: nx_int = 100
13
14func main() -> nx_exit {
15 println("=== Saturation loop (given-clause) smoke ===" as *u8)
16
17 // Classic UNSAT: clauses { {p(a)}, {~p(a)} } -- empty clause derivable
18 let p_a_args: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
19 p_a_args.kind = NX_TERM_CONST; p_a_args.sym = SYM_A
20 p_a_args.n_args = 0; p_a_args.args = 0 as *Term
21 let atom_p_a: *Term = nx_term_app(SYM_P, 1, p_a_args)
22
23 let c1: *Clause = nx_clause_new()
24 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, atom_p_a))
25 let c2: *Clause = nx_clause_new()
26 let _r2: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_NEG, atom_p_a))
27
28 let s: *Saturation = nx_saturation_new(100)
29 let _u1: *NxResult = nx_sat_add_unproc(s, c1)
30 let _u2: *NxResult = nx_sat_add_unproc(s, c2)
31
32 let verdict: nx_int = nx_sat_run(s)
33 print(" {p(a)} + {~p(a)} -> verdict=" as *u8)
34 if verdict == NX_SAT_VERDICT_UNSAT { println("UNSAT (empty clause derived)" as *u8) }
35 if verdict == NX_SAT_VERDICT_UNKNOWN { println("UNKNOWN" as *u8) }
36 if verdict != NX_SAT_VERDICT_UNSAT { return 1 }
37
38 println("" as *u8)
39
40 // SAT-leaning case: {p(a)}, {q(a)} -- no contradiction; saturates without empty
41 let q_atom: *Term = nx_term_app(201, 1, p_a_args)
42 let c3: *Clause = nx_clause_new()
43 let _r3: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, atom_p_a))
44 let c4: *Clause = nx_clause_new()
45 let _r4: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS, q_atom))
46
47 let s2: *Saturation = nx_saturation_new(50)
48 let _u3: *NxResult = nx_sat_add_unproc(s2, c3)
49 let _u4: *NxResult = nx_sat_add_unproc(s2, c4)
50
51 let verdict2: nx_int = nx_sat_run(s2)
52 print(" {p(a)} + {q(a)} -> verdict=" as *u8)
53 if verdict2 == NX_SAT_VERDICT_UNSAT { println("UNSAT" as *u8); return 10 }
54 if verdict2 == NX_SAT_VERDICT_UNKNOWN { println("UNKNOWN (no contradiction; consistent with SAT)" as *u8) }
55
56 println("" as *u8)
57
58 // Factoring test: {p(x), p(a)} with sigma {x -> a} -> {p(a)}
59 let p_x_args: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
60 p_x_args.kind = NX_TERM_VAR; p_x_args.sym = 1
61 p_x_args.n_args = 0; p_x_args.args = 0 as *Term
62 let atom_p_x: *Term = nx_term_app(SYM_P, 1, p_x_args)
63
64 let c_fac_in: *Clause = nx_clause_new()
65 let _f1: *NxResult = nx_clause_add(c_fac_in, nx_lit_make(NX_LIT_POS, atom_p_x))
66 let _f2: *NxResult = nx_clause_add(c_fac_in, nx_lit_make(NX_LIT_POS, atom_p_a))
67
68 let c_fac_out: *Clause = nx_clause_new()
69 let r_fac: *NxResult = nx_factor(c_fac_in, 0, 1, c_fac_out)
70 if nx_result_is_err(r_fac) == 1 {
71 print("FAIL factor expected OK got " as *u8)
72 print(nx_err_name(nx_result_err_code(r_fac))); println("" as *u8)
73 return 20
74 }
75 print(" factor {p(x), p(a)} -> n_lits=" as *u8); print_i64(c_fac_out.n_lits); println("" as *u8)
76 if c_fac_out.n_lits != 1 { return 21 }
77 let lit_fac: *Literal = nx_clause_lit_at(c_fac_out, 0)
78 if lit_fac.atom.sym != SYM_P { return 22 }
79
80 println("" as *u8)
81 println("=== Saturation + factoring smoke PASS ===" as *u8)
82 return 0
83}