nx_smtlib_parse_test.nx source
↩ module page · 88 lines · 4321 B
1// nx_smtlib_parse_test.nx -- SMT-LIB parser smoke + end-to-end solve.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_str.nx"
7import "nx_result.nx"
8import "nx_sat_solver.nx"
9import "nx_smtlib_parse.nx"
10
11func mk_input(s: *u8) -> *u8 {
12 let len: nx_int = nx_str_len(s)
13 let buf: *u8 = sys_mmap((len + 1) as i64)
14 var i: nx_int = 0
15 while i < len { buf[i] = s[i]; i = i + 1 }
16 buf[len] = 0
17 return buf
18}
19
20func main() -> nx_exit {
21 println("=== SMT-LIB parser smoke ===" as *u8)
22 var fails: nx_int = 0
23
24 // ---------- Test 1: simple SAT case -------------------------
25 // (assert p) -- one unit clause [p]; SAT (set p=true)
26 let s1: *u8 = "(set-logic QF_UF) (declare-const p Bool) (assert p) (check-sat) (exit)" as *u8
27 let buf1: *u8 = mk_input(s1)
28 let len1: nx_int = nx_str_len(s1)
29 let f1: *SatFormula = nx_smtlib_parse(buf1, len1)
30 let v1: nx_int = nx_sat_solve(f1)
31 print(" 1. (assert p) -> n_clauses=" as *u8); print_i64(f1.n_clauses); print(" verdict=" as *u8); print_i64(v1); println("" as *u8)
32 if f1.n_clauses == 1 {
33 if v1 == NX_SAT_SAT { println(" SAT PASS" as *u8) }
34 else { println(" expected SAT FAIL" as *u8); fails = fails + 1 }
35 } else { println(" wrong clause count FAIL" as *u8); fails = fails + 1 }
36
37 // ---------- Test 2: contradiction -- UNSAT ------------------
38 // (assert p) (assert (not p)) -- two unit clauses, UNSAT
39 let s2: *u8 = "(declare-const p Bool) (assert p) (assert (not p)) (check-sat)" as *u8
40 let buf2: *u8 = mk_input(s2)
41 let len2: nx_int = nx_str_len(s2)
42 let f2: *SatFormula = nx_smtlib_parse(buf2, len2)
43 let v2: nx_int = nx_sat_solve(f2)
44 print(" 2. (assert p)(assert (not p)) -> n=" as *u8); print_i64(f2.n_clauses); print(" verdict=" as *u8); print_i64(v2); println("" as *u8)
45 if v2 == NX_SAT_UNSAT { println(" UNSAT PASS" as *u8) }
46 else { println(" expected UNSAT FAIL" as *u8); fails = fails + 1 }
47
48 // ---------- Test 3: disjunction ------------------------------
49 // (assert (or p q)) (assert (not p)) (assert (not q)) -- UNSAT
50 let s3: *u8 = "(declare-const p Bool) (declare-const q Bool) (assert (or p q)) (assert (not p)) (assert (not q)) (check-sat)" as *u8
51 let buf3: *u8 = mk_input(s3)
52 let len3: nx_int = nx_str_len(s3)
53 let f3: *SatFormula = nx_smtlib_parse(buf3, len3)
54 let v3: nx_int = nx_sat_solve(f3)
55 print(" 3. (or p q) + ~p + ~q -> n=" as *u8); print_i64(f3.n_clauses); print(" verdict=" as *u8); print_i64(v3); println("" as *u8)
56 if v3 == NX_SAT_UNSAT { println(" UNSAT PASS" as *u8) }
57 else { println(" expected UNSAT FAIL" as *u8); fails = fails + 1 }
58
59 // ---------- Test 4: implication -----------------------------
60 // (assert (=> p q)) (assert p) (assert (not q)) -- UNSAT
61 let s4: *u8 = "(declare-const p Bool) (declare-const q Bool) (assert (=> p q)) (assert p) (assert (not q)) (check-sat)" as *u8
62 let buf4: *u8 = mk_input(s4)
63 let len4: nx_int = nx_str_len(s4)
64 let f4: *SatFormula = nx_smtlib_parse(buf4, len4)
65 let v4: nx_int = nx_sat_solve(f4)
66 print(" 4. (=> p q) + p + ~q -> n=" as *u8); print_i64(f4.n_clauses); print(" verdict=" as *u8); print_i64(v4); println("" as *u8)
67 if v4 == NX_SAT_UNSAT { println(" UNSAT (modus ponens) PASS" as *u8) }
68 else { println(" expected UNSAT FAIL" as *u8); fails = fails + 1 }
69
70 // ---------- Test 5: simple SAT with (and ...) ---------------
71 // (assert (and p q)) -- two unit clauses, SAT (p=q=true)
72 let s5: *u8 = "(declare-const p Bool) (declare-const q Bool) (assert (and p q)) (check-sat)" as *u8
73 let buf5: *u8 = mk_input(s5)
74 let len5: nx_int = nx_str_len(s5)
75 let f5: *SatFormula = nx_smtlib_parse(buf5, len5)
76 let v5: nx_int = nx_sat_solve(f5)
77 print(" 5. (and p q) -> n=" as *u8); print_i64(f5.n_clauses); print(" verdict=" as *u8); print_i64(v5); println("" as *u8)
78 if v5 == NX_SAT_SAT { println(" SAT PASS" as *u8) }
79 else { println(" expected SAT FAIL" as *u8); fails = fails + 1 }
80
81 println("" as *u8)
82 if fails == 0 {
83 println("=== ALL 5 SMT-LIB tests PASS ===" as *u8)
84 return 0
85 }
86 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
87 return 1
88}