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::branch::alt;
9use nom::bytes::complete::tag;
10use nom::character::complete::space1;
11use nom::combinator::{consumed, eof, map, rest, value};
12use nom::error::{ContextError, FromExternalError, ParseError};
13use nom::sequence::{preceded, terminated};
14use nom::IResult;
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::branch::alt;
123    use nom::character::complete::{line_ending, not_line_ending, space1, u64};
124    use nom::combinator::{consumed, eof, opt};
125    use nom::error::{ContextError, ParseError};
126    use nom::sequence::preceded;
127    use nom::IResult;
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 {
578                if let Some(l) = circuit.find_cycle() {
579                    return fail(
580                        and_gate_spans[l.get_gate_no().unwrap()].0,
581                        "and gate depends on itself",
582                    );
583                }
584            }
585        }
586
587        // symbol table
588        let (input, ()) = ascii::symbol_table(&h, &mut circuit.inputs, &mut aig)(input)?;
589
590        // optional comment section
591        let (input, _) = alt((preceded(tag("c"), rest), eof))(input)?;
592
593        if h.binary.1 {
594            // collect he map for binary mode at the very end since it cannot fail
595            debug_assert!(aig.map.is_empty());
596            aig.map.reserve(var_count);
597            aig.map
598                .extend((0..first_and_gate).map(|i| Literal::from_input_or_false(false, i)));
599            aig.map
600                .extend((0..h.and.1).map(|i| Literal::from_gate(false, i)));
601        }
602
603        let problem = Problem {
604            circuit,
605            details: ProblemDetails::AIGER(aig),
606        };
607
608        Ok((input, problem))
609    }
610}
611
612#[cfg(test)]
613mod tests {
614    use crate::tv_bitvec::TVBitVec;
615    use crate::util::test::OPTS_NO_ORDER;
616    use crate::{Circuit, Literal, Problem, ProblemDetails, VarSet, Vec2d};
617
618    use super::{usize_7bit, AIGERDetails};
619
620    impl Problem {
621        fn new_aig(vars: VarSet) -> Self {
622            let details = Box::new(AIGERDetails {
623                inputs: vars.len(),
624                latches: Vec::new(),
625                latch_init_values: TVBitVec::new(),
626                outputs: Vec::new(),
627                bad: Vec::new(),
628                invariants: Vec::new(),
629                justice: Vec2d::new(),
630                fairness: Vec::new(),
631
632                map: Vec::new(),
633
634                output_names: Vec::new(),
635                bad_names: Vec::new(),
636                invariant_names: Vec::new(),
637                justice_names: Vec::new(),
638                fairness_names: Vec::new(),
639            });
640            Self {
641                circuit: Circuit::new(vars),
642                details: ProblemDetails::AIGER(details),
643            }
644        }
645
646        fn with_outputs(mut self, outputs: impl IntoIterator<Item = Literal>) -> Self {
647            if let ProblemDetails::AIGER(aig) = &mut self.details {
648                aig.outputs = outputs.into_iter().collect()
649            }
650            self
651        }
652
653        fn with_named_outputs<'a>(
654            mut self,
655            outputs: impl IntoIterator<Item = (Literal, &'a str)>,
656        ) -> Self {
657            if let ProblemDetails::AIGER(aig) = &mut self.details {
658                (aig.outputs, aig.output_names) = outputs
659                    .into_iter()
660                    .map(|(l, s)| (l, Some(s.to_string())))
661                    .unzip();
662            }
663            self
664        }
665
666        fn with_and_gates(
667            mut self,
668            and_gates: impl IntoIterator<Item = (Literal, Literal)>,
669        ) -> Self {
670            let it = and_gates.into_iter();
671            let n = it.size_hint().0;
672            self.circuit.reserve_gates(n);
673            self.circuit.reserve_gate_inputs(2 * n);
674
675            for (l1, l2) in it {
676                self.circuit.push_gate(crate::GateKind::And);
677                self.circuit.push_gate_inputs([l1, l2]);
678            }
679
680            self
681        }
682
683        /// Add latches as well as the respective number of inputs to the
684        /// combinational circuit
685        fn with_latches(mut self, latches: impl IntoIterator<Item = Literal>) -> Self {
686            let ProblemDetails::AIGER(aig) = &mut self.details else {
687                panic!();
688            };
689            aig.latches = latches.into_iter().collect();
690            self.circuit.inputs.len += aig.latches.len();
691            aig.latch_init_values = TVBitVec::with_capacity(aig.latches.len());
692            for _ in 0..aig.latches.len() {
693                aig.latch_init_values.push(Some(false));
694            }
695
696            self
697        }
698
699        fn with_default_map(mut self) -> Self {
700            let inputs = self.circuit.inputs.len();
701            let gates = self.circuit.num_gates();
702
703            let ProblemDetails::AIGER(aig) = &mut self.details else {
704                panic!();
705            };
706            aig.map.clear();
707            aig.map.reserve(1 + inputs + gates);
708            aig.map
709                .extend((0..inputs + 1).map(|i| Literal::from_input_or_false(false, i)));
710            aig.map
711                .extend((0..gates).map(|i| Literal::from_gate(false, i)));
712
713            self
714        }
715
716        fn with_map(mut self, map: Vec<Literal>) -> Self {
717            if let ProblemDetails::AIGER(aig) = &mut self.details {
718                aig.map = map;
719            }
720            self
721        }
722
723        fn with_bad(mut self, bad: impl IntoIterator<Item = Literal>) -> Self {
724            let ProblemDetails::AIGER(aig) = &mut self.details else {
725                panic!();
726            };
727            aig.bad = bad.into_iter().collect();
728            self
729        }
730
731        fn with_invariants(mut self, invariants: impl IntoIterator<Item = Literal>) -> Self {
732            let ProblemDetails::AIGER(aig) = &mut self.details else {
733                panic!();
734            };
735            aig.invariants = invariants.into_iter().collect();
736            self
737        }
738
739        fn with_justice<'a>(mut self, justice: impl IntoIterator<Item = &'a [Literal]>) -> Self {
740            let ProblemDetails::AIGER(aig) = &mut self.details else {
741                panic!();
742            };
743            aig.justice = Vec2d::from_iter(justice);
744            self
745        }
746
747        fn with_fairness(mut self, fairness: impl IntoIterator<Item = Literal>) -> Self {
748            let ProblemDetails::AIGER(aig) = &mut self.details else {
749                panic!();
750            };
751            aig.fairness = fairness.into_iter().collect();
752            self
753        }
754    }
755
756    #[test]
757    fn decode_7bit() {
758        // cases taken from https://github.com/arminbiere/aiger/blob/master/FORMAT
759        let cases: &[(usize, &[u8])] = &[
760            (0, b"\x00"),
761            (1, b"\x01"),
762            ((1 << 7) - 1, b"\x7f"),
763            ((1 << 7), b"\x80\x01"),
764            ((1 << 8) + 2, b"\x82\x02"),
765            ((1 << 14) - 1, b"\xff\x7f"),
766            ((1 << 14) + 3, b"\x83\x80\x01"),
767            ((1 << 28) - 1, b"\xff\xff\xff\x7f"),
768            ((1 << 28) + 7, b"\x87\x80\x80\x80\x01"),
769        ];
770
771        for &(expected, input) in cases {
772            let (remaining, val) = usize_7bit(input).unwrap();
773            assert!(remaining.is_empty());
774            assert_eq!(val, expected);
775        }
776    }
777
778    fn test_aag_aig_match(aag: &[u8], aig: &[u8], expected: Problem) {
779        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aag).unwrap();
780        assert_eq!(problem, expected, "aag does not match expected");
781        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aig).unwrap();
782        assert_eq!(problem, expected, "aig does not match expected");
783    }
784
785    // cases (mostly) taken from https://github.com/arminbiere/aiger/blob/master/FORMAT
786
787    #[test]
788    fn aag_aig_match_empty() {
789        test_aag_aig_match(
790            b"aag 0 0 0 0 0\n",
791            b"aig 0 0 0 0 0\n",
792            Problem::new_aig(VarSet::new(0)).with_default_map(),
793        );
794    }
795
796    #[test]
797    fn aag_aig_match_false_out() {
798        test_aag_aig_match(
799            b"aag 0 0 0 1 0\n0\n",
800            b"aig 0 0 0 1 0\n0\n",
801            Problem::new_aig(VarSet::new(0))
802                .with_outputs([Literal::FALSE])
803                .with_default_map(),
804        );
805    }
806
807    #[test]
808    fn aag_aig_match_true_out() {
809        test_aag_aig_match(
810            b"aag 0 0 0 1 0\n1\n",
811            b"aig 0 0 0 1 0\n1\n",
812            Problem::new_aig(VarSet::new(0))
813                .with_outputs([Literal::TRUE])
814                .with_default_map(),
815        );
816    }
817
818    #[test]
819    fn aag_aig_match_in_out() {
820        test_aag_aig_match(
821            b"aag 1 1 0 1 0\n2\n2\n",
822            b"aig 1 1 0 1 0\n2\n",
823            Problem::new_aig(VarSet::new(1))
824                .with_outputs([Literal::from_input(false, 0)])
825                .with_default_map(),
826        );
827    }
828
829    #[test]
830    fn aag_aig_match_neg() {
831        test_aag_aig_match(
832            b"aag 1 1 0 1 0\n2\n3\n",
833            b"aig 1 1 0 1 0\n3\n",
834            Problem::new_aig(VarSet::new(1))
835                .with_outputs([Literal::from_input(true, 0)])
836                .with_default_map(),
837        );
838    }
839
840    #[test]
841    fn aag_aig_match_and() {
842        test_aag_aig_match(
843            b"aag 3 2 0 1 1\n2\n4\n6\n6 4 2\n",
844            b"aig 3 2 0 1 1\n6\n\x02\x02",
845            Problem::new_aig(VarSet::new(2))
846                .with_outputs([Literal::from_gate(false, 0)])
847                .with_and_gates([(Literal::from_input(false, 1), Literal::from_input(false, 0))])
848                .with_default_map(),
849        );
850    }
851
852    #[test]
853    fn aag_aig_match_or() {
854        test_aag_aig_match(
855            b"aag 3 2 0 1 1\n2\n4\n7\n6 5 3\n",
856            b"aig 3 2 0 1 1\n7\n\x01\x02",
857            Problem::new_aig(VarSet::new(2))
858                .with_outputs([Literal::from_gate(true, 0)])
859                .with_and_gates([(Literal::from_input(true, 1), Literal::from_input(true, 0))])
860                .with_default_map(),
861        );
862    }
863
864    #[test]
865    fn aag_half_adder() {
866        // Since we do not normalize the parsed AIG and also include a literal map, it
867        // is difficult to compare the ASCII and binary versions of this example
868        // directly. Hence, we have two test cases here.
869        let aag = b"aag 7 2 0 2 3\n\
870            2\n\
871            4\n\
872            6\n\
873            12\n\
874            6 13 15\n\
875            12 2 4\n\
876            14 3 5\n\
877            i0 x\n\
878            i1 y\n\
879            o0 s\n\
880            o1 c\n\
881            c\nhalf adder\n";
882        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aag).unwrap();
883
884        let map = vec![
885            Literal::FALSE,
886            Literal::from_input(false, 0),
887            Literal::from_input(false, 1),
888            Literal::from_gate(false, 0),
889            Literal::UNDEF,
890            Literal::UNDEF,
891            Literal::from_gate(false, 1),
892            Literal::from_gate(false, 2),
893        ];
894
895        let expected =
896            Problem::new_aig(VarSet::with_names(vec![Some("x".into()), Some("y".into())]))
897                .with_named_outputs([(map[6 >> 1], "s"), (map[12 >> 1], "c")])
898                .with_and_gates([
899                    (!map[13 >> 1], !map[15 >> 1]),
900                    (map[2 >> 1], map[4 >> 1]),
901                    (!map[3 >> 1], !map[5 >> 1]),
902                ])
903                .with_map(map);
904        assert_eq!(problem, expected);
905    }
906
907    #[test]
908    fn aig_half_adder() {
909        let aig = b"aig 5 2 0 2 3\n\
910            10\n\
911            6\n\
912            \x02\x02\
913            \x03\x02\
914            \x01\x02\
915            i0 x\n\
916            i1 y\n\
917            o0 s\n\
918            o1 c\n\
919            c\nhalf adder\n";
920        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aig).unwrap();
921
922        let expected =
923            Problem::new_aig(VarSet::with_names(vec![Some("x".into()), Some("y".into())]))
924                .with_named_outputs([
925                    (Literal::from_gate(false, 2), "s"),
926                    (Literal::from_gate(false, 0), "c"),
927                ])
928                .with_and_gates([
929                    (Literal::from_input(false, 1), Literal::from_input(false, 0)),
930                    (Literal::from_input(true, 1), Literal::from_input(true, 0)),
931                    (Literal::from_gate(true, 1), Literal::from_gate(true, 0)),
932                ])
933                .with_default_map();
934
935        assert_eq!(problem, expected);
936    }
937
938    #[test]
939    fn aag_aig_match_toggle() {
940        test_aag_aig_match(
941            b"aag 1 0 1 2 0\n2 3\n2\n3\n",
942            b"aig 1 0 1 2 0\n3\n2\n3\n",
943            Problem::new_aig(VarSet::new(0))
944                .with_latches([Literal::from_input(true, 0)])
945                .with_outputs([Literal::from_input(false, 0), Literal::from_input(true, 0)])
946                .with_default_map(),
947        );
948    }
949
950    #[test]
951    fn aag_toggle_with_reset() {
952        let aag = b"aag 7 2 1 2 4\n\
953            2\n\
954            4\n\
955            6 8\n\
956            6\n\
957            7\n\
958            8 4 10\n\
959            10 13 15\n\
960            12 2 6\n\
961            14 3 7\n\
962            i0 toggle\n\
963            i1 ~reset\n\
964            o0 q\n\
965            o1 ~q\n\
966            l0 q\n\
967            c foobar\n";
968        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aag).unwrap();
969
970        let mut expected = Problem::new_aig(VarSet::with_names(vec![
971            Some("toggle".into()),
972            Some("~reset".into()),
973        ]))
974        .with_latches([Literal::from_gate(false, 0)])
975        .with_named_outputs([
976            (Literal::from_input(false, 2), "q"),
977            (Literal::from_input(true, 2), "~q"),
978        ])
979        .with_and_gates([
980            (Literal::from_input(false, 1), Literal::from_gate(false, 1)),
981            (Literal::from_gate(true, 2), Literal::from_gate(true, 3)),
982            (Literal::from_input(false, 0), Literal::from_input(false, 2)),
983            (Literal::from_input(true, 0), Literal::from_input(true, 2)),
984        ])
985        .with_default_map();
986
987        expected.circuit.inputs.set_name(2, "q");
988
989        assert_eq!(problem, expected);
990    }
991
992    #[test]
993    fn aig_toggle_with_reset() {
994        let aig = b"aig 7 2 1 2 4\n\
995            14\n\
996            6\n\
997            7\n\
998            \x02\x04\
999            \x03\x04\
1000            \x01\x02\
1001            \x02\x08";
1002        let (_, problem) = super::parse::<()>(&OPTS_NO_ORDER)(aig).unwrap();
1003
1004        let expected = Problem::new_aig(VarSet::new(2))
1005            .with_latches([Literal::from_gate(false, 3)])
1006            .with_outputs([Literal::from_input(false, 2), Literal::from_input(true, 2)])
1007            .with_and_gates([
1008                (Literal::from_input(false, 2), Literal::from_input(false, 0)),
1009                (Literal::from_input(true, 2), Literal::from_input(true, 0)),
1010                (Literal::from_gate(true, 1), Literal::from_gate(true, 0)),
1011                (Literal::from_gate(false, 2), Literal::from_input(false, 1)),
1012            ])
1013            .with_default_map();
1014        assert_eq!(problem, expected);
1015    }
1016
1017    // next case taken from "AIGER 1.9 And Beyond"
1018
1019    #[test]
1020    fn aag_aig_match_bad_and_invariant() {
1021        test_aag_aig_match(
1022            b"aag 5 1 1 0 3 1 1\n\
1023            2\n\
1024            4 10 0\n\
1025            4\n\
1026            3\n\
1027            6 5 3\n\
1028            8 4 2\n\
1029            10 9 7\n",
1030            b"aig 5 1 1 0 3 1 1\n\
1031            10 0\n\
1032            4\n\
1033            3\n\
1034            \x01\x02\x04\x02\x01\x02",
1035            Problem::new_aig(VarSet::new(1))
1036                .with_latches([Literal::from_gate(false, 2)])
1037                .with_and_gates([
1038                    (Literal::from_input(true, 1), Literal::from_input(true, 0)),
1039                    (Literal::from_input(false, 1), Literal::from_input(false, 0)),
1040                    (Literal::from_gate(true, 1), Literal::from_gate(true, 0)),
1041                ])
1042                .with_bad([Literal::from_input(false, 1)])
1043                .with_invariants([Literal::from_input(true, 0)])
1044                .with_default_map(),
1045        );
1046    }
1047
1048    #[test]
1049    fn aag_aig_match_extra_properties() {
1050        // M I L O A B C J F
1051        test_aag_aig_match(
1052            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",
1053            b"aig 3 2 0 1 1 1 1 2 1\n6\n2\n3\n1\n2\n1\n4\n5\n6\n\x02\x02",
1054            Problem::new_aig(VarSet::new(2))
1055                .with_outputs([Literal::from_gate(false, 0)])
1056                .with_and_gates([(Literal::from_input(false, 1), Literal::from_input(false, 0))])
1057                .with_bad([Literal::from_input(false, 0)])
1058                .with_invariants([Literal::from_input(true, 0)])
1059                .with_justice([
1060                    [Literal::TRUE].as_slice(),
1061                    &[Literal::from_input(false, 1), Literal::from_input(true, 1)],
1062                ])
1063                .with_fairness([Literal::from_gate(false, 0)])
1064                .with_default_map(),
1065        );
1066    }
1067}
oxidd_parser/aiger.rs

oxidd_parser/
aiger.rs
