Data.AIG.Interface

Interfaces for building, simulating and analysing And-Inverter Graphs (AIG).

Main interface classes

class IsLit l where

Methods

not :: l s -> l s

Negate a literal.

(===) :: l s -> l s -> Bool

Tests whether two lits are identical. This is only a syntactic check, and may return false even if the two literals represent the same predicate.

class IsLit l => IsAIG l g | g -> l where

An And-Inverter-Graph is a data structure storing bit-level nodes.

Graphs are and-inverter graphs, which contain a number of input literals and Boolean operations for creating new literals. Every literal is part of a specific graph, and literals from different networks may not be mixed.

Both the types for literals and graphs must take a single phantom type for an arugment that is used to ensure that literals from different networks cannot be used in the same operation.

Methods

withNewGraph

Arguments

:: Proxy l g

A Proxy value, used for selecting the concrete implementation typeclass

-> (forall s. g s -> IO a)

The AIG graph computation to run

-> IO a

Create a temporary graph, and use it to compute a result value.

newGraph :: Proxy l g -> IO (SomeGraph g)

Build a new graph instance, and packge it into the SomeGraph type that remembers the IsAIG implementation.

aigerNetwork :: Proxy l g -> FilePath -> IO (Network l g)

Read an AIG from a file, assumed to be in Aiger format

trueLit :: g s -> l s

Get unique literal in graph representing constant true.

falseLit :: g s -> l s

Get unique literal in graph representing constant false.

constant :: g s -> Bool -> l s

Generate a constant literal value

asConstant :: g s -> l s -> Maybe Bool

Return if the literal is a fixed constant. If the literal is symbolic, return Nothing.

newInput :: g s -> IO (l s)

Generate a fresh input literal

and :: g s -> l s -> l s -> IO (l s)

Compute the logical and of two literals

ands :: g s -> [l s] -> IO (l s)

Build the conjunction of a list of literals

or :: g s -> l s -> l s -> IO (l s)

Compute the logical or of two literals

eq :: g s -> l s -> l s -> IO (l s)

Compute the logical equality of two literals

implies :: g s -> l s -> l s -> IO (l s)

Compute the logical implication of two literals

xor :: g s -> l s -> l s -> IO (l s)

Compute the exclusive or of two literals

mux :: g s -> l s -> l s -> l s -> IO (l s)

Perform a mux (if-then-else on the bits).

inputCount :: g s -> IO Int

Return number of inputs in the graph.

getInput :: g s -> Int -> IO (l s)

Get input at given index in the graph.

writeAiger :: FilePath -> Network l g -> IO ()

Write network out to AIGER file.

checkSat :: g s -> l s -> IO SatResult

Check if literal is satisfiable in network.

cec :: Network l g -> Network l g -> IO VerifyResult

Perform combinational equivalence checking.

evaluator :: g s -> [Bool] -> IO (l s -> Bool)

Evaluate the network on a set of concrete inputs.

evaluate :: Network l g -> [Bool] -> IO [Bool]

Evaluate the network on a set of concrete inputs.

Helper datatypes

data Proxy l g where

A proxy is used to identify a specific AIG instance when calling methods that create new AIGs.

Constructors

Proxy :: IsAIG l g => (forall a. a -> a) -> Proxy l g

data SomeGraph g where

Some graph quantifies over the state phantom variable for a graph.

Constructors

SomeGraph :: g s -> SomeGraph g

data Network l g where

A network is an and-inverstor graph paired with it's outputs, thus representing a complete combinational circuit.

Constructors

Network :: IsAIG l g => g s -> [l s] -> Network l g

networkInputCount :: Network l g -> IO Int

Representations of prover results

data SatResult

Satisfiability check result.

Constructors

Unsat

Sat ![Bool]

Instances

Eq SatResult

Show SatResult

data VerifyResult

Result of a verification check.

Constructors

Valid

Invalid [Bool]

Instances

Eq VerifyResult

Show VerifyResult

toSatResult :: VerifyResult -> SatResult

Convert a verify result to a sat result by negating it.

toVerifyResult :: SatResult -> VerifyResult

Convert a sat result to a verify result by negating it.