nx_fof.nx
buildroot/runtime/nx_fof.nx
about
nx_fof.nx -- TPTP FOF (First-Order Form) formula tree.
Per Vampire-displacement roadmap Phase 2. CNF (already shipped via
nx_tptp_formula.nx) covers conjunctive-normal-form clauses; FOF is
the richer language with explicit quantifiers (forall, exists) and
the full connective set (&, |, =>, <=>, ~). The CASC FOF division
uses FOF directly; problems must be CNF-converted (Skolemize +
distribute) before saturation, but the parser produces the FOF
tree as a separate primitive so callers can inspect, transform,
and convert at their leisure.
Sealed kind enum. Each node holds the operator + 1-2 child Fof
pointers + (for quantified nodes) a bound-variable id from the
shared TptpSymtab.
dependencies 5 imports · 8 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_result.nxnx_unify.nx
imported by: nx_casc_runner_test.nxnx_fof_cnf.nxnx_fof_cnf_test.nxnx_fof_parse.nxnx_fof_parse_test.nxnx_fof_tseitin.nxnx_fof_tseitin_test.nxnx_tptp_load_any.nx
structs
| 38 | struct Fof |
consts
| 29 | const NX_FOF_ATOM: nx_int = 1 |
| 30 | const NX_FOF_NEG: nx_int = 2 |
| 31 | const NX_FOF_AND: nx_int = 3 |
| 32 | const NX_FOF_OR: nx_int = 4 |
| 33 | const NX_FOF_IMP: nx_int = 5 // a => b |
| 34 | const NX_FOF_IFF: nx_int = 6 // a <=> b |
| 35 | const NX_FOF_FORALL: nx_int = 7 // ![X]: a |
| 36 | const NX_FOF_EXISTS: nx_int = 8 // ?[X]: a |
| 46 | const NX_FOF_BYTES: nx_int = 40 |
functions
| 49 | func nx_fof_atom(a: *Term) -> *Fof |
| 59 | func nx_fof_neg(child: *Fof) -> *Fof |
| 69 | func nx_fof_binary(kind: nx_int, l: *Fof, r: *Fof) -> *Fof called by 11: nx_fof_elim_iffnx_fof_elim_impnx_fof_to_nnfnx_fof_subst_varnx_fof_skolem_walknx_fof_drop_forall+5 calls 1: sys_mmap |
| 79 | func nx_fof_quantified(kind: nx_int, var_id: nx_int, body: *Fof) -> *Fof |
| 90 | func nx_fof_kind_name(k: nx_int) -> *u8 called by 1: report |