-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | And-inverter graphs in Haskell.
--   
--   This package provides a generic interfaces for working with
--   And-Inverter graphs (AIGs) in Haskell. And-Inverter graphs are a
--   useful format for representing combinatorial and sequential boolean
--   circuits in a way that is amenable to simulation and analysis. These
--   interfaces allow clients to write code that can create and use AIGs
--   without depending on a particular AIG package.
@package aig
@version 0.2


-- | Interfaces for building, simulating and analysing And-Inverter Graphs
--   (AIG).
module Data.AIG.Interface
class IsLit l
not :: IsLit l => l s -> l s
(===) :: IsLit l => l s -> l s -> Bool

-- | 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.
class IsLit l => IsAIG l g | g -> l where withNewGraph p f = newGraph p >>= (`withSomeGraph` f) newGraph p = withNewGraph p (return . SomeGraph) constant g True = trueLit g constant g False = falseLit g asConstant g l | l === trueLit g = Just True | l === falseLit g = Just False | otherwise = Nothing ands g [] = return (trueLit g) ands g (x : r) = foldM (and g) x r or g x y = not <$> and g (not x) (not y) eq g x y = not <$> xor g x y implies g x y = or g (not x) y xor g x y = do { o <- or g x y; a <- and g x y; and g o (not a) } mux g c x y = do { x' <- and g c x; y' <- and g (not c) y; or g x' y' } evaluate (Network g outputs) inputs = do { f <- evaluator g inputs; return (f <$> outputs) }
withNewGraph :: IsAIG l g => Proxy l g -> (forall s. g s -> IO a) -> IO a
newGraph :: IsAIG l g => Proxy l g -> IO (SomeGraph g)
aigerNetwork :: IsAIG l g => Proxy l g -> FilePath -> IO (Network l g)
trueLit :: IsAIG l g => g s -> l s
falseLit :: IsAIG l g => g s -> l s
constant :: IsAIG l g => g s -> Bool -> l s
asConstant :: IsAIG l g => g s -> l s -> Maybe Bool
newInput :: IsAIG l g => g s -> IO (l s)
and :: IsAIG l g => g s -> l s -> l s -> IO (l s)
ands :: IsAIG l g => g s -> [l s] -> IO (l s)
or :: IsAIG l g => g s -> l s -> l s -> IO (l s)
eq :: IsAIG l g => g s -> l s -> l s -> IO (l s)
implies :: IsAIG l g => g s -> l s -> l s -> IO (l s)
xor :: IsAIG l g => g s -> l s -> l s -> IO (l s)
mux :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s)
inputCount :: IsAIG l g => g s -> IO Int
getInput :: IsAIG l g => g s -> Int -> IO (l s)
writeAiger :: IsAIG l g => FilePath -> Network l g -> IO ()
checkSat :: IsAIG l g => g s -> l s -> IO SatResult
cec :: IsAIG l g => Network l g -> Network l g -> IO VerifyResult
evaluator :: IsAIG l g => g s -> [Bool] -> IO (l s -> Bool)
evaluate :: IsAIG l g => Network l g -> [Bool] -> IO [Bool]
abstractEvaluateAIG :: IsAIG l g => g s -> (LitView a -> IO a) -> IO (l s -> IO a)

-- | Short-cutting mux operator that optimizes the case where the test bit
--   is a concrete literal
lazyMux :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s) -> IO (l s)

-- | A proxy is used to identify a specific AIG instance when calling
--   methods that create new AIGs.
data Proxy l g
Proxy :: (forall a. a -> a) -> Proxy l g

-- | Some graph quantifies over the state phantom variable for a graph.
data SomeGraph g
SomeGraph :: g s -> SomeGraph g

-- | A network is an and-inverstor graph paired with it's outputs, thus
--   representing a complete combinational circuit.
data Network l g
Network :: g s -> [l s] -> Network l g
networkInputCount :: Network l g -> IO Int

-- | Concrete datatype representing the ways an AIG can be constructed.
data LitView a
And :: !a -> !a -> LitView a
NotAnd :: !a -> !a -> LitView a
Input :: !Int -> LitView a
NotInput :: !Int -> LitView a
TrueLit :: LitView a
FalseLit :: LitView a
newtype LitTree
LitTree :: LitView LitTree -> LitTree
unLitTree :: LitTree -> LitView LitTree

-- | Extract a tree representation of the given literal
toLitTree :: IsAIG l g => g s -> l s -> IO LitTree

-- | Construct an AIG literal from a tree representation
fromLitTree :: IsAIG l g => g s -> LitTree -> IO (l s)

-- | Extract a forest representation of the given list of literal s
toLitForest :: IsAIG l g => g s -> [l s] -> IO [LitTree]

-- | Construct a list of AIG literals from a forest representation
fromLitForest :: IsAIG l g => g s -> [LitTree] -> IO [l s]

-- | Evaluate the given literal using the provided view function
foldAIG :: IsAIG l g => g s -> (LitView a -> IO a) -> l s -> IO a

-- | Evaluate the given list of literals using the provided view function
foldAIGs :: IsAIG l g => g s -> (LitView a -> IO a) -> [l s] -> IO [a]

-- | Build an AIG literal by unfolding a constructor function
unfoldAIG :: IsAIG l g => g s -> (a -> IO (LitView a)) -> a -> IO (l s)

-- | Build a list of AIG literals by unfolding a constructor function
unfoldAIGs :: IsAIG l g => g s -> (a -> IO (LitView a)) -> [a] -> IO [l s]

-- | Satisfiability check result.
data SatResult
Unsat :: SatResult
Sat :: !([Bool]) -> SatResult
SatUnknown :: SatResult

-- | Result of a verification check.
data VerifyResult
Valid :: VerifyResult
Invalid :: [Bool] -> VerifyResult
VerifyUnknown :: VerifyResult

-- | Convert a verify result to a sat result by negating it.
toSatResult :: VerifyResult -> SatResult

-- | Convert a sat result to a verify result by negating it.
toVerifyResult :: SatResult -> VerifyResult

-- | Generate an arbitrary <a>LitView</a> given a generator for <tt>a</tt>
genLitView :: Gen a -> Gen (LitView a)

-- | Generate an arbitrary <a>LitTree</a>
genLitTree :: Gen LitTree

-- | Given a LitTree, calculate the maximum input number in the tree.
--   Returns 0 if no inputs are referenced.
getMaxInput :: LitTree -> Int

-- | Given a list of LitTree, construct a corresponding AIG network
buildNetwork :: IsAIG l g => Proxy l g -> [LitTree] -> IO (Network l g)

-- | Generate a random network by building a random <a>LitTree</a> and
--   using that to construct a network.
randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g)
instance Eq a => Eq (LitView a)
instance Show a => Show (LitView a)
instance Ord a => Ord (LitView a)
instance Functor LitView
instance Eq LitTree
instance Show LitTree
instance Ord LitTree
instance Eq SatResult
instance Show SatResult
instance Eq VerifyResult
instance Show VerifyResult
instance Arbitrary LitTree


-- | A collection of higher-level operations (mostly 2's complement
--   arithmetic operations) that can be built from the primitive
--   And-Inverter Graph interface.
module Data.AIG.Operations

-- | A BitVector consists of a sequence of symbolic bits and can be used
--   for symbolic machine-word arithmetic.
data BV l

-- | Empty bitvector
empty :: BV l

-- | Number of bits in a bit vector
length :: BV l -> Int

-- | Project the individual bits of a BitVector. <tt>x <a>at</a> 0</tt> is
--   the most significant bit. It is an error to request an out-of-bounds
--   bit.
at :: BV l -> Int -> l

-- | Select bits from a bitvector, starting from the least significant bit.
--   <tt>x ! 0</tt> is the least significant bit. It is an error to request
--   an out-of-bounds bit.
(!) :: BV l -> Int -> l

-- | Append two bitvectors, with the most significant bitvector given
--   first.
(++) :: BV l -> BV l -> BV l

-- | Concatenate a list of bitvectors, with the most significant bitvector
--   at the head of the list.
concat :: [BV l] -> BV l

-- | Project out the <tt>n</tt> most significant bits from a bitvector.
take :: Int -> BV l -> BV l

-- | Drop the <tt>n</tt> most significant bits from a bitvector.
drop :: Int -> BV l -> BV l

-- | Extract <tt>n</tt> bits starting at index <tt>i</tt>. The vector must
--   contain at least <tt>i+n</tt> elements
slice :: BV l -> Int -> Int -> BV l

-- | Extract <tt>n</tt> bits starting at index <tt>i</tt>, counting from
--   the end of the vector instead of the beginning. The vector must
--   contain at least <tt>i+n</tt> elements.
sliceRev :: BV l -> Int -> Int -> BV l

-- | Apply a monadic operation to each element of a bitvector in sequence
mapM :: Monad m => (a -> m b) -> BV a -> m (BV b)

-- | Combine two bitvectors with a bitwise function
zipWith :: (l -> l -> l) -> BV l -> BV l -> BV l

-- | Combine two bitvectors with a bitwise monadic combiner action.
zipWithM :: Monad m => (l -> l -> m l) -> BV l -> BV l -> m (BV l)

-- | Retrieve the most significant bit of a bitvector.
msb :: BV l -> l

-- | Retrieve the least significant bit of a bitvector.
lsb :: BV l -> l

-- | Test syntactic equalify of two bitvectors using the <a>===</a>
--   operation
bvSame :: IsLit l => BV (l s) -> BV (l s) -> Bool

-- | Display a bitvector as a string of bits with most significant bits
--   first. Concrete literals are displayed as '0' or '1', whereas symbolic
--   literals are displayed as <tt>x</tt>.
bvShow :: IsAIG l g => g s -> BV (l s) -> String

-- | Generate a bitvector of length <tt>n</tt>, using monadic function
--   <tt>f</tt> to generate the bit literals. The indexes to <tt>f</tt> are
--   given in MSB-first order, i.e., <tt>f 0</tt> is the most significant
--   bit.
generateM_msb0 :: Monad m => Int -> (Int -> m l) -> m (BV l)

-- | Generate a bitvector of length <tt>n</tt>, using function <tt>f</tt>
--   to specify the bit literals. The indexes to <tt>f</tt> are given in
--   MSB-first order, i.e., <tt>f 0</tt> is the most significant bit.
generate_msb0 :: Int -> (Int -> l) -> BV l

-- | Generate a bitvector of length <tt>n</tt>, using monadic function
--   <tt>f</tt> to generate the bit literals. The indexes to <tt>f</tt> are
--   given in LSB-first order, i.e., <tt>f 0</tt> is the least significant
--   bit.
generateM_lsb0 :: MonadIO m => Int -> (Int -> m l) -> m (BV l)

-- | Generate a bitvector of length <tt>n</tt>, using function <tt>f</tt>
--   to specify the bit literals. The indexes to <tt>f</tt> are given in
--   LSB-first order, i.e., <tt>f 0</tt> is the least significant bit.
generate_lsb0 :: Int -> (Int -> l) -> BV l

-- | Generate a bit vector of length <tt>n</tt> where every bit value is
--   literal <tt>l</tt>.
replicate :: Int -> l -> BV l

-- | Generate a bit vector of length <tt>n</tt> where every bit value is
--   generated in turn by <tt>m</tt>.
replicateM :: Monad m => Int -> m l -> m (BV l)

-- | Generate a bitvector from an integer value, using 2's complement
--   representation.
bvFromInteger :: IsAIG l g => g s -> Int -> Integer -> BV (l s)

-- | Convert a list to a bitvector, assuming big-endian bit order.
bvFromList :: [l] -> BV l

-- | <tt>muxInteger mergeFn maxValue lv valueFn</tt> returns a circuit
--   whose result is <tt>valueFn v</tt> when <tt>lv</tt> has value
--   <tt>v</tt>.
muxInteger :: (Integral i, Monad m) => (l -> m a -> m a -> m a) -> i -> BV l -> (i -> m a) -> m a

-- | Generate a one-element bitvector containing the given literal
singleton :: l -> BV l

-- | Build a short-cut AND circuit. If the left argument evaluates to the
--   constant false, the right argument will not be evaluated.
lAnd :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
lAnd' :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Build a short-cut OR circuit. If the left argument evaluates to the
--   constant true, the right argument will not be evaluated.
lOr :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
lOr' :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Construct a lazy xor. If both arguments are constants, the output will
--   also be a constant.
lXor :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
lXor' :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Construct a lazy equality test. If both arguments are constants, the
--   output will also be a constant.
lEq :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s)
lEq' :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Lazy negation of a circuit.
lNot :: IsAIG l g => g s -> IO (l s) -> IO (l s)
lNot' :: IsAIG l g => g s -> l s -> l s

-- | If-then-else combinator for bitvectors.
ite :: IsAIG l g => g s -> l s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | If-then-else combinator for bitvector computations with optimistic
--   shortcutting. If the test bit is concrete, we can avoid generating
--   either the if or the else circuit.
iteM :: IsAIG l g => g s -> l s -> IO (BV (l s)) -> IO (BV (l s)) -> IO (BV (l s))

-- | Interpret a bitvector as an unsigned integer. Return <tt>Nothing</tt>
--   if the bitvector is not concrete.
asUnsigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer

-- | Interpret a bitvector as a signed integer. Return <tt>Nothing</tt> if
--   the bitvector is not concrete.
asSigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer

-- | Convert a bitvector to a list, most significant bit first.
bvToList :: BV l -> [l]

-- | Compute the 2's complement negation of a bitvector
neg :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))

-- | Add two bitvectors with the same size. Discard carry bit.
add :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Add two bitvectors with the same size with carry.
addC :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), l s)

-- | Subtract one bitvector from another with the same size. Discard carry
--   bit.
sub :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Subtract one bitvector from another with the same size with carry.
subC :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), l s)

-- | Add a constant value to a bitvector
addConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s))

-- | Add a constant value to a bitvector
subConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s))

-- | Multiply two bitvectors with the same size, with result of the same
--   size as the arguments. Overflow is silently discarded.
mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Unsigned multiply two bitvectors with size <tt>m</tt> and size
--   <tt>n</tt>, resulting in a vector of size <tt>m+n</tt>.
mulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Signed multiply two bitvectors with size <tt>m</tt> and size
--   <tt>n</tt>, resulting in a vector of size <tt>m+n</tt>.
smulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Compute the signed quotient of two signed bitvectors with the same
--   size.
squot :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Compute the signed division remainder of two signed bitvectors with
--   the same size.
srem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Compute the unsigned quotient of two unsigned bitvectors with the same
--   size.
uquot :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Compute the unsigned division remainder of two unsigned bitvectors
--   with the same size.
urem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Shift left. The least significant bit becomes 0.
shl :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Signed right shift. The most significant bit is copied.
sshr :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Unsigned right shift. The most significant bit becomes 0.
ushr :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Rotate left.
rol :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Rotate right.
ror :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Test equality of two bitvectors with the same size.
bvEq :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)

-- | Test if a bitvector is equal to zero
isZero :: IsAIG l g => g s -> BV (l s) -> IO (l s)

-- | Test if a bitvector is distinct from zero
nonZero :: IsAIG l g => g s -> BV (l s) -> IO (l s)

-- | Signed less-than-or-equal on bitvector with the same size.
sle :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)

-- | Signed less-than on bitvector with the same size.
slt :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)

-- | Unsigned less-than-or-equal on bitvector with the same size.
ule :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)

-- | Unsigned less-than on bitvector with the same size.
ult :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)

-- | Return absolute value of signed bitvector.
sabs :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))

-- | <tt>sext v n</tt> sign extends <tt>v</tt> to be a vector with length
--   <tt>n</tt>. This function requires that <tt>n &gt;= length v</tt> and
--   <tt>length v &gt; 0</tt>.
sext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s)

-- | <tt>zext g v n</tt> zero extends <tt>v</tt> to be a vector with length
--   <tt>n</tt>. This function requires that <tt>n &gt;= length v</tt>.
zext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s)

-- | Truncate the given bit vector to the specified length
trunc :: Int -> BV (l s) -> BV (l s)

-- | Truncate or zero-extend a bitvector to have the specified number of
--   bits
zeroIntCoerce :: IsAIG l g => g s -> Int -> BV (l s) -> BV (l s)

-- | Truncate or sign-extend a bitvector to have the specified number of
--   bits
signIntCoerce :: IsAIG l g => g s -> Int -> BV (l s) -> BV (l s)

-- | Polynomial multiplication. Note that the algorithm works the same no
--   matter which endianness convention is used. Result length is <tt>max 0
--   (m+n-1)</tt>, where <tt>m</tt> and <tt>n</tt> are the lengths of the
--   inputs.
pmul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))

-- | Polynomial mod with symbolic modulus. Return value has length one less
--   than the length of the modulus.
pmod :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
instance Eq l => Eq (BV l)
instance Ord l => Ord (BV l)
instance Show l => Show (BV l)
instance Functor BV


-- | A tracing wrapper AIG interface. Given an underlying AIG interface,
--   this wrapper intercepts all interface calls and logs them to a file
--   for debugging purposes.
module Data.AIG.Trace
class Traceable l
compareLit :: Traceable l => l s -> l s -> Ordering
showLit :: Traceable l => l s -> String
newtype TraceLit l s
TraceLit :: l s -> TraceLit l s
unTraceLit :: TraceLit l s -> l s
data TraceGraph (l :: * -> *) g s
TraceGraph :: g s -> IORef (Maybe Handle) -> TraceGraph g s
tGraph :: TraceGraph g s -> g s
tActive :: TraceGraph g s -> IORef (Maybe Handle)
proxy :: Traceable l => Proxy l g -> Proxy (TraceLit l) (TraceGraph l g)
activateTracing :: TraceGraph l g s -> FilePath -> IO ()
deactiveTracing :: TraceGraph l g s -> IO ()
withTracing :: TraceGraph l g s -> FilePath -> IO a -> IO a
class TraceOp l g a
traceOp :: (TraceOp l g a, Traceable l, IsAIG l g) => TraceGraph l g s -> String -> a -> a
class TraceOutput l g x
traceOutput :: (TraceOutput l g x, Traceable l, IsAIG l g) => TraceGraph l g s -> x -> String
withNewGraphTracing :: (IsAIG l g, Traceable l) => Proxy l g -> FilePath -> (forall s. TraceGraph l g s -> IO a) -> IO a
instance (IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g)
instance TraceOutput l g VerifyResult
instance TraceOutput l g SatResult
instance TraceOutput l g ()
instance TraceOutput l g Int
instance TraceOutput l g (TraceLit l s)
instance TraceOutput l g x => TraceOp l g (IO x)
instance TraceOp l g b => TraceOp l g (FilePath -> b)
instance TraceOp l g b => TraceOp l g ([TraceLit l s] -> b)
instance TraceOp l g b => TraceOp l g (TraceLit l s -> b)
instance TraceOp l g b => TraceOp l g (Int -> b)
instance Traceable l => Ord (TraceLit l s)
instance Traceable l => Eq (TraceLit l s)
instance IsLit l => IsLit (TraceLit l)


module Data.AIG