Copyright	Galois, Inc. 2010-2014
License	BSD3
Maintainer	jhendrix@galois.com
Stability	experimental
Portability	non-portable (language extensions)
Safe Haskell	None
Language	Haskell98

Data.ABC.GIA

Contents

Building lits
Inspection
File IO
QBF
Re-exports

Description

GIA defines a set of functions for manipulating scalable and-inverter graph networks directly from ABC. This module should be imported qualified, e.g.

import Data.ABC.GIA (GIA)
import qualified Data.ABC.GIA as GIA

Scalable and-inverter graphs are briefly described at the Berkeley Verification and Synthesis Research Center's website. http://bvsrc.org/research.html#AIG%20Package It is a more memory efficient method of storing AIG graphs.

Synopsis

Documentation

data GIA s Source #

An and-invertor graph network in GIA form.

Instances

IsAIG Lit GIA Source #

newGIA :: IO (SomeGraph GIA) Source #

Build a new empty GIA graph

Building lits

data Lit s Source #

Represent a literal.

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 GIA Source #
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) #
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 :: Lit s Source #

Constant true node.

false :: Lit s Source #

Constant false node

proxy :: Proxy Lit GIA Source #

Inspection

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 #

File IO

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

Read an AIGER file into a GIA graph

writeAigerWithLatches Source #

Arguments

:: FilePath
-> Network Lit GIA
-> Int	Number of latches.
-> IO ()

Write an AIGER file with the given number of latches. If the number of latches is denoted by "n", then the last n inputs and last n outputs are treated as the latch input and outputs respectively. The other inputs and outputs represent primary inputs and outputs.

QBF

check_exists_forall Source #

Arguments

:: GIA s	The GIA network used to store the terms.
-> Int	The number of existential variables.
-> Lit s	The proposition to verify.
-> [Bool]	Initial value to use in search for universal variables. (should equal number of universal variables.).
-> CInt	Number of iterations to try solver.
-> IO (Either String SatResult)

Check a formula of the form Ex.Ay p(x,y). This function takes a network where input variables are used to represent both the existentially and the universally quantified variables. The existentially quantified variables must precede the universally quantified variables, and the number of extential variables is defined by an extraInt@ paramter.

Re-exports

data Proxy l g :: (* -> *) -> (* -> *) -> * #

A proxy is used to identify a specific AIG instance when calling methods that create new AIGs.

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

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

Constructors

SomeGraph :: SomeGraph g

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 #

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

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

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 #