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

Re-exports

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

Synopsis

Documentation

data AIG s Source #

Instances

IsAIG Lit AIG Source #

newAIG :: IO (SomeGraph AIG) Source #

Build a new, empty AIG graph

readAiger :: FilePath -> IO (Network Lit AIG) Source #

Read an AIGER file as an AIG network

proxy :: Proxy Lit AIG Source #

Proxy for building AIG networks

data Lit s Source #

Instances

Traceable Lit Source #
Methods compareLit :: Lit s -> Lit s -> Ordering # showLit :: Lit s -> String #
IsLit Lit Source #
Methods not :: Lit s -> Lit s # (===) :: Lit s -> Lit s -> Bool #
IsAIG Lit AIG Source #
Methods withNewGraph :: Proxy Lit AIG -> (forall s. AIG s -> IO a) -> IO a # newGraph :: Proxy Lit AIG -> IO (SomeGraph AIG) # aigerNetwork :: Proxy Lit AIG -> FilePath -> IO (Network Lit AIG) # trueLit :: AIG s -> Lit s # falseLit :: AIG s -> Lit s # constant :: AIG s -> Bool -> Lit s # asConstant :: AIG s -> Lit s -> Maybe Bool # newInput :: AIG s -> IO (Lit s) # and :: AIG s -> Lit s -> Lit s -> IO (Lit s) # ands :: AIG s -> [Lit s] -> IO (Lit s) # or :: AIG s -> Lit s -> Lit s -> IO (Lit s) # eq :: AIG s -> Lit s -> Lit s -> IO (Lit s) # implies :: AIG s -> Lit s -> Lit s -> IO (Lit s) # xor :: AIG s -> Lit s -> Lit s -> IO (Lit s) # mux :: AIG s -> Lit s -> Lit s -> Lit s -> IO (Lit s) # inputCount :: AIG s -> IO Int # getInput :: AIG s -> Int -> IO (Lit s) # writeAiger :: FilePath -> Network Lit AIG -> IO () # writeCNF :: AIG s -> Lit s -> FilePath -> IO [Int] # checkSat :: AIG s -> Lit s -> IO SatResult # cec :: Network Lit AIG -> Network Lit AIG -> IO VerifyResult # evaluator :: AIG s -> [Bool] -> IO (Lit s -> Bool) # evaluate :: Network Lit AIG -> [Bool] -> IO [Bool] # litView :: AIG s -> Lit s -> IO (LitView (Lit s)) # abstractEvaluateAIG :: AIG s -> (LitView a -> IO a) -> IO (Lit s -> IO a) #
Eq (Lit s) Source #
Methods (==) :: Lit s -> Lit s -> Bool # (/=) :: Lit s -> Lit s -> Bool #
Ord (Lit s) Source #
Methods compare :: Lit s -> Lit s -> Ordering # (<) :: Lit s -> Lit s -> Bool # (<=) :: Lit s -> Lit s -> Bool # (>) :: Lit s -> Lit s -> Bool # (>=) :: Lit s -> Lit s -> Bool # max :: Lit s -> Lit s -> Lit s # min :: Lit s -> Lit s -> Lit s #
Storable (Lit s) Source #
Methods sizeOf :: Lit s -> Int # alignment :: Lit s -> Int # peekElemOff :: Ptr (Lit s) -> Int -> IO (Lit s) # pokeElemOff :: Ptr (Lit s) -> Int -> Lit s -> IO () # peekByteOff :: Ptr b -> Int -> IO (Lit s) # pokeByteOff :: Ptr b -> Int -> Lit s -> IO () # peek :: Ptr (Lit s) -> IO (Lit s) # poke :: Ptr (Lit s) -> Lit s -> IO () #

true :: AIG s -> Lit s Source #

false :: AIG s -> Lit s Source #

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.

checkSat' :: Ptr Abc_Ntk_t -> IO SatResult Source #

Returns true is the literal is satisfiabile.

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.

Constructors

Network :: Network l g

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

Instances

IsAIG Lit AIG #
Methods withNewGraph :: Proxy Lit AIG -> (forall s. AIG s -> IO a) -> IO a # newGraph :: Proxy Lit AIG -> IO (SomeGraph AIG) # aigerNetwork :: Proxy Lit AIG -> FilePath -> IO (Network Lit AIG) # trueLit :: AIG s -> Lit s # falseLit :: AIG s -> Lit s # constant :: AIG s -> Bool -> Lit s # asConstant :: AIG s -> Lit s -> Maybe Bool # newInput :: AIG s -> IO (Lit s) # and :: AIG s -> Lit s -> Lit s -> IO (Lit s) # ands :: AIG s -> [Lit s] -> IO (Lit s) # or :: AIG s -> Lit s -> Lit s -> IO (Lit s) # eq :: AIG s -> Lit s -> Lit s -> IO (Lit s) # implies :: AIG s -> Lit s -> Lit s -> IO (Lit s) # xor :: AIG s -> Lit s -> Lit s -> IO (Lit s) # mux :: AIG s -> Lit s -> Lit s -> Lit s -> IO (Lit s) # inputCount :: AIG s -> IO Int # getInput :: AIG s -> Int -> IO (Lit s) # writeAiger :: FilePath -> Network Lit AIG -> IO () # writeCNF :: AIG s -> Lit s -> FilePath -> IO [Int] # checkSat :: AIG s -> Lit s -> IO SatResult # cec :: Network Lit AIG -> Network Lit AIG -> IO VerifyResult # evaluator :: AIG s -> [Bool] -> IO (Lit s -> Bool) # evaluate :: Network Lit AIG -> [Bool] -> IO [Bool] # litView :: AIG s -> Lit s -> IO (LitView (Lit s)) # abstractEvaluateAIG :: AIG s -> (LitView a -> IO a) -> IO (Lit s -> IO a) #
IsAIG Lit GIA #
Methods withNewGraph :: Proxy Lit GIA -> (forall s. GIA s -> IO a) -> IO a # newGraph :: Proxy Lit GIA -> IO (SomeGraph GIA) # aigerNetwork :: Proxy Lit GIA -> FilePath -> IO (Network Lit GIA) # trueLit :: GIA s -> Lit s # falseLit :: GIA s -> Lit s # constant :: GIA s -> Bool -> Lit s # asConstant :: GIA s -> Lit s -> Maybe Bool # newInput :: GIA s -> IO (Lit s) # and :: GIA s -> Lit s -> Lit s -> IO (Lit s) # ands :: GIA s -> [Lit s] -> IO (Lit s) # or :: GIA s -> Lit s -> Lit s -> IO (Lit s) # eq :: GIA s -> Lit s -> Lit s -> IO (Lit s) # implies :: GIA s -> Lit s -> Lit s -> IO (Lit s) # xor :: GIA s -> Lit s -> Lit s -> IO (Lit s) # mux :: GIA s -> Lit s -> Lit s -> Lit s -> IO (Lit s) # inputCount :: GIA s -> IO Int # getInput :: GIA s -> Int -> IO (Lit s) # writeAiger :: FilePath -> Network Lit GIA -> IO () # writeCNF :: GIA s -> Lit s -> FilePath -> IO [Int] # checkSat :: GIA s -> Lit s -> IO SatResult # cec :: Network Lit GIA -> Network Lit GIA -> IO VerifyResult # evaluator :: GIA s -> [Bool] -> IO (Lit s -> Bool) # evaluate :: Network Lit GIA -> [Bool] -> IO [Bool] # litView :: GIA s -> Lit s -> IO (LitView (Lit s)) # abstractEvaluateAIG :: GIA s -> (LitView a -> IO a) -> IO (Lit 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 () # 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) #

class IsLit l where #

Instances

IsLit Lit #
Methods not :: Lit s -> Lit s # (===) :: Lit s -> Lit s -> Bool #
IsLit Lit #
Methods not :: Lit s -> Lit s # (===) :: Lit s -> Lit s -> Bool #
IsLit l => IsLit (TraceLit l)
Methods not :: TraceLit l s -> TraceLit l s # (===) :: TraceLit l s -> TraceLit l s -> Bool #

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 #

data SomeGraph g :: (* -> *) -> * where #

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

Constructors

SomeGraph :: SomeGraph g