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}