| Copyright | Galois, Inc. 2010-2014 |
|---|---|
| License | BSD3 |
| Maintainer | jhendrix@galois.com |
| Stability | stable |
| Portability | non-portable (language extensions) |
| Safe Haskell | None |
| Language | Haskell98 |
Data.ABC.AIG
Contents
Description
Warning: The Data.ABC.AIG module has known bugs (http:/github.comGaloisIncabcBridgeissues/4) for which solutions do not currently exist. Consider using Data.ABC.GIA instead.
Data.ABC.AIG defines a set of higher level functions for manipulating
and-inverter graph networks (AIG) directly from ABC. This module
should be imported qualified, e.g.
import Data.ABC.AIG (AIG) import qualified Data.ABC.AIG as AIG
- data AIG s
- newAIG :: IO (SomeGraph AIG)
- readAiger :: FilePath -> IO (Network Lit AIG)
- proxy :: Proxy Lit AIG
- data Lit s
- true :: AIG s -> Lit s
- false :: AIG s -> Lit s
- writeAIGManToCNFWithMapping :: Aig_Man_t -> FilePath -> IO (Vector Int)
- checkSat' :: Ptr Abc_Ntk_t -> IO SatResult
- data Network l g :: (* -> *) -> (* -> *) -> * where
- networkInputCount :: Network l g -> IO Int
- 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)
- class IsLit l where
- data SatResult :: *
- = Unsat
- | Sat ![Bool]
- | SatUnknown
- data VerifyResult :: *
- = Valid
- | Invalid [Bool]
- | VerifyUnknown
- data SomeGraph g :: (* -> *) -> * where
Documentation
writeAIGManToCNFWithMapping :: Aig_Man_t -> FilePath -> IO (Vector Int) Source
Convert the network referred to by an AIG manager into CNF format and write to a file, returning a mapping from ABC object IDs to CNF variable numbers.
Re-exports
data Network l g :: (* -> *) -> (* -> *) -> * where
A network is an and-invertor graph paired with it's outputs, thus representing a complete combinational circuit.
networkInputCount :: Network l g -> IO Int
Get number of inputs associated with current network.
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, 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)
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.
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.
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
class IsLit l where
Methods
not :: l s -> l s
Negate a literal.
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.
data VerifyResult :: *
Result of a verification check.
Constructors
| Valid | |
| Invalid [Bool] | |
| VerifyUnknown |
Instances