aig-0.2.5: And-inverter graphs in Haskell.

Copyright(c) Galois Inc. 2014-2017
LicenseBSD3
Maintainerjhendrix@galois.com
Stabilityexperimental
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Data.AIG.Interface

Contents

Description

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

Synopsis

Main interface classes

class IsLit l where Source #

Minimal complete definition

not, (===)

Methods

not :: l s -> l s Source #

Negate a literal.

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

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 Source # 

Methods

not :: BasicLit s -> BasicLit s Source #

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

IsLit l => IsLit (TraceLit l) Source # 

Methods

not :: TraceLit l s -> TraceLit l s Source #

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

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

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 :: Proxy l g -> (forall s. g s -> IO a) -> IO a Source #

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

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

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) Source #

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

trueLit :: g s -> l s Source #

Get unique literal in graph representing constant true.

falseLit :: g s -> l s Source #

Get unique literal in graph representing constant false.

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

Generate a constant literal value

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

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

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

Generate a fresh input literal

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

Compute the logical and of two literals

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

Build the conjunction of a list of literals

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

Compute the logical or of two literals

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

Compute the logical equality of two literals

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

Compute the logical implication of two literals

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

Compute the exclusive or of two literals

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

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

inputCount :: g s -> IO Int Source #

Return number of inputs in the graph.

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

Get input at given index in the graph.

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

Write network out to AIGER file.

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

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

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

Check if literal is satisfiable in network.

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

Perform combinational equivalence checking.

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

Evaluate the network on a set of concrete inputs.

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

Evaluate the network on a set of concrete inputs.

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

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) Source #

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

Instances

IsAIG BasicLit BasicGraph Source # 

Methods

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

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

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

trueLit :: BasicGraph s -> BasicLit s Source #

falseLit :: BasicGraph s -> BasicLit s Source #

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

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

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

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

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

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

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

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

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

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

inputCount :: BasicGraph s -> IO Int Source #

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

inputCount :: TraceGraph l g s -> IO Int Source #

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

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

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

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

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

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

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

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

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

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

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

Helper datatypes

data Proxy l g where Source #

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 Source #

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

Constructors

SomeGraph :: g s -> SomeGraph g 

data Network l g where Source #

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 Source #

Get number of inputs associated with current network.

networkOutputCount :: Network l g -> Int Source #

Number of outputs associated with a network.

Literal representations

data LitView a Source #

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 Source # 

Methods

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

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

Foldable LitView Source # 

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 Source # 

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) Source # 

Methods

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

Eq a => Eq (LitView a) Source # 

Methods

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

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

Ord a => Ord (LitView a) Source # 

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) Source # 

Methods

showsPrec :: Int -> LitView a -> ShowS #

show :: LitView a -> String #

showList :: [LitView a] -> ShowS #

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

Extract a tree representation of the given literal

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

Construct an AIG literal from a tree representation

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

Extract a forest representation of the given list of literal s

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

Construct a list of AIG literals from a forest representation

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

Evaluate the given literal using the provided view function

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

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) Source #

Build an AIG literal by unfolding a constructor function

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

Build a list of AIG literals by unfolding a constructor function

Representations of prover results

data SatResult Source #

Satisfiability check result.

Constructors

Unsat 
Sat ![Bool] 
SatUnknown 

toSatResult :: VerifyResult -> SatResult Source #

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

toVerifyResult :: SatResult -> VerifyResult Source #

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

QuickCheck generators and testing

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

Generate an arbitrary LitView given a generator for a

genLitTree :: Gen LitTree Source #

Generate an arbitrary LitTree

getMaxInput :: LitTree -> Int Source #

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) Source #

Given a list of LitTree, construct a corresponding AIG network

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

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

data BasicGraph s Source #

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 Source # 

Methods

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

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

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

trueLit :: BasicGraph s -> BasicLit s Source #

falseLit :: BasicGraph s -> BasicLit s Source #

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

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

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

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

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

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

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

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

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

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

inputCount :: BasicGraph s -> IO Int Source #

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

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

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

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

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

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

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

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

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

data BasicLit s Source #

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 Source # 

Methods

not :: BasicLit s -> BasicLit s Source #

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

IsAIG BasicLit BasicGraph Source # 

Methods

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

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

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

trueLit :: BasicGraph s -> BasicLit s Source #

falseLit :: BasicGraph s -> BasicLit s Source #

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

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

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

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

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

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

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

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

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

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

inputCount :: BasicGraph s -> IO Int Source #

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

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

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

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

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

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

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

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

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

Show (BasicLit s) Source # 

Methods

showsPrec :: Int -> BasicLit s -> ShowS #

show :: BasicLit s -> String #

showList :: [BasicLit s] -> ShowS #