Module aig 

And-inverter graphs: a circuit as two-input AND gates over complemented edges, read and written in the AIGER format (Biere, The AIGER And-Inverter Graph Format, Version 20071012, and its 1.9 extension).

An Aig is built bottom-up and kept in topological order: every gate is created after its operands, so a gate’s node index exceeds both of theirs. Aig::and hashes structurally (Kuehlmann & Krohm, DAC 1997): an operand pair it has seen returns the existing gate, and a constant, repeated or complementary operand folds away, so two circuits built into one graph share every gate they compute the same way. Inputs and latches are leaves; a latch’s next-state literal may name any node, which is how a sequential circuit closes its loops without breaking the order.

Aig::parse reads the ASCII (aag) and binary (aig) forms, including latch initial values, bad-state and invariant-constraint sections and the symbol table, and refuses justice and fairness properties by name. ASCII gates may be defined in any order; they are rebuilt in dependency order without recursion, so a chain of any depth reads. Aig::to_ascii and Aig::to_binary write the canonical numbering: inputs, then latches, then gates in node order.

Aig::eval evaluates one assignment and Aig::simulate sixty-four assignments a word over any number of words: the signatures SAT sweeping (crate::sweep) groups candidate equivalences by.

Structs

Aig

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

AigLit

A literal of an and-inverter graph: node n as 2n, its complement as 2n + 1, the AIGER encoding. Node 0 is the constant false.

Latch

Port

An input (its node, uncomplemented), output, bad-state property or invariant constraint, with its symbol.

Enums

AigerError

Why an AIGER file was refused. Lines count from 1.

Init

A latch’s value before the first clock.

Leaf

A leaf of a graph being imported into another (Aig::import).

Node

What a node is.