code wiki / (root) / nx_unify.nx

nx_unify.nx

buildroot/runtime/nx_unify.nx

9248 B257 linesdepth 4pulls 4 transitivereach 208 importersview sourcekind library
docsdependenciesstructsconstsfunctions

about

nx_unify.nx -- first-order terms + Robinson unification. Per user 2026-05-14 "keep going" + the CASC-leap cardinal: this is the bits-up unification primitive every CASC entrant (Vampire/E/ Otter/Waldmeister/SPASS/SETHEO) builds on. Robinson 1965 algorithm. Term kinds (sealed): VAR identified by integer var_id CONST identified by integer symbol_id (constant or 0-arity fn) APP function symbol_id + n_args + array of child Terms Substitution = parallel arrays of (var_id, term) bindings. Result-typed throughout: no -1 sentinels, no null-as-error. nx_safety_envelope: intended_use: "Robinson unification -- substitution computation for first-order theorem prover + type inference + pattern matching" sil_target: SIL2 (unification correctness gates every consumer's soundness) asil_target: QM dal_target: DAL B evidence: [Robinson_1965_canonical_basis, occurs_check_enabled, Result_typed_no_sentinel, sealed_unification_error_enum] hazard_register: [bug-tape-unification-without-occurs-check, bug-tape-exponential-substitution-blowup, bug-tape-cycle-in-mgu-not-detected] residual_risk: "Occurs-check is ENFORCED. Substrate documents O(n^2) worst-case without sharing; Martelli-Montanari O(n) variant queued for performance-critical paths." verdict: NOT_YET_EVALUATED

dependencies 4 imports · 74 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_result.nx nx_unify.nx nx_answer.nx nx_answer_test.nx nx_avatar_encode.nx nx_avatar_encode_test.nx nx_avatar_solve_test.nx nx_avatar_split.nx nx_avatar_split_test.nx nx_backward_subsume_test.nx nx_casc_bench.nx nx_casc_runner_test.nx

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

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nx

imported by: nx_answer.nxnx_answer_test.nxnx_avatar_encode.nxnx_avatar_encode_test.nxnx_avatar_solve_test.nxnx_avatar_split.nxnx_avatar_split_test.nxnx_backward_subsume_test.nxnx_casc_bench.nxnx_casc_runner_test.nxnx_clause_components.nxnx_clause_components_test.nxnx_clause_weight_test.nxnx_demodulation.nxnx_demodulation_test.nxnx_discount_test.nxnx_disctree.nxnx_disctree_test.nxnx_eq_factor.nxnx_eq_factor_test.nxnx_fmb.nxnx_fmb_test.nxnx_fof.nxnx_fof_cnf.nxnx_fof_cnf_test.nxnx_fof_parse.nxnx_fof_parse_test.nxnx_fof_tseitin.nxnx_fof_tseitin_test.nxnx_hyperres.nxnx_hyperres_test.nxnx_indexed_subsume_test.nxnx_inst_gen.nxnx_inst_gen_test.nxnx_kernel_v2.nxnx_kernel_v2_test.nxnx_lpo.nxnx_lpo_test.nxnx_paramodulation.nxnx_paramodulation_test.nxnx_pre_sat.nxnx_pre_sat_test.nxnx_proof_sqrt2_v2.nxnx_proof_sqrt2_v3.nxnx_pure_lit.nxnx_pure_lit_test.nxnx_resolution.nxnx_resolution_test.nxnx_saturation.nxnx_saturation_test.nxnx_selection.nxnx_selection_test.nxnx_sine.nxnx_sine_test.nxnx_solve.nxnx_solve_test.nxnx_subsumption.nxnx_subsumption_test.nxnx_tautology.nxnx_tautology_test.nxnx_term_order.nxnx_term_order_test.nxnx_tptp_emit.nxnx_tptp_emit_test.nxnx_tptp_formula.nxnx_tptp_formula_test.nxnx_tptp_load.nxnx_tptp_load_any.nxnx_tptp_load_test.nxnx_tptp_term.nxnx_tptp_write_test.nxnx_tstp_emit.nxnx_tstp_emit_test.nxnx_unify_test.nx

structs

46struct Term
118struct Subst

consts

41const NX_TERM_VAR: nx_int = 1
42const NX_TERM_CONST: nx_int = 2
43const NX_TERM_APP: nx_int = 3
53const NX_TERM_BYTES: nx_int = 32
116const NX_SUBST_MAX_BINDINGS: nx_int = 256
124const NX_SUBST_BYTES: nx_int = 24

functions

55func nx_term_var(var_id: nx_int) -> *Term
called by 23: nx_calc_varnx_calc_xt3_subst_vart5_maclaurin_x2t2_integrate_xt3_integrate_power+17 calls 1: sys_mmap
64func nx_term_const(sym_id: nx_int) -> *Term
called by 50: nx_arith_zeronx_calc_unknownmainmainmainnx_fmb_subst_term+44 calls 1: sys_mmap
73func nx_term_app(sym_id: nx_int, n_args: nx_int, args: *Term) -> *Term
called by 87: nx_answer_litmk_p_varmk_p_constnx_arith_succnx_arith_plusnx_arith_mult+81 calls 1: sys_mmap
83func nx_term_arg(t: *Term, i: nx_int) -> *Term
called by 62: nx_clause_extract_answernx_calc_derivt3_subst_vart2_integrate_xt4_integrate_sinnx_calc_integrate+56
88func nx_term_eq(a: *Term, b: *Term) -> nx_int
called by 30: nx_proof_ctx_lookupaf_decidenx_fmb_prop_idnx_k2_hyps_containsnx_k2_hyps_removenx_k2_eq_trans+24 calls 2: nx_term_eqnx_term_arg
101func nx_term_contains_var(t: *Term, var_id: nx_int) -> nx_int
called by 3: nx_lpo_comparenx_term_contains_varnx_unify calls 2: nx_term_contains_varnx_term_arg
126func nx_subst_new() -> *Subst
called by 9: nx_demodulate_termnx_eq_factornx_hyperresolvenx_inst_gennx_paramodulatenx_resolve+3 calls 1: sys_mmap
135func nx_subst_lookup(s: *Subst, var_id: nx_int) -> *Term
called by 3: nx_subst_applynx_matchmain
147func nx_subst_add(s: *Subst, var_id: nx_int, t: *Term) -> *NxResult
called by 2: nx_unifynx_match calls 2: nx_result_errnx_result_ok
160func nx_subst_apply(t: *Term, s: *Subst) -> *Term
called by 6: nx_demodulate_termnx_eq_factornx_paramod_walknx_lit_apply_substnx_subst_applynx_unify calls 5: nx_subst_lookupnx_subst_applysys_mmapnx_term_argnx_term_app
188func nx_unify(t1: *Term, t2: *Term, s: *Subst) -> *NxResult
called by 8: nx_eq_factornx_hyperresolvenx_inst_gennx_paramod_walknx_resolvenx_factor+2 calls 9: nx_subst_applynx_term_eqnx_result_oknx_term_contains_varnx_result_errnx_subst_add+3
232func nx_match(pattern: *Term, term: *Term, s: *Subst) -> *NxResult
called by 3: nx_demodulate_termnx_subsumes_fromnx_match calls 8: nx_subst_lookupnx_term_eqnx_result_oknx_result_errnx_subst_addnx_match+2