Data.AIG.Interface

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

Main interface classes

class IsLit l where

Minimal complete definition

not, (===)

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.

Instances

IsLit BasicLit

Methods

not :: BasicLit s -> BasicLit s

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

IsLit l => IsLit (TraceLit l)

Methods

not :: TraceLit l s -> TraceLit l s

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

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.

Minimal complete definition

aigerNetwork, trueLit, falseLit, newInput, and, inputCount, getInput, writeAiger, writeAigerWithLatches, writeCNF, checkSat, cec, evaluator, litView, abstractEvaluateAIG

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.

writeAigerWithLatches :: FilePath -> Network l g -> Int -> IO ()

Write network out to AIGER file with some inputs designated as latches.

writeCNF :: g s -> l s -> FilePath -> IO [Int]

Write network out to DIMACS CNF file. Returns vector mapping combinational inputs to CNF Variable numbers.

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.

litView :: g s -> l s -> IO (LitView (l s))

Examine the outermost structure of a literal to see how it was constructed

abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a)

Build an evaluation function over an AIG using the provided view function

Instances

IsAIG BasicLit BasicGraph

Methods

withNewGraph :: Proxy BasicLit BasicGraph -> (forall s. BasicGraph s -> IO a) -> IO a

newGraph :: Proxy BasicLit BasicGraph -> IO (SomeGraph BasicGraph)

aigerNetwork :: Proxy BasicLit BasicGraph -> FilePath -> IO (Network BasicLit BasicGraph)

trueLit :: BasicGraph s -> BasicLit s

falseLit :: BasicGraph s -> BasicLit s

constant :: BasicGraph s -> Bool -> BasicLit s

asConstant :: BasicGraph s -> BasicLit s -> Maybe Bool

newInput :: BasicGraph s -> IO (BasicLit s)

and :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

ands :: BasicGraph s -> [BasicLit s] -> IO (BasicLit s)

or :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

eq :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

implies :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

xor :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

mux :: BasicGraph s -> BasicLit s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

inputCount :: BasicGraph s -> IO Int

getInput :: BasicGraph s -> Int -> IO (BasicLit s)

writeAiger :: FilePath -> Network BasicLit BasicGraph -> IO ()

writeAigerWithLatches :: FilePath -> Network BasicLit BasicGraph -> Int -> IO ()

writeCNF :: BasicGraph s -> BasicLit s -> FilePath -> IO [Int]

checkSat :: BasicGraph s -> BasicLit s -> IO SatResult

cec :: Network BasicLit BasicGraph -> Network BasicLit BasicGraph -> IO VerifyResult

evaluator :: BasicGraph s -> [Bool] -> IO (BasicLit s -> Bool)

evaluate :: Network BasicLit BasicGraph -> [Bool] -> IO [Bool]

litView :: BasicGraph s -> BasicLit s -> IO (LitView (BasicLit s))

abstractEvaluateAIG :: BasicGraph s -> (LitView a -> IO a) -> IO (BasicLit s -> IO a)

(IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g)

Methods

withNewGraph :: Proxy (TraceLit l) (TraceGraph l g) -> (forall s. TraceGraph l g s -> IO a) -> IO a

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

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

trueLit :: TraceGraph l g s -> TraceLit l s

falseLit :: TraceGraph l g s -> TraceLit l s

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

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

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

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

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

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

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

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

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

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

inputCount :: TraceGraph l g s -> IO Int

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

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

writeAigerWithLatches :: FilePath -> Network (TraceLit l) (TraceGraph l g) -> Int -> IO ()

writeCNF :: TraceGraph l g s -> TraceLit l s -> FilePath -> IO [Int]

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

cec :: Network (TraceLit l) (TraceGraph l g) -> Network (TraceLit l) (TraceGraph l g) -> IO VerifyResult

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

evaluate :: Network (TraceLit l) (TraceGraph l g) -> [Bool] -> IO [Bool]

litView :: TraceGraph l g s -> TraceLit l s -> IO (LitView (TraceLit l s))

abstractEvaluateAIG :: TraceGraph l g s -> (LitView a -> IO a) -> IO (TraceLit l s -> IO a)

lazyMux :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s) -> IO (l s)

Short-cutting mux operator that optimizes the case where the test bit is a concrete literal

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-invertor 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

Get number of inputs associated with current network.

networkOutputCount :: Network l g -> Int

Number of outputs associated with a network.

Literal representations

data LitView a

Concrete datatype representing the ways an AIG can be constructed.

Constructors

And !a !a

NotAnd !a !a

Input !Int

NotInput !Int

TrueLit

FalseLit

Instances

Functor LitView

Methods

fmap :: (a -> b) -> LitView a -> LitView b

(<$) :: a -> LitView b -> LitView a

Foldable LitView

Methods

fold :: Monoid m => LitView m -> m

foldMap :: Monoid m => (a -> m) -> LitView a -> m

foldr :: (a -> b -> b) -> b -> LitView a -> b

foldr' :: (a -> b -> b) -> b -> LitView a -> b

foldl :: (b -> a -> b) -> b -> LitView a -> b

foldl' :: (b -> a -> b) -> b -> LitView a -> b

foldr1 :: (a -> a -> a) -> LitView a -> a

foldl1 :: (a -> a -> a) -> LitView a -> a

toList :: LitView a -> [a]

null :: LitView a -> Bool

length :: LitView a -> Int

elem :: Eq a => a -> LitView a -> Bool

maximum :: Ord a => LitView a -> a

minimum :: Ord a => LitView a -> a

sum :: Num a => LitView a -> a

product :: Num a => LitView a -> a

Traversable LitView

Methods

traverse :: Applicative f => (a -> f b) -> LitView a -> f (LitView b)

sequenceA :: Applicative f => LitView (f a) -> f (LitView a)

mapM :: Monad m => (a -> m b) -> LitView a -> m (LitView b)

sequence :: Monad m => LitView (m a) -> m (LitView a)

TraceOutput l g x => TraceOutput l g (LitView x)

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> LitView x -> String

Eq a => Eq (LitView a)

Methods

(==) :: LitView a -> LitView a -> Bool

(/=) :: LitView a -> LitView a -> Bool

Ord a => Ord (LitView a)

Methods

compare :: LitView a -> LitView a -> Ordering

(<) :: LitView a -> LitView a -> Bool

(<=) :: LitView a -> LitView a -> Bool

(>) :: LitView a -> LitView a -> Bool

(>=) :: LitView a -> LitView a -> Bool

max :: LitView a -> LitView a -> LitView a

min :: LitView a -> LitView a -> LitView a

Show a => Show (LitView a)

Methods

showsPrec :: Int -> LitView a -> ShowS

show :: LitView a -> String

showList :: [LitView a] -> ShowS

negateLitView :: LitView a -> LitView a

newtype LitTree

Constructors

LitTree

Fields

• unLitTree :: LitView LitTree

Instances

Eq LitTree

Methods

(==) :: LitTree -> LitTree -> Bool

(/=) :: LitTree -> LitTree -> Bool

Ord LitTree

Methods

compare :: LitTree -> LitTree -> Ordering

(<) :: LitTree -> LitTree -> Bool

(<=) :: LitTree -> LitTree -> Bool

(>) :: LitTree -> LitTree -> Bool

(>=) :: LitTree -> LitTree -> Bool

max :: LitTree -> LitTree -> LitTree

min :: LitTree -> LitTree -> LitTree

Show LitTree

Methods

showsPrec :: Int -> LitTree -> ShowS

show :: LitTree -> String

showList :: [LitTree] -> ShowS

Arbitrary LitTree

Methods

arbitrary :: Gen LitTree

shrink :: LitTree -> [LitTree]

toLitTree :: IsAIG l g => g s -> l s -> IO LitTree

Extract a tree representation of the given literal

fromLitTree :: IsAIG l g => g s -> LitTree -> IO (l s)

Construct an AIG literal from a tree representation

toLitForest :: IsAIG l g => g s -> [l s] -> IO [LitTree]

Extract a forest representation of the given list of literal s

fromLitForest :: IsAIG l g => g s -> [LitTree] -> IO [l s]

Construct a list of AIG literals from a forest representation

foldAIG :: IsAIG l g => g s -> (LitView a -> IO a) -> l s -> IO a

Evaluate the given literal using the provided view function

foldAIGs :: IsAIG l g => g s -> (LitView a -> IO a) -> [l s] -> IO [a]

Evaluate the given list of literals using the provided view function

unfoldAIG :: IsAIG l g => g s -> (a -> IO (LitView a)) -> a -> IO (l s)

Build an AIG literal by unfolding a constructor function

unfoldAIGs :: IsAIG l g => g s -> (a -> IO (LitView a)) -> [a] -> IO [l s]

Build a list of AIG literals by unfolding a constructor function

Representations of prover results

data SatResult

Satisfiability check result.

Constructors

Unsat

Sat ![Bool]

SatUnknown

Instances

Eq SatResult

Methods

(==) :: SatResult -> SatResult -> Bool

(/=) :: SatResult -> SatResult -> Bool

Show SatResult

Methods

showsPrec :: Int -> SatResult -> ShowS

show :: SatResult -> String

showList :: [SatResult] -> ShowS

TraceOutput l g SatResult

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> SatResult -> String

data VerifyResult

Result of a verification check.

Constructors

Valid

Invalid [Bool]

VerifyUnknown

Instances

Eq VerifyResult

Methods

(==) :: VerifyResult -> VerifyResult -> Bool

(/=) :: VerifyResult -> VerifyResult -> Bool

Show VerifyResult

Methods

showsPrec :: Int -> VerifyResult -> ShowS

show :: VerifyResult -> String

showList :: [VerifyResult] -> ShowS

TraceOutput l g VerifyResult

Methods

traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> VerifyResult -> String

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.

QuickCheck generators and testing

genLitView :: Gen a -> Gen (LitView a)

Generate an arbitrary LitView given a generator for a

genLitTree :: Gen LitTree

Generate an arbitrary LitTree

getMaxInput :: LitTree -> Int

Given a LitTree, calculate the maximum input number in the tree. Returns 0 if no inputs are referenced.

buildNetwork :: IsAIG l g => Proxy l g -> [LitTree] -> IO (Network l g)

Given a list of LitTree, construct a corresponding AIG network

randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g)

Generate a random network by building a random LitTree and using that to construct a network.

data BasicGraph s

A basic Graph datastructure based on LitTrees. This is a totally naive implementation of the AIG structure that exists exclusively for testing purposes.

Instances

IsAIG BasicLit BasicGraph

Methods

withNewGraph :: Proxy BasicLit BasicGraph -> (forall s. BasicGraph s -> IO a) -> IO a

newGraph :: Proxy BasicLit BasicGraph -> IO (SomeGraph BasicGraph)

aigerNetwork :: Proxy BasicLit BasicGraph -> FilePath -> IO (Network BasicLit BasicGraph)

trueLit :: BasicGraph s -> BasicLit s

falseLit :: BasicGraph s -> BasicLit s

constant :: BasicGraph s -> Bool -> BasicLit s

asConstant :: BasicGraph s -> BasicLit s -> Maybe Bool

newInput :: BasicGraph s -> IO (BasicLit s)

and :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

ands :: BasicGraph s -> [BasicLit s] -> IO (BasicLit s)

or :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

eq :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

implies :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

xor :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

mux :: BasicGraph s -> BasicLit s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

inputCount :: BasicGraph s -> IO Int

getInput :: BasicGraph s -> Int -> IO (BasicLit s)

writeAiger :: FilePath -> Network BasicLit BasicGraph -> IO ()

writeAigerWithLatches :: FilePath -> Network BasicLit BasicGraph -> Int -> IO ()

writeCNF :: BasicGraph s -> BasicLit s -> FilePath -> IO [Int]

checkSat :: BasicGraph s -> BasicLit s -> IO SatResult

cec :: Network BasicLit BasicGraph -> Network BasicLit BasicGraph -> IO VerifyResult

evaluator :: BasicGraph s -> [Bool] -> IO (BasicLit s -> Bool)

evaluate :: Network BasicLit BasicGraph -> [Bool] -> IO [Bool]

litView :: BasicGraph s -> BasicLit s -> IO (LitView (BasicLit s))

abstractEvaluateAIG :: BasicGraph s -> (LitView a -> IO a) -> IO (BasicLit s -> IO a)

data BasicLit s

A basic AIG literal datastructure based on LitTrees. This is a totally naive implementation of the AIG structure that exists exclusively for testing purposes.

Instances

IsLit BasicLit

Methods

not :: BasicLit s -> BasicLit s

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

IsAIG BasicLit BasicGraph

Methods

withNewGraph :: Proxy BasicLit BasicGraph -> (forall s. BasicGraph s -> IO a) -> IO a

newGraph :: Proxy BasicLit BasicGraph -> IO (SomeGraph BasicGraph)

aigerNetwork :: Proxy BasicLit BasicGraph -> FilePath -> IO (Network BasicLit BasicGraph)

trueLit :: BasicGraph s -> BasicLit s

falseLit :: BasicGraph s -> BasicLit s

constant :: BasicGraph s -> Bool -> BasicLit s

asConstant :: BasicGraph s -> BasicLit s -> Maybe Bool

newInput :: BasicGraph s -> IO (BasicLit s)

and :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

ands :: BasicGraph s -> [BasicLit s] -> IO (BasicLit s)

or :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

eq :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

implies :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

xor :: BasicGraph s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

mux :: BasicGraph s -> BasicLit s -> BasicLit s -> BasicLit s -> IO (BasicLit s)

inputCount :: BasicGraph s -> IO Int

getInput :: BasicGraph s -> Int -> IO (BasicLit s)

writeAiger :: FilePath -> Network BasicLit BasicGraph -> IO ()

writeAigerWithLatches :: FilePath -> Network BasicLit BasicGraph -> Int -> IO ()

writeCNF :: BasicGraph s -> BasicLit s -> FilePath -> IO [Int]

checkSat :: BasicGraph s -> BasicLit s -> IO SatResult

cec :: Network BasicLit BasicGraph -> Network BasicLit BasicGraph -> IO VerifyResult

evaluator :: BasicGraph s -> [Bool] -> IO (BasicLit s -> Bool)

evaluate :: Network BasicLit BasicGraph -> [Bool] -> IO [Bool]

litView :: BasicGraph s -> BasicLit s -> IO (LitView (BasicLit s))

abstractEvaluateAIG :: BasicGraph s -> (LitView a -> IO a) -> IO (BasicLit s -> IO a)

Show (BasicLit s)

Methods

showsPrec :: Int -> BasicLit s -> ShowS

show :: BasicLit s -> String

showList :: [BasicLit s] -> ShowS

basicProxy :: Proxy BasicLit BasicGraph

newBasicGraph :: IO (BasicGraph s)