code wiki / (root) / nx_saturation.nx

nx_saturation.nx

buildroot/runtime/nx_saturation.nx

27486 B661 linesdepth 7pulls 10 transitivereach 15 importersview sourcekind library
docsdependenciesstructsconstsfunctions

about

nx_saturation.nx -- given-clause saturation loop with factoring. Per user 2026-05-14 "keep going till we can submit to casc". This is the proof-search engine on top of unify + resolution. Given a set of clauses (typically the negation of a conjecture), iterate resolution + factoring until either: - the empty clause is derived -> UNSAT (proof of original conjecture) - no new clauses can be derived -> UNKNOWN / SAT - resource budget exhausted -> TIMEOUT Discovery-Otter-Vampire-E-SPASS use this same skeleton; their performance differences come from clause selection heuristic + indexing + subsumption.

dependencies 10 imports · 15 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_result.nx nx_unify.nx nx_resolution.nx nx_subsumption.nx nx_tautology.nx nx_disctree.nx nx_paramodulation.nx nx_saturation.nx nx_avatar_solve_test.nx nx_backward_subsume_test.nx nx_casc_bench.nx nx_casc_runner_test.nx nx_clause_weight_test.nx nx_discount_test.nx nx_fof_cnf_test.nx nx_fof_tseitin_test.nx nx_indexed_subsume_test.nx nx_saturation_test.nx

diagram shows first 10 each side; +0 more imports, +5 more importers in the complete lists below.

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nxnx_resolution.nxnx_subsumption.nxnx_tautology.nxnx_disctree.nxnx_paramodulation.nx

imported by: nx_avatar_solve_test.nxnx_backward_subsume_test.nxnx_casc_bench.nxnx_casc_runner_test.nxnx_clause_weight_test.nxnx_discount_test.nxnx_fof_cnf_test.nxnx_fof_tseitin_test.nxnx_indexed_subsume_test.nxnx_saturation_test.nxnx_solve.nxnx_solve_test.nxnx_tptp_formula_test.nxnx_tptp_load_test.nxnx_tptp_write_test.nx

structs

83struct Saturation

consts

31const NX_MAGIC_9223372036854775807: i64 = 9223372036854775807
80const NX_SAT_MAX_PROCESSED: nx_int = 256
81const NX_SAT_MAX_UNPROCESSED: nx_int = 1024
104const NX_SAT_BYTES: nx_int = 72
170const NX_SAT_VERDICT_UNSAT: nx_int = 2
171const NX_SAT_VERDICT_UNKNOWN: nx_int = 5

functions

39func nx_factor(c: *Clause, i: nx_int, j: nx_int, c_out: *Clause) -> *NxResult
called by 1: main calls 8: nx_result_errnx_clause_lit_atnx_subst_newnx_unifynx_result_is_errnx_lit_apply_subst+2
106func nx_saturation_new(initial_budget: nx_int) -> *Saturation
called by 15: mainmainrun_problemrun_problemmainmain+9 calls 2: sys_mmapnx_dt_new
125func nx_sat_proc_subsumes_indexed(s: *Saturation, c: *Clause) -> nx_int;
called by 3: nx_sat_add_unproc_filterednx_sat_run_discount_lrsnx_sat_run_discount
128func nx_sat_rebuild_index(s: *Saturation);
131func nx_sat_unproc_at(s: *Saturation, i: nx_int) -> *Clause
called by 4: nx_sat_add_unprocnx_sat_pick_givennx_sat_pick_given_best_firstnx_sat_pick_given_oldest_unpicked
135func nx_sat_proc_at(s: *Saturation, i: nx_int) -> *Clause
called by 8: nx_sat_move_to_processednx_sat_runnx_sat_proc_subsumesnx_sat_backward_subsumenx_sat_index_clausenx_sat_proc_subsumes_indexed+2
140func nx_sat_add_unproc(s: *Saturation, c: *Clause) -> *NxResult
called by 18: mainmainmk_p1mk_p2mk_p3run_problem+12 calls 3: nx_result_errnx_sat_unproc_atnx_result_ok
150func nx_sat_pick_given(s: *Saturation) -> *Clause
called by 2: nx_sat_runnx_sat_run_discount calls 1: nx_sat_unproc_at
158func nx_sat_move_to_processed(s: *Saturation, given: *Clause) -> *NxResult
called by 5: mainpushnx_sat_runnx_sat_run_discount_lrsnx_sat_run_discount calls 3: nx_result_errnx_sat_proc_atnx_result_ok
173func nx_sat_try_resolve_pair(s: *Saturation, given: *Clause, other: *Clause) -> nx_int
called by 1: nx_sat_run calls 5: nx_clause_newnx_resolvenx_result_is_oknx_clause_is_emptynx_sat_add_unproc
192func nx_sat_run(s: *Saturation) -> nx_int
called by 3: run_problemmainmain calls 4: nx_sat_pick_givennx_sat_proc_atnx_sat_try_resolve_pairnx_sat_move_to_processed
240func nx_sat_proc_subsumes(s: *Saturation, c: *Clause) -> nx_int
called by 2: comparemain calls 2: nx_sat_proc_atnx_subsumes
255func nx_sat_clause_dedup(c: *Clause) -> *Clause
called by 1: nx_sat_add_unproc_filtered calls 4: nx_clause_newnx_clause_lit_atnx_term_eqnx_clause_add
288func nx_sat_add_unproc_filtered(s: *Saturation, c: *Clause, eq_sym: nx_int) -> nx_int
called by 2: nx_sat_try_paramodulate_pair_filterednx_sat_try_resolve_pair_filtered calls 5: nx_sat_clause_dedupnx_is_tautologynx_sat_proc_subsumes_indexednx_sat_add_unprocnx_result_is_err
302func nx_sat_try_paramodulate_pair_filtered(s: *Saturation, eq_clause: *Clause,
called by 2: nx_sat_run_discount_lrsnx_sat_run_discount calls 6: nx_clause_lit_atnx_clause_newnx_paramodulatenx_result_is_oknx_clause_is_emptynx_sat_add_unproc_filtered
336func nx_sat_try_resolve_pair_filtered(s: *Saturation, given: *Clause,
called by 2: nx_sat_run_discount_lrsnx_sat_run_discount calls 5: nx_clause_newnx_resolvenx_result_is_oknx_clause_is_emptynx_sat_add_unproc_filtered
367func nx_sat_backward_subsume(s: *Saturation, newest: *Clause) -> nx_int
called by 3: mainnx_sat_run_discount_lrsnx_sat_run_discount calls 3: nx_sat_proc_atnx_subsumesnx_dt_delete_value
400func nx_sat_index_clause(s: *Saturation, clause_idx: nx_int)
called by 4: pushnx_sat_run_discount_lrsnx_sat_rebuild_indexnx_sat_run_discount calls 3: nx_sat_proc_atnx_clause_lit_atnx_dt_insert
423func nx_sat_proc_subsumes_indexed(s: *Saturation, c: *Clause) -> nx_int
called by 2: comparemain calls 5: sys_mmapnx_clause_lit_atnx_dt_find_generalizationsnx_sat_proc_atnx_subsumes
460func nx_clause_weight_term(t: *Term) -> nx_int
called by 2: nx_clause_weight_termnx_clause_weight calls 2: nx_clause_weight_termnx_term_arg
472func nx_clause_weight(c: *Clause) -> nx_int
called by 2: mainnx_sat_pick_given_best_first calls 2: nx_clause_lit_atnx_clause_weight_term
489func nx_sat_pick_given_best_first(s: *Saturation) -> *Clause
called by 2: mainnx_sat_pick_given_lrs calls 2: nx_sat_unproc_atnx_clause_weight
508func nx_sat_pick_given_oldest_unpicked(s: *Saturation) -> *Clause
called by 1: nx_sat_pick_given_lrs calls 1: nx_sat_unproc_at
532func nx_sat_pick_given_lrs(s: *Saturation, counter: nx_int, ratio: nx_int) -> *Clause
called by 1: nx_sat_run_discount_lrs calls 2: nx_sat_pick_given_oldest_unpickednx_sat_pick_given_best_first
541func nx_sat_run_discount_lrs(s: *Saturation, eq_sym: nx_int, ratio: nx_int) -> nx_int
called by 1: run_problem calls 9: nx_sat_pick_given_lrsnx_is_tautologynx_sat_proc_subsumes_indexednx_sat_try_resolve_pair_filterednx_sat_proc_atnx_sat_try_paramodulate_pair_filtered+3
589func nx_sat_rebuild_index(s: *Saturation)
calls 2: nx_dt_newnx_sat_index_clause
609func nx_sat_run_discount(s: *Saturation, eq_sym: nx_int) -> nx_int
called by 12: mainmainrun_problemrun_problemmainmain+6 calls 9: nx_sat_pick_givennx_is_tautologynx_sat_proc_subsumes_indexednx_sat_try_resolve_pair_filterednx_sat_proc_atnx_sat_try_paramodulate_pair_filtered+3