nx_discount_test.nx source
↩ module page · 116 lines · 5291 B
1// nx_discount_test.nx -- discount-loop saturation strategy smoke.
2//
3// Verifies: (a) discount loop derives the empty clause (UNSAT) on the
4// classic test, (b) discount prunes more clauses than Otter on the
5// same input, (c) tautological inputs are dropped.
6
7import "nx_syscalls.nx"
8import "nx_runtime.nx"
9import "nx_tier.nx"
10import "nx_result.nx"
11import "nx_unify.nx"
12import "nx_resolution.nx"
13import "nx_subsumption.nx"
14import "nx_tautology.nx"
15import "nx_saturation.nx"
16
17const SYM_A: nx_int = 100
18const SYM_P: nx_int = 200
19const SYM_Q: nx_int = 201
20const SYM_EQ: nx_int = 50
21
22func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
23 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
24 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
25 return nx_term_app(p_sym, 1, arg)
26}
27
28func main() -> nx_exit {
29 println("=== Discount-loop saturation smoke ===" as *u8)
30 var fails: nx_int = 0
31
32 // ---------- Test 1: discount derives UNSAT on {p(a), ~p(a)} ---
33 let c1a: *Clause = nx_clause_new()
34 let _r1a: *NxResult = nx_clause_add(c1a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
35 let c1b: *Clause = nx_clause_new()
36 let _r1b: *NxResult = nx_clause_add(c1b, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
37
38 let s1: *Saturation = nx_saturation_new(50)
39 let _u1a: *NxResult = nx_sat_add_unproc(s1, c1a)
40 let _u1b: *NxResult = nx_sat_add_unproc(s1, c1b)
41 let v1: nx_int = nx_sat_run_discount(s1, SYM_EQ)
42 print(" 1. discount {p(a), ~p(a)} -> verdict=" as *u8); print_i64(v1)
43 if v1 == NX_SAT_VERDICT_UNSAT { println(" UNSAT PASS" as *u8) }
44 else { println(" FAIL" as *u8); fails = fails + 1 }
45
46 // ---------- Test 2: discount drops a tautology before processing
47 // Inputs: {p(a)}, {q(a), ~q(a)} (tautology). Expect:
48 // - n_processed after run <= 1 (tautology never enters processed)
49 let c2a: *Clause = nx_clause_new()
50 let _r2a: *NxResult = nx_clause_add(c2a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
51 let c2b: *Clause = nx_clause_new()
52 let _r2b: *NxResult = nx_clause_add(c2b, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
53 let _r2c: *NxResult = nx_clause_add(c2b, nx_lit_make(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
54
55 let s2: *Saturation = nx_saturation_new(50)
56 let _u2a: *NxResult = nx_sat_add_unproc(s2, c2a)
57 let _u2b: *NxResult = nx_sat_add_unproc(s2, c2b)
58 let v2: nx_int = nx_sat_run_discount(s2, SYM_EQ)
59 print(" 2. discount {p(a), {q(a),~q(a)}} -> n_processed=" as *u8)
60 print_i64(s2.n_processed); print(" verdict=" as *u8); print_i64(v2); println("" as *u8)
61 if s2.n_processed <= 1 {
62 println(" tautology dropped before processed PASS" as *u8)
63 } else {
64 println(" tautology NOT dropped FAIL" as *u8); fails = fails + 1
65 }
66
67 // ---------- Test 3: discount drops a subsumed clause -----------
68 // Inputs: {p(a)}, {p(a), q(a)}. Second is subsumed by first.
69 // After processing first (goes to processed), second should be
70 // dropped on pick (proc_subsumes -> 1). Expect n_processed = 1.
71 let c3a: *Clause = nx_clause_new()
72 let _r3a: *NxResult = nx_clause_add(c3a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
73 let c3b: *Clause = nx_clause_new()
74 let _r3b: *NxResult = nx_clause_add(c3b, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
75 let _r3c: *NxResult = nx_clause_add(c3b, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
76
77 let s3: *Saturation = nx_saturation_new(50)
78 let _u3a: *NxResult = nx_sat_add_unproc(s3, c3a)
79 let _u3b: *NxResult = nx_sat_add_unproc(s3, c3b)
80 let v3: nx_int = nx_sat_run_discount(s3, SYM_EQ)
81 print(" 3. discount {p(a), {p(a),q(a)}} -> n_processed=" as *u8)
82 print_i64(s3.n_processed); print(" verdict=" as *u8); print_i64(v3); println("" as *u8)
83 if s3.n_processed == 1 {
84 println(" subsumed clause dropped PASS" as *u8)
85 } else {
86 println(" subsumed clause NOT dropped FAIL" as *u8); fails = fails + 1
87 }
88
89 // ---------- Test 4: side-by-side -- discount n_proc <= otter n_proc
90 // Inputs: {p(a)}, {p(a), q(a)} same as test 3.
91 let c4a: *Clause = nx_clause_new()
92 let _r4a: *NxResult = nx_clause_add(c4a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
93 let c4b: *Clause = nx_clause_new()
94 let _r4b: *NxResult = nx_clause_add(c4b, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
95 let _r4c: *NxResult = nx_clause_add(c4b, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
96
97 let s4: *Saturation = nx_saturation_new(50)
98 let _u4a: *NxResult = nx_sat_add_unproc(s4, c4a)
99 let _u4b: *NxResult = nx_sat_add_unproc(s4, c4b)
100 let _v4: nx_int = nx_sat_run(s4) // OTTER = no pruning
101 print(" 4. otter processes both -> n_processed=" as *u8)
102 print_i64(s4.n_processed); println("" as *u8)
103 if s4.n_processed >= s3.n_processed {
104 println(" discount <= otter on processed count PASS" as *u8)
105 } else {
106 println(" discount > otter -- regression FAIL" as *u8); fails = fails + 1
107 }
108
109 println("" as *u8)
110 if fails == 0 {
111 println("=== ALL 4 discount-loop tests PASS ===" as *u8)
112 return 0
113 }
114 print("=== " as *u8); print_i64(fails); println(" discount-loop tests FAILED ===" as *u8)
115 return 1
116}