nx_clause_components.nx
buildroot/runtime/nx_clause_components.nx
about
nx_clause_components.nx -- variable-disjoint clause components.
Per Vampire-displacement roadmap Phase 2. Foundational analysis
for AVATAR-style splitting: a clause whose literals partition into
variable-disjoint groups can be solved component-by-component, with
the SAT solver coordinating which combinations are consistent.
Definition: two literals are in the same COMPONENT iff they share
at least one variable. Constants and matching predicates without
shared variables are independent.
Algorithm: union-find over literals, where literal i and literal j
are unioned iff they share any variable. Output: for each literal,
the component id (canonical root) it belongs to.
Single-component clause: the standard case; AVATAR doesn't split
it. Multi-component clause: AVATAR introduces a fresh propositional
var for each component and asks the SAT solver to coordinate.
API:
nx_clause_n_components(c) -> int (# distinct components)
nx_clause_component_of(c, lit_idx) -> int (component id 0..n-1)
nx_clause_components_classify(c, out_ids) -- fills out_ids[lit_idx] = comp_id
dependencies 6 imports · 7 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nxnx_resolution.nx
imported by: nx_avatar_encode.nxnx_avatar_encode_test.nxnx_avatar_solve_test.nxnx_avatar_split.nxnx_avatar_split_test.nxnx_clause_components_test.nxnx_solve.nx
structs
| none |
consts
| 38 | const NX_COMP_MAX_VARS_PER_LIT: nx_int = 32 |
functions
| 42 | func nx_comp_collect_vars(t: *Term, out: *nx_int, n_out: nx_int) -> nx_int called by 2: nx_comp_collect_varsnx_clause_components_classify calls 2: nx_comp_collect_varsnx_term_arg |
| 67 | func nx_comp_vars_share(a: *nx_int, na: nx_int, b: *nx_int, nb: nx_int) -> nx_int called by 1: nx_clause_components_classify |
| 81 | func nx_comp_uf_find(parent: *nx_int, x: nx_int) -> nx_int |
| 97 | func nx_comp_uf_union(parent: *nx_int, a: nx_int, b: nx_int) |
| 106 | func nx_clause_components_classify(c: *Clause, out_ids: *nx_int) -> nx_int |
| 166 | func nx_clause_n_components(c: *Clause) -> nx_int |