Struct Circuit

pub struct Circuit { /* private fields */ }

Combinational circuit with negation as well as n-ary AND, OR, and XOR gates

Implementations

impl Circuit

pub fn new(inputs: VarSet) -> Self

Create an empty circuit with the given circuit inputs

pub fn inputs(&self) -> &VarSet

Get the circuit inputs

pub fn inputs_mut(&mut self) -> &mut VarSet

Get a mutable reference to the circuit inputs

pub fn reserve_gates(&mut self, additional: usize)

Reserve space for at least additional more gates. Note that this will not reserve space for gate inputs. To that end, use Self::reserve_gate_inputs().

This is essentially a wrapper around Vec::reserve(), so the documentation there provides more details.

pub fn reserve_gate_inputs(&mut self, additional: usize)

Reserve space for at least additional more gate inputs (the space is shared between all gates). Note that this will not reserve space for the gate metadata. To that end, use Self::reserve_gates().

This is essentially a wrapper around Vec::reserve(), so the documentation there provides more details.

pub fn num_gates(&self) -> usize

Get the number of gates in this circuit

pub fn gate(&self, literal: Literal) -> Option<Gate<'_>>

Get the Gate for literal

Returns None iff literal refers to a constant, a circuit input, or a gate that is not present in this circuit.

See also: Self::gate_for_no()

pub fn gate_for_no(&self, gate_no: Var) -> Option<Gate<'_>>

Get the Gate for gate_no

Returns None iff literal refers to a gate that is not present in this circuit.

See also: Self::gate()

pub fn gate_inputs_mut(&mut self, literal: Literal) -> Option<&mut [Literal]>

Get a mutable reference to the gate inputs

Returns None iff literal refers to a constant, a circuit input, or a gate that is not present in this circuit.

pub fn gate_inputs_mut_for_no(&mut self, gate_no: Var) -> Option<&mut [Literal]>

Get a mutable reference to the gate inputs

Returns None iff literal refers to a constant, a circuit input, or a gate that is not present in this circuit.

pub fn set_gate_kind(&mut self, literal: Literal, kind: GateKind)

Set the kind of the gate referenced by literal

Panics if literal does not refer to a gate in this circuit.

pub fn set_gate_kind_for_no(&mut self, gate_no: Var, kind: GateKind)

Set the kind of the gate referenced by gate_no

Panics if literal does not refer to a gate in this circuit.

pub fn set_last_gate_kind(&mut self, kind: GateKind)

Set the kind of the gate referenced by literal

Panics if the circuit is empty.

pub fn first_gate(&self) -> Option<Gate<'_>>

Get the first gate

Returns None iff literal refers to a constant, a circuit input, or a gate that is not present in this circuit.

pub fn last_gate(&self) -> Option<Gate<'_>>

Get the last gate

Returns None iff literal refers to a constant, a circuit input, or a gate that is not present in this circuit.

pub fn push_gate(&mut self, kind: GateKind) -> Literal

Create a new empty gate at the end of the sequence

pub fn pop_gate(&mut self) -> bool

Remove the last gate (if there is one)

Returns true iff the number of gates was positive before removal.

pub fn push_gate_input(&mut self, literal: Literal)

Add an input to the last gate

There must be already one gate in the circuit, otherwise this method triggers a debug assertion or does not do anything, respectively.

pub fn push_gate_inputs(&mut self, literals: impl IntoIterator<Item = Literal>)

Add inputs to the last gate

There must be already one gate in the circuit, otherwise this method triggers a debug assertion or does not do anything, respectively.

pub fn iter_gates(&self) -> CircuitGateIter<'_>

Iterate over all gates in the circuit

The iteration order is from first to last in the gate sequence.

pub fn retain_gates(&mut self, predicate: impl FnMut(&mut [Literal]) -> bool)

Retain the gates for which predicate returns true

Note that removing one gate changes the gate numbers of all subsequent gates, but this method does not automatically update the gate inputs.

pub fn clear_gates(&mut self)

Remove all gate definitions from the circuit

pub fn find_cycle(&self) -> Option<Literal>

Check if this circuit is acyclic

Returns None if acyclic, or Some(literal) if literal depends on itself.

pub fn simplify( &self, roots: impl IntoIterator<Item = Literal>, ) -> Result<(Self, Vec<Literal>), Literal>

Simplify the circuit such that

1. no gate has constant inputs
2. no inputs of XOR gates are negated (only the output)
3. for every gate, all its inputs are distinct (disregarding polarities)
4. all gates have at least two inputs
5. there are no two structurally equivalent gates (same kind and inputs, disregarding the input order)

Additionally, the new circuit will only contain gates reachable from roots. The order of gate inputs in the resulting circuit follows the order of the first discovered equivalent gate (with duplicates etc. removed).

If the reachable circuit fragment contains a cycle, this method returns Err(l), where l represents a gate that is part of the cycle. Likewise, if the reachable fragment depends on unknown inputs (input_number >= self.inputs().len(), including Literal::UNDEF), the return value is Err(l), where l is the unknown literal.

On success, the gates in the returned circuit are topologically sorted. The additional Vec<Literal> maps the gates of self to literals valid in the simplified circuit.

Hint: Problem::simplify uses this method to simplify the circuit and also maps the

Trait Implementations

impl Clone for Circuit

fn clone(&self) -> Circuit

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Circuit

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for Circuit

fn eq(&self, other: &Circuit) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Circuit

impl StructuralPartialEq for Circuit