nx_saturation.nx source

1// nx_saturation.nx -- given-clause saturation loop with factoring. 2// 3// Per user 2026-05-14 "keep going till we can submit to casc". This 4// is the proof-search engine on top of unify + resolution. Given a 5// set of clauses (typically the negation of a conjecture), iterate 6// resolution + factoring until either: 7// - the empty clause is derived -> UNSAT (proof of original conjecture) 8// - no new clauses can be derived -> UNKNOWN / SAT 9// - resource budget exhausted -> TIMEOUT 10// 11// Discovery-Otter-Vampire-E-SPASS use this same skeleton; their 12// performance differences come from clause selection heuristic + 13// indexing + subsumption. 14 15// nx_safety_envelope: 16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 17// sil_target: SIL1 18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 19// verdict: NOT_YET_EVALUATED 20 21import "nx_syscalls.nx" 22import "nx_runtime.nx" 23import "nx_tier.nx" 24import "nx_result.nx" 25import "nx_unify.nx" 26import "nx_resolution.nx" 27import "nx_subsumption.nx" 28import "nx_tautology.nx" 29import "nx_disctree.nx" 30import "nx_paramodulation.nx" 31const NX_MAGIC_9223372036854775807: i64 = 9223372036854775807 32 33// ===== Factoring rule =============================================== 34// Factoring: within ONE clause, if two literals can be unified, we 35// can collapse them. Example: {p(x), p(a)} -> {p(a)} after 36// applying {x -> a}. 37// Returns Result<n_factored_lits, NX_ERR_*>. Builds the factored 38// clause in c_out. 39func nx_factor(c: *Clause, i: nx_int, j: nx_int, c_out: *Clause) -> *NxResult { 40 if i < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 41 if j < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 42 if i == j { return nx_result_err(NX_ERR_INVALID_INPUT) } 43 if i >= c.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 44 if j >= c.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) } 45 46 let l1: *Literal = nx_clause_lit_at(c, i) 47 let l2: *Literal = nx_clause_lit_at(c, j) 48 49 // Same sign required for factoring 50 if l1.sign != l2.sign { return nx_result_err(NX_ERR_TAG_MISMATCH) } 51 52 // Try to unify the atoms 53 let s: *Subst = nx_subst_new() 54 let r_un: *NxResult = nx_unify(l1.atom, l2.atom, s) 55 if nx_result_is_err(r_un) == 1 { return r_un } 56 57 // Build factored clause: drop literal j, apply subst to the rest 58 var k: nx_int = 0 59 while k < c.n_lits { 60 if k != j { 61 let lk: *Literal = nx_clause_lit_at(c, k) 62 let lk_subst: *Literal = nx_lit_apply_subst(lk, s) 63 let r: *NxResult = nx_clause_add(c_out, lk_subst) 64 if nx_result_is_err(r) == 1 { return r } 65 } 66 k = k + 1 67 } 68 return nx_result_ok(c_out.n_lits) 69} 70 71// ===== Given-clause saturation loop ================================= 72// 73// State: processed clauses + unprocessed clauses + step budget. 74// Each iteration: pick the oldest unprocessed clause (FIFO = "given"); 75// try to resolve it against every processed clause; add the 76// resolvents to unprocessed; if empty clause derived, halt with UNSAT. 77// 78// Discipline: bounded budget (steps); honest Result on timeout. 79 80const NX_SAT_MAX_PROCESSED: nx_int = 256 81const NX_SAT_MAX_UNPROCESSED: nx_int = 1024 82 83struct Saturation { 84 processed: *Clause, // flat array of Clause structs 85 n_processed: nx_int, 86 unprocessed: *Clause, 87 n_unproc: nx_int, 88 head_unproc: nx_int, // FIFO head index (used by nx_sat_pick_given) 89 budget: nx_int, // remaining inference steps 90 picked: *nx_int, // [NX_SAT_MAX_UNPROCESSED] -- 1 if consumed 91 // by a non-FIFO picker 92 // (nx_sat_pick_given_best_first) 93 proc_index: *DiscTree, // discrim tree indexing processed 94 // clauses' literal atoms; values 95 // are clause indices into processed[] 96 proc_deleted: *nx_int, // [NX_SAT_MAX_PROCESSED] -- tombstone 97 // bit per processed slot. Backward 98 // simp marks deleted=1 instead of 99 // compacting; iteration skips 100 // tombstoned slots; discrim tree 101 // stays valid without rebuild. 102} 103 104const NX_SAT_BYTES: nx_int = 72 105 106func nx_saturation_new(initial_budget: nx_int) -> *Saturation { 107 let s: *Saturation = (sys_mmap(NX_SAT_BYTES as i64)) as *Saturation 108 s.processed = (sys_mmap((NX_SAT_MAX_PROCESSED * NX_CLAUSE_BYTES) as i64)) as *Clause 109 s.n_processed = 0 110 s.unprocessed = (sys_mmap((NX_SAT_MAX_UNPROCESSED * NX_CLAUSE_BYTES) as i64)) as *Clause 111 s.n_unproc = 0 112 s.head_unproc = 0 113 s.budget = initial_budget 114 s.picked = (sys_mmap((NX_SAT_MAX_UNPROCESSED * 8) as i64)) as *nx_int 115 s.proc_index = nx_dt_new() 116 s.proc_deleted = (sys_mmap((NX_SAT_MAX_PROCESSED * 8) as i64)) as *nx_int 117 return s 118} 119 120// Forward declaration: nx_sat_add_unproc_filtered (defined further 121// down) calls nx_sat_proc_subsumes_indexed (defined further down 122// still). nxc2 supports forward decls via the `func name(...) -> T;` 123// syntax (parse.c line 1971). Type *Saturation must be declared 124// first -- which it is, just above. 125func nx_sat_proc_subsumes_indexed(s: *Saturation, c: *Clause) -> nx_int; 126// nx_sat_run_discount_lrs (LRS variant) calls nx_sat_rebuild_index 127// which lives further down. 128func nx_sat_rebuild_index(s: *Saturation); 129 130// Get the i-th unprocessed clause (FIFO ordered). 131func nx_sat_unproc_at(s: *Saturation, i: nx_int) -> *Clause { 132 return ((s.unprocessed as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause 133} 134 135func nx_sat_proc_at(s: *Saturation, i: nx_int) -> *Clause { 136 return ((s.processed as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause 137} 138 139// Add a clause to the unprocessed queue. 140func nx_sat_add_unproc(s: *Saturation, c: *Clause) -> *NxResult { 141 if s.n_unproc >= NX_SAT_MAX_UNPROCESSED { return nx_result_err(NX_ERR_OVERFLOW) } 142 let slot: *Clause = nx_sat_unproc_at(s, s.n_unproc) 143 slot.n_lits = c.n_lits 144 slot.lits = c.lits 145 s.n_unproc = s.n_unproc + 1 146 return nx_result_ok(s.n_unproc) 147} 148 149// Pick the next given clause (FIFO). Returns the clause + advances head. 150func nx_sat_pick_given(s: *Saturation) -> *Clause { 151 if s.head_unproc >= s.n_unproc { return 0 as *Clause } 152 let c: *Clause = nx_sat_unproc_at(s, s.head_unproc) 153 s.head_unproc = s.head_unproc + 1 154 return c 155} 156 157// Move given to processed. 158func nx_sat_move_to_processed(s: *Saturation, given: *Clause) -> *NxResult { 159 if s.n_processed >= NX_SAT_MAX_PROCESSED { return nx_result_err(NX_ERR_OVERFLOW) } 160 let slot: *Clause = nx_sat_proc_at(s, s.n_processed) 161 slot.n_lits = given.n_lits 162 slot.lits = given.lits 163 s.n_processed = s.n_processed + 1 164 return nx_result_ok(s.n_processed) 165} 166 167// Try to resolve `given` against `other` on every complementary literal pair. 168// Adds any resolvents to unprocessed. Returns NX_VERDICT_UNSAT (= 2) on 169// empty-clause derivation; NX_VERDICT_UNKNOWN otherwise. 170const NX_SAT_VERDICT_UNSAT: nx_int = 2 171const NX_SAT_VERDICT_UNKNOWN: nx_int = 5 172 173func nx_sat_try_resolve_pair(s: *Saturation, given: *Clause, other: *Clause) -> nx_int { 174 var i: nx_int = 0 175 while i < given.n_lits { 176 var j: nx_int = 0 177 while j < other.n_lits { 178 let resolvent: *Clause = nx_clause_new() 179 let r: *NxResult = nx_resolve(given, i, other, j, resolvent) 180 if nx_result_is_ok(r) == 1 { 181 if nx_clause_is_empty(resolvent) == 1 { return NX_SAT_VERDICT_UNSAT } 182 let _add: *NxResult = nx_sat_add_unproc(s, resolvent) 183 } 184 j = j + 1 185 } 186 i = i + 1 187 } 188 return NX_SAT_VERDICT_UNKNOWN 189} 190 191// Main saturation loop. Returns verdict. 192func nx_sat_run(s: *Saturation) -> nx_int { 193 while s.budget > 0 { 194 let given: *Clause = nx_sat_pick_given(s) 195 if (given as nx_int) == 0 { return NX_SAT_VERDICT_UNKNOWN } // queue exhausted 196 197 // Resolve given against every processed 198 var p: nx_int = 0 199 while p < s.n_processed { 200 let other: *Clause = nx_sat_proc_at(s, p) 201 let v: nx_int = nx_sat_try_resolve_pair(s, given, other) 202 if v == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 203 p = p + 1 204 } 205 206 // Self-resolve given against itself (covers tautologies + self-contradictions) 207 let v2: nx_int = nx_sat_try_resolve_pair(s, given, given) 208 if v2 == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 209 210 // Move given to processed 211 let _: *NxResult = nx_sat_move_to_processed(s, given) 212 s.budget = s.budget - 1 213 } 214 return NX_SAT_VERDICT_UNKNOWN 215} 216 217// ===== Discount-loop strategy ======================================= 218// 219// The DISCOUNT loop differs from the OTTER loop above by aggressively 220// pruning clauses through forward subsumption + tautology deletion at 221// every insertion point. Vampire's default mode. Trades a small 222// per-clause cost (subsumption check) for a much smaller passive set, 223// which dominates total runtime on non-trivial CASC problems. 224// 225// What's pruned: 226// - Tautological clauses (drop on insertion) 227// - Clauses subsumed by any processed (drop on insertion + on pick) 228// 229// Backward simplification (deleting subsumed processed clauses when a 230// new general clause is added) is deferred -- requires array compaction 231// over `processed`, which is a Phase 2 follow-up. 232// 233// eq_sym: caller-provided symbol id of the equality predicate (for 234// tautology check). Pass any unused sym_id when equations aren't in 235// play -- the reflexive-equality branch will simply never fire. 236 237// True iff some processed clause subsumes c. Skips tombstoned slots 238// (proc_deleted=1) so callers using this linear variant get the same 239// semantic answer as the indexed variant. 240func nx_sat_proc_subsumes(s: *Saturation, c: *Clause) -> nx_int { 241 var i: nx_int = 0 242 while i < s.n_processed { 243 if s.proc_deleted[i] == 0 { 244 let other: *Clause = nx_sat_proc_at(s, i) 245 if nx_subsumes(other, c) == NX_SUBSUMES_YES { return 1 } 246 } 247 i = i + 1 248 } 249 return 0 250} 251 252// Dedup duplicate literals in-place (return new clause). Used on 253// resolvents before they enter unprocessed -- without dedup, resolvents 254// like {q, q} accumulate and overflow the queue without ever closing. 255func nx_sat_clause_dedup(c: *Clause) -> *Clause { 256 let out: *Clause = nx_clause_new() 257 var i: nx_int = 0 258 while i < c.n_lits { 259 let li: *Literal = nx_clause_lit_at(c, i) 260 var dup: nx_int = 0 261 var j: nx_int = 0 262 while j < out.n_lits { 263 let lj: *Literal = nx_clause_lit_at(out, j) 264 if li.sign == lj.sign { 265 if nx_term_eq(li.atom, lj.atom) == 1 { dup = 1 } 266 } 267 j = j + 1 268 } 269 if dup == 0 { 270 let _r: *NxResult = nx_clause_add(out, li) 271 } 272 i = i + 1 273 } 274 return out 275} 276 277// Tautology + forward-subsumption gate before adding to unprocessed. 278// Returns 1 if added, 0 if filtered, NX_ERR_OVERFLOW on capacity. 279// 280// Uses indexed subsumption (proc_index discrim tree) for the candidate 281// lookup -- replaces the O(n_processed) linear scan with an O(d) trie 282// walk. Same semantic answer; faster on large processed sets. 283// 284// Dedups literals before insertion so resolvent shapes like {q, q} get 285// reduced to {q} (without this, the discount loop overflows on 286// problems whose resolvents naturally produce duplicates -- e.g. 287// pel009 hit the 1024-clause unprocessed cap without it). 288func nx_sat_add_unproc_filtered(s: *Saturation, c: *Clause, eq_sym: nx_int) -> nx_int { 289 let dedup_c: *Clause = nx_sat_clause_dedup(c) 290 if nx_is_tautology(dedup_c, eq_sym) == NX_TAUTOLOGY { return 0 } 291 if nx_sat_proc_subsumes_indexed(s, dedup_c) == 1 { return 0 } 292 let r: *NxResult = nx_sat_add_unproc(s, dedup_c) 293 if nx_result_is_err(r) == 1 { return 0 - NX_ERR_OVERFLOW } 294 return 1 295} 296 297// Paramodulate eq_clause into target_clause: for each positive 298// equality literal in eq_clause and each literal in target_clause, 299// attempt paramodulation and filter the result through the discount 300// gate. Returns NX_SAT_VERDICT_UNSAT if a paramodulant turns out 301// empty; NX_SAT_VERDICT_UNKNOWN otherwise. 302func nx_sat_try_paramodulate_pair_filtered(s: *Saturation, eq_clause: *Clause, 303 target_clause: *Clause, eq_sym: nx_int) -> nx_int { 304 var i: nx_int = 0 305 while i < eq_clause.n_lits { 306 let li: *Literal = nx_clause_lit_at(eq_clause, i) 307 // Only positive equality literals can be the rewriting source. 308 if li.sign == NX_LIT_POS { 309 if li.atom.kind == NX_TERM_APP { 310 if li.atom.sym == eq_sym { 311 if li.atom.n_args == 2 { 312 var j: nx_int = 0 313 while j < target_clause.n_lits { 314 let resolvent: *Clause = nx_clause_new() 315 let r: *NxResult = nx_paramodulate(eq_clause, i, 316 target_clause, j, eq_sym, resolvent) 317 if nx_result_is_ok(r) == 1 { 318 if nx_clause_is_empty(resolvent) == 1 { 319 return NX_SAT_VERDICT_UNSAT 320 } 321 let _add: nx_int = nx_sat_add_unproc_filtered(s, resolvent, eq_sym) 322 } 323 j = j + 1 324 } 325 } 326 } 327 } 328 } 329 i = i + 1 330 } 331 return NX_SAT_VERDICT_UNKNOWN 332} 333 334// Resolve given x other, filtering each resolvent through the discount 335// gate before it lands in unprocessed. 336func nx_sat_try_resolve_pair_filtered(s: *Saturation, given: *Clause, 337 other: *Clause, eq_sym: nx_int) -> nx_int { 338 var i: nx_int = 0 339 while i < given.n_lits { 340 var j: nx_int = 0 341 while j < other.n_lits { 342 let resolvent: *Clause = nx_clause_new() 343 let r: *NxResult = nx_resolve(given, i, other, j, resolvent) 344 if nx_result_is_ok(r) == 1 { 345 if nx_clause_is_empty(resolvent) == 1 { return NX_SAT_VERDICT_UNSAT } 346 let _add: nx_int = nx_sat_add_unproc_filtered(s, resolvent, eq_sym) 347 } 348 j = j + 1 349 } 350 i = i + 1 351 } 352 return NX_SAT_VERDICT_UNKNOWN 353} 354 355// Backward subsumption: remove every processed clause that the 356// freshly-added clause `newest` subsumes. Marks subsumed slots 357// with proc_deleted=1 (tombstones) instead of array compaction. 358// Tombstoning preserves clause indices so the discrim tree's stored 359// values remain valid -- no rebuild required, eliminating the 360// O(n_processed) hot-loop step that blew up qemu memory on 361// pel012-class problems. Iteration over processed[] elsewhere 362// must skip slots where proc_deleted == 1. 363// 364// Closes Phase 1's deferred backward-simplification axis. Combined 365// with forward subsumption, this is the two-sided pruning Vampire 366// uses to keep the processed set minimal. 367func nx_sat_backward_subsume(s: *Saturation, newest: *Clause) -> nx_int { 368 var removed: nx_int = 0 369 var i: nx_int = 0 370 while i < s.n_processed { 371 if s.proc_deleted[i] == 0 { 372 let other: *Clause = nx_sat_proc_at(s, i) 373 // Don't subsume `newest` against itself. 374 if (other as nx_int) != (newest as nx_int) { 375 if nx_subsumes(newest, other) == NX_SUBSUMES_YES { 376 s.proc_deleted[i] = 1 377 // Also delete this clause's discrim-tree entries so 378 // the index doesn't grow monotonically with 379 // tombstoned values. Removes the OOM that pel012- 380 // class (deeply-Tseitined) problems hit otherwise. 381 nx_dt_delete_value(s.proc_index, i) 382 removed = removed + 1 383 } 384 } 385 } 386 i = i + 1 387 } 388 return removed 389} 390 391// ===== Discrim-tree-backed forward subsumption ==================== 392// Insert a clause's literal atoms into proc_index. Each literal's 393// atom is indexed with the given clause_idx as its associated value; 394// duplicate literals (same atom) just create extra entries -- dedup 395// happens at lookup time via the seen[] bitmap. 396// 397// Caller invokes this AFTER nx_sat_move_to_processed (clause_idx = 398// s.n_processed - 1). The integration into nx_sat_run_discount is a 399// separate refactor; this primitive ships standalone for now. 400func nx_sat_index_clause(s: *Saturation, clause_idx: nx_int) { 401 if clause_idx < 0 { return } 402 if clause_idx >= s.n_processed { return } 403 let c: *Clause = nx_sat_proc_at(s, clause_idx) 404 var i: nx_int = 0 405 while i < c.n_lits { 406 let l: *Literal = nx_clause_lit_at(c, i) 407 nx_dt_insert(s.proc_index, l.atom, clause_idx) 408 i = i + 1 409 } 410} 411 412// Indexed forward-subsumption check: query proc_index with c[0]'s atom 413// to get a candidate set of processed clauses, dedup, then verify each 414// candidate via the full nx_subsumes check. Returns 1 if any 415// processed clause subsumes c, else 0. Same semantic answer as the 416// linear nx_sat_proc_subsumes, with O(d) lookup vs O(n_processed) 417// scan. 418// 419// Pre-condition: nx_sat_index_clause has been called for every clause 420// currently in processed[]. Backward-simp invalidation is the caller's 421// responsibility (rebuild the index after compacting processed if you 422// want to keep this primitive sound under that pattern). 423func nx_sat_proc_subsumes_indexed(s: *Saturation, c: *Clause) -> nx_int { 424 if c.n_lits == 0 { return 0 } 425 let candidates: *nx_int = (sys_mmap((NX_DT_MAX_RESULTS * 8) as i64)) as *nx_int 426 let n_cand_p: *nx_int = (sys_mmap(8)) as *nx_int 427 n_cand_p[0] = 0 428 let first: *Literal = nx_clause_lit_at(c, 0) 429 nx_dt_find_generalizations(s.proc_index, first.atom, candidates, n_cand_p) 430 431 // Dedup via a fixed bitmap (size NX_SAT_MAX_PROCESSED). Skip 432 // tombstoned (proc_deleted=1) candidates -- the discrim tree may 433 // still hold their entries since we don't delete on tombstone, 434 // but they're no longer live. 435 let seen: *nx_int = (sys_mmap((NX_SAT_MAX_PROCESSED * 8) as i64)) as *nx_int 436 var i: nx_int = 0 437 while i < n_cand_p[0] { 438 let idx: nx_int = candidates[i] 439 if idx >= 0 { 440 if idx < NX_SAT_MAX_PROCESSED { 441 if seen[idx] == 0 { 442 seen[idx] = 1 443 if s.proc_deleted[idx] == 0 { 444 let d: *Clause = nx_sat_proc_at(s, idx) 445 if nx_subsumes(d, c) == NX_SUBSUMES_YES { return 1 } 446 } 447 } 448 } 449 } 450 i = i + 1 451 } 452 return 0 453} 454 455// ===== Clause weight + best-first picking ========================= 456// Symbolic weight of a term: 1 + sum of weights of children. Variables 457// count as 1. Total clause weight = sum over literals. Used as a 458// best-first heuristic for picking from the passive set -- lighter 459// clauses are typically more general and faster to process. 460func nx_clause_weight_term(t: *Term) -> nx_int { 461 if t.kind == NX_TERM_VAR { return 1 } 462 if t.kind == NX_TERM_CONST { return 1 } 463 var w: nx_int = 1 464 var i: nx_int = 0 465 while i < t.n_args { 466 w = w + nx_clause_weight_term(nx_term_arg(t, i)) 467 i = i + 1 468 } 469 return w 470} 471 472func nx_clause_weight(c: *Clause) -> nx_int { 473 var w: nx_int = 0 474 var i: nx_int = 0 475 while i < c.n_lits { 476 let l: *Literal = nx_clause_lit_at(c, i) 477 w = w + nx_clause_weight_term(l.atom) 478 i = i + 1 479 } 480 return w 481} 482 483// Pick the lightest unpicked unprocessed clause. Marks it picked so 484// the next call won't see it again. Returns null if all consumed. 485// 486// O(n_unproc) per call -- a real heap would amortize but the linear 487// scan is acceptable for CASC-Easy problem sizes. Caller uses this 488// instead of (not in addition to) nx_sat_pick_given. 489func nx_sat_pick_given_best_first(s: *Saturation) -> *Clause { 490 var best: nx_int = 0 - 1 491 var best_w: nx_int = NX_MAGIC_9223372036854775807 // i64 max 492 var i: nx_int = 0 493 while i < s.n_unproc { 494 if s.picked[i] == 0 { 495 let c: *Clause = nx_sat_unproc_at(s, i) 496 let w: nx_int = nx_clause_weight(c) 497 if w < best_w { best_w = w; best = i } 498 } 499 i = i + 1 500 } 501 if best < 0 { return 0 as *Clause } 502 s.picked[best] = 1 503 return nx_sat_unproc_at(s, best) 504} 505 506// Pick the oldest unpicked unprocessed clause (FIFO over picked set). 507// Used as the "age" half of the LRS picker. 508func nx_sat_pick_given_oldest_unpicked(s: *Saturation) -> *Clause { 509 var i: nx_int = 0 510 while i < s.n_unproc { 511 if s.picked[i] == 0 { 512 s.picked[i] = 1 513 return nx_sat_unproc_at(s, i) 514 } 515 i = i + 1 516 } 517 return 0 as *Clause 518} 519 520// LRS (Limited Resource Strategy) picker -- Vampire's signature. 521// Alternates between weight-based (lightest unpicked) and age-based 522// (oldest unpicked) picks per a counter modulo (ratio + 1). 523// 524// counter == 0 (mod ratio+1) -> age-based pick 525// otherwise -> weight-based pick 526// 527// ratio=1: alternates 1:1 (light, age, light, age, ...) 528// ratio=5: 5 light then 1 age repeating (more aggressive best-first) 529// 530// Caller-supplied counter so the strategy works without growing the 531// Saturation struct further. 532func nx_sat_pick_given_lrs(s: *Saturation, counter: nx_int, ratio: nx_int) -> *Clause { 533 let div: nx_int = ratio + 1 534 let phase: nx_int = counter - ((counter / div) * div) 535 if phase == 0 { return nx_sat_pick_given_oldest_unpicked(s) } 536 return nx_sat_pick_given_best_first(s) 537} 538 539// LRS variant of the discount loop. Uses LRS picker; otherwise 540// identical pruning + inference paths. 541func nx_sat_run_discount_lrs(s: *Saturation, eq_sym: nx_int, ratio: nx_int) -> nx_int { 542 var counter: nx_int = 0 543 while s.budget > 0 { 544 let given: *Clause = nx_sat_pick_given_lrs(s, counter, ratio) 545 if (given as nx_int) == 0 { return NX_SAT_VERDICT_UNKNOWN } 546 counter = counter + 1 547 548 if nx_is_tautology(given, eq_sym) == NX_TAUTOLOGY { 549 s.budget = s.budget - 1 550 continue 551 } 552 if nx_sat_proc_subsumes_indexed(s, given) == 1 { 553 s.budget = s.budget - 1 554 continue 555 } 556 557 let v_self: nx_int = nx_sat_try_resolve_pair_filtered(s, given, given, eq_sym) 558 if v_self == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 559 560 var p: nx_int = 0 561 while p < s.n_processed { 562 if s.proc_deleted[p] == 0 { 563 let other: *Clause = nx_sat_proc_at(s, p) 564 let v: nx_int = nx_sat_try_resolve_pair_filtered(s, given, other, eq_sym) 565 if v == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 566 let vp1: nx_int = nx_sat_try_paramodulate_pair_filtered(s, given, other, eq_sym) 567 if vp1 == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 568 let vp2: nx_int = nx_sat_try_paramodulate_pair_filtered(s, other, given, eq_sym) 569 if vp2 == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 570 } 571 p = p + 1 572 } 573 574 let _: *NxResult = nx_sat_move_to_processed(s, given) 575 nx_sat_index_clause(s, s.n_processed - 1) 576 // Backward subsume tombstones removed slots (no compaction); 577 // discrim tree stays valid -- no rebuild needed. The 578 // tombstone path is O(removed) instead of O(n_processed). 579 let _bk: nx_int = nx_sat_backward_subsume(s, nx_sat_proc_at(s, s.n_processed - 1)) 580 s.budget = s.budget - 1 581 } 582 return NX_SAT_VERDICT_UNKNOWN 583} 584 585// Rebuild proc_index from scratch. Kept as a utility for callers 586// that want a fresh index after manual processed-array manipulation 587// outside the discount loop. Internal callers (the loops above) use 588// the tombstone path instead. 589func nx_sat_rebuild_index(s: *Saturation) { 590 s.proc_index = nx_dt_new() 591 var i: nx_int = 0 592 while i < s.n_processed { 593 if s.proc_deleted[i] == 0 { 594 nx_sat_index_clause(s, i) 595 } 596 i = i + 1 597 } 598} 599 600// Discount-loop entry: gate given itself + each new resolvent through 601// tautology + forward subsumption. After moving given to processed, 602// run backward subsumption so any older now-redundant clauses are 603// dropped immediately. 604// 605// Forward subsumption uses the discrim-tree-backed lookup 606// (nx_sat_proc_subsumes_indexed); proc_index is updated after every 607// move_to_processed and rebuilt after any backward-simp removal so 608// indexed lookups stay sound. 609func nx_sat_run_discount(s: *Saturation, eq_sym: nx_int) -> nx_int { 610 while s.budget > 0 { 611 let given: *Clause = nx_sat_pick_given(s) 612 if (given as nx_int) == 0 { return NX_SAT_VERDICT_UNKNOWN } 613 614 // Forward-prune given itself. If pruned, charge a step and skip 615 // the inference work -- still consumes budget so we don't loop 616 // forever on a queue full of tautologies. 617 if nx_is_tautology(given, eq_sym) == NX_TAUTOLOGY { 618 s.budget = s.budget - 1 619 continue 620 } 621 if nx_sat_proc_subsumes_indexed(s, given) == 1 { 622 s.budget = s.budget - 1 623 continue 624 } 625 626 // Self-resolve, then resolve against each processed clause. 627 let v_self: nx_int = nx_sat_try_resolve_pair_filtered(s, given, given, eq_sym) 628 if v_self == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 629 630 var p: nx_int = 0 631 while p < s.n_processed { 632 if s.proc_deleted[p] == 0 { 633 let other: *Clause = nx_sat_proc_at(s, p) 634 let v: nx_int = nx_sat_try_resolve_pair_filtered(s, given, other, eq_sym) 635 if v == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 636 637 // Paramodulation: try given as eq-source into other, AND 638 // other as eq-source into given. Both directions because 639 // the discount loop fires given against existing actives, 640 // and equality rewriting may apply either way. 641 let vp1: nx_int = nx_sat_try_paramodulate_pair_filtered(s, given, other, eq_sym) 642 if vp1 == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 643 let vp2: nx_int = nx_sat_try_paramodulate_pair_filtered(s, other, given, eq_sym) 644 if vp2 == NX_SAT_VERDICT_UNSAT { return NX_SAT_VERDICT_UNSAT } 645 } 646 p = p + 1 647 } 648 649 let _: *NxResult = nx_sat_move_to_processed(s, given) 650 // Index the freshly-added clause for future indexed lookups. 651 nx_sat_index_clause(s, s.n_processed - 1) 652 653 // Backward simplification: tombstones old processed clauses 654 // that `given` subsumes (no array compaction). Discrim tree 655 // stays valid; no rebuild needed. 656 let _bk: nx_int = nx_sat_backward_subsume(s, nx_sat_proc_at(s, s.n_processed - 1)) 657 658 s.budget = s.budget - 1 659 } 660 return NX_SAT_VERDICT_UNKNOWN 661}