nx_pure_lit.nx

nx_pure_lit.nx -- pure-literal elimination preprocessing. A predicate symbol is "pure" if it appears with only one polarity across the entire clause set. Clauses containing a pure literal can be vacuously satisfied -- there's no clause that could ever contradict them, so removing them preserves UNSAT-equivalence. Standard SAT-solver preprocessing (Davis-Putnam 1960 lineage) extended to first-order: the predicate symbol is the unit of purity, not the literal. A clause containing ANY pure-positive literal of pred p (or ANY pure-negative literal of pred p) is dropped. Iterating to fixpoint can cascade: dropping clauses may make other predicates become pure. API: nx_pure_lit_eliminate(input, n_input, out, *out_n) -- one pass. Caller iterates to fixpoint if desired. Bits-up nx_int.