nx_answer.nx source
↩ module page · 88 lines · 3420 B
1// nx_answer.nx -- AnswerLiteral support for "find a witness" queries.
2//
3// Per Vampire-displacement roadmap Phase 2. When a conjecture has
4// the shape ∃X. p(X) and we want to know WHICH X works (not just that
5// some X exists), we attach a special $answer(X) literal to the
6// negated conjecture clause. Saturation tracks the answer literal
7// through every inference; when the proof closes (empty-clause-modulo-
8// answer), the surviving $answer(witness) literal carries the X
9// instantiation that closed the proof.
10//
11// Convention: the answer predicate symbol id is caller-supplied (no
12// magic constant, same shape as eq_sym in nx_tautology / nx_tptp_load).
13// Recommended: NX_ANS_BASE (700_000) -- distinct from user (1_000+),
14// Tseitin (800_000+), Skolem (900_000+).
15//
16// API:
17// nx_answer_attach(c, ans_sym, witness_var_id) -- adds $answer(X) literal
18// nx_clause_is_answer_only(c, ans_sym) -- 1 iff c only has $answer(...)
19// nx_clause_extract_answer(c, ans_sym) -- returns the witness term, null if none
20
21// nx_safety_envelope:
22// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
23// sil_target: SIL1
24// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
25// verdict: NOT_YET_EVALUATED
26
27import "nx_syscalls.nx"
28import "nx_runtime.nx"
29import "nx_tier.nx"
30import "nx_result.nx"
31import "nx_unify.nx"
32import "nx_resolution.nx"
33
34const NX_ANS_BASE: nx_int = 700000
35
36// Build a $answer(X) literal where X is a variable with the given id.
37// The answer atom is a positive APP of `ans_sym` over a single arg.
38func nx_answer_lit(ans_sym: nx_int, witness_var_id: nx_int) -> *Literal {
39 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
40 arg.kind = NX_TERM_VAR
41 arg.sym = witness_var_id
42 arg.n_args = 0
43 arg.args = 0 as *Term
44 let atom: *Term = nx_term_app(ans_sym, 1, arg)
45 return nx_lit_make(NX_LIT_POS, atom)
46}
47
48// Attach an answer literal to a conjecture clause. The clause is
49// modified in place; returns Result<n_lits_after_add, NX_ERR_*>.
50func nx_answer_attach(c: *Clause, ans_sym: nx_int, witness_var_id: nx_int) -> *NxResult {
51 return nx_clause_add(c, nx_answer_lit(ans_sym, witness_var_id))
52}
53
54// True iff every literal in c is a positive $answer(...) literal.
55// This is the post-saturation predicate that says "this is the
56// answer-bearing 'empty' clause".
57func nx_clause_is_answer_only(c: *Clause, ans_sym: nx_int) -> nx_int {
58 if c.n_lits == 0 { return 0 }
59 var i: nx_int = 0
60 while i < c.n_lits {
61 let l: *Literal = nx_clause_lit_at(c, i)
62 if l.sign != NX_LIT_POS { return 0 }
63 if l.atom.kind != NX_TERM_APP { return 0 }
64 if l.atom.sym != ans_sym { return 0 }
65 i = i + 1
66 }
67 return 1
68}
69
70// Extract the witness term from a clause's first answer literal.
71// Returns the term inside $answer(...), or null if no answer literal.
72func nx_clause_extract_answer(c: *Clause, ans_sym: nx_int) -> *Term {
73 var i: nx_int = 0
74 while i < c.n_lits {
75 let l: *Literal = nx_clause_lit_at(c, i)
76 if l.sign == NX_LIT_POS {
77 if l.atom.kind == NX_TERM_APP {
78 if l.atom.sym == ans_sym {
79 if l.atom.n_args >= 1 {
80 return nx_term_arg(l.atom, 0)
81 }
82 }
83 }
84 }
85 i = i + 1
86 }
87 return 0 as *Term
88}