| Copyright | (c) Galois, Inc. 2014 |
|---|---|
| License | BSD3 |
| Maintainer | jhendrix@galois.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Data.AIG.Interface
Contents
Description
Interfaces for building, simulating and analysing And-Inverter Graphs (AIG).
- class IsLit l where
- class IsLit l => IsAIG l g | g -> l where
- withNewGraph :: Proxy l g -> (forall s. g s -> IO a) -> IO a
- newGraph :: Proxy l g -> IO (SomeGraph g)
- aigerNetwork :: Proxy l g -> FilePath -> IO (Network l g)
- trueLit :: g s -> l s
- falseLit :: g s -> l s
- constant :: g s -> Bool -> l s
- asConstant :: g s -> l s -> Maybe Bool
- newInput :: g s -> IO (l s)
- and :: g s -> l s -> l s -> IO (l s)
- ands :: g s -> [l s] -> IO (l s)
- or :: g s -> l s -> l s -> IO (l s)
- eq :: g s -> l s -> l s -> IO (l s)
- implies :: g s -> l s -> l s -> IO (l s)
- xor :: g s -> l s -> l s -> IO (l s)
- mux :: g s -> l s -> l s -> l s -> IO (l s)
- inputCount :: g s -> IO Int
- getInput :: g s -> Int -> IO (l s)
- writeAiger :: FilePath -> Network l g -> IO ()
- writeCNF :: g s -> l s -> FilePath -> IO [Int]
- checkSat :: g s -> l s -> IO SatResult
- cec :: Network l g -> Network l g -> IO VerifyResult
- evaluator :: g s -> [Bool] -> IO (l s -> Bool)
- evaluate :: Network l g -> [Bool] -> IO [Bool]
- litView :: g s -> l s -> IO (LitView (l s))
- abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a)
- lazyMux :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s) -> IO (l s)
- data Proxy l g where
- data SomeGraph g where
- data Network l g where
- networkInputCount :: Network l g -> IO Int
- networkOutputCount :: Network l g -> Int
- data LitView a
- newtype LitTree = LitTree {}
- toLitTree :: IsAIG l g => g s -> l s -> IO LitTree
- fromLitTree :: IsAIG l g => g s -> LitTree -> IO (l s)
- toLitForest :: IsAIG l g => g s -> [l s] -> IO [LitTree]
- fromLitForest :: IsAIG l g => g s -> [LitTree] -> IO [l s]
- foldAIG :: IsAIG l g => g s -> (LitView a -> IO a) -> l s -> IO a
- foldAIGs :: IsAIG l g => g s -> (LitView a -> IO a) -> [l s] -> IO [a]
- unfoldAIG :: IsAIG l g => g s -> (a -> IO (LitView a)) -> a -> IO (l s)
- unfoldAIGs :: IsAIG l g => g s -> (a -> IO (LitView a)) -> [a] -> IO [l s]
- data SatResult
- = Unsat
- | Sat ![Bool]
- | SatUnknown
- data VerifyResult
- = Valid
- | Invalid [Bool]
- | VerifyUnknown
- toSatResult :: VerifyResult -> SatResult
- toVerifyResult :: SatResult -> VerifyResult
- genLitView :: Gen a -> Gen (LitView a)
- genLitTree :: Gen LitTree
- getMaxInput :: LitTree -> Int
- buildNetwork :: IsAIG l g => Proxy l g -> [LitTree] -> IO (Network l g)
- randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g)
Main interface classes
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.
Minimal complete definition
aigerNetwork, trueLit, falseLit, newInput, and, inputCount, getInput, writeAiger, writeCNF, checkSat, cec, evaluator, litView, abstractEvaluateAIG
Methods
Arguments
| :: Proxy l g | A |
| -> (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) 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
Get unique literal in graph representing constant true.
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
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
A proxy is used to identify a specific AIG instance when calling methods that create new AIGs.
Some graph quantifies over the state phantom variable for a graph.
A network is an and-invertor graph paired with it's outputs, thus representing a complete combinational circuit.
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
Concrete datatype representing the ways an AIG can be constructed.
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
Satisfiability check result.
Constructors
| Unsat | |
| Sat ![Bool] | |
| SatUnknown |
data VerifyResult Source
Result of a verification check.
Constructors
| Valid | |
| Invalid [Bool] | |
| VerifyUnknown |
Instances
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
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.