oxidd_parser/
nnf.rs

1//! Negation normal form parser for an extended version of [c2d's][c2d] d-DNNF
2//! output format
3//!
4//! The format extensions subsume [Bella's][bella] wDNNF format.
5//!
6//! [c2d]: http://reasoning.cs.ucla.edu/c2d/
7//! [bella]: https://github.com/Illner/BellaCompiler
8
9// spell-checker:ignore multispace
10
11use 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
25/// Parses a problem line, i.e., `nnf <#nodes> <#edges> <#inputs>`
26///
27/// Returns the three numbers along with their spans.
28fn 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
52/// Parses the preamble, i.e., all `c` and `nnf` lines at the beginning of the
53/// file
54///
55/// Note: `parse_orders` only instructs the parser to treat comment lines as
56/// order lines. In case a var order is given, this function ensures that they
57/// are valid. However, if no var order is given, then the returned var order is
58/// empty.
59fn 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(); // in the name mapping / linear order
75            let mut tree_max_var = ([].as_slice(), 0); // dummy value
76            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                    // variable order tree
85                    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                    // The variable order tree takes precedence (and determines the linear order)
94                    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                    // var order line
102                    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                    // always write Some to mark the variable as present
121                    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            // cleanup: we used `Some(String::new())` to mark unnamed variables as present
175            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
199/// Parse a NNF file
200pub 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                            // In contrast to the original c2d format, we do not enforce a
246                            // topological order on the input. We just collect the node IDs now and
247                            // map them to `Literal`s later.
248                            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    /// NNF taken from the c2d manual
345    #[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), // L -3
374            !v(1), // L -2
375            v(0),  // L 1
376            g(0),  // A 3 2 1 0
377            v(2),  // L 3
378            g(1),  // O 3 2 4 3
379            !v(3), // L -4
380            g(2),  // A 2 6 5
381            v(3),  // L 4
382            g(3),  // A 2 2 8
383            g(4),  // A 2 1 4
384            v(1),  // L 2
385            g(5),  // O 2 2 11 10
386            g(6),  // A 2 12 9
387            g(7),  // O 4 2 13 7
388        ];
389        assert_eq!(root, *nodes.last().unwrap());
390
391        for (i, &gate) in [
392            Gate::and(&[nodes[2], nodes[1], nodes[0]]), // 0: A 3 2 1 0
393            Gate::or(&[nodes[4], nodes[3]]),            // 1: O 3 2 4 3
394            Gate::and(&[nodes[6], nodes[5]]),           // 2: A 2 6 5
395            Gate::and(&[nodes[2], nodes[8]]),           // 3: A 2 2 8
396            Gate::and(&[nodes[1], nodes[4]]),           // 4: A 2 1 4
397            Gate::or(&[nodes[11], nodes[10]]),          // 5: O 2 2 11 10
398            Gate::and(&[nodes[12], nodes[9]]),          // 6: A 2 12 9
399            Gate::or(&[nodes[13], nodes[7]]),           // 7: O 4 2 13 7
400        ]
401        .iter()
402        .enumerate()
403        {
404            assert_eq!(circuit.gate(g(i)), Some(gate), "mismatch for gate {i}");
405        }
406    }
407}