-- 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.5


-- | Interfaces for building, simulating and analysing And-Inverter Graphs
--   (AIG).
module Data.AIG.Interface
class IsLit l

-- | Negate a literal.
not :: IsLit l => l s -> l s

-- | 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.
(===) :: 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) }

-- | Create a temporary graph, and use it to compute a result value.
withNewGraph :: IsAIG l g => Proxy l g -> (forall s. g s -> IO a) -> IO a

-- | Build a new graph instance, and packge it into the <a>SomeGraph</a>
--   type that remembers the IsAIG implementation.
newGraph :: IsAIG l g => Proxy l g -> IO (SomeGraph g)

-- | Read an AIG from a file, assumed to be in Aiger format
aigerNetwork :: IsAIG l g => Proxy l g -> FilePath -> IO (Network l g)

-- | Get unique literal in graph representing constant true.
trueLit :: IsAIG l g => g s -> l s

-- | Get unique literal in graph representing constant false.
falseLit :: IsAIG l g => g s -> l s

-- | Generate a constant literal value
constant :: IsAIG l g => g s -> Bool -> l s

-- | Return if the literal is a fixed constant. If the literal is symbolic,
--   return <tt>Nothing</tt>.
asConstant :: IsAIG l g => g s -> l s -> Maybe Bool

-- | Generate a fresh input literal
newInput :: IsAIG l g => g s -> IO (l s)

-- | Compute the logical and of two literals
and :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Build the conjunction of a list of literals
ands :: IsAIG l g => g s -> [l s] -> IO (l s)

-- | Compute the logical or of two literals
or :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Compute the logical equality of two literals
eq :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Compute the logical implication of two literals
implies :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Compute the exclusive or of two literals
xor :: IsAIG l g => g s -> l s -> l s -> IO (l s)

-- | Perform a mux (if-then-else on the bits).
mux :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s)

-- | Return number of inputs in the graph.
inputCount :: IsAIG l g => g s -> IO Int

-- | Get input at given index in the graph.
getInput :: IsAIG l g => g s -> Int -> IO (l s)

-- | Write network out to AIGER file.
writeAiger :: IsAIG l g => FilePath -> Network l g -> IO ()

-- | Write network out to DIMACS CNF file. Returns vector mapping
--   combinational inputs to CNF Variable numbers.
writeCNF :: IsAIG l g => g s -> l s -> FilePath -> IO [Int]

-- | Check if literal is satisfiable in network.
checkSat :: IsAIG l g => g s -> l s -> IO SatResult

-- | Perform combinational equivalence checking.
cec :: IsAIG l g => Network l g -> Network l g -> IO VerifyResult

-- | Evaluate the network on a set of concrete inputs.
evaluator :: IsAIG l g => g s -> [Bool] -> IO (l s -> Bool)

-- | Evaluate the network on a set of concrete inputs.
evaluate :: IsAIG l g => Network l g -> [Bool] -> IO [Bool]

-- | Examine the outermost structure of a literal to see how it was
--   constructed
litView :: IsAIG l g => g s -> l s -> IO (LitView (l s))

-- | Build an evaluation function over an AIG using the provided view
--   function
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] :: IsAIG l g => (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-invertor graph paired with it's outputs, thus
--   representing a complete combinational circuit.
data Network l g
[Network] :: IsAIG l g => g s -> [l s] -> Network l g

-- | Get number of inputs associated with current network.
networkInputCount :: Network l g -> IO Int

-- | Number of outputs associated with a network.
networkOutputCount :: Network l g -> 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
negateLitView :: LitView a -> 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)

-- | A basic <a>Graph</a> datastructure based on LitTrees. This is a
--   totally naive implementation of the AIG structure that exists
--   exclusively for testing purposes.
data BasicGraph s

-- | A basic AIG literal datastructure based on LitTrees. This is a totally
--   naive implementation of the AIG structure that exists exclusively for
--   testing purposes.
data BasicLit s
basicProxy :: Proxy BasicLit BasicGraph
newBasicGraph :: IO (BasicGraph s)
instance GHC.Show.Show (Data.AIG.Interface.BasicLit s)
instance GHC.Show.Show Data.AIG.Interface.VerifyResult
instance GHC.Classes.Eq Data.AIG.Interface.VerifyResult
instance GHC.Show.Show Data.AIG.Interface.SatResult
instance GHC.Classes.Eq Data.AIG.Interface.SatResult
instance GHC.Classes.Ord Data.AIG.Interface.LitTree
instance GHC.Show.Show Data.AIG.Interface.LitTree
instance GHC.Classes.Eq Data.AIG.Interface.LitTree
instance Data.Traversable.Traversable Data.AIG.Interface.LitView
instance Data.Foldable.Foldable Data.AIG.Interface.LitView
instance GHC.Base.Functor Data.AIG.Interface.LitView
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.AIG.Interface.LitView a)
instance GHC.Show.Show a => GHC.Show.Show (Data.AIG.Interface.LitView a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.AIG.Interface.LitView a)
instance Test.QuickCheck.Arbitrary.Arbitrary Data.AIG.Interface.LitTree
instance Data.AIG.Interface.IsLit Data.AIG.Interface.BasicLit
instance Data.AIG.Interface.IsAIG Data.AIG.Interface.BasicLit Data.AIG.Interface.BasicGraph


-- | 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. Bits are stored in
--   most-significant-bit first order.
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

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

-- | Priority encoder. Given a bitvector, calculate the bit position of the
--   most-significant 1 bit, with position 0 corresponding to the
--   least-significant-bit. Return the "valid" bit, which is set iff at
--   least one bit in the input is set; and the calcuated bit position. If
--   no bits are set in the input (i.e. if the valid bit is false), the
--   calculated bit position is zero. The indicated bitwidth must be large
--   enough to hold the answer; in particular, we must have (length bv
--   &lt;= 2^w).
priorityEncode :: IsAIG l g => g s -> Int -> BV (l s) -> IO (l s, BV (l s))

-- | Compute the rounded-down base2 logarithm of the input bitvector. For x
--   &gt; 0, this uniquely satisfies 2^(logBase2_down(x)) &lt;= x &lt;
--   2^(logBase2_down(x)+1). For x = 0, we set logBase2(x) = -1. The output
--   bitvector has the same width as the input bitvector.
logBase2_down :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))

-- | Compute the rounded-up base2 logarithm of the input bitvector. For x
--   &gt; 1, this uniquely satisfies 2^(logBase2_up(x) - 1) &lt; x &lt;=
--   2^(logBase2_up(x)). For x = 1, logBase2_up 1 = 0. For x = 0, we get
--   logBase2_up 0 = <a>bitvector length</a>; this just happens to work out
--   from the defining fomula `logBase2_up x = logBase2_down (x-1) + 1`
--   when interpreted in 2's complement. The output bitvector has the same
--   width as the input bitvector.
logBase2_up :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))

-- | Count the number of leading zeros in the input vector; that is, the
--   number of more-significant digits set to 0 above the most significant
--   digit that is set. If the input vector is 0, the output of this
--   function is the length of the bitvector (i.e., all digits are counted
--   as leading zeros). The output bitvector has the same width as the
--   input bitvector.
countLeadingZeros :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s))

-- | Count the number of trailing zeros in the input vector; that is, the
--   number of less-significant digits set to 0 below the least significant
--   digit which is set. If the input vector is 0, the output of this
--   function is the length of the bitvector (i.e., all digits are counted
--   as trailing zeros). The output bitvector has the same width as the
--   input bitvector.
countTrailingZeros :: IsAIG l g => g s -> BV (l s) -> IO (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 division. Return value has length equal to the first
--   argument.
pdiv :: 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. This implementation is optimized for
--   the (common) case where the modulus is concrete.
pmod :: forall l g s. IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
instance Data.Traversable.Traversable Data.AIG.Operations.BV
instance Data.Foldable.Foldable Data.AIG.Operations.BV
instance GHC.Base.Functor Data.AIG.Operations.BV
instance GHC.Show.Show l => GHC.Show.Show (Data.AIG.Operations.BV l)
instance GHC.Classes.Ord l => GHC.Classes.Ord (Data.AIG.Operations.BV l)
instance GHC.Classes.Eq l => GHC.Classes.Eq (Data.AIG.Operations.BV l)


-- | 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 Data.AIG.Interface.IsLit l => Data.AIG.Interface.IsLit (Data.AIG.Trace.TraceLit l)
instance Data.AIG.Trace.Traceable l => GHC.Classes.Eq (Data.AIG.Trace.TraceLit l s)
instance Data.AIG.Trace.Traceable l => GHC.Classes.Ord (Data.AIG.Trace.TraceLit l s)
instance Data.AIG.Trace.TraceOp l g b => Data.AIG.Trace.TraceOp l g (GHC.Types.Int -> b)
instance Data.AIG.Trace.TraceOp l g b => Data.AIG.Trace.TraceOp l g (Data.AIG.Trace.TraceLit l s -> b)
instance Data.AIG.Trace.TraceOp l g b => Data.AIG.Trace.TraceOp l g ([Data.AIG.Trace.TraceLit l s] -> b)
instance Data.AIG.Trace.TraceOp l g b => Data.AIG.Trace.TraceOp l g (GHC.IO.FilePath -> b)
instance Data.AIG.Trace.TraceOutput l g x => Data.AIG.Trace.TraceOp l g (GHC.Types.IO x)
instance Data.AIG.Trace.TraceOutput l g a => Data.AIG.Trace.TraceOutput l g [a]
instance Data.AIG.Trace.TraceOutput l g (Data.AIG.Trace.TraceLit l s)
instance Data.AIG.Trace.TraceOutput l g GHC.Types.Int
instance Data.AIG.Trace.TraceOutput l g ()
instance Data.AIG.Trace.TraceOutput l g Data.AIG.Interface.SatResult
instance Data.AIG.Trace.TraceOutput l g Data.AIG.Interface.VerifyResult
instance Data.AIG.Trace.TraceOutput l g x => Data.AIG.Trace.TraceOutput l g (Data.AIG.Interface.LitView x)
instance (Data.AIG.Interface.IsAIG l g, Data.AIG.Trace.Traceable l) => Data.AIG.Interface.IsAIG (Data.AIG.Trace.TraceLit l) (Data.AIG.Trace.TraceGraph l g)


module Data.AIG