aig 0.1.0.0 → 0.2

raw patch · 4 files changed

+788/−110 lines, 4 filesdep +QuickCheckPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck

API changes (from Hackage documentation)

Files

• aig.cabal +6/−3
• src/Data/AIG/Interface.hs +176/−1
• src/Data/AIG/Operations.hs +418/−106
• src/Data/AIG/Trace.hs +188/−0

@@ -1,5 +1,5 @@ Name:               aig-Version:            0.1.0.0+Version:            0.2 License:            BSD3 License-file:       LICENSE Author:             Galois Inc.@@ -34,13 +34,16 @@     Data.AIG     Data.AIG.Interface     Data.AIG.Operations+    Data.AIG.Trace    default-Language: Haskell2010-  ghc-options:      -Wall+  ghc-options:      -Wall -fno-ignore-asserts -O2+  ghc-prof-options: -prof -auto-all -caf-all   build-depends:     base == 4.*,     mtl,-    vector+    vector,+    QuickCheck >= 2.7  -- Ugh. Temporary fix to make Hackage happy. --  if flag(enable-hpc)

@@ -1,6 +1,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE DeriveFunctor #-}  {- | Module      : Data.AIG.Interface@@ -17,6 +18,7 @@   ( -- * Main interface classes     IsLit(..)   , IsAIG(..)+  , lazyMux      -- * Helper datatypes   , Proxy(..)@@ -24,17 +26,51 @@   , Network(..)   , networkInputCount +  -- * Literal representations+  , LitView(..)+  , LitTree(..)+  , toLitTree+  , fromLitTree+  , toLitForest+  , fromLitForest+  , foldAIG+  , foldAIGs+  , unfoldAIG+  , unfoldAIGs+     -- * Representations of prover results   , SatResult(..)   , VerifyResult(..)   , toSatResult   , toVerifyResult++    -- * QuickCheck generators and testing+  , genLitView+  , genLitTree+  , getMaxInput+  , buildNetwork+  , randomNetwork   ) where -import Control.Applicative ((<$>))+import Control.Applicative import Control.Monad import Prelude hiding (not, and, or)+import Test.QuickCheck (Gen, Arbitrary(..), generate, oneof, sized, choose) +-- | Concrete datatype representing the ways+--   an AIG can be constructed.+data LitView a+  = And !a !a+  | NotAnd !a !a+  | Input !Int+  | NotInput !Int+  | TrueLit+  | FalseLit+ deriving (Eq,Show,Ord,Functor)++newtype LitTree = LitTree { unLitTree :: LitView LitTree }+ deriving (Eq,Show,Ord)+ class IsLit l where   -- | Negate a literal.   not :: l s -> l s@@ -163,6 +199,82 @@     f <- evaluator g inputs     return (f <$> outputs) +  -- | Build an evaluation function over an AIG using the provided view function+  abstractEvaluateAIG+          :: g s+          -> (LitView a -> IO a)+          -> IO (l s -> IO a)++-- | Evaluate the given literal using the provided view function+foldAIG :: IsAIG l g+        => g s+        -> (LitView a -> IO a)+        -> l s+        -> IO a+foldAIG n view l = do+   eval <- abstractEvaluateAIG n view+   eval l++-- | 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]+foldAIGs n view ls = do+   eval <- abstractEvaluateAIG n view+   mapM eval ls+++-- | Build an AIG literal by unfolding a constructor function+unfoldAIG :: IsAIG l g+          => g s+          -> (a -> IO (LitView a))+          -> a -> IO (l s)+unfoldAIG n unfold = f+ where f = unfold >=> g+       g (And x y)    = and' (f x) (f y)+       g (NotAnd x y) = fmap not $ and' (f x) (f y)+       g (Input i)    = getInput n i+       g (NotInput i) = fmap not $ getInput n i+       g TrueLit      = return $ trueLit n+       g FalseLit     = return $ falseLit n+       and' mx my = do+          x <- mx+          y <- my+          and n x y++-- | 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]+unfoldAIGs n unfold = mapM (unfoldAIG n unfold)++-- | Extract a tree representation of the given literal+toLitTree :: IsAIG l g => g s -> l s -> IO LitTree+toLitTree g = foldAIG g (return . LitTree)++-- | Construct an AIG literal from a tree representation+fromLitTree :: IsAIG l g => g s -> LitTree -> IO (l s)+fromLitTree g = unfoldAIG g (return . unLitTree)++-- | Extract a forest representation of the given list of literal s+toLitForest :: IsAIG l g => g s -> [l s] -> IO [LitTree]+toLitForest g = foldAIGs g (return . LitTree)++-- | Construct a list of AIG literals from a forest representation+fromLitForest :: IsAIG l g => g s -> [LitTree] -> IO [l s]+fromLitForest g = unfoldAIGs g (return . unLitTree)++-- | 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)+lazyMux g c+  | c === (trueLit g)  = \x _y -> x+  | c === (falseLit g) = \_x y -> y+  | otherwise = \x y -> join $ pure (mux g c) <*> x <*> y+ -- | A network is an and-inverstor graph paired with it's outputs, --   thus representing a complete combinational circuit. data Network l g where@@ -185,20 +297,83 @@ data SatResult    = Unsat    | Sat !([Bool])+   | SatUnknown   deriving (Eq,Show)  -- | Result of a verification check. data VerifyResult    = Valid    | Invalid [Bool]+   | VerifyUnknown   deriving (Eq, Show)  -- | Convert a sat result to a verify result by negating it. toVerifyResult :: SatResult -> VerifyResult toVerifyResult Unsat = Valid toVerifyResult (Sat l) = Invalid l+toVerifyResult SatUnknown = VerifyUnknown  -- | Convert a verify result to a sat result by negating it. toSatResult :: VerifyResult -> SatResult toSatResult Valid = Unsat toSatResult (Invalid l) = Sat l+toSatResult VerifyUnknown = SatUnknown++-- | Generate an arbitrary `LitView` given a generator for `a`+genLitView :: Gen a -> Gen (LitView a)+genLitView gen = oneof+     [ return TrueLit+     , return FalseLit+     , sized $ \n -> choose (0,n-1) >>= \i -> return (Input i)+     , sized $ \n -> choose (0,n-1) >>= \i -> return (NotInput i)+     , do x <- gen+          y <- gen+          return (And x y)+     , do x <- gen+          y <- gen+          return (NotAnd x y)+     ]++-- | Generate an arbitrary `LitTree`+genLitTree :: Gen LitTree+genLitTree = fmap LitTree $ genLitView genLitTree++-- | Given a LitTree, calculate the maximum input number in the tree.+--   Returns 0 if no inputs are referenced.+getMaxInput :: LitTree -> Int+getMaxInput (LitTree x) =+  case x of+     TrueLit -> 0+     FalseLit -> 0+     Input i -> i+     NotInput i -> i+     And a b -> max (getMaxInput a) (getMaxInput b)+     NotAnd a b -> max (getMaxInput a) (getMaxInput b)++instance Arbitrary LitTree where+  arbitrary = genLitTree+  shrink (LitTree TrueLit)      = []+  shrink (LitTree FalseLit)     = []+  shrink (LitTree (Input _))    = [LitTree TrueLit, LitTree FalseLit]+  shrink (LitTree (NotInput _)) = [LitTree TrueLit, LitTree FalseLit]+  shrink (LitTree (And x y)) =+      [ LitTree TrueLit, LitTree FalseLit, x, y ] +++      [ LitTree (And x' y') | (x',y') <- shrink (x,y) ]+  shrink (LitTree (NotAnd x y)) =+      [ LitTree TrueLit, LitTree FalseLit, x, y ] +++      [ LitTree (NotAnd x' y') | (x',y') <- shrink (x,y) ]+++-- | Given a list of LitTree, construct a corresponding AIG network+buildNetwork :: IsAIG l g => Proxy l g -> [LitTree] -> IO (Network l g)+buildNetwork proxy litForrest = do+   let maxInput = foldr max 0 $ map getMaxInput litForrest+   (SomeGraph g) <- newGraph proxy+   forM_ [0..maxInput] (\_ -> newInput g)+   ls <- fromLitForest g litForrest+   return (Network g ls)++-- | Generate a random network by building a random `LitTree`+--   and using that to construct a network.+randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g)+randomNetwork proxy = generate arbitrary >>= buildNetwork proxy

@@ -8,13 +8,14 @@ Stability   : experimental Portability : portable -A collection of higher-level operations (mostly various 2's complement arithmetic operations)-that can be build from the primitive And-Inverter Graph interface.+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   ( -- * Bitvectors     BV+  , empty   , length   , at   , (!)@@ -23,9 +24,14 @@   , take   , drop   , slice+  , sliceRev+  , mapM+  , zipWith   , zipWithM   , msb   , lsb+  , bvSame+  , bvShow      -- ** Building bitvectors   , generateM_msb0@@ -33,9 +39,28 @@   , generateM_lsb0   , generate_lsb0   , replicate+  , replicateM   , bvFromInteger+  , bvFromList   , muxInteger+  , singleton +    -- ** Lazy operators+  , lAnd+  , lAnd'+  , lOr+  , lOr'+  , lXor+  , lXor'+  , lEq+  , lEq'+  , lNot+  , lNot'++    -- ** Conditionals+  , ite+  , iteM+     -- ** Deconstructing bitvectors   , asUnsigned   , asSigned@@ -48,9 +73,13 @@   , addC   , sub   , subC+  , addConst+  , subConst      -- ** Multiplication and division   , mul+  , mulFull+  , smulFull   , squot   , srem   , uquot@@ -65,55 +94,52 @@      -- ** Numeric comparisons   , bvEq+  , isZero+  , nonZero   , sle   , slt   , ule   , ult+  , sabs      -- ** Extensions   , sext   , zext+  , trunc+  , zeroIntCoerce+  , signIntCoerce      -- * Polynomial multiplication and modulus   , pmul   , pmod   ) where -import Control.Applicative+import Control.Applicative hiding (empty) import Control.Exception import qualified Control.Monad-import Control.Monad.State hiding (zipWithM)+import Control.Monad.State hiding (zipWithM, replicateM, mapM) import Data.Bits ((.|.), setBit, shiftL, testBit) import qualified Data.Vector as V-import Prelude hiding (and, concat, length, not, or, replicate, splitAt, tail, (++), take, drop)+import qualified Data.Vector.Generic.Mutable as MV++import Prelude hiding (and, concat, length, not, or, replicate, splitAt, tail, (++), take, drop, zipWith, mapM) import qualified Prelude  import Data.AIG.Interface --- | A full adder which takes three inputs and returns output and carry.-halfAdder :: IsAIG l g => g s -> l s -> l s -> IO (l s, l s)-halfAdder g b c = do-  b_or_c <- or g b c-  c_out <- and g b c-  s <- and g b_or_c (not c_out)-  return (s, c_out) --- | A full adder which takes three inputs and returns output and carry.-fullAdder :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s, l s)-fullAdder g a b c_in = do-  a_xor_b <- xor g a b-  s <- xor g a_xor_b c_in-  a_and_b <- and g a b-  c_out <- or g a_and_b =<< and g a_xor_b c_in-  return (s, c_out)- -- | A BitVector consists of a sequence of symbolic bits and can be used --   for symbolic machine-word arithmetic. newtype BV l = BV { unBV :: V.Vector l }+  deriving (Eq, Ord, Show)  instance Functor BV where   fmap f (BV v) = BV (f <$> v) +-- | Empty bitvector+empty :: BV l+empty = BV V.empty+ -- | Number of bits in a bit vector length :: BV l -> Int length (BV v) = V.length v@@ -123,23 +149,47 @@  -- | Generate a bitvector of length @n@, using function @f@ to specify the bit literals. --   The indexes to @f@ are given in LSB-first order, i.e., @f 0@ is the least significant bit.+{-# INLINE generate_lsb0 #-} generate_lsb0    :: Int            -- ^ @n@, length of the generated bitvector    -> (Int -> l)     -- ^ @f@, function to calculate bit literals    -> BV l-generate_lsb0 c f = BV (V.generate c (\i -> f ((c-1)-i)))+generate_lsb0 c f = BV (V.reverse (V.generate c f))  -- | Generate a bitvector of length @n@, using monadic function @f@ to generate the bit literals. --   The indexes to @f@ are given in LSB-first order, i.e., @f 0@ is the least significant bit.+{-# INLINE generateM_lsb0 #-} generateM_lsb0-   :: Monad m+   :: MonadIO m    => Int            -- ^ @n@, length of the generated bitvector    -> (Int -> m l)   -- ^ @f@, computation to generate a bit literal    -> m (BV l)-generateM_lsb0 c f = return . BV . V.reverse =<< V.generateM c (\i -> f ((c-1)-i))+generateM_lsb0 c f = do+   mv <- liftIO (MV.new c)+   let buildVec i | i >= c = liftIO (V.unsafeFreeze mv) >>= return . BV+                  | otherwise = (f i >>= liftIO . MV.unsafeWrite mv (c-i-1)) >> (buildVec $! (i+1))+   buildVec 0+--generateM_lsb0 c f = return . BV . V.reverse =<< V.generateM c f +{-# INLINE generateM_scan_lsb0 #-}+generateM_scan_lsb0+   :: MonadIO m+   => Int            -- ^ @n@, length of the generated bitvector+   -> (Int -> a -> m (l,a))   -- ^ @f@, computation to generate a bit literal+   -> a+   -> m (BV l, a)+generateM_scan_lsb0 c f a0 = do+   mv <- liftIO (MV.new c)+   let buildVec i a | i >= c = liftIO (V.unsafeFreeze mv) >>= \v -> return (BV v, a)+                    | otherwise = do (x,a') <- f i a+                                     liftIO (MV.unsafeWrite mv (c-i-1) x)+                                     (buildVec $! (i+1)) a'+   buildVec 0 a0++ -- | Generate a bitvector of length @n@, using function @f@ to specify the bit literals. --   The indexes to @f@ are given in MSB-first order, i.e., @f 0@ is the most significant bit.+{-# INLINE generate_msb0 #-} generate_msb0    :: Int            -- ^ @n@, length of the generated bitvector    -> (Int -> l)     -- ^ @f@, function to calculate bit literals@@ -148,6 +198,7 @@  -- | Generate a bitvector of length @n@, using monadic function @f@ to generate the bit literals. --   The indexes to @f@ are given in MSB-first order, i.e., @f 0@ is the most significant bit.+{-# INLINE generateM_msb0 #-} generateM_msb0    :: Monad m    => Int            -- ^ @n@, length of the generated bitvector@@ -162,6 +213,18 @@    -> BV l replicate c e = BV (V.replicate c e) +-- | Generate a bit vector of length @n@ where every bit value is generated in turn by @m@.+replicateM+   :: Monad m+   => Int     -- ^ @n@, length of the bitvector+   -> m l     -- ^ @m@, the computation to produce a literal+   -> m (BV l)+replicateM c e = return . BV =<< V.replicateM c e++-- | Generate a one-element bitvector containing the given literal+singleton :: l -> BV l+singleton = BV . V.singleton+ -- | Project the individual bits of a BitVector. --   @x `at` 0@ is the most significant bit. --   It is an error to request an out-of-bounds bit.@@ -193,10 +256,29 @@       -> BV l  -- ^ a vector consisting of the bits from @i@ to @i+n-1@ slice (BV v) i n = BV (V.slice i n v) ++-- | Extract @n@ bits starting at index @i@, counting from+--   the end of the vector instead of the beginning.+--   The vector must contain at least @i+n@ elements.+sliceRev+      :: BV l+      -> Int   -- ^ @i@, 0-based start index from the end of the vector+      -> Int   -- ^ @n@, bits to take+      -> BV l+sliceRev (BV v) i n = BV (V.slice i' n v)+  where i' = V.length v - i - n++-- | Apply a monadic operation to each element of a bitvector in sequence+mapM :: Monad m => (a -> m b) -> BV a -> m (BV b)+mapM f (BV x) = V.mapM f x >>= return . BV++-- | Combine two bitvectors with a bitwise function+zipWith :: (l -> l -> l) -> BV l -> BV l -> BV l+zipWith f (BV x) (BV y) = assert (V.length x == V.length y) $ BV $ V.zipWith f x y+ -- | Combine two bitvectors with a bitwise monadic combiner action.-zipWithM :: (l -> l -> IO l) -> BV l -> BV l -> IO (BV l)-zipWithM f (BV x) (BV y) = assert (V.length x == V.length y) $-  BV <$> V.zipWithM f x y+zipWithM :: Monad m => (l -> l -> m l) -> BV l -> BV l -> m (BV l)+zipWithM f (BV x) (BV y) = assert (V.length x == V.length y) $ V.zipWithM f x y >>= return . BV  -- | Convert a bitvector to a list, most significant bit first. bvToList :: BV l -> [l]@@ -212,6 +294,14 @@ (!) :: BV l -> Int -> l (!) v i = v `at` (length v - 1 - i) +-- | 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 'x'.+bvShow :: IsAIG l g => g s -> BV (l s) -> String+bvShow g v = map f $ bvToList v+ where f x | x === trueLit g  = '1'+           | x === falseLit g = '0'+           | otherwise = 'x'+ -- | Generate a bitvector from an integer value, using 2's complement representation. bvFromInteger    :: IsAIG l g@@ -219,7 +309,8 @@    -> Int       -- ^ number of bits in the resulting bitvector    -> Integer   -- ^ integer value    -> BV (l s)-bvFromInteger g n v = generate_lsb0 n $ \i -> constant g (v `testBit` i)+bvFromInteger g n v = generate_msb0 n $ \i -> constant g (v `testBit` (n-i-1))+   --generate_lsb0 n $ \i -> constant g (v `testBit` i)  -- | Interpret a bitvector as an unsigned integer.  Return @Nothing@ if --   the bitvector is not concrete.@@ -229,25 +320,19 @@         go x i | i >= n = return x         go x i = do           b <- asConstant g (v `at` i)-          let y  = if b then 1 else 0-          let z = x `shiftL` 1 .|. y+          let y = if b then 1 else 0+          let z = (x `shiftL` 1) .|. y           seq z $ go z (i+1)  -- | Interpret a bitvector as a signed integer.  Return @Nothing@ if --   the bitvector is not concrete. asSigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer-asSigned g v = assert (n > 0) $ go 0 1+asSigned g v = assert (n > 0) $ (signfix =<< asUnsigned g (drop 1 v))   where n = length v-        m = n-1-        go x i | i < m = do-          b <- asConstant g (v `at` i)-          let y  = if b then 1 else 0-          let z = x `shiftL` 1 .|. y-          seq z $ go z (i+1)-        go x i = do-          msbv <- asConstant g (v `at` i)-          return $ if msbv then x - 2^m-                           else x+        signfix x+            | msb v === trueLit g  = Just (x - 2^(n-1))+            | msb v === falseLit g = Just x+            | otherwise = Nothing  -- | Retrieve the most significant bit of a bitvector. msb :: BV l -> l@@ -282,46 +367,179 @@   | c === falseLit g = y   | otherwise = join $ zipWithM (mux g c) <$> x <*> y +{-# INLINE lNot #-}+-- | Lazy negation of a circuit.+lNot :: IsAIG l g => g s -> IO (l s) -> IO (l s)+lNot g = fmap (lNot' g)++{-# INLINE lNot' #-}+lNot' :: IsAIG l g => g s -> l s -> l s+lNot' g x | x === trueLit g = falseLit g+          | x === falseLit g = trueLit g+          | otherwise = not x++{-# INLINE lOr #-}+-- | 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 g x y = lNot g (lAnd g (lNot g x) (lNot g y))++{-# INLINE lOr' #-}+lOr' :: IsAIG l g => g s -> l s -> l s -> IO (l s)+lOr' g x y = lNot g (lAnd' g (lNot' g x) (lNot' g y))++{-# INLINE lEq #-}+-- | 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 g x y = lNot g (lXor g x y)++{-# INLINE lEq' #-}+lEq' :: IsAIG l g => g s -> l s -> l s -> IO (l s)+lEq' g x y = lNot g (lXor' g x y)++-- | 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 g x y = do+  x' <- x+  if      x' === trueLit g  then y+  else if x' === falseLit g then return (falseLit g)+  else do+      y' <- y+      if      y' === trueLit g  then return x'+      else if y' === falseLit g then return (falseLit g)+      else and g x' y'++lAnd'' :: IsAIG l g => g s -> l s -> IO (l s) -> IO (l s)+lAnd'' g x y =+  if      x === trueLit g  then y+  else if x === falseLit g then return (falseLit g)+  else do+      y' <- y+      if      y' === trueLit g  then return x+      else if y' === falseLit g then return (falseLit g)+      else and g x y'++lAnd' :: IsAIG l g => g s -> l s -> l s -> IO (l s)+lAnd' g x y =+  if      x === trueLit g  then return y+  else if x === falseLit g then return (falseLit g)+  else if y === trueLit g  then return x+  else if y === falseLit g then return (falseLit g)+  else and g x y++lXor' :: IsAIG l g => g s -> l s -> l s -> IO (l s)+lXor' g x y =+  if      x === trueLit g  then return (not y)+  else if x === falseLit g then return y+  else if y === trueLit g  then return (not x)+  else if y === falseLit g then return x+  else xor g x y++-- | 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 g x y = do+  x' <- x+  y' <- y+  if      x' === trueLit g  then return (not y')+  else if x' === falseLit g then return y'+  else if y' === trueLit g  then return (not x')+  else if y' === falseLit g then return x'+  else xor g x' y'+++-- | A half adder which takes two inputs and returns output and carry.+{-# INLINE halfAdder #-}+halfAdder :: IsAIG l g => g s -> l s -> l s -> IO (l s, l s)+halfAdder g b c = do+  c_out <- lAnd' g b c+  s <- lAnd'' g (not c_out) (lOr' g b c)+  return (s, c_out)+++-- | A full adder which takes three inputs and returns output and carry.+{-# INLINE fullAdder #-}+fullAdder :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s, l s)+fullAdder g a b c_in = do+   s <- lXor' g c_in =<< lXor' g a b+   c_out <- lOr g (lAnd' g a b) (lAnd'' g c_in (lXor' g a b))+   return (s, c_out)+ -- | Implements a ripple carry adder.  Both addends are assumed to have --   the same length. ripple_add :: IsAIG l g            => g s            -> BV (l s)            -> BV (l s)-           -> l s                -- ^ carry-in bit            -> IO (BV (l s), l s) -- ^ sum and carry-out bit-ripple_add _ x _ c | length x == 0 = return (x, c)-ripple_add g x y c0 = do-  let unfold i = StateT $ \c -> do-        fullAdder g (x `at` i) (y `at` i) c-  runStateT (generateM_lsb0 (length x) unfold) c0+ripple_add g x _ | length x == 0 = return (x, falseLit g)+ripple_add g x y = do+   let unfold i = fullAdder g (x!i) (y!i)+   generateM_scan_lsb0 (length x) unfold (falseLit g) +-- ripple_add g x y = do+--     r <- newIORef (falseLit g)+--     let unfold i = do (s,c) <- fullAdder g (x!i) (y!i) =<< readIORef r+--                       writeIORef r c+--                       return s+--     sum <- generateM_lsb0 (length x) unfold+--     c_out <- readIORef r+--     return (sum,c_out)++ -- | A subtraction circuit which takes three inputs and returns output and carry.+{-# INLINE fullSub #-} fullSub :: IsAIG l g => g s -> l s -> l s -> l s -> IO (l s, l s) fullSub g x y b_in = do-  y_eq_b <- eq g y b_in-  s <- eq g x y_eq_b--  y_and_b <- and g y b_in-  c2 <- and g (not x) =<< or g y b_in-  b_out <- or g y_and_b c2+  s <- lEq' g x =<< (lEq' g y b_in)+  b_out <- lOr g (lAnd' g y b_in) (lAnd'' g (not x) (lOr' g y b_in))   return (s, b_out) + -- | Subtract two bit vectors, returning result and borrow bit.-full_sub :: IsAIG l g+ripple_sub :: IsAIG l g          => g s          -> BV (l s)          -> BV (l s)          -> IO (BV (l s), l s)-full_sub g x _ | length x == 0 = return (x,falseLit g)-full_sub g x y = do-  let unfold i = StateT $ \b -> fullSub g (x `at` i) (y `at` i) b-  runStateT (generateM_lsb0 (length x) unfold) (falseLit g)+ripple_sub g x _ | length x == 0 = return (x,falseLit g)+ripple_sub g x y = do+  let unfold i = fullSub g (x ! i) (y ! i)+  generateM_scan_lsb0 (length x) unfold (falseLit g) +-- ripple_sub g x y = do+--     r <- newIORef (falseLit g)+--     let unfold i = do (s,b) <- fullSub g (x!i) (y!i) =<< readIORef r+--                       writeIORef r b+--                       return s+--     diff <- generateM_lsb0 (length x) unfold+--     b_out <- readIORef r+--     return (diff,b_out)+++-- | Compute just the borrow bit of a subtraction.+{-# INLINE ripple_sub_borrow #-}+ripple_sub_borrow :: IsAIG l g+         => g s+         -> BV (l s)+         -> BV (l s)+         -> IO (l s)+ripple_sub_borrow g x y = go 0 (falseLit g)+   where n = length x+         go i b | i >= n = return b+                | otherwise = (go $! (i+1)) =<<+                                  (lOr g (lAnd' g b (y!i))+                                         (lAnd'' g (lNot' g (x!i)) (lOr' g (y!i) b))+                                  )+ -- | Compute the 2's complement negation of a bitvector neg :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s)) neg g x = evalStateT (generateM_lsb0 (length x) unfold) (trueLit g)-  where unfold i = StateT $ \c -> halfAdder g (not (x `at` i)) c+  where unfold i = StateT $ halfAdder g (lNot' g (x ! i))  -- | 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))@@ -329,7 +547,7 @@  -- | 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)-addC g x y = ripple_add g x y (falseLit g)+addC g x y = assert (length x == length y) $ ripple_add g x y  -- | 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))@@ -337,22 +555,70 @@  -- | 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)-subC g x y = ripple_add g x (not <$> y) (trueLit g)+subC g x y = assert (length x == length y) $ ripple_sub g x y +-- | Add a constant value to a bitvector+addConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s))+addConst g x y = do+  let n = length x+  m <- MV.new n+  let adderStepM c i+        | i == n = return ()+        | otherwise = do+          let a = x ! i+          let b = y `testBit` i+          ac <- lAnd' g a c+          negAnegC <- lAnd' g (lNot' g a) (lNot' g c)+          aEqC <- lOr' g ac negAnegC+          if b+            then do+              MV.write m (n-i-1) aEqC+              adderStepM (lNot' g negAnegC) (i+1)+            else do+              MV.write m (n-i-1) (lNot' g aEqC)+              adderStepM ac (i+1)+  adderStepM (falseLit g) 0+  fmap BV $ V.freeze m --- | Multiply two bitvectors with the same size.+--addConst g x c = add g x (bvFromInteger g (length x) c)++-- | Add a constant value to a bitvector+subConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s))+subConst g x c = addConst g x (-c)+++-- | 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))-mul g x y = do+mul g x y = assert (length x == length y) $ do   -- Create mutable array to store result.   let n = length y   -- Function to update bits.   let updateBits i z | i == n = return z       updateBits i z = do-        z_inc <- add g z (shlC g x i)-        z' <- ite g (y ! i) z_inc z+        z' <- iteM g (y ! i) (add g z (shlC g x i)) (return z)         updateBits (i+1) z'   updateBits 0 $ replicate (length x) (falseLit g) +-- | Unsigned multiply two bitvectors with size @m@ and size @n@,+--   resulting in a vector of size @m+n@.+mulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+mulFull g x y =+    let len = length x + length y+        x' = zext g x len+        y' = zext g y len+     in mul g x' y'++-- | Signed multiply two bitvectors with size @m@ and size @n@,+--   resulting in a vector of size @m+n@.+smulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))+smulFull g x y = do+    let len = length x + length y+        x' = sext g x len+        y' = sext g y len+     in mul g x' y'+ -- | 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)) squot g x y = fst <$> squotRem g x y@@ -365,19 +631,19 @@ shiftL1 :: BV l -> l -> BV l shiftL1 (BV v) e = assert (V.length v > 0) $ BV (V.tail v `V.snoc` e) --- | Cons value to start of list and shift other elements right.-shiftR1 :: l -> BV l -> BV l-shiftR1 e (BV v) = assert (V.length v > 0) $ BV (e `V.cons` V.init v)+-- -- | Cons value to start of list and shift other elements right.+-- shiftR1 :: l -> BV l -> BV l+-- shiftR1 e (BV v) = assert (V.length v > 0) $ BV (e `V.cons` V.init v) +-- stepN :: Monad m => Int -> (a -> m a) -> a -> m a+-- stepN n f x+--   | n > 0 = stepN (n-1) f =<< f x+--  | otherwise = return x+ splitAt :: Int -> BV l -> (BV l, BV l) splitAt n (BV v) = (BV x, BV y)   where (x,y) = V.splitAt n v -stepN :: Monad m => Int -> (a -> m a) -> a -> m a-stepN n f x-  | n > 0 = stepN (n-1) f =<< f x-  | otherwise = return x- -- | Return absolute value of signed bitvector. sabs :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s)) sabs g x = assert (length x > 0) $ negWhen g x (msb x)@@ -400,8 +666,8 @@           let rs = rr `shiftL1` p           let (r,q) = splitAt n rs            -- Subtract the divisor from the left half of the "remainder register"-          (s,b) <- full_sub g r divisor-          divStep (i+1) (not b) =<< ite g b rs (s ++ q)+          (s,b) <- ripple_sub g r divisor+          divStep (i+1) (lNot' g b) =<< ite g b rs (s ++ q)     divStep 0 (falseLit g) initial  -- Perform quotRem on the absolute value of the operands.  Then, negate the@@ -412,26 +678,39 @@          -> BV (l s)          -> BV (l s)          -> IO (BV (l s), BV (l s))-squotRem g dividend' divisor' = do-  let n = length dividend'-  assert (n > 0 && n == length divisor') $ do-    let dsign = msb dividend'-    dividend <- sabs g dividend'-    divisor  <- sabs g divisor'-    -- Given an n-bit dividend and divisor, 'initial' is the starting value of-    -- the 2n-bit "remainder register" that carries both the quotient and remainder;-    let initial = zext g dividend (2*n)-    let divStep rrOrig = do-          let (r,q) = splitAt n rrOrig-          s <- sub g r divisor-          ite g (msb s)-                (rrOrig `shiftL1` falseLit g)     -- rem < 0, orig rr's quot lsl'd w/ 0-                ((s ++ q) `shiftL1` trueLit g) -- rem >= 0, new rr's quot lsl'd w/ 1-    (qr,rr) <- splitAt n <$> stepN n divStep (initial `shiftL1` falseLit g)-    q' <- negWhen g qr =<< xor g dsign (msb divisor')-    r' <- negWhen g (falseLit g `shiftR1` rr) dsign-    return (q', r')+squotRem g dividend divisor =+    assert (length dividend > 0 && length dividend == length divisor) $ do+    let sign1 = msb dividend+    let sign2 = msb divisor+    signXor <- xor g sign1 sign2+    dividend' <- negWhen g dividend sign1+    divisor'  <- negWhen g divisor sign2+    (q,r) <- uquotRem g dividend' divisor'+    q' <- negWhen g q signXor+    r' <- negWhen g r sign1+    return (q',r') +-- This code seems to have a bug...+-- squotRem g dividend' divisor' = do+--   let n = length dividend'+--   assert (n > 0 && n == length divisor') $ do+--     let dsign = msb dividend'+--     dividend <- sabs g dividend'+--     divisor  <- sabs g divisor'+--     -- Given an n-bit dividend and divisor, 'initial' is the starting value of+--     -- the 2n-bit "remainder register" that carries both the quotient and remainder;+--     let initial = zext g dividend (2*n)+--     let divStep rrOrig = do+--           let (r,q) = splitAt n rrOrig+--           s <- sub g r divisor+--           ite g (msb s)+--                 (rrOrig `shiftL1` falseLit g)     -- rem < 0, orig rr's quot lsl'd w/ 0+--                 ((s ++ q) `shiftL1` trueLit g) -- rem >= 0, new rr's quot lsl'd w/ 1+--     (qr,rr) <- splitAt n <$> stepN n divStep (initial `shiftL1` falseLit g)+--     q' <- negWhen g qr =<< xor g dsign (msb divisor')+--     r' <- negWhen g (falseLit g `shiftR1` rr) dsign+--     return (q', r')+ -- | 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)) uquot g x y = fst <$> uquotRem g x y@@ -440,41 +719,53 @@ urem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) urem g x y = snd <$> uquotRem g x y +-- | Test syntactic equalify of two bitvectors using the `===` operation+bvSame :: IsLit l => BV (l s) -> BV (l s) -> Bool+bvSame (BV x) (BV y) = assert (V.length x == V.length y) $ V.foldr (&&) True $ V.zipWith (===) x y+ -- | Test equality of two bitvectors with the same size. bvEq :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)-bvEq g x y = go 0 (trueLit g)+bvEq g x y = assert (n == length y) $ go 0 (trueLit g)   where n = length x         go i r | i == n = return r         go i r = go (i+1) =<< and g r =<< eq g (x `at` i) (y `at` i) +-- | Test if a bitvector is equal to zero+isZero :: IsAIG l g => g s -> BV (l s) -> IO (l s)+isZero g (BV v) = V.foldM (\x y -> and g (lNot' g x) y) (trueLit g) v++-- | Test if a bitvector is distinct from zero+nonZero :: IsAIG l g => g s -> BV (l s) -> IO (l s)+nonZero g bv = lNot g $ isZero g bv+ -- | Unsigned less-than on bitvector with the same size. ult :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)-ult g x y = snd <$> full_sub g x y+ult g x y = assert (length x == length y) $ ripple_sub_borrow g x y  -- | 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)-ule g x y = not <$> ult g y x+ule g x y = lNot g $ ult g y x  -- | Signed less-than on bitvector with the same size. slt :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s)-slt g x y = do+slt g x y = assert (length x == length y) $ do   let xs = x `at` 0   let ys = y `at` 0   -- x is negative and y is positive.-  c0 <- and g xs (not ys)+  c0 <- and g xs (lNot' g ys)   -- x is positive and y is negative.-  c1 <- and g (not xs) ys-  c2 <- and g (not c1) =<< ult g (tail x) (tail y)+  c1 <- and g (lNot' g xs) ys+  c2 <- and g (lNot' g c1) =<< ult g (tail x) (tail y)   or g c0 c2  -- | 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)-sle g x y = not <$> slt g y x+sle g x y = lNot g $ slt g y x  -- | @sext v n@ sign extends @v@ to be a vector with length @n@. -- This function requires that @n >= length v@ and @length v > 0@.-sext :: BV l -> Int -> BV l-sext v r = assert (r >= n && n > 0) $ replicate (r - n) (msb v) ++ v+sext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s)+sext _g v r = assert (r >= n && n > 0) $ replicate (r - n) (msb v) ++ v   where n = length v  -- | @zext g v n@ zero extends @v@ to be a vector with length @n@.@@ -483,6 +774,27 @@ zext g v r = assert (r >= n) $ replicate (r - n) (falseLit g) ++ v   where n = length v +-- | Truncate the given bit vector to the specified length+trunc :: Int -> BV (l s) -> BV (l s)+trunc w vx = assert (length vx >= w) $ drop (length vx - w) vx++-- | 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)+zeroIntCoerce g r t+    | r > l = zext g t r+    | r < l = trunc r t+    | otherwise = t+  where l = length t++-- | 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)+signIntCoerce g r t+    | r > l = sext g t r+    | r < l = trunc r t+    | otherwise = t+  where l = length t++ -- | @muxInteger mergeFn maxValue lv valueFn@ returns a circuit -- whose result is @valueFn v@ when @lv@ has value @v@. muxInteger :: (Integral i, Monad m)@@ -606,7 +918,7 @@         next :: [l s] -> IO [l s]         next [] = return []         next (b : bs) = do-          m' <- mapM (and g b) m+          m' <- Prelude.mapM (and g b) m           let bs' = bs Prelude.++ [falseLit g]           Control.Monad.zipWithM (xor g) m' bs' @@ -614,7 +926,7 @@         go i p acc           | i >= length x = return acc           | otherwise = do-              px <- mapM (and g (x ! i)) p+              px <- Prelude.mapM (and g (x ! i)) p               acc' <- Control.Monad.zipWithM (xor g) px acc               p' <- next p               go (i+1) p' acc'

@@ -0,0 +1,188 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+++{- |+Module      : Data.AIG.Interface+Copyright   : (c) Galois, Inc. 2014+License     : BSD3+Maintainer  : jhendrix@galois.com+Stability   : experimental+Portability : portable++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 where++import Prelude hiding (not, and, or)+import Data.IORef+import System.IO+import Control.Exception+import System.IO.Unsafe++import Data.AIG.Interface+++class Traceable l where+  compareLit :: l s -> l s -> Ordering+  showLit :: l s -> String++newtype TraceLit l s = TraceLit { unTraceLit :: l s }++data TraceGraph (l :: * -> * ) g s+   = TraceGraph+   { tGraph :: g s+   , tActive :: IORef (Maybe Handle)+   }++proxy :: Traceable l => Proxy l g -> Proxy (TraceLit l) (TraceGraph l g)+proxy (Proxy _) = Proxy (\x -> x)++activateTracing :: TraceGraph l g s -> FilePath -> IO ()+activateTracing g fp = do+    maybe (return ()) hClose =<< readIORef (tActive g)+    h <- openFile fp WriteMode+    writeIORef (tActive g) (Just h)++deactiveTracing :: TraceGraph l g s -> IO ()+deactiveTracing g = do+    maybe (return ()) hClose =<< readIORef (tActive g)+    writeIORef (tActive g) Nothing++withTracing :: TraceGraph l g s -> FilePath -> IO a -> IO a+withTracing g fp m =+   bracket (do old <- readIORef (tActive g)+               h <- openFile fp WriteMode+               writeIORef (tActive g) (Just h)+               return (h,old))+           (\(h,old) -> hClose h >> writeIORef (tActive g) old)+           (\_ -> m)++instance IsLit l => IsLit (TraceLit l) where+  not (TraceLit l) = TraceLit (not l)+  (TraceLit x) === (TraceLit y) = x === y++instance Traceable l => Eq (TraceLit l s) where+  (TraceLit x) == (TraceLit y) = compareLit x y == EQ++instance Traceable l => Ord (TraceLit l s) where+  compare (TraceLit x) (TraceLit y) = compareLit x y+++class TraceOp l g a where+  traceOp :: (Traceable l, IsAIG l g) => TraceGraph l g s -> String -> a -> a++class TraceOutput l g x where+  traceOutput :: (Traceable l, IsAIG l g) => TraceGraph l g s -> x -> String++instance TraceOp l g b => TraceOp l g (Int -> b) where+  traceOp g msg f i = traceOp g (msg++" "++show i) (f i)++instance TraceOp l g b => TraceOp l g (TraceLit l s -> b) where+  traceOp g msg f i = traceOp g (msg++" "++showLit (unTraceLit i)) (f i)++instance TraceOp l g b => TraceOp l g ([TraceLit l s] -> b) where+  traceOp g msg f is = traceOp g (msg++" ["++unwords (map (showLit . unTraceLit) is)++"]") (f is)++instance TraceOp l g b => TraceOp l g (FilePath -> b) where+  traceOp g msg f i = traceOp g (msg++" "++i) (f i)++instance TraceOutput l g x => TraceOp l g (IO x) where+  traceOp g msg f = do+      mh <- readIORef (tActive g)+      case mh of+        Nothing -> f+        Just h -> do+            hPutStr h msg+            hFlush h+            x <- f+            hPutStrLn h $ " result "++traceOutput g x+            hFlush h+            return x++instance TraceOutput l g (TraceLit l s) where+  traceOutput _g (TraceLit l) = showLit l++instance TraceOutput l g Int where+  traceOutput _g i = show i++instance TraceOutput l g () where+  traceOutput _g () = "()"++instance TraceOutput l g SatResult where+  traceOutput _g r = show r++instance TraceOutput l g VerifyResult where+  traceOutput _g r = show r++withNewGraphTracing :: (IsAIG l g, Traceable l)+                    => Proxy l g+                    -> FilePath+                    -> (forall s. TraceGraph l g s -> IO a)+                    -> IO a+withNewGraphTracing _ fp f = withNewGraph undefined $ \g -> withTracing g fp (f g)++instance (IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g) where+  withNewGraph _ f = withNewGraph undefined $ \g -> do+                         r <- newIORef Nothing+                         f (TraceGraph g r)++  aigerNetwork _ fp = do+          (Network g outs) <- aigerNetwork undefined fp+          r <- newIORef Nothing+          return (Network (TraceGraph g r) (map TraceLit outs))++  trueLit g = TraceLit $ trueLit (tGraph g)+  falseLit g = TraceLit $ falseLit (tGraph g)++  newInput g = traceOp g "NewInput" $ fmap TraceLit $ newInput (tGraph g)++  and g = traceOp g "and" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ and (tGraph g) x y+  or g = traceOp g "or" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ or (tGraph g) x y+  implies g = traceOp g "implies" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ implies (tGraph g) x y+  eq g = traceOp g "eq" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $ eq (tGraph g) x y+  xor g = traceOp g "xor" $ \(TraceLit x) (TraceLit y) -> fmap TraceLit $  xor (tGraph g) x y+  mux g = traceOp g "mux" $ \(TraceLit x) (TraceLit y) (TraceLit z) -> fmap TraceLit $ mux (tGraph g) x y z++  inputCount g = traceOp g "inputCount" $ inputCount (tGraph g)++  getInput g = traceOp g "getInput" $ \i -> fmap TraceLit $ getInput (tGraph g) i++  writeAiger fp0 (Network g outs0) =+       (traceOp g "writeAiger" $ \fp outs -> writeAiger fp (Network (tGraph g) (map unTraceLit outs))) fp0 outs0++  checkSat g = traceOp g "checkSat" $ \(TraceLit x) -> checkSat (tGraph g) x++  cec (Network g1 outs1') (Network g2 outs2') =+      (traceOp g1 "cec" $ \outs1 outs2 ->+        cec (Network (tGraph g1) (map unTraceLit outs1))+            (Network (tGraph g2) (map unTraceLit outs2)))+            outs1' outs2'++  evaluator g ins =+        do mh <- readIORef (tActive g)+           maybe (return ()) (\h -> (hPutStrLn h $ unwords ["building evaluator",show ins]) >> hFlush h) mh+           let traceIO l x h = (hPutStrLn h $ unwords ["evaluator call",show ins,showLit l,show x]) >> hFlush h+           let trace l x =+                  case mh of+                     Nothing -> x+                     Just h  -> seq (unsafePerformIO (traceIO l x h)) x+           ev <- evaluator (tGraph g) ins+           return (\(TraceLit l) -> trace l $ ev l)++  abstractEvaluateAIG g f =+        do mh <- readIORef (tActive g)+           maybe (return ()) (\h -> (hPutStrLn h $ unwords ["building abstract evaluator"]) >> hFlush h) mh+           let traceIO l h = (hPutStrLn h $ unwords ["abstract evaluator call",showLit l]) >> hFlush h+           let trace l x =+                  case mh of+                     Nothing -> return x+                     Just h  -> traceIO l h >> return x+           ev <- abstractEvaluateAIG (tGraph g) f+           return (\(TraceLit l) -> trace l =<< ev l)