oxidd_parser/
aiger.rs

1//! AIGER parser based on
2//! "[The AIGER And-Inverter Graph (AIG) Format Version 20071012][spec1]" and
3//! "[AIGER 1.9 And Beyond][spec2]"
4//!
5//! [spec1]: https://github.com/arminbiere/aiger/blob/master/FORMAT
6//! [spec2]: https://fmv.jku.at/papers/BiereHeljankoWieringa-FMV-TR-11-2.pdf
7
8use nom::IResult;
9use nom::branch::alt;
10use nom::bytes::complete::tag;
11use nom::character::complete::space1;
12use nom::combinator::{consumed, eof, map, rest, value};
13use nom::error::{ContextError, FromExternalError, ParseError};
14use nom::sequence::{preceded, terminated};
15
16use crate::tv_bitvec::TVBitVec;
17use crate::util::{
18    collect, collect_pair, context_loc, eol_or_eof, fail, fail_with_contexts, line_span, usize,
19    word, word_span,
20};
21use crate::{
22    AIGERDetails, Circuit, GateKind, Literal, ParseOptions, Problem, ProblemDetails, Var, VarSet,
23    Vec2d,
24};
25
26// spell-checker:ignore toposort
27
28#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
29struct AIGLiteral(usize);
30
31impl AIGLiteral {
32    #[inline(always)]
33    fn negative(self) -> bool {
34        self.0 & 1 != 0
35    }
36
37    #[inline(always)]
38    fn variable(self) -> Var {
39        self.0 >> 1
40    }
41}
42
43#[derive(Clone, Copy)]
44struct Header<'a> {
45    binary: (&'a [u8], bool),
46    vars: (&'a [u8], usize),
47    inputs: (&'a [u8], usize),
48    latches: (&'a [u8], usize),
49    out: (&'a [u8], usize),
50    and: (&'a [u8], usize),
51    bad: (&'a [u8], usize),
52    inv: (&'a [u8], usize),
53    just: (&'a [u8], usize),
54    fair: (&'a [u8], usize),
55}
56
57/// Returns `Ok(.., false)` if `aag` (ASCII), `Ok(.., true)` if `aig` (binary)
58fn format<'a, E>(input: &'a [u8]) -> IResult<&'a [u8], bool, E>
59where
60    E: ParseError<&'a [u8]> + ContextError<&'a [u8]> + FromExternalError<&'a [u8], String>,
61{
62    context_loc(
63        || word_span(input),
64        "expected 'aag' (ASCII) or 'aig' (binary)",
65        word(alt((value(false, tag("aag")), value(true, tag("aig"))))),
66    )(input)
67}
68
69fn header<'a, E>(input: &'a [u8]) -> IResult<&'a [u8], Header<'a>, E>
70where
71    E: ParseError<&'a [u8]> + ContextError<&'a [u8]> + FromExternalError<&'a [u8], String>,
72{
73    let inner = |input| {
74        let (mut input, binary) = consumed(format)(input)?;
75        let mandatory = 5; // M I L O A
76        let mut numbers: [(&[u8], usize); 9] = [(&[], 0); 9]; // M I L O A B C J F
77        for (parsed, num) in numbers.iter_mut().enumerate() {
78            (input, *num) = match preceded(space1, consumed(usize))(input) {
79                Ok(p) => p,
80                Err(e) if parsed < mandatory => return Err(e),
81                Err(_) => break,
82            };
83        }
84        let (input, _) = eol_or_eof(input)?;
85        let h = Header {
86            binary,
87            vars: numbers[0],
88            inputs: numbers[1],
89            latches: numbers[2],
90            out: numbers[3],
91            and: numbers[4],
92            bad: numbers[5],
93            inv: numbers[6],
94            just: numbers[7],
95            fair: numbers[8],
96        };
97        let min_vars = h.inputs.1 + h.latches.1 + h.and.1;
98        if h.binary.1 {
99            if h.vars.1 != min_vars {
100                return fail(
101                    h.vars.0,
102                    "#vars must be equal to #inputs + #latches + #outputs",
103                );
104            }
105        } else if h.vars.1 < min_vars {
106            return fail(
107                h.vars.0,
108                "#vars must be at least #inputs + #latches + #outputs",
109            );
110        }
111        Ok((input, h))
112    };
113
114    context_loc(
115        || line_span(input),
116        "header line must have format 'aag|aig <#vars> <#inputs> <#latches> <#outputs> <#AND gates> [<#bad> [<#invariant constraints> [<#justice> [<#fairness>]]]]'",
117        inner,
118    )(input)
119}
120
121mod ascii {
122    use nom::IResult;
123    use nom::branch::alt;
124    use nom::character::complete::{line_ending, not_line_ending, space1, u64};
125    use nom::combinator::{consumed, eof, opt};
126    use nom::error::{ContextError, ParseError};
127    use nom::sequence::preceded;
128
129    use crate::util::{eol_or_eof, fail, fail_with_contexts, trim_end};
130    use crate::{AIGERDetails, VarSet};
131
132    use super::{AIGLiteral, Header};
133
134    pub fn literal<'a, E>(
135        vars: (&'a [u8], usize),
136    ) -> impl FnMut(&'a [u8]) -> IResult<&'a [u8], (&'a [u8], AIGLiteral), E>
137    where
138        E: ParseError<&'a [u8]> + ContextError<&'a [u8]>,
139    {
140        const MSG0: &str = "variable too large. The literal number given here divided by 2 must not be larger than the maximal variable number";
141        const MSG1: &str = "note: maximal variable number given here";
142
143        move |input| {
144            let (input, (span, lit)) = consumed(u64)(input)?;
145            if lit / 2 > vars.1 as u64 {
146                return fail_with_contexts([(span, MSG0), (vars.0, MSG1)]);
147            }
148            Ok((input, (span, AIGLiteral(lit as usize))))
149        }
150    }
151
152    pub fn input_line<'a, E>(
153        vars: (&'a [u8], usize),
154    ) -> impl FnMut(&'a [u8]) -> IResult<&'a [u8], (&'a [u8], AIGLiteral), E>
155    where
156        E: ParseError<&'a [u8]> + ContextError<&'a [u8]>,
157    {
158        move |input| {
159            let (input, lit) = literal(vars)(input)?;
160            if lit.1.negative() {
161                return fail(
162                    lit.0,
163                    "inputs mut not be negated (i.e., the number must be even)",
164                );
165            }
166            let (input, _) = eol_or_eof(input)?;
167            Ok((input, lit))
168        }
169    }
170
171    /// Optional init value, preceded by at least one space if present
172    pub fn latch_init_ext<'a, E>(
173        latch: AIGLiteral,
174    ) -> impl FnMut(&'a [u8]) -> IResult<&'a [u8], Option<bool>, E>
175    where
176        E: ParseError<&'a [u8]> + ContextError<&'a [u8]>,
177    {
178        const MSG: &str = "initial value must be 0, 1, or the latch literal itself";
179
180        move |input| {
181            let (input, init) = opt(preceded(space1, consumed(u64)))(input)?;
182            let init = match init {
183                None | Some((_, 0)) => Some(false),
184                Some((_, 1)) => Some(true),
185                Some((_, v)) if v == latch.0 as u64 => None,
186                Some((span, _)) => return fail(span, MSG),
187            };
188            Ok((input, init))
189        }
190    }
191
192    pub fn latch_line<'a, E>(
193        vars: (&'a [u8], usize),
194    ) -> impl FnMut(
195        &'a [u8],
196    ) -> IResult<
197        &'a [u8],
198        ((&'a [u8], AIGLiteral), (&'a [u8], AIGLiteral), Option<bool>),
199        E,
200    >
201    where
202        E: ParseError<&'a [u8]> + ContextError<&'a [u8]>,
203    {
204        move |input| {
205            let (input, lit) = literal(vars)(input)?;
206            let (input, _) = space1(input)?;
207            let (input, inp) = literal(vars)(input)?;
208
209            if lit.1.negative() {
210                return fail(
211                    lit.0,
212                    "latch literals mut not be negated (i.e., the number must be even)",
213                );
214            }
215
216            let (input, init) = latch_init_ext(lit.1)(input)?;
217            let (input, _) = eol_or_eof(input)?;
218            Ok((input, (lit, inp, init)))
219        }
220    }
221
222    pub fn symbol_table<'a, 'b, E>(
223        header: &'b Header<'a>,
224        inputs: &'b mut VarSet,
225        aig: &'b mut AIGERDetails,
226    ) -> impl 'b + FnMut(&'a [u8]) -> IResult<&'a [u8], (), E>
227    where
228        E: ParseError<&'a [u8]> + ContextError<&'a [u8]>,
229    {
230        const MSGS: [(&str, &str); 7] = [
231            ("input not defined", "number of inputs given here"),
232            ("latch not defined", "number of latches given here"),
233            ("output not defined", "number of outputs given here"),
234            (
235                "bad state literal not defined",
236                "number of bad state literals given here",
237            ),
238            (
239                "invariant constraint not defined",
240                "number of invariant constraints given here",
241            ),
242            (
243                "justice property not defined",
244                "number of justice properties given here",
245            ),
246            (
247                "fairness constraint not defined",
248                "number of fairness constraints given here",
249            ),
250        ];
251        move |mut input| {
252            let counts = [
253                header.inputs,
254                header.out,
255                header.bad,
256                header.inv,
257                header.just,
258                header.fair,
259                header.latches,
260            ];
261            let mut symbols = [const { Vec::<Option<String>>::new() }; 6];
262            loop {
263                let (inp, mut kind) = match input {
264                    [b'i', inp @ ..] => (inp, 0),
265                    [b'o', inp @ ..] => (inp, 1),
266                    [b'b', inp @ ..] => (inp, 2),
267                    [b'c', inp @ ..] => match inp {
268                        [b'0'..=b'9', ..] => (inp, 3),
269                        _ => break, // c is also used to begin the comment section
270                    },
271                    [b'j', inp @ ..] => (inp, 4),
272                    [b'f', inp @ ..] => (inp, 5),
273                    [b'l', inp @ ..] => (inp, 6),
274                    _ => break,
275                };
276
277                let (inp, (span, i)) = consumed(u64)(inp)?;
278                let (count_span, mut count) = counts[kind];
279                if i >= count as u64 {
280                    return fail_with_contexts([(span, MSGS[kind].0), (count_span, MSGS[kind].1)]);
281                }
282                let mut i = i as usize;
283
284                if kind == 6 {
285                    kind = 0;
286                    i += header.inputs.1;
287                    count += header.inputs.1;
288                } else if kind == 0 {
289                    count += header.latches.1;
290                }
291
292                let (inp, _) = space1(inp)?;
293                let (inp, name) = not_line_ending(inp)?;
294                (input, _) = alt((line_ending, eof))(inp)?;
295
296                let symbol_list = &mut symbols[kind];
297                if symbol_list.is_empty() {
298                    symbol_list.resize(count, None);
299                }
300                let symbol = &mut symbol_list[i];
301                let name = String::from_utf8_lossy(trim_end(name));
302                if let Some(symbol) = symbol {
303                    symbol.reserve(1 + name.len());
304                    symbol.push(' ');
305                    symbol.push_str(&name);
306                } else {
307                    *symbol = Some(name.to_string());
308                }
309            }
310
311            [
312                inputs.names,
313                aig.output_names,
314                aig.bad_names,
315                aig.invariant_names,
316                aig.justice_names,
317                aig.fairness_names,
318            ] = symbols;
319
320            Ok((input, ()))
321        }
322    }
323}
324
325fn usize_7bit(input: &[u8]) -> Result<(&[u8], usize), ()> {
326    let mut input = input;
327    let mut val = 0;
328    let mut shift = 0u32;
329    loop {
330        let &[b, ref rem @ ..] = input else {
331            return Err(());
332        };
333        input = rem;
334
335        val |= ((b & ((1 << 7) - 1)) as usize).wrapping_shl(shift);
336        if b & (1 << 7) == 0 {
337            return Ok((input, val));
338        }
339        shift += 7;
340    }
341}
342
343/// Parse a (binary or ASCII) AIGER file
344pub fn parse<'a, E>(options: &ParseOptions) -> impl FnMut(&'a [u8]) -> IResult<&'a [u8], Problem, E>
345where
346    E: ParseError<&'a [u8]> + ContextError<&'a [u8]> + FromExternalError<&'a [u8], String>,
347{
348    let check_acyclic = options.check_acyclic;
349    move |input| {
350        let (mut input, h) = header(input)?;
351
352        let mut circuit = Circuit::new(VarSet::new(h.inputs.1 + h.latches.1));
353        circuit.reserve_gates(h.and.1);
354        circuit.reserve_gate_inputs(h.and.1 * 2);
355        let mut aig = Box::new(AIGERDetails {
356            inputs: h.inputs.1,
357            latches: Vec::with_capacity(h.latches.1),
358            latch_init_values: TVBitVec::with_capacity(h.latches.1),
359            outputs: Vec::with_capacity(h.out.1),
360            bad: Vec::with_capacity(h.bad.1),
361            invariants: Vec::with_capacity(h.inv.1),
362            justice: Vec2d::with_capacity(h.just.1, 0),
363            fairness: Vec::with_capacity(h.fair.1),
364
365            map: Vec::new(),
366
367            output_names: Vec::new(),
368            bad_names: Vec::new(),
369            invariant_names: Vec::new(),
370            justice_names: Vec::new(),
371            fairness_names: Vec::new(),
372        });
373
374        let mut justice_len = Vec::<usize>::with_capacity(h.just.1);
375
376        let first_input = 1;
377        let first_latch = first_input + h.inputs.1;
378        let first_and_gate = first_latch + h.latches.1;
379        let var_count = first_and_gate + h.and.1; // reduced, including false
380
381        if h.binary.1 {
382            let make_literal = move |aig_literal: AIGLiteral| {
383                let var = aig_literal.variable();
384                let negative = aig_literal.negative();
385                if var >= first_and_gate {
386                    Literal::from_gate(negative, var - first_and_gate)
387                } else {
388                    Literal::from_input_or_false(negative, var)
389                }
390            };
391
392            // latches
393            for i in 0..h.latches.1 {
394                let (inp, (_, lit)) = ascii::literal(h.vars)(input)?;
395                let (inp, init) = ascii::latch_init_ext(AIGLiteral(i + first_latch * 2))(inp)?;
396                input = eol_or_eof(inp)?.0;
397                aig.latches.push(make_literal(lit));
398                aig.latch_init_values.push(init);
399            }
400
401            // outputs etc.
402            let mut literal = map(
403                terminated(ascii::literal(h.vars), eol_or_eof),
404                move |(_, l)| make_literal(l),
405            );
406            input = collect(h.out.1, &mut aig.outputs, &mut literal)(input)?.0;
407            input = collect(h.bad.1, &mut aig.bad, &mut literal)(input)?.0;
408            input = collect(h.inv.1, &mut aig.invariants, &mut literal)(input)?.0;
409            input = collect(h.just.1, &mut justice_len, terminated(usize, eol_or_eof))(input)?.0;
410            aig.justice.reserve_elements(justice_len.iter().sum());
411            for &n in &justice_len {
412                aig.justice.push_vec();
413                for _ in 0..n {
414                    let (inp, (_, lit)) = ascii::literal(h.vars)(input)?;
415                    (input, _) = eol_or_eof(inp)?;
416                    aig.justice.push_element(make_literal(lit));
417                }
418            }
419            input = collect(h.fair.1, &mut aig.fairness, &mut literal)(input)?.0;
420
421            // and gates
422            let and_gate_eof_err = fail(
423                h.binary.0,
424                "invalid binary: reached end of file while parsing an and gate",
425            );
426            for i in first_and_gate..var_count {
427                let Ok((inp, d1)) = usize_7bit(input) else {
428                    return and_gate_eof_err;
429                };
430                let Ok((inp, d2)) = usize_7bit(inp) else {
431                    return and_gate_eof_err;
432                };
433                input = inp;
434                let lhs = i * 2;
435                let in1 = lhs.wrapping_sub(d1);
436                if d1 > lhs || d1 == 0 || d2 > in1 {
437                    return fail(h.binary.0, "invalid binary: invalid and gate inputs");
438                }
439                let in2 = in1 - d2;
440                circuit.push_gate(GateKind::And);
441                circuit.push_gate_inputs([
442                    make_literal(AIGLiteral(in1)),
443                    make_literal(AIGLiteral(in2)),
444                ]);
445            }
446        } else {
447            // There may be undefined literals in the ASCII format (see the tests below).
448            // Since the numeric values of the `Literal` type do not match the `AIGLiteral`
449            // values anyway, we just map the literals into a contiguous space. `aig.map`
450            // maps variables to non-negated literals.
451            // Due to possible forward-references, we can only map the `AIGLiteral`s to
452            // `Literal`s once all definitions are read. Hence, we write intermediate values
453            // (`Literal(_.0)`) to the respective fields of `aig`.
454            aig.map = vec![Literal::UNDEF; h.vars.1 + 1];
455            aig.map[0] = Literal::FALSE;
456
457            // inputs
458            const SECOND_DEF_MSG: &str = "second variable definition";
459            for i in first_input..first_latch {
460                let (inp, (span, lit)) = ascii::input_line(h.vars)(input)?;
461                let var = lit.variable();
462                if aig.map[var] != Literal::UNDEF {
463                    return fail(span, SECOND_DEF_MSG);
464                }
465                aig.map[var] = Literal::from_input_or_false(false, i);
466                input = inp;
467            }
468
469            // latches
470            let mut latch_input_spans = Vec::with_capacity(h.latches.1);
471            for i in first_latch..first_and_gate {
472                let tmp = ascii::latch_line(h.vars)(input)?;
473                input = tmp.0;
474                let ((lit_span, lit), (inp_span, inp), init) = tmp.1;
475                let var = lit.variable();
476                if aig.map[var] != Literal::UNDEF {
477                    return fail(lit_span, SECOND_DEF_MSG);
478                }
479                aig.map[var] = Literal::from_input_or_false(false, i);
480                aig.latches.push(Literal(inp.0));
481                latch_input_spans.push(inp_span);
482                aig.latch_init_values.push(init);
483            }
484
485            // outputs etc.
486            let mut out_spans = Vec::with_capacity(h.out.1);
487            let mut bad_spans = Vec::with_capacity(h.bad.1);
488            let mut inv_spans = Vec::with_capacity(h.inv.1);
489            let mut literal = map(
490                terminated(ascii::literal(h.vars), eol_or_eof),
491                move |(s, l)| (s, Literal(l.0)),
492            );
493            input = collect_pair(h.out.1, &mut out_spans, &mut aig.outputs, &mut literal)(input)?.0;
494            input = collect_pair(h.bad.1, &mut bad_spans, &mut aig.bad, &mut literal)(input)?.0;
495            input =
496                collect_pair(h.inv.1, &mut inv_spans, &mut aig.invariants, &mut literal)(input)?.0;
497            input = collect(h.just.1, &mut justice_len, terminated(usize, eol_or_eof))(input)?.0;
498
499            // justice
500            let justice_elements = justice_len.iter().sum();
501            aig.justice.reserve_elements(justice_elements);
502            let mut just_spans = Vec::with_capacity(justice_elements);
503            for &n in &justice_len {
504                aig.justice.push_vec();
505                for _ in 0..n {
506                    let (inp, (span, lit)) = ascii::literal(h.vars)(input)?;
507                    (input, _) = eol_or_eof(inp)?;
508                    just_spans.push(span);
509                    aig.justice.push_element(Literal(lit.0));
510                }
511            }
512
513            // fairness
514            let mut fair_spans = Vec::with_capacity(h.fair.1);
515            input =
516                collect_pair(h.fair.1, &mut fair_spans, &mut aig.fairness, &mut literal)(input)?.0;
517
518            // and gates
519            let mut and_gate_spans = Vec::with_capacity(h.and.1);
520            for i in 0..h.and.1 {
521                let (inp, (lit_span, lit)) = ascii::literal(h.vars)(input)?;
522                let (inp, _) = space1(inp)?;
523                let (inp, (in1_span, in1)) = ascii::literal(h.vars)(inp)?;
524                let (inp, _) = space1(inp)?;
525                let (inp, (in2_span, in2)) = ascii::literal(h.vars)(inp)?;
526                input = eol_or_eof(inp)?.0;
527
528                if lit.negative() {
529                    return fail(lit_span, "gate literal must not be negative");
530                }
531                let var = lit.variable();
532                if aig.map[var] != Literal::UNDEF {
533                    return fail(lit_span, SECOND_DEF_MSG);
534                }
535                aig.map[var] = Literal::from_gate(false, i);
536                circuit.push_gate(GateKind::And);
537                circuit.push_gate_inputs([Literal(in1.0), Literal(in2.0)]);
538                and_gate_spans.push((lit_span, in1_span, in2_span));
539            }
540
541            // map literals
542            let mut undef = Vec::new();
543            let mut map = |l: Literal, span: &'a [u8]| {
544                let mapped_literal = aig.map[l.0 >> 1];
545                if mapped_literal == Literal::UNDEF {
546                    undef.push(span);
547                }
548                Literal(mapped_literal.0 | ((l.0 & 1) << Literal::POLARITY_BIT))
549            };
550            let mut map_slice = |slice: &mut [Literal], spans: &[&'a [u8]]| {
551                for (inp, &span) in slice.iter_mut().zip(spans.iter()) {
552                    *inp = map(*inp, span);
553                }
554            };
555            map_slice(&mut aig.latches, &latch_input_spans);
556            map_slice(&mut aig.outputs, &out_spans);
557            map_slice(&mut aig.bad, &bad_spans);
558            map_slice(&mut aig.invariants, &inv_spans);
559            let justice_elements = aig.justice.all_elements_mut();
560            map_slice(justice_elements, &just_spans);
561            map_slice(&mut aig.fairness, &fair_spans);
562            #[allow(clippy::needless_range_loop)]
563            // there is no iter_mut on Circuit (probably, we cannot implement that in Safe Rust)
564            for i in 0..circuit.num_gates() {
565                if let Some([in1, in2]) = circuit.gate_inputs_mut_for_no(i) {
566                    *in1 = map(*in1, and_gate_spans[i].1);
567                    *in2 = map(*in2, and_gate_spans[i].2);
568                } else {
569                    debug_assert!(false);
570                }
571            }
572            if !undef.is_empty() {
573                return fail_with_contexts(undef.iter().map(|&span| (span, "undefined literal")));
574            }
575
576            // check for cycles
577            if check_acyclic && let Some(l) = circuit.find_cycle() {
578                return fail(
579                    and_gate_spans[l.get_gate_no().unwrap()].0,
580                    "and gate depends on itself",
581                );
582            }
583        }
584
585        // symbol table
586        let (input, ()) = ascii::symbol_table(&h, &mut circuit.inputs, &mut aig)(input)?;
587
588        // optional comment section
589        let (input, _) = alt((preceded(tag("c"), rest), eof))(input)?;
590
591        if h.binary.1 {
592            // collect he map for binary mode at the very end since it cannot fail
593            debug_assert!(aig.map.is_empty());
594            aig.map.reserve(var_count);
595            aig.map
596                .extend((0..first_and_gate).map(|i| Literal::from_input_or_false(false, i)));
597            aig.map
598                .extend((0..h.and.1).map(|i| Literal::from_gate(false, i)));
599        }
600
601        let problem = Problem {
602            circuit,
603            details: ProblemDetails::AIGER(aig),
604        };
605
606        Ok((input, problem))
607    }
608}
609
610#[cfg(test)]
611mod tests {
612    use crate::tv_bitvec::TVBitVec;
613    use crate::util::test::OPTS_NO_ORDER;
614    use crate::{Circuit, Literal, Problem, ProblemDetails, VarSet, Vec2d};
615
616    use super::{AIGERDetails, usize_7bit};
617
618    impl Problem {
619        fn new_aig(vars: VarSet) -> Self {
620            let details = Box::new(AIGERDetails {
621                inputs: vars.len(),
622                latches: Vec::new(),
623                latch_init_values: TVBitVec::new(),
624                outputs: Vec::new(),
625                bad: Vec::new(),
626                invariants: Vec::new(),
627                justice: Vec2d::new(),
628                fairness: Vec::new(),
629
630                map: Vec::new(),
631
632                output_names: Vec::new(),
633                bad_names: Vec::new(),
634                invariant_names: Vec::new(),
635                justice_names: Vec::new(),
636                fairness_names: Vec::new(),
637            });
638            Self {
639                circuit: Circuit::new(vars),
640                details: ProblemDetails::AIGER(details),
641            }
642        }
643
644        fn with_outputs(mut self, outputs: impl IntoIterator<Item = Literal>) -> Self {
645            if let ProblemDetails::AIGER(aig) = &mut self.details {
646                aig.outputs = outputs.into_iter().collect()
647            }
648            self
649        }
650
651        fn with_named_outputs<'a>(
652            mut self,
653            outputs: impl IntoIterator<Item = (Literal, &'a str)>,
654        ) -> Self {
655            if let ProblemDetails::AIGER(aig) = &mut self.details {
656                (aig.outputs, aig.output_names) = outputs
657                    .into_iter()
658                    .map(|(l, s)| (l, Some(s.to_string())))
659                    .unzip();
660            }
661            self
662        }
663
664        fn with_and_gates(
665            mut self,
666            and_gates: impl IntoIterator<Item = (Literal, Literal)>,
667        ) -> Self {
668            let it = and_gates.into_iter();
669            let n = it.size_hint().0;
670            self.circuit.reserve_gates(n);
671            self.circuit.reserve_gate_inputs(2 * n);
672
673            for (l1, l2) in it {
674                self.circuit.push_gate(crate::GateKind::And);
675                self.circuit.push_gate_inputs([l1, l2]);
676            }
677
678            self
679        }
680
681        /// Add latches as well as the respective number of inputs to the
682        /// combinational circuit
683        fn with_latches(mut self, latches: impl IntoIterator<Item = Literal>) -> Self {
684            let ProblemDetails::AIGER(aig) = &mut self.details else {
685                panic!();
686            };
687            aig.latches = latches.into_iter().collect();
688            self.circuit.inputs.len += aig.latches.len();
689            aig.latch_init_values = TVBitVec::with_capacity(aig.latches.len());
690            for _ in 0..aig.latches.len() {
691                aig.latch_init_values.push(Some(false));
692            }
693
694            self
695        }
696
697        fn with_default_map(mut self) -> Self {
698            let inputs = self.circuit.inputs.len();
699            let gates = self.circuit.num_gates();
700
701            let ProblemDetails::AIGER(aig) = &mut self.details else {
702                panic!();
703            };
704            aig.map.clear();
705            aig.map.reserve(1 + inputs + gates);
706            aig.map
707                .extend((0..inputs + 1).map(|i| Literal::from_input_or_false(false, i)));
708            aig.map
709                .extend((0..gates).map(|i| Literal::from_gate(false, i)));
710
711            self
712        }
713
714        fn with_map(mut self, map: Vec<Literal>) -> Self {
715            if let ProblemDetails::AIGER(aig) = &mut self.details {
716                aig.map = map;
717            }
718            self
719        }
720
721        fn with_bad(mut self, bad: impl IntoIterator<Item = Literal>) -> Self {
722            let ProblemDetails::AIGER(aig) = &mut self.details else {
723                panic!();
724            };
725            aig.bad = bad.into_iter().collect();
726            self
727        }
728
729        fn with_invariants(mut self, invariants: impl IntoIterator<Item = Literal>) -> Self {
730            let ProblemDetails::AIGER(aig) = &mut self.details else {
731                panic!();
732            };
733            aig.invariants = invariants.into_iter().collect();
734            self
735        }
736
737        fn with_justice<'a>(mut self, justice: impl IntoIterator<Item = &'a [Literal]>) -> Self {
738            let ProblemDetails::AIGER(aig) = &mut self.details else {
739                panic!();
740            };
741            aig.justice = Vec2d::from_iter(justice);
742            self
743        }
744
745        fn with_fairness(mut self, fairness: impl IntoIterator<Item = Literal>) -> Self {
746            let ProblemDetails::AIGER(aig) = &mut self.details else {
747                panic!();
748            };
749            aig.fairness = fairness.into_iter().collect();
750            self
751        }
752    }
753
754    #[test]
755    fn decode_7bit() {
756        // cases taken from https://github.com/arminbiere/aiger/blob/master/FORMAT
757        let cases: &[(usize, &[u8])] = &[
758            (0, b"\x00"),
759            (1, b"\x01"),
760            ((1 << 7) - 1, b"\x7f"),
761            ((1 << 7), b"\x80\x01"),
762            ((1 << 8) + 2, b"\x82\x02"),
763            ((1 << 14) - 1, b"\xff\x7f"),
764            ((1 << 14) + 3, b"\x83\x80\x01"),
765            ((1 << 28) - 1, b"\xff\xff\xff\x7f"),
766            ((1 << 28) + 7, b"\x87\x80\x80\x80\x01"),
767        ];
768
769        for &(expected, input) in cases {
770            let (remaining, val) = usize_7bit(input).unwrap();
771            assert!(remaining.is_empty());
772            assert_eq!(val, expected);
773        }
774    }
775
776    fn test_aag_aig_match(aag: &[u8], aig: &[u8], expected: Problem) {
777        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aag).unwrap();
778        assert_eq!(problem, expected, "aag does not match expected");
779        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aig).unwrap();
780        assert_eq!(problem, expected, "aig does not match expected");
781    }
782
783    // cases (mostly) taken from https://github.com/arminbiere/aiger/blob/master/FORMAT
784
785    #[test]
786    fn aag_aig_match_empty() {
787        test_aag_aig_match(
788            b"aag 0 0 0 0 0\n",
789            b"aig 0 0 0 0 0\n",
790            Problem::new_aig(VarSet::new(0)).with_default_map(),
791        );
792    }
793
794    #[test]
795    fn aag_aig_match_false_out() {
796        test_aag_aig_match(
797            b"aag 0 0 0 1 0\n0\n",
798            b"aig 0 0 0 1 0\n0\n",
799            Problem::new_aig(VarSet::new(0))
800                .with_outputs([Literal::FALSE])
801                .with_default_map(),
802        );
803    }
804
805    #[test]
806    fn aag_aig_match_true_out() {
807        test_aag_aig_match(
808            b"aag 0 0 0 1 0\n1\n",
809            b"aig 0 0 0 1 0\n1\n",
810            Problem::new_aig(VarSet::new(0))
811                .with_outputs([Literal::TRUE])
812                .with_default_map(),
813        );
814    }
815
816    #[test]
817    fn aag_aig_match_in_out() {
818        test_aag_aig_match(
819            b"aag 1 1 0 1 0\n2\n2\n",
820            b"aig 1 1 0 1 0\n2\n",
821            Problem::new_aig(VarSet::new(1))
822                .with_outputs([Literal::from_input(false, 0)])
823                .with_default_map(),
824        );
825    }
826
827    #[test]
828    fn aag_aig_match_neg() {
829        test_aag_aig_match(
830            b"aag 1 1 0 1 0\n2\n3\n",
831            b"aig 1 1 0 1 0\n3\n",
832            Problem::new_aig(VarSet::new(1))
833                .with_outputs([Literal::from_input(true, 0)])
834                .with_default_map(),
835        );
836    }
837
838    #[test]
839    fn aag_aig_match_and() {
840        test_aag_aig_match(
841            b"aag 3 2 0 1 1\n2\n4\n6\n6 4 2\n",
842            b"aig 3 2 0 1 1\n6\n\x02\x02",
843            Problem::new_aig(VarSet::new(2))
844                .with_outputs([Literal::from_gate(false, 0)])
845                .with_and_gates([(Literal::from_input(false, 1), Literal::from_input(false, 0))])
846                .with_default_map(),
847        );
848    }
849
850    #[test]
851    fn aag_aig_match_or() {
852        test_aag_aig_match(
853            b"aag 3 2 0 1 1\n2\n4\n7\n6 5 3\n",
854            b"aig 3 2 0 1 1\n7\n\x01\x02",
855            Problem::new_aig(VarSet::new(2))
856                .with_outputs([Literal::from_gate(true, 0)])
857                .with_and_gates([(Literal::from_input(true, 1), Literal::from_input(true, 0))])
858                .with_default_map(),
859        );
860    }
861
862    #[test]
863    fn aag_half_adder() {
864        // Since we do not normalize the parsed AIG and also include a literal map, it
865        // is difficult to compare the ASCII and binary versions of this example
866        // directly. Hence, we have two test cases here.
867        let aag = b"aag 7 2 0 2 3\n\
868            2\n\
869            4\n\
870            6\n\
871            12\n\
872            6 13 15\n\
873            12 2 4\n\
874            14 3 5\n\
875            i0 x\n\
876            i1 y\n\
877            o0 s\n\
878            o1 c\n\
879            c\nhalf adder\n";
880        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aag).unwrap();
881
882        let map = vec![
883            Literal::FALSE,
884            Literal::from_input(false, 0),
885            Literal::from_input(false, 1),
886            Literal::from_gate(false, 0),
887            Literal::UNDEF,
888            Literal::UNDEF,
889            Literal::from_gate(false, 1),
890            Literal::from_gate(false, 2),
891        ];
892
893        let expected =
894            Problem::new_aig(VarSet::with_names(vec![Some("x".into()), Some("y".into())]))
895                .with_named_outputs([(map[6 >> 1], "s"), (map[12 >> 1], "c")])
896                .with_and_gates([
897                    (!map[13 >> 1], !map[15 >> 1]),
898                    (map[2 >> 1], map[4 >> 1]),
899                    (!map[3 >> 1], !map[5 >> 1]),
900                ])
901                .with_map(map);
902        assert_eq!(problem, expected);
903    }
904
905    #[test]
906    fn aig_half_adder() {
907        let aig = b"aig 5 2 0 2 3\n\
908            10\n\
909            6\n\
910            \x02\x02\
911            \x03\x02\
912            \x01\x02\
913            i0 x\n\
914            i1 y\n\
915            o0 s\n\
916            o1 c\n\
917            c\nhalf adder\n";
918        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aig).unwrap();
919
920        let expected =
921            Problem::new_aig(VarSet::with_names(vec![Some("x".into()), Some("y".into())]))
922                .with_named_outputs([
923                    (Literal::from_gate(false, 2), "s"),
924                    (Literal::from_gate(false, 0), "c"),
925                ])
926                .with_and_gates([
927                    (Literal::from_input(false, 1), Literal::from_input(false, 0)),
928                    (Literal::from_input(true, 1), Literal::from_input(true, 0)),
929                    (Literal::from_gate(true, 1), Literal::from_gate(true, 0)),
930                ])
931                .with_default_map();
932
933        assert_eq!(problem, expected);
934    }
935
936    #[test]
937    fn aag_aig_match_toggle() {
938        test_aag_aig_match(
939            b"aag 1 0 1 2 0\n2 3\n2\n3\n",
940            b"aig 1 0 1 2 0\n3\n2\n3\n",
941            Problem::new_aig(VarSet::new(0))
942                .with_latches([Literal::from_input(true, 0)])
943                .with_outputs([Literal::from_input(false, 0), Literal::from_input(true, 0)])
944                .with_default_map(),
945        );
946    }
947
948    #[test]
949    fn aag_toggle_with_reset() {
950        let aag = b"aag 7 2 1 2 4\n\
951            2\n\
952            4\n\
953            6 8\n\
954            6\n\
955            7\n\
956            8 4 10\n\
957            10 13 15\n\
958            12 2 6\n\
959            14 3 7\n\
960            i0 toggle\n\
961            i1 ~reset\n\
962            o0 q\n\
963            o1 ~q\n\
964            l0 q\n\
965            c foobar\n";
966        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aag).unwrap();
967
968        let mut expected = Problem::new_aig(VarSet::with_names(vec![
969            Some("toggle".into()),
970            Some("~reset".into()),
971        ]))
972        .with_latches([Literal::from_gate(false, 0)])
973        .with_named_outputs([
974            (Literal::from_input(false, 2), "q"),
975            (Literal::from_input(true, 2), "~q"),
976        ])
977        .with_and_gates([
978            (Literal::from_input(false, 1), Literal::from_gate(false, 1)),
979            (Literal::from_gate(true, 2), Literal::from_gate(true, 3)),
980            (Literal::from_input(false, 0), Literal::from_input(false, 2)),
981            (Literal::from_input(true, 0), Literal::from_input(true, 2)),
982        ])
983        .with_default_map();
984
985        expected.circuit.inputs.set_name(2, "q");
986
987        assert_eq!(problem, expected);
988    }
989
990    #[test]
991    fn aig_toggle_with_reset() {
992        let aig = b"aig 7 2 1 2 4\n\
993            14\n\
994            6\n\
995            7\n\
996            \x02\x04\
997            \x03\x04\
998            \x01\x02\
999            \x02\x08";
1000        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aig).unwrap();
1001
1002        let expected = Problem::new_aig(VarSet::new(2))
1003            .with_latches([Literal::from_gate(false, 3)])
1004            .with_outputs([Literal::from_input(false, 2), Literal::from_input(true, 2)])
1005            .with_and_gates([
1006                (Literal::from_input(false, 2), Literal::from_input(false, 0)),
1007                (Literal::from_input(true, 2), Literal::from_input(true, 0)),
1008                (Literal::from_gate(true, 1), Literal::from_gate(true, 0)),
1009                (Literal::from_gate(false, 2), Literal::from_input(false, 1)),
1010            ])
1011            .with_default_map();
1012        assert_eq!(problem, expected);
1013    }
1014
1015    // next case taken from "AIGER 1.9 And Beyond"
1016
1017    #[test]
1018    fn aag_aig_match_bad_and_invariant() {
1019        test_aag_aig_match(
1020            b"aag 5 1 1 0 3 1 1\n\
1021            2\n\
1022            4 10 0\n\
1023            4\n\
1024            3\n\
1025            6 5 3\n\
1026            8 4 2\n\
1027            10 9 7\n",
1028            b"aig 5 1 1 0 3 1 1\n\
1029            10 0\n\
1030            4\n\
1031            3\n\
1032            \x01\x02\x04\x02\x01\x02",
1033            Problem::new_aig(VarSet::new(1))
1034                .with_latches([Literal::from_gate(false, 2)])
1035                .with_and_gates([
1036                    (Literal::from_input(true, 1), Literal::from_input(true, 0)),
1037                    (Literal::from_input(false, 1), Literal::from_input(false, 0)),
1038                    (Literal::from_gate(true, 1), Literal::from_gate(true, 0)),
1039                ])
1040                .with_bad([Literal::from_input(false, 1)])
1041                .with_invariants([Literal::from_input(true, 0)])
1042                .with_default_map(),
1043        );
1044    }
1045
1046    #[test]
1047    fn aag_aig_match_extra_properties() {
1048        // M I L O A B C J F
1049        test_aag_aig_match(
1050            b"aag 3 2 0 1 1 1 1 2 1\n2\n4\n6\n2\n3\n1\n2\n1\n4\n5\n6\n6 4 2\n",
1051            b"aig 3 2 0 1 1 1 1 2 1\n6\n2\n3\n1\n2\n1\n4\n5\n6\n\x02\x02",
1052            Problem::new_aig(VarSet::new(2))
1053                .with_outputs([Literal::from_gate(false, 0)])
1054                .with_and_gates([(Literal::from_input(false, 1), Literal::from_input(false, 0))])
1055                .with_bad([Literal::from_input(false, 0)])
1056                .with_invariants([Literal::from_input(true, 0)])
1057                .with_justice([
1058                    [Literal::TRUE].as_slice(),
1059                    &[Literal::from_input(false, 1), Literal::from_input(true, 1)],
1060                ])
1061                .with_fairness([Literal::from_gate(false, 0)])
1062                .with_default_map(),
1063        );
1064    }
1065}
oxidd_parser/aiger.rs

oxidd_parser/
aiger.rs
