nx_selection.nx
buildroot/runtime/nx_selection.nx
about
nx_selection.nx -- literal selection functions for ordered resolution.
Per Vampire-displacement roadmap Phase 2. Standard saturation
refinement: instead of trying every literal of every clause as a
resolution partner, restrict to a single SELECTED literal per
clause. Dramatically prunes the search space.
Selectors shipped here:
nx_select_first_negative(c) first NEG literal index, -1 if none
nx_select_first_positive(c) first POS literal index, -1 if none
nx_select_last(c) last literal index, -1 if empty
nx_select_kbo_maximal(st, c) KBO-greatest atom's literal index
Sealed return: -1 = no selection (caller falls back to all-literal
resolution); otherwise a valid index in [0, c.n_lits).
dependencies 7 imports · 1 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nxnx_resolution.nxnx_term_order.nx
imported by: nx_selection_test.nx
structs
| none |
consts
| none |
functions
| 34 | func nx_select_first_negative(c: *Clause) -> nx_int |
| 45 | func nx_select_first_positive(c: *Clause) -> nx_int |
| 57 | func nx_select_last(c: *Clause) -> nx_int called by 1: main |
| 67 | func nx_select_kbo_maximal(st: *KboState, c: *Clause, max_var_id: nx_int) -> nx_int |