oxidd_parser/
lib.rs

1//! Collection of parsers for various logical problem formats
2//!
3//! Every format is parsed into a [`Circuit`], i.e., a propositional formula
4//! with structure sharing, to enable (mostly) uniform handling of different
5//! formats in an application.
6//!
7//! ## Example
8//!
9//! ```no_run
10//! # use oxidd_parser::*;
11//! let parse_options = ParseOptionsBuilder::default().build().unwrap();
12//! let Some(problem) = load_file("foo.dimacs", &parse_options) else {
13//!     return; // an error message has been printed to stderr
14//! };
15//! println!("circuit: {:?}", problem.circuit);
16//! println!("additional details: {:?}", problem.details);
17//! ```
18//!
19//! ## Feature flags
20#![doc = document_features::document_features!()]
21#![forbid(unsafe_code)]
22#![warn(missing_docs)]
23#![allow(clippy::type_complexity)]
24
25use std::collections::hash_map::Entry;
26use std::fmt::{self, Write};
27
28use bumpalo::boxed::Box as BumpBox;
29use bumpalo::collections::Vec as BumpVec;
30use derive_builder::Builder;
31use fixedbitset::FixedBitSet;
32use rustc_hash::FxHashMap;
33
34pub mod aiger;
35pub mod dimacs;
36pub mod nnf;
37mod tv_bitvec;
38mod util;
39mod vec2d;
40
41use tv_bitvec::TVBitVec;
42pub use vec2d::{Vec2d, Vec2dIter};
43
44#[cfg(feature = "load-file")]
45mod load_file;
46#[cfg(feature = "load-file")]
47pub use load_file::*;
48
49/// Variable type
50///
51/// The two most significant bits are never set.
52pub type Var = usize;
53
54/// A possibly negated variable
55///
56/// There are three kinds of variables: constants ([`Literal::FALSE`] and
57/// [`Literal::TRUE`]), circuit inputs, and gates.
58///
59/// Concerning ordering, the following properties hold: Given two [`Literal`]s
60/// `a, b`, `a <= b` is equivalent to the lexicographic comparison
61/// `(a.positive(), a.is_negative()) <= (b.positive(), b.is_negative())`.
62/// Furthermore, `Literal::FALSE <= a` holds (and thus `Literal::TRUE <= a` if
63/// `a != Literal::FALSE`).
64#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
65pub struct Literal(usize);
66
67impl Literal {
68    // We rely on POLARITY_BIT being the least significant bit for the ordering
69    const POLARITY_BIT: u32 = 0;
70    const GATE_BIT: u32 = 1;
71    const VAR_LSB: u32 = 2;
72
73    /// Maximum input number representable as literal
74    pub const MAX_INPUT: usize = (usize::MAX >> Self::VAR_LSB) - 2;
75    /// Maximum gate number representable as literal
76    pub const MAX_GATE: usize = usize::MAX >> Self::VAR_LSB;
77
78    /// Literal representing the constant `⊥`
79    ///
80    /// This is literal is considered to be positive (i.e., not negated):
81    ///
82    /// ```
83    /// # use oxidd_parser::Literal;
84    /// assert!(Literal::FALSE.is_positive());
85    /// assert!(Literal::FALSE < Literal::TRUE);
86    /// ```
87    pub const FALSE: Self = Self(0);
88    /// Literal representing the constant `⊤`
89    ///
90    /// This is literal is considered to be negated:
91    ///
92    /// ```
93    /// # use oxidd_parser::Literal;
94    /// assert!(Literal::TRUE.is_negative());
95    /// assert!(Literal::TRUE < Literal::from_input(false, 0));
96    /// assert!(Literal::TRUE < Literal::from_gate(false, 0));
97    /// ```
98    pub const TRUE: Self = Self(1 << Self::POLARITY_BIT);
99
100    /// Undefined literal
101    ///
102    /// This is considered to be a positive (i.e., not negated) input, but its
103    /// variable number is larger than `Self::MAX_INPUT`. Attempting to create
104    /// this literal using [`Self::from_input()`] will trigger a debug
105    /// assertion.
106    ///
107    /// ```
108    /// # use oxidd_parser::Literal;
109    /// assert!(Literal::UNDEF.is_positive());
110    /// assert!(Literal::UNDEF.is_input());
111    /// assert_eq!(Literal::UNDEF.get_input(), Some(Literal::MAX_INPUT + 1));
112    /// ```
113    pub const UNDEF: Self = Self((Self::MAX_INPUT + 2) << Self::VAR_LSB);
114
115    /// Create a new literal from an input variable
116    #[track_caller]
117    #[inline]
118    pub const fn from_input(negative: bool, input: Var) -> Self {
119        debug_assert!(input <= Self::MAX_INPUT, "input too large");
120        Self(((input + 1) << Self::VAR_LSB) | ((negative as usize) << Self::POLARITY_BIT))
121    }
122
123    /// Create a new literal from an input variable (value range `1..`) or false
124    /// (`0`)
125    #[track_caller]
126    #[inline]
127    const fn from_input_or_false(negative: bool, input: Var) -> Self {
128        debug_assert!(input <= Self::MAX_INPUT + 1, "input too large");
129        Self((input << Self::VAR_LSB) | ((negative as usize) << Self::POLARITY_BIT))
130    }
131
132    /// Create a new literal from a gate number
133    #[track_caller]
134    #[inline]
135    pub const fn from_gate(negative: bool, gate: Var) -> Self {
136        debug_assert!(gate <= Self::MAX_GATE, "gate number too large");
137        Self(
138            (gate << Self::VAR_LSB)
139                | (1 << Self::GATE_BIT)
140                | ((negative as usize) << Self::POLARITY_BIT),
141        )
142    }
143
144    /// Is the literal positive?
145    ///
146    /// Same as [`!self.is_negative()`][Self::is_negative]
147    ///
148    /// ```
149    /// # use oxidd_parser::Literal;
150    /// assert!(Literal::from_input(false, 42).is_positive());
151    /// assert!(!Literal::from_input(true, 1337).is_positive());
152    /// ```
153    #[inline(always)]
154    pub const fn is_positive(self) -> bool {
155        self.0 & (1 << Self::POLARITY_BIT) == 0
156    }
157    /// Is the literal negative?
158    ///
159    /// Same as [`!self.is_positive()`][Self::is_positive]
160    ///
161    /// ```
162    /// # use oxidd_parser::Literal;
163    /// assert!(Literal::from_gate(true, 42).is_negative());
164    /// assert!(!Literal::from_gate(false, 1337).is_negative());
165    /// ```
166    #[inline(always)]
167    pub const fn is_negative(self) -> bool {
168        !self.is_positive()
169    }
170
171    /// Get the positive variant of this literal
172    ///
173    /// ```
174    /// # use oxidd_parser::Literal;
175    /// assert!(Literal::from_input(true, 42).positive().is_positive());
176    /// ```
177    #[inline(always)]
178    pub const fn positive(self) -> Self {
179        Self(self.0 & !(1 << Self::POLARITY_BIT))
180    }
181
182    /// Get the negative variant of this literal
183    ///
184    /// ```
185    /// # use oxidd_parser::Literal;
186    /// assert_eq!(Literal::from_input(true, 42), Literal::from_input(false, 42).negative());
187    /// assert!(Literal::from_input(false, 42).negative().is_negative());
188    /// ```
189    #[inline(always)]
190    pub const fn negative(self) -> Self {
191        Self(self.0 | (1 << Self::POLARITY_BIT))
192    }
193
194    /// Does this literal refer to an input?
195    ///
196    /// ```
197    /// # use oxidd_parser::Literal;
198    /// assert!(Literal::from_input(false, 42).is_input());
199    /// assert!(!Literal::FALSE.is_input());
200    /// assert!(!Literal::TRUE.is_input());
201    /// assert!(!Literal::from_gate(false, 1337).is_input());
202    /// ```
203    #[inline(always)]
204    pub const fn is_input(self) -> bool {
205        self.get_input().is_some()
206    }
207
208    /// Check if this literal refers to a gate
209    ///
210    /// ```
211    /// # use oxidd_parser::Literal;
212    /// assert!(Literal::from_gate(false, 42).is_gate());
213    /// assert!(!Literal::FALSE.is_gate());
214    /// assert!(!Literal::TRUE.is_gate());
215    /// assert!(!Literal::from_input(false, 1337).is_gate());
216    /// ```
217    #[inline(always)]
218    pub const fn is_gate(self) -> bool {
219        self.0 & (1 << Self::GATE_BIT) != 0
220    }
221
222    /// Get the input number (if this literal refers to an input)
223    ///
224    /// ```
225    /// # use oxidd_parser::Literal;
226    /// assert_eq!(Literal::from_input(false, 42).get_input(), Some(42));
227    /// assert_eq!(Literal::FALSE.get_input(), None);
228    /// assert_eq!(Literal::TRUE.get_input(), None);
229    /// assert_eq!(Literal::from_gate(false, 42).get_input(), None);
230    /// ```
231    #[inline]
232    pub const fn get_input(self) -> Option<Var> {
233        if self.is_gate() {
234            return None;
235        }
236        (self.0 >> Self::VAR_LSB).checked_sub(1)
237    }
238
239    /// Get the gate number (if this literal refers to an input)
240    ///
241    /// ```
242    /// # use oxidd_parser::Literal;
243    /// assert_eq!(Literal::from_gate(false, 42).get_gate_no(), Some(42));
244    /// assert_eq!(Literal::FALSE.get_gate_no(), None);
245    /// assert_eq!(Literal::TRUE.get_gate_no(), None);
246    /// assert_eq!(Literal::from_input(false, 42).get_gate_no(), None);
247    /// ```
248    ///
249    /// See also: [`Circuit::gate()`]
250    #[inline]
251    pub const fn get_gate_no(self) -> Option<Var> {
252        if self.is_gate() {
253            return Some(self.0 >> Self::VAR_LSB);
254        }
255        None
256    }
257
258    /// Map this literal based on `gate_map`
259    ///
260    /// If this literal refers to a gate, the method performs a lookup for the
261    /// gate number in `gate_map`. If the gate number is in bounds, the return
262    /// value is the mapped literal with its sign adjusted, otherwise the return
263    /// value is [`Literal::UNDEF`]. Non-gate literals are returned as they are.
264    #[inline]
265    pub fn apply_gate_map(self, gate_map: &[Literal]) -> Self {
266        if let Some(gate) = self.get_gate_no() {
267            if let Some(mapped) = gate_map.get(gate) {
268                *mapped ^ self.is_negative()
269            } else {
270                Self::UNDEF
271            }
272        } else {
273            self
274        }
275    }
276}
277
278impl fmt::Display for Literal {
279    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
280        let i = self.0 >> Literal::VAR_LSB;
281        let (kind, i) = if self.0 & (1 << Self::GATE_BIT) != 0 {
282            ('g', i)
283        } else {
284            if i == 0 {
285                return f.write_char(if self.is_positive() { '⊤' } else { '⊥' });
286            }
287            if i == Literal::MAX_INPUT + 2 {
288                return f.write_str(if self.is_positive() { "+U" } else { "-U" });
289            }
290            ('i', i - 1)
291        };
292
293        let sign = if self.is_positive() { '+' } else { '-' };
294        write!(f, "{sign}{kind}{i}")
295    }
296}
297impl fmt::Debug for Literal {
298    #[inline(always)]
299    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
300        <Self as fmt::Display>::fmt(self, f)
301    }
302}
303
304impl std::ops::Not for Literal {
305    type Output = Self;
306
307    fn not(self) -> Self {
308        Self(self.0 ^ (1 << Self::POLARITY_BIT))
309    }
310}
311
312impl std::ops::BitXor<bool> for Literal {
313    type Output = Self;
314
315    #[inline(always)]
316    fn bitxor(self, rhs: bool) -> Self::Output {
317        Self(self.0 ^ ((rhs as usize) << Self::POLARITY_BIT))
318    }
319}
320
321/// Rooted tree with values of type `T` at the leaves
322#[allow(missing_docs)]
323#[derive(Clone, PartialEq, Eq, Debug)]
324pub enum Tree<T> {
325    Inner(Box<[Tree<T>]>),
326    Leaf(T),
327}
328
329impl<T: Clone> Tree<T> {
330    fn flatten_into(&self, into: &mut Vec<T>) {
331        match self {
332            Tree::Inner(sub) => sub.iter().for_each(|t| t.flatten_into(into)),
333            Tree::Leaf(v) => into.push(v.clone()),
334        }
335    }
336}
337
338/// Problem that may be returned by the problem parsers
339#[derive(Clone, PartialEq, Eq, Debug)]
340pub struct Problem {
341    /// Combinational circuit as the core of the problem
342    pub circuit: Circuit,
343
344    /// Additional details on the problem
345    pub details: ProblemDetails,
346}
347
348impl Problem {
349    /// Simplify the circuit (see [`Circuit::simplify()`]), and map the gate
350    /// literals in the additional problem details accordingly
351    ///
352    /// If the reachable circuit fragment contains a cycle, this method returns
353    /// `Err(l)`, where `l` represents a gate that is part of the cycle.
354    ///
355    /// On success, `simplify()` returns the simplified problem along with a
356    /// `Vec<Literal>` which maps the gates of `self` to literals valid in the
357    /// simplified circuit. The simplified circuit only contains gates reachable
358    /// from the problem details (except for the
359    /// [AIGER literal map][AIGERDetails::map_aiger_literal]).
360    pub fn simplify(&self) -> Result<(Self, Vec<Literal>), Literal> {
361        let (circuit, map) = match &self.details {
362            ProblemDetails::Root(l) => self.circuit.simplify([*l]),
363            ProblemDetails::AIGER(aig) => {
364                let aig = &**aig;
365                self.circuit.simplify(
366                    aig.latches
367                        .iter()
368                        .chain(aig.outputs.iter())
369                        .chain(aig.bad.iter())
370                        .chain(aig.invariants.iter())
371                        .chain(aig.justice.all_elements().iter())
372                        .chain(aig.fairness.iter())
373                        .copied(),
374                )
375            }
376        }?;
377        let new_problem = Self {
378            circuit,
379            details: self.details.apply_gate_map(&map),
380        };
381        Ok((new_problem, map))
382    }
383}
384
385/// Details of a [`Problem`] in addition to the circuit structure
386#[derive(Clone, PartialEq, Eq, Debug)]
387pub enum ProblemDetails {
388    /// Simple circuit with a single root
389    Root(Literal),
390    /// Details from the AIGER format
391    AIGER(Box<AIGERDetails>),
392}
393
394impl ProblemDetails {
395    /// Map the literals in `self` based on `gate_map`
396    ///
397    /// See [`Literal::apply_gate_map()`] for more details.
398    pub fn apply_gate_map(&self, map: &[Literal]) -> Self {
399        match self {
400            ProblemDetails::Root(l) => ProblemDetails::Root(l.apply_gate_map(map)),
401            ProblemDetails::AIGER(aig) => ProblemDetails::AIGER(Box::new(aig.apply_gate_map(map))),
402        }
403    }
404
405    /// In-place version of [`Self::apply_gate_map()`]
406    pub fn apply_gate_map_in_place(&mut self, map: &[Literal]) {
407        match self {
408            ProblemDetails::Root(l) => *l = l.apply_gate_map(map),
409            ProblemDetails::AIGER(aig) => aig.apply_gate_map_in_place(map),
410        }
411    }
412}
413
414/// Variable set, potentially along with a variable order and variable names
415///
416/// The variable numbers are in range `0..self.len()`.
417#[derive(Clone, PartialEq, Eq, Debug)]
418pub struct VarSet {
419    /// Number of variables
420    len: usize,
421
422    /// Permutation of the variables. `order[0]` is supposed to be the number of
423    /// the top-most variable.
424    order: Vec<Var>,
425    /// If present, `order` is just the flattened tree
426    order_tree: Option<Tree<Var>>,
427
428    /// Mapping from variable numbers to optional names. Has minimal length,
429    /// i.e., `names.last() != Some(&None)`.
430    names: Vec<Option<String>>,
431}
432
433impl VarSet {
434    /// Create a variable set without a variable order and names
435    #[inline(always)]
436    pub const fn new(n: usize) -> Self {
437        Self {
438            len: n,
439            order: Vec::new(),
440            order_tree: None,
441            names: Vec::new(),
442        }
443    }
444
445    /// Create a variable set with the given names
446    ///
447    /// The number of variables is given by `names.len()`.
448    pub fn with_names(mut names: Vec<Option<String>>) -> Self {
449        let len = names.len();
450        while let Some(None) = names.last() {
451            names.pop();
452        }
453        Self {
454            len,
455            order: Vec::new(),
456            order_tree: None,
457            names,
458        }
459    }
460
461    /// Number of variables
462    #[inline(always)]
463    pub fn len(&self) -> usize {
464        self.len
465    }
466
467    /// Returns true iff the number of variables is 0
468    #[inline(always)]
469    pub fn is_empty(&self) -> bool {
470        self.len == 0
471    }
472
473    /// Get the linear variable order, if present
474    ///
475    /// The order is given as a mapping from positions to variables.
476    ///
477    /// If [`self.order_tree()`][Self::order_tree] is not `None`, then it is the
478    /// flattened tree.
479    #[inline]
480    pub fn order(&self) -> Option<&[Var]> {
481        if self.len != self.order.len() {
482            None
483        } else {
484            Some(&self.order)
485        }
486    }
487
488    /// Get the tree of variable groups, if present
489    ///
490    /// This may be useful for, e.g., group sifting.
491    #[inline]
492    pub fn order_tree(&self) -> Option<&Tree<Var>> {
493        self.order_tree.as_ref()
494    }
495
496    /// Returns `true` if any variable has a name
497    #[inline]
498    pub fn has_names(&self) -> bool {
499        !self.names.is_empty()
500    }
501
502    /// Get the name for variable `var`
503    #[inline]
504    pub fn name(&self, var: Var) -> Option<&str> {
505        self.names.get(var)?.as_deref()
506    }
507    /// Set the name for variable `var`. Returns the previous name.
508    #[track_caller]
509    pub fn set_name(&mut self, var: Var, name: impl Into<String>) -> Option<String> {
510        if var >= self.names.len() {
511            if var >= self.len {
512                return None;
513            }
514            self.names.resize(var + 1, None);
515        }
516        self.names[var].replace(name.into())
517    }
518
519    #[allow(unused)]
520    fn check_valid(&self) {
521        assert!(self.order.is_empty() || self.order.len() == self.len);
522        assert!(!self.order.is_empty() || self.order_tree.is_none());
523        assert_ne!(self.names.last(), Some(&None));
524    }
525}
526
527type GateVec2d = vec2d::with_metadata::Vec2d<Literal, { Circuit::GATE_METADATA_BITS }>;
528
529/// Combinational circuit with negation as well as n-ary AND, OR, and XOR gates
530#[derive(Clone, PartialEq, Eq)]
531pub struct Circuit {
532    inputs: VarSet,
533    gates: GateVec2d,
534}
535
536/// Logical gate including the literals representing its inputs
537///
538/// This enum type includes the phony gate variants `False` (representing the
539/// constant false) and `Input` (for a circuit input). This is mainly to make
540/// using [`Circuit::gate()`] more ergonomic.
541#[allow(missing_docs)]
542#[derive(Clone, Copy, PartialEq, Eq)]
543pub struct Gate<'a> {
544    pub kind: GateKind,
545    pub inputs: &'a [Literal],
546}
547
548impl fmt::Debug for Gate<'_> {
549    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
550        let mut builder = f.debug_tuple(match self.kind {
551            GateKind::And => "and",
552            GateKind::Or => "or",
553            GateKind::Xor => "xor",
554        });
555        for literal in self.inputs {
556            builder.field(literal);
557        }
558        builder.finish()
559    }
560}
561
562#[allow(unused)] // used in tests
563impl<'a> Gate<'a> {
564    const fn and(inputs: &'a [Literal]) -> Self {
565        Self {
566            kind: GateKind::And,
567            inputs,
568        }
569    }
570    const fn or(inputs: &'a [Literal]) -> Self {
571        Self {
572            kind: GateKind::Or,
573            inputs,
574        }
575    }
576    const fn xor(inputs: &'a [Literal]) -> Self {
577        Self {
578            kind: GateKind::Xor,
579            inputs,
580        }
581    }
582}
583
584/// Kind of a logical gate in a [`Circuit`]
585#[allow(missing_docs)]
586#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
587pub enum GateKind {
588    And,
589    Or,
590    Xor,
591}
592
593impl GateKind {
594    /// Get the literal representing a gate of this kind without any inputs
595    const fn empty_gate(self) -> Literal {
596        match self {
597            GateKind::And => Literal::TRUE,
598            GateKind::Or | GateKind::Xor => Literal::FALSE,
599        }
600    }
601}
602
603impl From<usize> for GateKind {
604    fn from(value: usize) -> Self {
605        match value {
606            _ if value == GateKind::And as usize => GateKind::And,
607            _ if value == GateKind::Or as usize => GateKind::Or,
608            _ => GateKind::Xor,
609        }
610    }
611}
612
613impl Circuit {
614    const GATE_METADATA_BITS: u32 = 2;
615
616    /// Create an empty circuit with the given circuit inputs
617    #[inline(always)]
618    pub fn new(inputs: VarSet) -> Self {
619        Self {
620            inputs,
621            gates: Default::default(),
622        }
623    }
624
625    /// Get the circuit inputs
626    #[inline(always)]
627    pub fn inputs(&self) -> &VarSet {
628        &self.inputs
629    }
630    /// Get a mutable reference to the circuit inputs
631    #[inline(always)]
632    pub fn inputs_mut(&mut self) -> &mut VarSet {
633        &mut self.inputs
634    }
635
636    /// Reserve space for at least `additional` more gates. Note that this will
637    /// not reserve space for gate inputs. To that end, use
638    /// [`Self::reserve_gate_inputs()`].
639    ///
640    /// This is essentially a wrapper around [`Vec::reserve()`], so the
641    /// documentation there provides more details.
642    #[inline(always)]
643    pub fn reserve_gates(&mut self, additional: usize) {
644        self.gates.reserve_vectors(additional);
645    }
646
647    /// Reserve space for at least `additional` more gate inputs (the space is
648    /// shared between all gates). Note that this will not reserve space for
649    /// the gate metadata. To that end, use [`Self::reserve_gates()`].
650    ///
651    /// This is essentially a wrapper around [`Vec::reserve()`], so the
652    /// documentation there provides more details.
653    #[inline(always)]
654    pub fn reserve_gate_inputs(&mut self, additional: usize) {
655        self.gates.reserve_elements(additional);
656    }
657
658    /// Get the number of gates in this circuit
659    #[inline(always)]
660    pub fn num_gates(&self) -> usize {
661        self.gates.len()
662    }
663
664    /// Get the [`Gate`] for `literal`
665    ///
666    /// Returns [`None`] iff `literal` refers to a constant, a circuit input, or
667    /// a gate that is not present in this circuit.
668    ///
669    /// See also: [`Self::gate_for_no()`]
670    #[inline]
671    pub fn gate(&self, literal: Literal) -> Option<Gate<'_>> {
672        self.gate_for_no(literal.get_gate_no()?)
673    }
674
675    /// Get the [`Gate`] for `gate_no`
676    ///
677    /// Returns [`None`] iff `literal` refers to a gate that is not present in
678    /// this circuit.
679    ///
680    /// See also: [`Self::gate()`]
681    pub fn gate_for_no(&self, gate_no: Var) -> Option<Gate<'_>> {
682        if let Some((kind, inputs)) = self.gates.get(gate_no) {
683            Some(Gate {
684                kind: kind.into(),
685                inputs,
686            })
687        } else {
688            None
689        }
690    }
691
692    /// Get a mutable reference to the gate inputs
693    ///
694    /// Returns [`None`] iff `literal` refers to a constant, a circuit input, or
695    /// a gate that is not present in this circuit.
696    #[inline]
697    pub fn gate_inputs_mut(&mut self, literal: Literal) -> Option<&mut [Literal]> {
698        self.gates.get_mut(literal.get_gate_no()?)
699    }
700
701    /// Get a mutable reference to the gate inputs
702    ///
703    /// Returns [`None`] iff `literal` refers to a constant, a circuit input, or
704    /// a gate that is not present in this circuit.
705    #[inline(always)]
706    pub fn gate_inputs_mut_for_no(&mut self, gate_no: Var) -> Option<&mut [Literal]> {
707        self.gates.get_mut(gate_no)
708    }
709
710    /// Set the kind of the gate referenced by `literal`
711    ///
712    /// Panics if `literal` does not refer to a gate in this circuit.
713    #[track_caller]
714    #[inline]
715    pub fn set_gate_kind(&mut self, literal: Literal, kind: GateKind) {
716        self.gates.set_metadata(
717            literal
718                .get_gate_no()
719                .expect("`literal` must refer to a gate"),
720            kind as usize,
721        );
722    }
723
724    /// Set the kind of the gate referenced by `gate_no`
725    ///
726    /// Panics if `literal` does not refer to a gate in this circuit.
727    #[track_caller]
728    #[inline(always)]
729    pub fn set_gate_kind_for_no(&mut self, gate_no: Var, kind: GateKind) {
730        self.gates.set_metadata(gate_no, kind as usize);
731    }
732
733    /// Set the kind of the gate referenced by `literal`
734    ///
735    /// Panics if the circuit is empty.
736    #[track_caller]
737    #[inline]
738    pub fn set_last_gate_kind(&mut self, kind: GateKind) {
739        let n = self.gates.len();
740        if n == 0 {
741            panic!("there are no gates in the circuit");
742        }
743        self.gates.set_metadata(n - 1, kind as usize);
744    }
745
746    /// Get the first gate
747    ///
748    /// Returns [`None`] iff `literal` refers to a constant, a circuit input, or
749    /// a gate that is not present in this circuit.
750    pub fn first_gate(&self) -> Option<Gate<'_>> {
751        let (kind, inputs) = self.gates.first()?;
752        Some(Gate {
753            kind: kind.into(),
754            inputs,
755        })
756    }
757
758    /// Get the last gate
759    ///
760    /// Returns [`None`] iff `literal` refers to a constant, a circuit input, or
761    /// a gate that is not present in this circuit.
762    pub fn last_gate(&self) -> Option<Gate<'_>> {
763        let (kind, inputs) = self.gates.last()?;
764        Some(Gate {
765            kind: kind.into(),
766            inputs,
767        })
768    }
769
770    /// Create a new empty gate at the end of the sequence
771    pub fn push_gate(&mut self, kind: GateKind) -> Literal {
772        let l = Literal::from_gate(false, self.gates.len());
773        self.gates.push_vec(kind as _);
774        l
775    }
776
777    /// Remove the last gate (if there is one)
778    ///
779    /// Returns true iff the number of gates was positive before removal.
780    #[inline(always)]
781    pub fn pop_gate(&mut self) -> bool {
782        self.gates.pop_vec()
783    }
784
785    /// Add an input to the last gate
786    ///
787    /// There must be already one gate in the circuit, otherwise this method
788    /// triggers a debug assertion or does not do anything, respectively.
789    #[inline(always)]
790    #[track_caller]
791    pub fn push_gate_input(&mut self, literal: Literal) {
792        self.gates.push_element(literal);
793    }
794
795    /// Add inputs to the last gate
796    ///
797    /// There must be already one gate in the circuit, otherwise this method
798    /// triggers a debug assertion or does not do anything, respectively.
799    #[inline(always)]
800    #[track_caller]
801    pub fn push_gate_inputs(&mut self, literals: impl IntoIterator<Item = Literal>) {
802        self.gates.push_elements(literals);
803    }
804
805    /// Iterate over all gates in the circuit
806    ///
807    /// The iteration order is from first to last in the gate sequence.
808    #[inline(always)]
809    pub fn iter_gates(&self) -> CircuitGateIter<'_> {
810        CircuitGateIter(self.gates.iter())
811    }
812
813    /// Retain the gates for which `predicate` returns `true`
814    ///
815    /// Note that removing one gate changes the gate numbers of all subsequent
816    /// gates, but this method does not automatically update the gate inputs.
817    #[inline]
818    pub fn retain_gates(&mut self, mut predicate: impl FnMut(&mut [Literal]) -> bool) {
819        self.gates.retain(move |_, inputs| predicate(inputs))
820    }
821
822    /// Remove all gate definitions from the circuit
823    #[inline(always)]
824    pub fn clear_gates(&mut self) {
825        self.gates.clear();
826    }
827
828    /// Check if this circuit is acyclic
829    ///
830    /// Returns [`None`] if acyclic, or [`Some(literal)`][Some] if `literal`
831    /// depends on itself.
832    pub fn find_cycle(&self) -> Option<Literal> {
833        let mut visited = FixedBitSet::with_capacity(self.gates.len() * 2);
834
835        fn inner(gates: &GateVec2d, visited: &mut FixedBitSet, index: usize) -> bool {
836            if visited.contains(index * 2 + 1) {
837                return false; // finished
838            }
839            if visited.contains(index * 2) {
840                return true; // discovered -> cycle
841            }
842            visited.insert(index * 2); // discovered
843
844            for &l in gates.get(index).unwrap().1 {
845                if l.is_gate() && inner(gates, visited, l.0 >> Literal::VAR_LSB) {
846                    return true;
847                }
848            }
849
850            visited.insert(index * 2 + 1); // finished
851            false
852        }
853
854        for index in 0..self.gates.len() {
855            if inner(&self.gates, &mut visited, index) {
856                return Some(Literal::from_gate(false, index));
857            }
858        }
859        None
860    }
861
862    /// Simplify the circuit such that
863    ///
864    /// 1. no gate has constant inputs
865    /// 2. no inputs of XOR gates are negated (only the output)
866    /// 3. for every gate, all its inputs are distinct (disregarding polarities)
867    /// 4. all gates have at least two inputs
868    /// 5. there are no two structurally equivalent gates (same kind and inputs,
869    ///    disregarding the input order)
870    ///
871    /// Additionally, the new circuit will only contain gates reachable from
872    /// `roots`. The order of gate inputs in the resulting circuit follows the
873    /// order of the first discovered equivalent gate (with duplicates etc.
874    /// removed).
875    ///
876    /// If the reachable circuit fragment contains a cycle, this method returns
877    /// `Err(l)`, where `l` represents a gate that is part of the cycle.
878    /// Likewise, if the reachable fragment depends on unknown inputs
879    /// (`input_number >= self.inputs().len()`, including [`Literal::UNDEF`]),
880    /// the return value is `Err(l)`, where `l` is the unknown literal.
881    ///
882    /// On success, the gates in the returned circuit are topologically sorted.
883    /// The additional `Vec<Literal>` maps the gates of `self` to literals valid
884    /// in the simplified circuit.
885    ///
886    /// Hint: [`Problem::simplify()`] uses this method to simplify the circuit
887    /// and also maps the literals in the problem details accordingly.
888    pub fn simplify(
889        &self,
890        roots: impl IntoIterator<Item = Literal>,
891    ) -> Result<(Self, Vec<Literal>), Literal> {
892        const DISCOVERED: Literal = Literal::UNDEF.negative();
893
894        let bump = bumpalo::Bump::new();
895        let mut gate_map = Vec::new();
896        gate_map.resize(self.gates.len(), Literal::UNDEF);
897        // Whether a non-constant literal (hence 2 * vars) is an input to the
898        // current gate
899        let mut input_set = FixedBitSet::with_capacity(2 * (self.gates.len() + self.inputs.len()));
900        let mut new_gates: GateVec2d =
901            GateVec2d::with_capacity(self.gates.len(), self.gates.all_elements().len());
902        let mut unique_map = FxHashMap::default();
903        unique_map.reserve(self.gates.len());
904
905        fn inner<'a>(
906            bump: &'a bumpalo::Bump,
907            gates: &GateVec2d,
908            index: usize,
909            input_set: &mut FixedBitSet,
910            unique_map: &mut FxHashMap<(GateKind, BumpBox<'a, [Literal]>), Literal>,
911            new_gates: &mut GateVec2d,
912            gate_map: &mut [Literal],
913        ) -> Result<(), Literal> {
914            if gate_map[index] == DISCOVERED {
915                // discovered -> cycle
916                return Err(Literal::from_gate(false, index));
917            }
918            if gate_map[index] != Literal::UNDEF {
919                return Ok(()); // finished
920            }
921            gate_map[index] = DISCOVERED;
922
923            let (meta, inputs) = gates.get(index).unwrap();
924            let kind = GateKind::from(meta);
925
926            for &l in inputs {
927                if let Some(gate) = l.get_gate_no() {
928                    inner(
929                        bump, gates, gate, input_set, unique_map, new_gates, gate_map,
930                    )?;
931                }
932            }
933
934            // apply `gate_map` to the inputs and establish conditions 1+2
935            let mut neg_out = false;
936            let mut mapped = BumpVec::with_capacity_in(inputs.len(), bump);
937            let known_inputs = input_set.len() - gates.len();
938            match kind {
939                GateKind::And | GateKind::Or => {
940                    let (identity, dominator) = match kind {
941                        GateKind::And => (Literal::TRUE, Literal::FALSE),
942                        GateKind::Or => (Literal::FALSE, Literal::TRUE),
943                        _ => unreachable!(),
944                    };
945                    for &l in inputs {
946                        let l = l.get_gate_no().map_or(l, |i| gate_map[i] ^ l.is_negative());
947                        if l.is_input() && l.get_input().unwrap() > known_inputs {
948                            return Err(l);
949                        }
950                        if l == dominator {
951                            gate_map[index] = dominator;
952                            return Ok(());
953                        }
954                        if l != identity {
955                            mapped.push(l);
956                        }
957                    }
958                }
959                GateKind::Xor => {
960                    for &l in inputs {
961                        neg_out ^= l.is_negative(); // negate for every flip
962                        let l = if let Some(i) = l.get_gate_no() {
963                            let l = gate_map[i];
964                            neg_out ^= l.is_negative();
965                            l.positive()
966                        } else {
967                            let l = l.positive();
968                            debug_assert!(l != Literal::TRUE);
969                            if l == Literal::FALSE {
970                                continue; // x ⊕ ⊥ ≡ x
971                            }
972                            l
973                        };
974                        if l.is_input() && l.get_input().unwrap() > known_inputs {
975                            return Err(l);
976                        }
977                        mapped.push(l);
978                    }
979                }
980            };
981            let mut inputs = mapped;
982
983            // first part of condition 4
984            if inputs.is_empty() {
985                gate_map[index] = match kind {
986                    GateKind::And => Literal::TRUE,
987                    GateKind::Or => Literal::FALSE,
988                    GateKind::Xor => Literal::TRUE ^ neg_out,
989                };
990                return Ok(());
991            }
992
993            // condition 3 with fast-path for exactly two different inputs
994            if inputs.len() >= 3
995                || (inputs.len() == 2 && inputs[0].negative() == inputs[1].negative())
996            {
997                let no_gate_add = 2 * gates.len() - 2; // -2 for constants
998                let map = move |l: Literal| {
999                    const { assert!(Literal::POLARITY_BIT == 0) };
1000                    let i = ((l.0 >> Literal::VAR_LSB) << 1) | (l.0 & (1 << Literal::POLARITY_BIT));
1001                    if l.is_gate() {
1002                        i
1003                    } else {
1004                        i + no_gate_add
1005                    }
1006                };
1007
1008                match kind {
1009                    GateKind::And | GateKind::Or => {
1010                        for (i, &l) in inputs.iter().enumerate() {
1011                            if input_set.contains(map(!l)) {
1012                                // found complement literal -> clear `input_set` and return ⊥/⊤
1013                                for &l in &inputs[..i] {
1014                                    input_set.remove(map(l));
1015                                }
1016                                gate_map[index] = match kind {
1017                                    GateKind::And => Literal::FALSE, // x ∧ ¬x ≡ ⊥
1018                                    GateKind::Or => Literal::TRUE,   // x ∨ ¬x ≡ ⊤
1019                                    _ => unreachable!(),
1020                                };
1021                                return Ok(());
1022                            }
1023                            input_set.insert(map(l));
1024                        }
1025                    }
1026                    GateKind::Xor => {
1027                        for &l in &inputs {
1028                            let i = map(l);
1029                            input_set.toggle(i);
1030                        }
1031                    }
1032                }
1033
1034                inputs.retain(|&l| {
1035                    let i = map(l);
1036                    if input_set.contains(i) {
1037                        input_set.remove(i);
1038                        true
1039                    } else {
1040                        false
1041                    }
1042                });
1043            }
1044            // second part of condition 4
1045            if let [l] = &inputs[..] {
1046                gate_map[index] = *l ^ neg_out;
1047                return Ok(());
1048            }
1049
1050            // save the children in the current order and sort
1051            let new_gate_no = new_gates.len();
1052            new_gates.push_vec(kind as usize);
1053            new_gates.push_elements(inputs.iter().copied());
1054            inputs.sort_unstable();
1055
1056            let l = match unique_map.entry((kind, inputs.into_boxed_slice())) {
1057                Entry::Occupied(e) => {
1058                    new_gates.pop_vec();
1059                    *e.get()
1060                }
1061                Entry::Vacant(e) => *e.insert(Literal::from_gate(false, new_gate_no)),
1062            };
1063            gate_map[index] = l ^ neg_out;
1064
1065            Ok(())
1066        }
1067
1068        for root in roots {
1069            if let Some(i) = root.get_gate_no() {
1070                inner(
1071                    &bump,
1072                    &self.gates,
1073                    i,
1074                    &mut input_set,
1075                    &mut unique_map,
1076                    &mut new_gates,
1077                    &mut gate_map,
1078                )?;
1079            }
1080        }
1081
1082        let new_circuit = Self {
1083            inputs: self.inputs.clone(),
1084            gates: new_gates,
1085        };
1086        Ok((new_circuit, gate_map))
1087    }
1088}
1089
1090/// Iterator returned by [`Circuit::iter_gates()`]
1091#[derive(Clone)]
1092pub struct CircuitGateIter<'a>(
1093    vec2d::with_metadata::Vec2dIter<'a, Literal, { Circuit::GATE_METADATA_BITS }>,
1094);
1095
1096impl<'a> Iterator for CircuitGateIter<'a> {
1097    type Item = Gate<'a>;
1098
1099    #[inline]
1100    fn next(&mut self) -> Option<Self::Item> {
1101        let (kind, inputs) = self.0.next()?;
1102        Some(Gate {
1103            kind: kind.into(),
1104            inputs,
1105        })
1106    }
1107
1108    #[inline(always)]
1109    fn size_hint(&self) -> (usize, Option<usize>) {
1110        self.0.size_hint()
1111    }
1112}
1113
1114impl ExactSizeIterator for CircuitGateIter<'_> {
1115    #[inline(always)]
1116    fn len(&self) -> usize {
1117        self.0.len()
1118    }
1119}
1120
1121impl fmt::Debug for CircuitGateIter<'_> {
1122    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1123        f.debug_list().entries(self.clone()).finish()
1124    }
1125}
1126
1127impl fmt::Debug for Circuit {
1128    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1129        f.debug_struct("Circuit")
1130            .field("inputs", &self.inputs)
1131            .field("gates", &self.iter_gates())
1132            .finish()
1133    }
1134}
1135
1136/// Problem details such as latches, outputs, and bad states for an and-inverter
1137/// graph
1138///
1139/// Latches are not natively supported by [`Circuit`s][Circuit], but each latch
1140/// output is modeled as a an additional circuit input, and each latch input is
1141/// modeled as a Boolean function, concretely a [`Literal`]. In the current
1142/// implementation, the input numbers for latches are in range
1143/// `(self.inputs() + 1)..(self.inputs() + self.latches().len())`.
1144#[derive(Clone, PartialEq, Eq, Debug)]
1145pub struct AIGERDetails {
1146    /// Number of input variables
1147    inputs: usize,
1148    /// Latch inputs
1149    latches: Vec<Literal>,
1150    /// Latch initial values
1151    latch_init_values: TVBitVec,
1152    /// Outputs
1153    outputs: Vec<Literal>,
1154    /// Bad state literals
1155    bad: Vec<Literal>,
1156    /// Invariant constraints
1157    invariants: Vec<Literal>,
1158    /// Justice properties
1159    justice: Vec2d<Literal>,
1160    /// Fairness constraints
1161    fairness: Vec<Literal>,
1162
1163    /// Mapping from AIGER variable numbers (literals divided by 2) to literals
1164    /// in the circuit
1165    map: Vec<Literal>,
1166
1167    /// Output names
1168    ///
1169    /// Either empty or has the same length as `outputs`
1170    output_names: Vec<Option<String>>,
1171    /// Bad state literal names
1172    ///
1173    /// Either empty or has the same length as `bad`
1174    bad_names: Vec<Option<String>>,
1175    /// Invariant state names
1176    ///
1177    /// Either empty or has the same length as `invariants`
1178    invariant_names: Vec<Option<String>>,
1179    /// Justice property names
1180    ///
1181    /// Either empty or has the same length as `justice`
1182    justice_names: Vec<Option<String>>,
1183    /// Fairness constraint names
1184    ///
1185    /// Either empty or has the same length as `fairness`
1186    fairness_names: Vec<Option<String>>,
1187}
1188
1189impl AIGERDetails {
1190    /// Get the latch number of `literal`, if it refers to a latch
1191    ///
1192    /// If the return value is `Some(index)`, `index` is valid for the slice
1193    /// returned by [`Self::latches()`].
1194    #[inline]
1195    pub fn get_latch_no(&self, literal: Literal) -> Option<usize> {
1196        if literal.is_gate() {
1197            return None;
1198        }
1199        let first_latch = 1 + self.inputs;
1200        let result = (literal.0 >> Literal::VAR_LSB).checked_sub(first_latch)?;
1201        if result >= self.latches.len() {
1202            return None;
1203        }
1204        Some(result)
1205    }
1206
1207    /// Get the number of input variables
1208    #[inline(always)]
1209    pub fn inputs(&self) -> usize {
1210        self.inputs
1211    }
1212
1213    /// Get the input literals of each latch
1214    #[inline(always)]
1215    pub fn latches(&self) -> &[Literal] {
1216        &self.latches
1217    }
1218    /// Get the initial value of latch `i`
1219    #[inline(always)]
1220    pub fn latch_init_value(&self, i: usize) -> Option<bool> {
1221        self.latch_init_values.at(i)
1222    }
1223
1224    /// Get the output definitions
1225    #[inline(always)]
1226    pub fn outputs(&self) -> &[Literal] {
1227        &self.outputs
1228    }
1229
1230    /// Map the given AIGER literal to a [`Literal`] for use with the
1231    /// [`Circuit`]
1232    ///
1233    /// Note that the literals in [`AIGERDetails`] are already mapped
1234    /// accordingly. This method is useful if you want to refer to specific
1235    /// gates or literals using the values from the AIGER source.
1236    #[inline(always)]
1237    pub fn map_aiger_literal(&self, literal: usize) -> Option<Literal> {
1238        let l = *self.map.get(literal >> 1)?;
1239        Some(if literal & 1 != 0 { !l } else { l })
1240    }
1241
1242    /// Get the name for output `i`
1243    #[inline(always)]
1244    pub fn output_name(&self, i: usize) -> Option<&str> {
1245        self.output_names.get(i)?.as_deref()
1246    }
1247    /// Get the name for bad state literal `i`
1248    #[inline(always)]
1249    pub fn bad_name(&self, i: usize) -> Option<&str> {
1250        self.bad_names.get(i)?.as_deref()
1251    }
1252    /// Get the name for invariant constraint `i`
1253    #[inline(always)]
1254    pub fn invariant_name(&self, i: usize) -> Option<&str> {
1255        self.invariant_names.get(i)?.as_deref()
1256    }
1257    /// Get the name for justice constraint `i`
1258    #[inline(always)]
1259    pub fn justice_name(&self, i: usize) -> Option<&str> {
1260        self.justice_names.get(i)?.as_deref()
1261    }
1262
1263    /// Map the literals in `self` based on `gate_map`
1264    ///
1265    /// See [`Literal::apply_gate_map()`] for more details.
1266    pub fn apply_gate_map(&self, gate_map: &[Literal]) -> Self {
1267        let map_slice = move |slice: &[Literal]| {
1268            slice
1269                .iter()
1270                .map(move |l| l.apply_gate_map(gate_map))
1271                .collect::<Vec<_>>()
1272        };
1273
1274        let mut justice =
1275            Vec2d::with_capacity(self.justice.len(), self.justice.all_elements().len());
1276        for j in self.justice.iter() {
1277            justice.push_vec();
1278            justice.push_elements(j.iter().map(move |l| l.apply_gate_map(gate_map)));
1279        }
1280
1281        Self {
1282            inputs: self.inputs,
1283            latches: map_slice(&self.latches),
1284            latch_init_values: self.latch_init_values.clone(),
1285            outputs: map_slice(&self.outputs),
1286            bad: map_slice(&self.bad),
1287            invariants: map_slice(&self.invariants),
1288            justice,
1289            fairness: map_slice(&self.fairness),
1290            map: map_slice(&self.map),
1291            output_names: self.output_names.clone(),
1292            bad_names: self.bad_names.clone(),
1293            invariant_names: self.invariant_names.clone(),
1294            justice_names: self.justice_names.clone(),
1295            fairness_names: self.fairness_names.clone(),
1296        }
1297    }
1298
1299    /// In-place version of [`Self::apply_gate_map()`]
1300    pub fn apply_gate_map_in_place(&mut self, map: &[Literal]) {
1301        let map_slice = move |slice: &mut [Literal]| {
1302            for l in slice.iter_mut() {
1303                *l = l.apply_gate_map(map);
1304            }
1305        };
1306
1307        map_slice(&mut self.latches);
1308        map_slice(&mut self.outputs);
1309        map_slice(&mut self.bad);
1310        map_slice(&mut self.invariants);
1311        map_slice(self.justice.all_elements_mut());
1312        map_slice(&mut self.fairness);
1313        map_slice(&mut self.map);
1314    }
1315}
1316
1317/// Options for the parsers
1318#[non_exhaustive]
1319#[derive(Clone, Builder, Default, Debug)]
1320pub struct ParseOptions {
1321    /// Whether to parse a variable orders
1322    ///
1323    /// The [DIMACS satisfiability formats][dimacs], for instance, do not
1324    /// natively support specifying a variable order, however it is not uncommon
1325    /// to use the comment lines for this purpose. But while some files may
1326    /// contain a variable order in the comment lines, others may use them for
1327    /// arbitrary comments. Hence, it may be desired to turn on parsing orders
1328    /// for some files and turn it off for other files.
1329    #[builder(default = "false")]
1330    pub var_order: bool,
1331
1332    /// Whether to parse a clause tree (for [DIMACS CNF][dimacs])
1333    ///
1334    /// If the CNF contains, e.g., five clauses, and one of the comment lines
1335    /// contains `co [[0, 1], [2, 3, 4]]`, then the parsed circuit will have
1336    /// three AND gates (one with clauses 0 and 1 as input, one with clauses
1337    /// 2, 3, and 4, as well as one with those two conjuncts).
1338    #[builder(default = "false")]
1339    pub clause_tree: bool,
1340
1341    /// Whether to check that the circuit is acyclic
1342    ///
1343    /// The time complexity of this check is linear in the circuit's size, and
1344    /// therefore rather inexpensive. Therefore, it is enabled by default.
1345    #[builder(default = "true")]
1346    pub check_acyclic: bool,
1347}
1348
1349#[cfg(test)]
1350mod tests {
1351    use super::*;
1352    use crate::util::test::*;
1353
1354    #[test]
1355    fn simplify() {
1356        let mut circuit = Circuit::new(VarSet::new(3));
1357        circuit.push_gate(GateKind::Xor);
1358        circuit.push_gate_inputs([!v(0), v(1), v(2)]);
1359        circuit.push_gate(GateKind::And);
1360        circuit.push_gate_input(g(0));
1361
1362        let (simplified, map) = circuit.simplify([Literal::from_gate(false, 1)]).unwrap();
1363        assert_eq!(simplified.num_gates(), 1);
1364        assert_eq!(
1365            simplified.gate_for_no(0),
1366            Some(Gate::xor(&[v(0), v(1), v(2)]))
1367        );
1368        assert_eq!(&map, &[!g(0), !g(0)]);
1369    }
1370}