nx_fof_cnf.nx
buildroot/runtime/nx_fof_cnf.nx
about
nx_fof_cnf.nx -- FOF -> CNF conversion pipeline.
Per Vampire-displacement roadmap Phase 2. Closes the FOF axis end-
to-end: a parsed *Fof tree (from nx_fof_parse) becomes an array of
*Clause that the saturation loop can consume. Required for the
CASC FOF division -- competition problems are stated in FOF and
must be CNF-converted before resolution + paramodulation can fire.
Standard pipeline:
1. eliminate IFF A<=>B => (A=>B) & (B=>A)
2. eliminate IMP A=>B => ~A | B
3. NNF (push NEG) ~~A=>A; De Morgan; swap quantifiers
4. Skolemize ?[X]:F => F[X := sk_N(U_1..U_k)] where U_i
are the universal vars in scope
5. drop FORALL all remaining vars become implicitly free
6. distribute & / | A|(B&C) => (A|B)&(A|C) (may iterate)
7. extract clauses AND-of-OR-of-literals -> array of *Clause
Each pipeline stage is a pure function -- callers can inspect
intermediate forms. Top-level entry nx_fof_to_cnf chains them.
dependencies 8 imports · 4 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nxnx_resolution.nxnx_tptp_symtab.nxnx_fof.nx
imported by: nx_casc_runner_test.nxnx_fof_cnf_test.nxnx_fof_tseitin_test.nxnx_tptp_load_any.nx
structs
| none |
consts
| 40 | const NX_TPTP_SK_BASE: nx_int = 900000 |
| 208 | const NX_FOF_SK_MAX_UNIV: nx_int = 64 |
functions
| 44 | func nx_fof_elim_iff(f: *Fof) -> *Fof |
| 69 | func nx_fof_elim_imp(f: *Fof) -> *Fof |
| 97 | func nx_fof_to_nnf(f: *Fof) -> *Fof |
| 146 | func nx_term_subst_var(t: *Term, var_id: nx_int, replacement: *Term) -> *Term called by 2: nx_term_subst_varnx_fof_subst_var calls 4: sys_mmapnx_term_argnx_term_subst_varnx_term_app |
| 177 | func nx_fof_subst_var(f: *Fof, var_id: nx_int, replacement: *Term) -> *Fof |
| 210 | func nx_fof_skolem_walk(f: *Fof, univ_vars: *nx_int, n_univ: nx_int, |
| 262 | func nx_fof_skolemize(f: *Fof) -> *Fof called by 4: nx_fof_to_cnfnx_fof_to_nnf_quantifier_freemainparse_to_nnf calls 2: sys_mmapnx_fof_skolem_walk |
| 273 | func nx_fof_drop_forall(f: *Fof) -> *Fof |
| 292 | func nx_fof_distribute_step(f: *Fof) -> *Fof called by 3: nx_fof_distribute_stepnx_fof_to_cnfmain calls 3: nx_fof_negnx_fof_distribute_stepnx_fof_binary |
| 322 | func nx_fof_collect_lits(f: *Fof, c: *Clause) -> nx_int called by 2: nx_fof_collect_litsnx_fof_extract_clauses calls 3: nx_fof_collect_litsnx_clause_addnx_lit_make |
| 342 | func nx_fof_extract_clauses(f: *Fof, out_clauses: *Clause, out_n: *nx_int, called by 2: nx_fof_extract_clausesnx_fof_to_cnf calls 3: nx_fof_extract_clausesnx_clause_newnx_fof_collect_lits |
| 363 | func nx_fof_to_cnf(f: *Fof, out_clauses: *Clause, out_n: *nx_int, |
| 384 | func nx_fof_to_nnf_quantifier_free(f: *Fof) -> *Fof |
| 395 | func nx_fof_count_iff_imp(f: *Fof) -> nx_int |