nx_tptp_formula.nx source
↩ module page · 158 lines · 6289 B
1// nx_tptp_formula.nx -- TPTP CNF formula body parser.
2//
3// Per Vampire-displacement roadmap Phase 1.6: closes the BLOCKED axis
4// from the CASC bench harness. Reads a TPTP CNF formula body and
5// emits a *Clause ready for the saturation loop.
6//
7// Grammar handled (TPTP CNF subset):
8// clause ::= [ "(" ] literal { "|" literal } [ ")" ]
9// literal ::= [ "~" ] atom
10// atom ::= predicate-application
11// | term "=" term (equality)
12// | term "!=" term (inequality)
13// term ::= delegated to nx_tptp_term
14//
15// Equality is mapped to a caller-supplied eq_sym (a normal binary
16// predicate sym_id reserved for "="). Inequality literal flips the
17// sign of the surrounding literal.
18//
19// Bits-up parsing. Returns null on parse failure (the smoke test
20// covers both the success and failure paths).
21//
22// FOF (quantifiers, &, =>, <=>, etc.) is Phase 2 -- CNF alone is
23// what the CASC FOF division accepts after a TPTP-tooled CNF
24// transformation, and is what TPTP-Easy provides directly.
25
26// nx_safety_envelope:
27// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
28// sil_target: SIL1
29// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
30// verdict: NOT_YET_EVALUATED
31
32import "nx_syscalls.nx"
33import "nx_runtime.nx"
34import "nx_tier.nx"
35import "nx_str.nx"
36import "nx_result.nx"
37import "nx_unify.nx"
38import "nx_resolution.nx"
39import "nx_tptp_symtab.nx"
40import "nx_tptp_term.nx"
41
42// Note: this module calls nx_tptp_term_skip_ws directly rather than via
43// a fml_skip_ws wrapper. An earlier codegen bug in nxc2 riscv.c
44// emit_call corrupted caller state across void function calls (emitted
45// `sd a0, -1(sp)`); the bug is fixed in nxc2 (2026-05-15) but the
46// inlined call sites are kept since the wrapper added no value.
47
48// Parse one literal -- returns *Literal or null on failure.
49func nx_tptp_parse_literal(buf: *u8, n: nx_int, pos: *nx_int,
50 symtab: *TptpSymtab, eq_sym: nx_int) -> *Literal {
51 nx_tptp_term_skip_ws(buf, n, pos)
52 if pos[0] >= n { return 0 as *Literal }
53
54 var sign: nx_int = NX_LIT_POS
55 let c: nx_int = buf[pos[0]] as nx_int
56 if c == 126 { // '~' -- negation
57 sign = NX_LIT_NEG
58 pos[0] = pos[0] + 1
59 nx_tptp_term_skip_ws(buf, n, pos)
60 }
61
62 let t1: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
63 if (t1 as nx_int) == 0 { return 0 as *Literal }
64
65 nx_tptp_term_skip_ws(buf, n, pos)
66 if pos[0] >= n { return nx_lit_make(sign, t1) }
67
68 let next_c: nx_int = buf[pos[0]] as nx_int
69
70 // Equality: t1 = t2
71 if next_c == 61 { // '='
72 pos[0] = pos[0] + 1
73 let t2: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
74 if (t2 as nx_int) == 0 { return 0 as *Literal }
75 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
76 let a0: *Term = args
77 a0.kind = t1.kind; a0.sym = t1.sym; a0.n_args = t1.n_args; a0.args = t1.args
78 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
79 a1.kind = t2.kind; a1.sym = t2.sym; a1.n_args = t2.n_args; a1.args = t2.args
80 let eq_atom: *Term = nx_term_app(eq_sym, 2, args)
81 return nx_lit_make(sign, eq_atom)
82 }
83
84 // Inequality: t1 != t2 -- flips the literal sign
85 if next_c == 33 { // '!'
86 if (pos[0] + 1) >= n { return 0 as *Literal }
87 let after: nx_int = buf[pos[0] + 1] as nx_int
88 if after != 61 { return 0 as *Literal } // need '!='
89 pos[0] = pos[0] + 2
90 let t2b: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
91 if (t2b as nx_int) == 0 { return 0 as *Literal }
92 let args2: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
93 let b0: *Term = args2
94 b0.kind = t1.kind; b0.sym = t1.sym; b0.n_args = t1.n_args; b0.args = t1.args
95 let b1: *Term = ((args2 as nx_int) + NX_TERM_BYTES) as *Term
96 b1.kind = t2b.kind; b1.sym = t2b.sym; b1.n_args = t2b.n_args; b1.args = t2b.args
97 let neq_atom: *Term = nx_term_app(eq_sym, 2, args2)
98 // Flip sign: != means NOT equal
99 var flipped: nx_int = NX_LIT_POS
100 if sign == NX_LIT_POS { flipped = NX_LIT_NEG }
101 return nx_lit_make(flipped, neq_atom)
102 }
103
104 // Otherwise t1 is the atom itself.
105 return nx_lit_make(sign, t1)
106}
107
108// Parse a CNF clause body (disjunction of literals). Allows an
109// optional outer "( ... )" wrapper. Returns null on failure.
110//
111// Caller MUST call nx_tptp_symtab_reset_vars(symtab) before calling
112// per CNF clause: TPTP variables are clause-local.
113func nx_tptp_parse_cnf_clause(buf: *u8, n: nx_int, pos: *nx_int,
114 symtab: *TptpSymtab, eq_sym: nx_int) -> *Clause {
115 nx_tptp_term_skip_ws(buf, n, pos)
116 if pos[0] >= n { return 0 as *Clause }
117
118 // Optional outer parens
119 var consumed_paren: nx_int = 0
120 let leadc: nx_int = buf[pos[0]] as nx_int
121 if leadc == 40 { // '('
122 pos[0] = pos[0] + 1
123 consumed_paren = 1
124 nx_tptp_term_skip_ws(buf, n, pos)
125 }
126
127 let c: *Clause = nx_clause_new()
128
129 // First literal (mandatory)
130 let l1: *Literal = nx_tptp_parse_literal(buf, n, pos, symtab, eq_sym)
131 if (l1 as nx_int) == 0 { return 0 as *Clause }
132 let _r1: *NxResult = nx_clause_add(c, l1)
133
134 // Subsequent literals separated by '|'
135 var done: nx_int = 0
136 while done == 0 {
137 nx_tptp_term_skip_ws(buf, n, pos)
138 if pos[0] >= n { done = 1 }
139 if done == 0 {
140 let nc: nx_int = buf[pos[0]] as nx_int
141 if nc == 124 { // '|'
142 pos[0] = pos[0] + 1
143 let lk: *Literal = nx_tptp_parse_literal(buf, n, pos, symtab, eq_sym)
144 if (lk as nx_int) == 0 { return 0 as *Clause }
145 let _rk: *NxResult = nx_clause_add(c, lk)
146 }
147 if nc != 124 { done = 1 }
148 }
149 }
150
151 if consumed_paren == 1 {
152 nx_tptp_term_skip_ws(buf, n, pos)
153 if pos[0] >= n { return 0 as *Clause }
154 if buf[pos[0]] != 41 { return 0 as *Clause } // expect ')'
155 pos[0] = pos[0] + 1
156 }
157 return c
158}