aig 0.2.4 → 0.2.5

raw patch · 5 files changed

+453/−10 lines, 5 filesdep +aigdep +tastydep +tasty-ant-xmlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: aig, tasty, tasty-ant-xml, tasty-quickcheck

API changes (from Hackage documentation)

Files

• aig.cabal +21/−2
• src/Data/AIG/Interface.hs +120/−2
• src/Data/AIG/Operations.hs +12/−6
• tests/Tests/Operations.hs +271/−0
• tests/aig-test.hs +29/−0

@@ -1,10 +1,10 @@ Name:               aig-Version:            0.2.4+Version:            0.2.5 License:            BSD3 License-file:       LICENSE Author:             Galois Inc. Maintainer:         jhendrix@galois.com-Copyright:          (c) 2014-2015 Galois Inc.+Copyright:          (c) 2014-2017 Galois Inc. Category:           Data build-type:         Simple cabal-Version:      >= 1.10@@ -38,4 +38,23 @@     base-compat >= 0.6.0,     mtl,     vector,+    QuickCheck >= 2.7++test-suite aig-test+  type: exitcode-stdio-1.0+  hs-source-dirs: tests++  ghc-options: -Wall+  default-language: Haskell2010++  main-is: aig-test.hs+  other-modules:+    Tests.Operations++  build-depends:+    base == 4.*,+    aig,+    tasty,+    tasty-ant-xml,+    tasty-quickcheck >= 0.8.1,     QuickCheck >= 2.7

@@ -1,6 +1,6 @@ {- | Module      : Data.AIG.Interface-Copyright   : (c) Galois, Inc. 2014+Copyright   : (c) Galois, Inc. 2014-2017 License     : BSD3 Maintainer  : jhendrix@galois.com Stability   : experimental@@ -28,6 +28,7 @@   , networkOutputCount   -- * Literal representations   , LitView(..)+  , negateLitView   , LitTree(..)   , toLitTree   , fromLitTree@@ -50,11 +51,16 @@   , getMaxInput   , buildNetwork   , randomNetwork+  , BasicGraph+  , BasicLit+  , basicProxy+  , newBasicGraph   ) where +import qualified Prelude as Prelude import Control.Applicative import Control.Monad-import Prelude()+import Data.IORef import Prelude.Compat hiding (not, and, or, mapM) import Test.QuickCheck (Gen, Arbitrary(..), generate, oneof, sized, choose) @@ -69,6 +75,16 @@   | FalseLit  deriving (Eq,Show,Ord,Functor,Foldable,Traversable) +negateLitView :: LitView a -> LitView a+negateLitView l = case l of+     TrueLit    -> FalseLit+     FalseLit   -> TrueLit+     Input i    -> NotInput i+     NotInput i -> Input i+     And x y    -> NotAnd x y+     NotAnd x y -> And x y++ newtype LitTree = LitTree { unLitTree :: LitView LitTree }  deriving (Eq,Show,Ord) @@ -391,3 +407,105 @@ --   and using that to construct a network. randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g) randomNetwork proxy = generate arbitrary >>= buildNetwork proxy++------------------------------------------------------------------+-- | A basic "Graph" datastructure based on LitTrees.  This is a totally+--   naive implementation of the AIG structure that exists+--   exclusively for testing purposes.+newtype BasicGraph s = BasicGraph (IORef Int)++------------------------------------------------------------------+-- | A basic AIG literal datastructure based on LitTrees.+--   This is a totally+--   naive implementation of the AIG structure that exists+--   exclusively for testing purposes.+newtype BasicLit s = BasicLit LitTree+ deriving (Show)++basicProxy :: Proxy BasicLit BasicGraph+basicProxy = Proxy (\x -> x)++notTree :: LitTree -> LitTree+notTree (LitTree x) = LitTree . negateLitView $ x++andTree :: LitTree -> LitTree -> LitTree+andTree (LitTree FalseLit) _    = LitTree FalseLit+andTree _ (LitTree FalseLit)    = LitTree FalseLit+andTree (LitTree TrueLit) y     = y+andTree x (LitTree TrueLit)     = x+andTree x y                     = LitTree (And x y)++newBasicGraph :: IO (BasicGraph s)+newBasicGraph =+  do r <- newIORef 0+     return (BasicGraph r)++instance IsLit BasicLit where+  not (BasicLit x) = BasicLit . notTree $ x+  (BasicLit x) === (BasicLit y) = x == y++instance IsAIG BasicLit BasicGraph where+  withNewGraph _proxy k = k =<< newBasicGraph++  aigerNetwork _proxy _fp =+    fail "Cannot read AIGER files from the BasicGraph implementation"++  trueLit  _g = BasicLit . LitTree $ TrueLit+  falseLit _g = BasicLit . LitTree $ FalseLit++  newInput (BasicGraph r) =+     atomicModifyIORef' r (\n -> (n+1, BasicLit . LitTree . Input $ n))++  and _g (BasicLit x) (BasicLit  y) = return . BasicLit $ andTree x y++  inputCount (BasicGraph r) = readIORef r++  -- | Get input at given index in the graph.+  getInput _g i = return . BasicLit . LitTree . Input $ i++  writeAiger _fp _ntk =+     fail "Cannot write AIGER files from the BasicGraph implementation"++  writeCNF _g _l _fp =+     fail "Cannot write CNF files from the BasicGraph implementation"++  checkSat _g _l =+     fail "Cannot SAT check graphs in the BasicGraph implementation"++  cec _g1 _g2 =+     fail "Cannot CEC graphs in the BasicGraph implementation"++  asConstant _g (BasicLit bl) = go bl+    where+     go (LitTree l) = go' l++     go' l = case l of+         TrueLit    -> pure True+         FalseLit   -> pure False+         And x y    -> (&&) <$> go x <*> go y+         NotAnd x y -> Prelude.not <$> go' (And x y)+         Input _    -> Nothing+         NotInput _ -> Nothing++  -- | Evaluate the network on a set of concrete inputs.+  evaluator _g xs = return (\(BasicLit x) -> eval x)+    where+     eval :: LitTree -> Bool+     eval (LitTree x) = eval' x++     eval' :: LitView LitTree -> Bool+     eval' TrueLit      = True+     eval' FalseLit     = False+     eval' (And x y)    = eval x && eval y+     eval' (NotAnd x y) = Prelude.not (eval' (And x y))+     eval' (Input i)    = case drop i xs of+                            (b:_) -> b+                            []    -> error $ unwords ["Input value out of bounds", show i]+     eval' (NotInput i) = Prelude.not (eval' (Input i))++  -- | Examine the outermost structure of a literal to see how it was constructed+  litView _ (BasicLit (LitTree x)) = return (fmap BasicLit x)++  -- | Build an evaluation function over an AIG using the provided view function+  abstractEvaluateAIG _g f = return (\(BasicLit x) -> h x)+   where h (LitTree x) = f =<< traverse h x

@@ -877,9 +877,12 @@     -> BV (l s)    -- ^ the value to rotate     -> BV (l s)    -- ^ how many places to rotate     -> IO (BV (l s))-rol g x y = do-  r <- urem g y (bvFromInteger g (length y) (toInteger (length x)))-  muxInteger (iteM g) (length x - 1) r (return . rolC x)+rol g x0 (BV ys) = fst <$> V.foldM f (x0, 1) (V.reverse ys)+  where+    f (x, p) y = do+      x' <- ite g y (rolC x p) x+      let p' = (2*p) `mod` length x0+      return (x', p')  -- | Rotate right. ror :: IsAIG l g@@ -887,9 +890,12 @@     -> BV (l s)    -- ^ the value to rotate     -> BV (l s)    -- ^ how many places to rotate     -> IO (BV (l s))-ror g x y = do-  r <- urem g y (bvFromInteger g (length y) (toInteger (length x)))-  muxInteger (iteM g) (length x - 1) r (return . rorC x)+ror g x0 (BV ys) = fst <$> V.foldM f (x0, 1) (V.reverse ys)+  where+    f (x, p) y = do+      x' <- ite g y (rorC x p) x+      let p' = (2*p) `mod` length x0+      return (x', p')   -- | Compute the rounded-down base2 logarithm of the input bitvector.

@@ -0,0 +1,271 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}+module Tests.Operations (op_tests) where++import Test.Tasty+import Test.Tasty.QuickCheck+--import Test.QuickCheck++import           Data.AIG.Interface (BasicGraph, BasicLit, newBasicGraph)+import qualified Data.AIG.Interface as AIG+import qualified Data.AIG.Operations as AIG+import Data.Bits+import Data.Int+import Data.Word++type BV s = AIG.BV (BasicLit s)++--------------------------------------------------------------------------+-- Some test harness stuff to make writing down unit tests easier++class Precond x where+  precond :: x -> Bool+  precond _ = True++class Arbitrary x => AIGTestableValue g x y where+  injectArg  :: g -> x -> y+  extractArg :: g -> y -> Maybe x++class PushIO y where+  pushIO  :: (a -> y) -> IO a -> y++instance PushIO (IO b) where+  pushIO f x = x >>= f++instance PushIO b => PushIO (a -> b) where+  pushIO f x a = pushIO (\x' -> f x' a) x++class (Testable p, PushIO y) => AIGTestable g x y p | g x y -> p where+  runTest :: IO g -> x -> y -> Bool -> p++newtype Denom a = Denom a+ deriving (Eq, Ord, Show)++instance Precond Bool+instance Precond Word32+instance Precond Word64+instance Precond Int32+instance Precond Int64+instance Precond Integer++instance (Integral a, Eq a) => Precond (Denom a) where+  precond (Denom x) = x /= 0+instance Precond Int where+  precond x = 0 <= x && x < 64++instance Arbitrary a => Arbitrary (Denom a) where+  arbitrary = Denom <$> arbitrary++instance (AIGTestableValue g a x, AIGTestableValue g b y) =>+    AIGTestableValue g (a,b) (x,y) where+  injectArg g (a,b) = (injectArg g a, injectArg g b)+  extractArg g (x,y) = (,) <$> extractArg g x <*> extractArg g y++instance AIGTestableValue g a b => AIGTestableValue g (Denom a) b where+  injectArg g (Denom x) = injectArg g x+  extractArg g x = Denom <$> extractArg g x++instance AIGTestableValue (BasicGraph s) Int (BV s) where+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)+  extractArg g x = fromInteger <$> AIG.asSigned g x++instance AIGTestableValue (BasicGraph s) Word32 (BV s) where+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)+  extractArg g x = fromInteger <$> AIG.asUnsigned g x++instance AIGTestableValue (BasicGraph s) Word64 (BV s) where+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)+  extractArg g x = fromInteger <$> AIG.asUnsigned g x++instance AIGTestableValue (BasicGraph s) Int32 (BV s) where+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)+  extractArg g x = fromInteger <$> AIG.asSigned g x++instance AIGTestableValue (BasicGraph s) Int64 (BV s) where+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)+  extractArg g x = fromInteger <$> AIG.asSigned g x++instance AIGTestableValue (BasicGraph s) Integer Integer where+  injectArg _g x = x+  extractArg _g x = Just x++instance AIGTestableValue (BasicGraph s) Bool (BasicLit s) where+  injectArg g x  = AIG.constant g x+  extractArg g x = AIG.asConstant g x++instance (Eq x, Show x, AIGTestableValue g x y) => AIGTestable g x (IO y) Property+ where+   runTest gph x y pre = pre ==> ioProperty $+     do gph' <- gph+        y' <- y+        case extractArg gph' y' of+          Nothing -> fail $ unwords ["Expected concrete output"]+          Just z+            | x == z    -> return True+            | otherwise -> fail $ unwords ["Expected", show x, "but got", show z]++instance+   (Precond x, Show x, AIGTestableValue g x y, AIGTestable g a b p) =>+   AIGTestable g (x -> a) (y -> b) (x -> p)+ where+   runTest gph f g pre = \x ->+     let y = (gph >>= \gph' -> return $ injectArg gph' x)+      in runTest gph (f x) (pushIO g y) (precond x && pre)+++------------------------------------------------------------------------------------+-- Make a unit test from a concrete operation and an operation on AIGs++mkTest :: forall a b p+        . (Testable p, AIGTestable (BasicGraph ()) a b p)+       => String+       -> a+       -> (BasicGraph () -> b)+       -> TestTree+mkTest nm a b =+  withResource newBasicGraph (\_ -> return ()) $ \(g :: IO (BasicGraph ())) ->+    testProperty nm $ (runTest g a (pushIO b g) True :: p)+++op_tests :: [TestTree]+op_tests =+  [ mkTest "ite"  (\b (x :: Word64) y -> if b then x else y) AIG.ite++  , mkTest "neg"  (negate :: Int64 -> Int64) AIG.neg+  , mkTest "add"  ((+)  :: Word64 -> Word64 -> Word64) AIG.add+  , mkTest "addC" addC AIG.addC+  , mkTest "sub"  ((-)  :: Word64 -> Word64 -> Word64) AIG.sub+  , mkTest "subC" subC AIG.subC+  , mkTest "addConst" addConst AIG.addConst+  , mkTest "subConst" subConst AIG.subConst++  , mkTest "mul"  ((*)  :: Word64 -> Word64 -> Word64) AIG.mul+  , mkTest "mulFull"  mulFull  AIG.mulFull+  , mkTest "smulFull" smulFull AIG.smulFull+  , mkTest "squot" squot AIG.squot+  , mkTest "srem"  srem  AIG.srem+  , mkTest "uquot" uquot AIG.uquot+  , mkTest "urem"  urem  AIG.urem++  , mkTest "shl"  (shiftL  :: Word64 -> Int -> Word64) AIG.shl+  , mkTest "ushr" (shiftR  :: Word64 -> Int -> Word64) AIG.ushr+  , mkTest "sshr" (shiftR  :: Int64  -> Int -> Int64)  AIG.sshr+  , mkTest "rol"  (rotateL :: Word64 -> Int -> Word64) AIG.rol+  , mkTest "ror"  (rotateR :: Word64 -> Int -> Word64) AIG.ror++  , mkTest "bvEq"    ((==) :: Word64 -> Word64 -> Bool) AIG.bvEq+  , mkTest "isZero"  (\x -> (x :: Word64) == 0) AIG.isZero+  , mkTest "nonZero" (\x -> (x :: Word64) /= 0) AIG.nonZero+  , mkTest "sle"  ((<=) :: Int64 -> Int64 -> Bool) AIG.sle+  , mkTest "slt"  ((<)  :: Int64 -> Int64 -> Bool) AIG.slt+  , mkTest "ule"  ((<=) :: Word64 -> Word64 -> Bool) AIG.ule+  , mkTest "ult"  ((<)  :: Word64 -> Word64 -> Bool) AIG.ult+  , mkTest "sabs" (abs  :: Int64 -> Int64) AIG.sabs++  , mkTest "sext" sext (\g x -> (return $ AIG.sext g x 64) :: IO _)+  , mkTest "zext" zext (\g x -> (return $ AIG.zext g x 64) :: IO _)+  , mkTest "trunc" trunc (\(_ :: BasicGraph ()) (x :: BV ()) -> (return $ AIG.trunc 64 x) :: IO _)++  , mkTest "priorityEncode" priorityEncode (\g -> AIG.priorityEncode g 32)+  , mkTest "logBase2_down" log2down AIG.logBase2_down+  , mkTest "logBase2_up"   log2up   AIG.logBase2_up+  , mkTest "clz"  clz AIG.countLeadingZeros+  , mkTest "ctz"  ctz AIG.countTrailingZeros++  , mkTest "pmul" pmul AIG.pmul+  , mkTest "pdiv" pdiv AIG.pdiv+  , mkTest "pmod" pmod AIG.pmod+  ]++addC :: Word32 -> Word32 -> (Word32, Bool)+addC x y = ( fromIntegral z, testBit z 32 )+ where z :: Word64+       z = fromIntegral x + fromIntegral y++subC :: Word32 -> Word32 -> (Word32, Bool)+subC x y = ( fromIntegral z, testBit z 32 )+ where z :: Word64+       z = fromIntegral x - fromIntegral y++addConst :: Word64 -> Integer -> Word64+addConst x y = x + fromInteger y++subConst :: Word64 -> Integer -> Word64+subConst x y = x - fromInteger y++mulFull :: Word32 -> Word32 -> Word64+mulFull x y = fromIntegral x * fromIntegral y++smulFull :: Int32 -> Int32 -> Int64+smulFull x y = fromIntegral x * fromIntegral y++uquot :: Word64 -> Denom Word64 -> Word64+uquot x (Denom y) = quot x y++urem :: Word64 -> Denom Word64 -> Word64+urem x (Denom y) = rem x y++squot :: Int64 -> Denom Int64 -> Int64+squot x (Denom y) = quot x y++srem :: Int64 -> Denom Int64 -> Int64+srem x (Denom y) = rem x y++sext :: Int32 -> Int64+sext = fromIntegral++zext :: Word32 -> Word64+zext = fromIntegral++trunc :: Word64 -> Word32+trunc = fromIntegral++log2down :: Word64 -> Int64+log2down x = fromIntegral (finiteBitSize x) - 1 - fromIntegral (countLeadingZeros x)++log2up :: Word64 -> Int64+log2up x = log2down (x - 1) + 1++clz :: Word64 -> Word64+clz = fromIntegral . countLeadingZeros++ctz :: Word64 -> Word64+ctz = fromIntegral . countTrailingZeros++pmul :: Word32 -> Word32 -> Word64+pmul x y = foldr xor zeroBits pprods+ where+  pprods = [ if testBit y i+                then shiftL (fromIntegral x) i+                else 0+           | i <- [0 .. finiteBitSize y - 1]+           ]++priorityEncode :: Word64 -> (Bool, Word32)+priorityEncode x+  | x == 0    = (False, 0)+  | otherwise = (True, fromIntegral (finiteBitSize x) - 1 - fromIntegral (countLeadingZeros x))++pdiv :: Word64 -> Denom Word32 -> Word64+pdiv x (Denom y) = fst $ pdivmod x y++pmod :: Word64 -> Denom Word32 -> Word32+pmod x (Denom y) = snd $ pdivmod x y++pdivmod :: Word64 -> Word32 -> (Word64, Word32)+pdivmod x y = go 0 x (finiteBitSize x - 1) start+  where+   start = finiteBitSize x - finiteBitSize y + countLeadingZeros y+   y'    = fromIntegral y++   go q r i j+     | j <  0      = (q,fromIntegral r)+     | testBit r i = go (setBit q j) (r `xor` (y' `shiftL` j)) (i-1) (j-1)+     | otherwise   = go q            r                         (i-1) (j-1)

@@ -0,0 +1,29 @@+module Main (main) where++import Test.Tasty+import Test.Tasty.Ingredients+import Test.Tasty.Runners.AntXML++import Tests.Operations++------------------------------------------------------------------------+-- Runner+------------------------------------------------------------------------++main :: IO ()+main = do+  defaultMainWithIngredients ingrs tests++ingrs :: [Ingredient]+ingrs =+   [ antXMLRunner+   ]+   +++   defaultIngredients+++tests :: TestTree+tests =+    testGroup "AIG"+    [ testGroup "Bitvector operations" $ op_tests+    ]