nx_answer_test.nx source
↩ module page · 94 lines · 4157 B
1// nx_answer_test.nx -- AnswerLiteral 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_answer.nx"
10
11const SYM_A: nx_int = 100
12const SYM_P: nx_int = 200
13const SYM_ANS: nx_int = 700001 // in NX_ANS_BASE range
14const VAR_X: nx_int = 0
15
16func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
17 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
18 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
19 return nx_term_app(p_sym, 1, arg)
20}
21
22func mk_p_const(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("=== AnswerLiteral smoke ===" as *u8)
30 var fails: nx_int = 0
31
32 // ---------- Test 1: attach answer ---------------------------
33 // Negated conjecture: {~p(X)}, attach $answer(X) -> {~p(X), $answer(X)}
34 let c1: *Clause = nx_clause_new()
35 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_NEG, mk_p_var(SYM_P, VAR_X)))
36 let _r1b: *NxResult = nx_answer_attach(c1, SYM_ANS, VAR_X)
37 print(" 1. attach answer -> n_lits=" as *u8); print_i64(c1.n_lits); println("" as *u8)
38 if c1.n_lits == 2 {
39 println(" 2 literals (orig + answer) PASS" as *u8)
40 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
41
42 // ---------- Test 2: clause with non-answer is not answer-only -
43 let aok1: nx_int = nx_clause_is_answer_only(c1, SYM_ANS)
44 print(" 2. is_answer_only({~p,$ans}) -> " as *u8); print_i64(aok1); println("" as *u8)
45 if aok1 == 0 {
46 println(" mixed clause not flagged PASS" as *u8)
47 } else { println(" wrong FAIL" as *u8); fails = fails + 1 }
48
49 // ---------- Test 3: pure-answer clause IS answer-only --------
50 // After resolution would give us {$answer(a)} -- pure answer.
51 let c3: *Clause = nx_clause_new()
52 let ans_a: *Term = mk_p_const(SYM_ANS, SYM_A) // $answer(a)
53 let _r3: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, ans_a))
54 let aok3: nx_int = nx_clause_is_answer_only(c3, SYM_ANS)
55 print(" 3. is_answer_only({$ans(a)}) -> " as *u8); print_i64(aok3); println("" as *u8)
56 if aok3 == 1 {
57 println(" answer-only flagged PASS" as *u8)
58 } else { println(" wrong FAIL" as *u8); fails = fails + 1 }
59
60 // ---------- Test 4: extract witness -------------------------
61 let witness: *Term = nx_clause_extract_answer(c3, SYM_ANS)
62 if (witness as nx_int) == 0 {
63 println(" 4. extract witness -> NULL FAIL" as *u8); fails = fails + 1
64 } else {
65 if witness.sym == SYM_A {
66 if witness.kind == NX_TERM_CONST {
67 println(" 4. extract witness -> CONST(a) PASS" as *u8)
68 } else { println(" 4. wrong kind FAIL" as *u8); fails = fails + 1 }
69 } else { print(" 4. wrong sym=" as *u8); print_i64(witness.sym); println(" FAIL" as *u8); fails = fails + 1 }
70 }
71
72 // ---------- Test 5: empty clause is not answer-only ----------
73 let c5: *Clause = nx_clause_new()
74 let aok5: nx_int = nx_clause_is_answer_only(c5, SYM_ANS)
75 if aok5 == 0 {
76 println(" 5. is_answer_only({}) -> 0 PASS" as *u8)
77 } else { println(" 5. empty wrongly flagged FAIL" as *u8); fails = fails + 1 }
78
79 // ---------- Test 6: extract from non-answer clause ----------
80 let plain: *Clause = nx_clause_new()
81 let _rp: *NxResult = nx_clause_add(plain, nx_lit_make(NX_LIT_POS, mk_p_const(SYM_P, SYM_A)))
82 let no_ans: *Term = nx_clause_extract_answer(plain, SYM_ANS)
83 if (no_ans as nx_int) == 0 {
84 println(" 6. extract({p(a)}) -> NULL PASS" as *u8)
85 } else { println(" 6. spurious answer FAIL" as *u8); fails = fails + 1 }
86
87 println("" as *u8)
88 if fails == 0 {
89 println("=== ALL 6 AnswerLiteral tests PASS ===" as *u8)
90 return 0
91 }
92 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
93 return 1
94}