`nx_pre_sat.nx` source

1// nx_pre_sat.nx -- pre-saturation simplification of input clause set.
2//
3// Per Vampire-displacement roadmap Phase 2.  Before the saturation
4// loop starts, run a pass that drops tautologies + forward-subsumed
5// clauses from the input.  Reduces the initial working set, which
6// compounds with the discount loop's per-step pruning.
7//
8// Pure composition over existing primitives:
9//   - nx_is_tautology (nx_tautology.nx)
10//   - nx_subsumes     (nx_subsumption.nx)
11//
12// Algorithm (linear-quadratic in n_input):
13//   For each input clause C in order:
14//     1. If C is a tautology -> drop.
15//     2. If any already-kept clause subsumes C -> drop.
16//     3. Otherwise: backward-subsume the kept set against C
17//        (drop any older C' that the new C subsumes), then add C.
18//
19// This is a one-shot variant of the discount loop's per-pick filter,
20// applied to the input batch only -- it doesn't re-saturate.
21
22// nx_safety_envelope:
23//   intended_use:       AUTO_APPLIED -- primitive-specific tuning queued
24//   sil_target:         SIL1
25//   evidence:           [bulk_applied_2026-05-16, see-file-comment-for-detail]
26//   verdict:            NOT_YET_EVALUATED
27
28import "nx_syscalls.nx"
29import "nx_runtime.nx"
30import "nx_tier.nx"
31import "nx_result.nx"
32import "nx_unify.nx"
33import "nx_resolution.nx"
34import "nx_subsumption.nx"
35import "nx_tautology.nx"
36
37// Returns the number of clauses kept; populates out[] with kept
38// clauses (caller-allocated, capacity = at least n_input).
39func nx_pre_sat_simplify(input: *Clause, n_input: nx_int, eq_sym: nx_int,
40                         out: *Clause) -> nx_int {
41    var n_out: nx_int = 0
42    var i: nx_int = 0
43    while i < n_input {
44        let c: *Clause = ((input as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
45
46        // (1) Tautology drop.
47        var keep: nx_int = 1
48        if nx_is_tautology(c, eq_sym) == NX_TAUTOLOGY { keep = 0 }
49
50        // (2) Forward subsumption check against kept clauses.
51        if keep == 1 {
52            var j: nx_int = 0
53            while j < n_out {
54                let kept: *Clause = ((out as nx_int) + (j * NX_CLAUSE_BYTES)) as *Clause
55                if nx_subsumes(kept, c) == NX_SUBSUMES_YES { keep = 0; j = n_out }
56                if keep == 1 { j = j + 1 }
57            }
58        }
59
60        if keep == 1 {
61            // (3) Backward subsumption: drop any kept clause that c
62            // subsumes (c is more general).  Compact in place.
63            var read: nx_int = 0
64            var write: nx_int = 0
65            while read < n_out {
66                let kept2: *Clause = ((out as nx_int) + (read * NX_CLAUSE_BYTES)) as *Clause
67                var keep_kept: nx_int = 1
68                if nx_subsumes(c, kept2) == NX_SUBSUMES_YES { keep_kept = 0 }
69                if keep_kept == 1 {
70                    if read != write {
71                        let dest: *Clause = ((out as nx_int) + (write * NX_CLAUSE_BYTES)) as *Clause
72                        dest.n_lits = kept2.n_lits
73                        dest.lits   = kept2.lits
74                    }
75                    write = write + 1
76                }
77                read = read + 1
78            }
79            n_out = write
80
81            // Add c to the kept set.
82            let dest_new: *Clause = ((out as nx_int) + (n_out * NX_CLAUSE_BYTES)) as *Clause
83            dest_new.n_lits = c.n_lits
84            dest_new.lits   = c.lits
85            n_out = n_out + 1
86        }
87        i = i + 1
88    }
89    return n_out
90}
nx_pre_sat.nx source

`nx_pre_sat.nx` source
