Struct Aig 

pub struct Aig { /* private fields */ }

An and-inverter graph with its inputs, latches, outputs, bad-state properties, invariant constraints and comments.

Implementations

impl Aig

pub fn new() -> Aig

A graph holding only the constant node.

pub fn add_input(&mut self, name: Option<String>) -> AigLit

pub fn add_latch(&mut self, name: Option<String>, init: Init) -> usize

A latch whose next state is false until Aig::set_next; returns its index.

pub fn latch_lit(&self, latch: usize) -> AigLit

The latch’s current-state literal.

pub fn set_next(&mut self, latch: usize, next: AigLit)

pub fn and(&mut self, a: AigLit, b: AigLit) -> AigLit

a ∧ b, folded and structurally hashed.

pub fn or(&mut self, a: AigLit, b: AigLit) -> AigLit

pub fn xor(&mut self, a: AigLit, b: AigLit) -> AigLit

pub fn xnor(&mut self, a: AigLit, b: AigLit) -> AigLit

pub fn mux(&mut self, s: AigLit, t: AigLit, e: AigLit) -> AigLit

s ? t : e.

pub fn add_output(&mut self, lit: AigLit, name: Option<String>)

pub fn add_bad(&mut self, lit: AigLit, name: Option<String>)

pub fn add_constraint(&mut self, lit: AigLit, name: Option<String>)

pub fn node(&self, n: u32) -> Node

pub fn num_nodes(&self) -> usize

pub fn num_ands(&self) -> usize

pub fn inputs(&self) -> &[Port]

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

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

pub fn bad(&self) -> &[Port]

pub fn constraints(&self) -> &[Port]

pub fn comments(&self) -> &[String]

pub fn input_index(&self, name: &str) -> Option<usize>

pub fn output_index(&self, name: &str) -> Option<usize>

pub fn eval(&self, inputs: &[bool], latches: &[bool]) -> Vec<bool>

The value of every node under one assignment of the inputs and the latches.

pub fn value(values: &[bool], lit: AigLit) -> bool

A literal’s value among Aig::eval’s node values.

pub fn simulate( &self, words: usize, inputs: &[u64], latches: &[u64], ) -> Vec<u64>

Every node’s value under 64 · words assignments at once: input i’s words are inputs[i·words .. (i+1)·words], likewise each latch’s. The result holds node n’s words at n·words .. (n+1)·words.

pub fn word(sim: &[u64], words: usize, lit: AigLit, w: usize) -> u64

Word w of a literal’s value in a Aig::simulate result.

pub fn cone(&self, roots: &[AigLit]) -> Vec<u32>

The nodes the roots depend on, themselves included, in increasing order.

pub fn compact(&self) -> (Aig, Vec<Option<AigLit>>)

The graph with only the nodes something reads: every input and latch in order, the outputs, bad and constraint properties and latches’ next states, and the nodes in their cones; with each node’s literal in the result, None for one nothing reads.

pub fn compact_keeping(&self, keep: &[AigLit]) -> (Aig, Vec<Option<AigLit>>)

Aig::compact, the cones of keep kept as well.

pub fn sequential_cone(&self, outputs: &[usize]) -> Aig

The graph the outputs outputs (by index) read through any number of clocks: those outputs, in the order given; every latch whose value reaches one of them (a latch a kept latch’s next state reads, to a fixpoint), in order, with its name and initial value; every input, in order; and the nodes their cones need.

pub fn import( &mut self, other: &Aig, leaves: &mut dyn FnMut(Leaf) -> AigLit, ) -> Vec<AigLit>

Copy every node of other into this graph, each leaf replaced by the literal leaves gives it. Returns the literal each of other’s nodes became, indexed by node.

pub fn to_ascii(&self) -> String

The canonical ASCII AIGER text.

pub fn to_binary(&self) -> Vec<u8>

The canonical binary AIGER bytes.

pub fn parse(bytes: &[u8]) -> Result<Aig, AigerError>

Read an ASCII (aag) or binary (aig) AIGER file.

Trait Implementations

impl Clone for Aig

fn clone(&self) -> Aig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Aig

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

Formats the value using the given formatter.

impl Default for Aig

fn default() -> Aig

Returns the “default value” for a type.