Struct AIGERDetails

pub struct AIGERDetails { /* private fields */ }

Problem details such as latches, outputs, and bad states for an and-inverter graph

Latches are not natively supported by Circuits, but each latch output is modeled as a an additional circuit input, and each latch input is modeled as a Boolean function, concretely a Literal. In the current implementation, the input numbers for latches are in range (self.inputs() + 1)..(self.inputs() + self.latches().len()).

Implementations

impl AIGERDetails

pub fn get_latch_no(&self, literal: Literal) -> Option<usize>

Get the latch number of literal, if it refers to a latch

If the return value is Some(index), index is valid for the slice returned by Self::latches().

pub fn inputs(&self) -> usize

Get the number of input variables

pub fn latches(&self) -> &[Literal]

Get the input literals of each latch

pub fn latch_init_value(&self, i: usize) -> Option<bool>

Get the initial value of latch i

pub fn outputs(&self) -> &[Literal]

Get the output definitions

pub fn map_aiger_literal(&self, literal: usize) -> Option<Literal>

Map the given AIGER literal to a Literal for use with the Circuit

Note that the literals in AIGERDetails are already mapped accordingly. This method is useful if you want to refer to specific gates or literals using the values from the AIGER source.

pub fn output_name(&self, i: usize) -> Option<&str>

Get the name for output i

pub fn bad_name(&self, i: usize) -> Option<&str>

Get the name for bad state literal i

pub fn invariant_name(&self, i: usize) -> Option<&str>

Get the name for invariant constraint i

pub fn justice_name(&self, i: usize) -> Option<&str>

Get the name for justice constraint i

pub fn apply_gate_map(&self, gate_map: &[Literal]) -> Self

Map the literals in self based on gate_map

See Literal::apply_gate_map() for more details.

pub fn apply_gate_map_in_place(&mut self, map: &[Literal])

In-place version of Self::apply_gate_map()

Trait Implementations

impl Clone for AIGERDetails

fn clone(&self) -> AIGERDetails

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AIGERDetails

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

Formats the value using the given formatter.

impl PartialEq for AIGERDetails

fn eq(&self, other: &AIGERDetails) -> 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 AIGERDetails

impl StructuralPartialEq for AIGERDetails