nx_fof.nx source
↩ module page · 100 lines · 3452 B
1// nx_fof.nx -- TPTP FOF (First-Order Form) formula tree.
2//
3// Per Vampire-displacement roadmap Phase 2. CNF (already shipped via
4// nx_tptp_formula.nx) covers conjunctive-normal-form clauses; FOF is
5// the richer language with explicit quantifiers (forall, exists) and
6// the full connective set (&, |, =>, <=>, ~). The CASC FOF division
7// uses FOF directly; problems must be CNF-converted (Skolemize +
8// distribute) before saturation, but the parser produces the FOF
9// tree as a separate primitive so callers can inspect, transform,
10// and convert at their leisure.
11//
12// Sealed kind enum. Each node holds the operator + 1-2 child Fof
13// pointers + (for quantified nodes) a bound-variable id from the
14// shared TptpSymtab.
15
16// nx_safety_envelope:
17// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
18// sil_target: SIL1
19// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
20// verdict: NOT_YET_EVALUATED
21
22import "nx_syscalls.nx"
23import "nx_runtime.nx"
24import "nx_tier.nx"
25import "nx_result.nx"
26import "nx_unify.nx"
27
28// ===== Sealed kind ==================================================
29const NX_FOF_ATOM: nx_int = 1
30const NX_FOF_NEG: nx_int = 2
31const NX_FOF_AND: nx_int = 3
32const NX_FOF_OR: nx_int = 4
33const NX_FOF_IMP: nx_int = 5 // a => b
34const NX_FOF_IFF: nx_int = 6 // a <=> b
35const NX_FOF_FORALL: nx_int = 7 // ![X]: a
36const NX_FOF_EXISTS: nx_int = 8 // ?[X]: a
37
38struct Fof {
39 kind: nx_int, // one of NX_FOF_*
40 var_id: nx_int, // bound variable id (FORALL/EXISTS only; -1 otherwise)
41 atom: *Term, // term-side payload (ATOM only; null otherwise)
42 left: *Fof, // left child (binary connectives + quantifiers + NEG)
43 right: *Fof, // right child (binary connectives only; null otherwise)
44}
45
46const NX_FOF_BYTES: nx_int = 40
47
48// ===== Constructors =================================================
49func nx_fof_atom(a: *Term) -> *Fof {
50 let f: *Fof = (sys_mmap(NX_FOF_BYTES as i64)) as *Fof
51 f.kind = NX_FOF_ATOM
52 f.var_id = 0 - 1
53 f.atom = a
54 f.left = 0 as *Fof
55 f.right = 0 as *Fof
56 return f
57}
58
59func nx_fof_neg(child: *Fof) -> *Fof {
60 let f: *Fof = (sys_mmap(NX_FOF_BYTES as i64)) as *Fof
61 f.kind = NX_FOF_NEG
62 f.var_id = 0 - 1
63 f.atom = 0 as *Term
64 f.left = child
65 f.right = 0 as *Fof
66 return f
67}
68
69func nx_fof_binary(kind: nx_int, l: *Fof, r: *Fof) -> *Fof {
70 let f: *Fof = (sys_mmap(NX_FOF_BYTES as i64)) as *Fof
71 f.kind = kind
72 f.var_id = 0 - 1
73 f.atom = 0 as *Term
74 f.left = l
75 f.right = r
76 return f
77}
78
79func nx_fof_quantified(kind: nx_int, var_id: nx_int, body: *Fof) -> *Fof {
80 let f: *Fof = (sys_mmap(NX_FOF_BYTES as i64)) as *Fof
81 f.kind = kind
82 f.var_id = var_id
83 f.atom = 0 as *Term
84 f.left = body
85 f.right = 0 as *Fof
86 return f
87}
88
89// ===== Verdict helpers ==============================================
90func nx_fof_kind_name(k: nx_int) -> *u8 {
91 if k == NX_FOF_ATOM { return "ATOM" as *u8 }
92 if k == NX_FOF_NEG { return "NEG" as *u8 }
93 if k == NX_FOF_AND { return "AND" as *u8 }
94 if k == NX_FOF_OR { return "OR" as *u8 }
95 if k == NX_FOF_IMP { return "IMP" as *u8 }
96 if k == NX_FOF_IFF { return "IFF" as *u8 }
97 if k == NX_FOF_FORALL { return "FORALL" as *u8 }
98 if k == NX_FOF_EXISTS { return "EXISTS" as *u8 }
99 return "?" as *u8
100}