nx_selection.nx source
↩ module page · 79 lines · 2935 B
1// nx_selection.nx -- literal selection functions for ordered resolution.
2//
3// Per Vampire-displacement roadmap Phase 2. Standard saturation
4// refinement: instead of trying every literal of every clause as a
5// resolution partner, restrict to a single SELECTED literal per
6// clause. Dramatically prunes the search space.
7//
8// Selectors shipped here:
9// nx_select_first_negative(c) first NEG literal index, -1 if none
10// nx_select_first_positive(c) first POS literal index, -1 if none
11// nx_select_last(c) last literal index, -1 if empty
12// nx_select_kbo_maximal(st, c) KBO-greatest atom's literal index
13//
14// Sealed return: -1 = no selection (caller falls back to all-literal
15// resolution); otherwise a valid index in [0, c.n_lits).
16
17// nx_safety_envelope:
18// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
19// sil_target: SIL1
20// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
21// verdict: NOT_YET_EVALUATED
22
23import "nx_syscalls.nx"
24import "nx_runtime.nx"
25import "nx_tier.nx"
26import "nx_result.nx"
27import "nx_unify.nx"
28import "nx_resolution.nx"
29import "nx_term_order.nx"
30
31// Select the first negative literal. Standard "negative selection"
32// heuristic -- if a negative literal exists, it's the only resolution
33// candidate; otherwise no selection (caller falls back).
34func nx_select_first_negative(c: *Clause) -> nx_int {
35 var i: nx_int = 0
36 while i < c.n_lits {
37 let l: *Literal = nx_clause_lit_at(c, i)
38 if l.sign == NX_LIT_NEG { return i }
39 i = i + 1
40 }
41 return 0 - 1
42}
43
44// Select the first positive literal (mirror of negative selection).
45func nx_select_first_positive(c: *Clause) -> nx_int {
46 var i: nx_int = 0
47 while i < c.n_lits {
48 let l: *Literal = nx_clause_lit_at(c, i)
49 if l.sign == NX_LIT_POS { return i }
50 i = i + 1
51 }
52 return 0 - 1
53}
54
55// Select the last literal. Useful for ordered strategies that
56// process arguments right-to-left.
57func nx_select_last(c: *Clause) -> nx_int {
58 if c.n_lits == 0 { return 0 - 1 }
59 return c.n_lits - 1
60}
61
62// Select the KBO-maximal literal. Returns the index of the literal
63// whose ATOM is greatest under KBO compared with all other atoms in
64// the clause. Falls back to last-index if KBO can't compare every
65// pair (INCOMP). max_var_id is the variable space upper bound (caller
66// knows; e.g., NX_KBO_MAX_VARS or per-clause upper).
67func nx_select_kbo_maximal(st: *KboState, c: *Clause, max_var_id: nx_int) -> nx_int {
68 if c.n_lits == 0 { return 0 - 1 }
69 var best: nx_int = 0
70 var i: nx_int = 1
71 while i < c.n_lits {
72 let li: *Literal = nx_clause_lit_at(c, i)
73 let lb: *Literal = nx_clause_lit_at(c, best)
74 let cmp: nx_int = nx_kbo_compare(st, li.atom, lb.atom, max_var_id)
75 if cmp == NX_KBO_GT { best = i }
76 i = i + 1
77 }
78 return best
79}