1use nom::bytes::complete::tag;
12use nom::character::complete::{char, i64, line_ending, multispace0, space0, space1, u64};
13use nom::combinator::{consumed, cut, eof, value};
14use nom::error::{context, ContextError, FromExternalError, ParseError};
15use nom::multi::many0_count;
16use nom::sequence::{preceded, terminated};
17use nom::{IResult, Offset};
18use rustc_hash::FxHashSet;
19
20use crate::util::{
21 self, context_loc, eol, fail, fail_with_contexts, line_span, usize, word_span, MAX_CAPACITY,
22};
23use crate::{Circuit, GateKind, Literal, ParseOptions, Problem, Tree, Var, VarSet};
24
25fn problem_line<'a, E: ParseError<&'a [u8]> + ContextError<&'a [u8]>>(
29 input: &'a [u8],
30) -> IResult<&'a [u8], [(&'a [u8], usize); 3], E> {
31 let inner = |input| {
32 let (input, _) = context(
33 "all lines in the preamble must begin with 'c' or 'nnf'",
34 cut(tag("nnf")),
35 )(input)?;
36 let (input, _) = space1(input)?;
37 let (input, num_nodes) = consumed(usize)(input)?;
38 let (input, _) = space1(input)?;
39 let (input, num_edges) = consumed(usize)(input)?;
40 let (input, _) = space1(input)?;
41 let (input, num_inputs) = consumed(usize)(input)?;
42 value([num_nodes, num_edges, num_inputs], line_ending)(input)
43 };
44
45 context_loc(
46 || line_span(input),
47 "problem line must have format 'nnf <#nodes> <#edges> <#inputs>'",
48 cut(inner),
49 )(input)
50}
51
52fn preamble<'a, E>(
60 parse_var_order: bool,
61) -> impl Fn(&'a [u8]) -> IResult<&'a [u8], (VarSet, [(&'a [u8], usize); 3]), E>
62where
63 E: ParseError<&'a [u8]> + ContextError<&'a [u8]> + FromExternalError<&'a [u8], String>,
64{
65 move |mut input| {
66 if parse_var_order {
67 let mut vars = VarSet {
68 len: 0,
69 order: Vec::new(),
70 order_tree: None,
71 names: Vec::new(),
72 };
73
74 let mut max_var_span = [].as_slice(); let mut tree_max_var = ([].as_slice(), 0); let mut name_set: FxHashSet<&str> = Default::default();
77
78 loop {
79 let next_input = match preceded(char::<_, E>('c'), space1)(input) {
80 Ok((i, _)) => i,
81 Err(_) => break,
82 };
83 if let Ok((next_input, _)) = preceded(tag("vo"), space1::<_, E>)(next_input) {
84 if vars.order_tree.is_some() {
86 let msg = "variable order tree may only be given once";
87 return fail(line_span(input), msg);
88 }
89 let t: Tree<Var>;
90 (input, (t, tree_max_var)) =
91 terminated(util::tree(true, true), eol)(next_input)?;
92
93 vars.order.clear();
95 vars.order.reserve(tree_max_var.1 + 1);
96 t.flatten_into(&mut vars.order);
97 vars.order_tree = Some(t);
98 } else if let Ok((next_input, ((var_span, var), name))) =
99 util::var_order_record::<E>(next_input)
100 {
101 input = next_input;
103 if var == 0 {
104 return fail(var_span, "variable number must be greater than 0");
105 }
106 if var > MAX_CAPACITY {
107 return fail(var_span, "variable number too large");
108 }
109
110 let num_vars = var as usize;
111 let var = num_vars - 1;
112
113 if num_vars > vars.names.len() {
114 vars.names.resize(num_vars, None);
115 vars.order.reserve(num_vars - vars.names.len());
116 max_var_span = var_span;
117 } else if vars.names[var].is_some() {
118 return fail(var_span, "second occurrence of variable in order");
119 }
120 vars.names[var] = Some(if let Some(name) = name {
122 let Ok(name) = std::str::from_utf8(name) else {
123 return fail(name, "invalid UTF-8");
124 };
125 if !name_set.insert(name) {
126 return fail(name.as_bytes(), "second occurrence of variable name");
127 }
128 name.to_owned()
129 } else {
130 String::new()
131 });
132 if vars.order_tree.is_none() {
133 vars.order.push(var);
134 }
135 } else {
136 return fail(
137 line_span(input),
138 "expected a variable order record ('c <var> [<name>]') or a variable order tree ('c vo <tree>')",
139 );
140 }
141 }
142
143 if vars.order_tree.is_none() && vars.names.len() != vars.order.len() {
144 return fail_with_contexts([
145 (input, "expected another variable order line"),
146 (max_var_span, "note: maximal variable number given here"),
147 ]);
148 }
149
150 let (next_input, sizes) = problem_line(input)?;
151 let [_, _, num_vars] = sizes;
152 if vars.order_tree.is_none() {
153 if !vars.order.is_empty() && num_vars.1 != vars.order.len() {
154 return fail_with_contexts([
155 (num_vars.0, "number of variables does not match"),
156 (max_var_span, "note: maximal variable number given here"),
157 ]);
158 }
159 } else {
160 if num_vars.1 != tree_max_var.1 + 1 {
161 return fail_with_contexts([
162 (num_vars.0, "number of variables does not match"),
163 (tree_max_var.0, "note: maximal variable number given here"),
164 ]);
165 }
166 if vars.names.len() > num_vars.1 {
167 return fail_with_contexts([
168 (max_var_span, "name assigned to non-existing variable"),
169 (num_vars.0, "note: number of variables given here"),
170 ]);
171 }
172 }
173
174 while let Some(name) = vars.names.last() {
176 if !name.as_ref().is_some_and(String::is_empty) {
177 break;
178 }
179 vars.names.pop();
180 }
181 for name in &mut vars.names {
182 if name.as_ref().is_some_and(String::is_empty) {
183 *name = None;
184 }
185 }
186
187 vars.len = num_vars.1;
188 #[cfg(debug_assertions)]
189 vars.check_valid();
190 Ok((next_input, (vars, sizes)))
191 } else {
192 let (input, sizes) = preceded(many0_count(util::comment), problem_line)(input)?;
193 let [_, _, (_, num_vars)] = sizes;
194 Ok((input, (VarSet::new(num_vars), sizes)))
195 }
196 }
197}
198
199pub fn parse<'a, E>(options: &ParseOptions) -> impl FnMut(&'a [u8]) -> IResult<&'a [u8], Problem, E>
201where
202 E: ParseError<&'a [u8]> + ContextError<&'a [u8]> + FromExternalError<&'a [u8], String>,
203{
204 let parse_var_orders = options.var_order;
205 let check_acyclic = options.check_acyclic;
206
207 move |input| {
208 let (mut input, (vars, [num_nodes, num_edges, num_inputs])) =
209 preamble(parse_var_orders)(input)?;
210
211 if num_nodes.1 == 0 {
212 return fail(num_nodes.0, "NNF must have at least one node");
213 }
214
215 let mut circuit = Circuit::new(vars);
216 circuit.reserve_gates(num_nodes.1);
217 circuit.reserve_gate_inputs(num_edges.1);
218
219 let mut nodes = Vec::with_capacity(num_nodes.1);
220 let mut gate_spans = Vec::with_capacity(num_nodes.1);
221
222 for _ in 0..num_nodes.1 {
223 let (inp, l) = match input {
224 [kind @ (b'A' | b'a' | b'B' | b'b' | b'X' | b'x'), inp @ ..] => {
225 let kind = if let b'X' | b'x' = kind {
226 GateKind::Xor
227 } else {
228 GateKind::And
229 };
230 let (mut inp, children) = preceded(space1, u64)(inp)?;
231 if children == 0 {
232 (inp, kind.empty_gate())
233 } else {
234 let l = circuit.push_gate(kind);
235 for _ in 0..children {
236 let (i, child) = preceded(space1, consumed(u64))(inp)?;
237 inp = i;
238
239 if child.1 >= num_nodes.1 as u64 {
240 return fail_with_contexts([
241 (child.0, "invalid node number"),
242 (num_nodes.0, "number of nodes given here"),
243 ]);
244 }
245 circuit.push_gate_input(Literal(child.1 as usize));
249 }
250 gate_spans.push(&input[..input.offset(inp)]);
251 (inp, l)
252 }
253 }
254 [b'O' | b'o', inp @ ..] => {
255 let (inp, conflict) = preceded(space1, consumed(u64))(inp)?;
256 if conflict.1 > num_inputs.1 as u64 {
257 return fail_with_contexts([
258 (conflict.0, "invalid variable"),
259 (num_inputs.0, "number of input variables given here"),
260 ]);
261 }
262
263 let (mut inp, children) = preceded(space1, consumed(u64))(inp)?;
264
265 if conflict.1 != 0 && children.1 != 2 {
266 return fail_with_contexts([
267 (children.0, "expected 2 children, since a conflict variable is given"),
268 (conflict.0, "using 0 in place of the conflict variable here allows arbitrary arity"),
269 ]);
270 }
271
272 if children.1 == 0 {
273 (inp, Literal::FALSE)
274 } else {
275 let l = circuit.push_gate(GateKind::Or);
276 for _ in 0..children.1 {
277 let (i, child) = preceded(space1, consumed(u64))(inp)?;
278 inp = i;
279
280 if child.1 >= num_nodes.1 as u64 {
281 return fail_with_contexts([
282 (child.0, "invalid node number"),
283 (num_nodes.0, "number of nodes given here"),
284 ]);
285 }
286 circuit.push_gate_input(Literal(child.1 as usize));
287 }
288 gate_spans.push(&input[..input.offset(inp)]);
289 (inp, l)
290 }
291 }
292 [b'L' | b'l', inp @ ..] => {
293 let (inp, lit) = preceded(space1, consumed(i64))(inp)?;
294 let var = lit.1.unsigned_abs();
295 if var == 0 || var > num_inputs.1 as u64 {
296 return fail_with_contexts([
297 (lit.0, "invalid literal"),
298 (num_inputs.0, "number of input variables given here"),
299 ]);
300 }
301 (inp, Literal::from_input(lit.1 < 0, (var - 1) as usize))
302 }
303 inp => {
304 return fail(
305 word_span(inp),
306 "expected a node ('A', 'B', 'O', 'X', or 'L')",
307 )
308 }
309 };
310 nodes.push(l);
311 input = preceded(space0, line_ending)(inp)?.0;
312 }
313
314 let (input, _) = preceded(multispace0, eof)(input)?;
315
316 for l in circuit.gates.all_elements_mut() {
317 *l = nodes[l.0];
318 }
319 if check_acyclic {
320 if let Some(l) = circuit.find_cycle() {
321 return fail(
322 gate_spans[l.get_gate_no().unwrap()],
323 "node depends on itself",
324 );
325 }
326 }
327
328 let problem = Problem {
329 circuit,
330 details: crate::ProblemDetails::Root(*nodes.last().unwrap()),
331 };
332 Ok((input, problem))
333 }
334}
335
336#[cfg(test)]
337mod tests {
338 use nom::Finish;
339
340 use crate::{util::test::*, Gate};
341
342 use super::*;
343
344 #[test]
346 fn c2d_example() {
347 let input = b"nnf 15 17 4\n\
348 L -3\n\
349 L -2\n\
350 L 1\n\
351 A 3 2 1 0\n\
352 L 3\n\
353 O 3 2 4 3\n\
354 L -4\n\
355 A 2 6 5\n\
356 L 4\n\
357 A 2 2 8\n\
358 A 2 1 4\n\
359 L 2\n\
360 O 2 2 11 10\n\
361 A 2 12 9\n\
362 O 4 2 13 7\n";
363
364 let (input, problem) = parse::<()>(&OPTS_NO_ORDER)(input).finish().unwrap();
365 assert!(input.is_empty());
366
367 let (circuit, root) = unwrap_problem(problem);
368 let inputs = circuit.inputs();
369 assert_eq!(inputs.len(), 4);
370 assert!(inputs.order().is_none());
371
372 let nodes = &[
373 !v(2), !v(1), v(0), g(0), v(2), g(1), !v(3), g(2), v(3), g(3), g(4), v(1), g(5), g(6), g(7), ];
389 assert_eq!(root, *nodes.last().unwrap());
390
391 for (i, &gate) in [
392 Gate::and(&[nodes[2], nodes[1], nodes[0]]), Gate::or(&[nodes[4], nodes[3]]), Gate::and(&[nodes[6], nodes[5]]), Gate::and(&[nodes[2], nodes[8]]), Gate::and(&[nodes[1], nodes[4]]), Gate::or(&[nodes[11], nodes[10]]), Gate::and(&[nodes[12], nodes[9]]), Gate::or(&[nodes[13], nodes[7]]), ]
401 .iter()
402 .enumerate()
403 {
404 assert_eq!(circuit.gate(g(i)), Some(gate), "mismatch for gate {i}");
405 }
406 }
407}