Basic.hs

{-# LANGUAGE PatternGuards #-}
module Tests.Basic
  ( basic_tests
  ) where

import Control.Exception
import Control.Monad.Compat
import System.Directory
import System.IO
import Prelude ()
import Prelude.Compat

import Test.Tasty
import Test.Tasty.HUnit as HU
import Test.Tasty.QuickCheck

import qualified Data.ABC as ABC
import qualified Data.AIG.Trace as Tr

tryIO :: IO a -> IO (Either IOException a)
tryIO = try

basic_tests :: Tr.Traceable l => ABC.Proxy l g -> [TestTree]
basic_tests proxy@(ABC.Proxy f) = f $
  [ testCase "test_true" $ do
      ABC.SomeGraph g <- ABC.newGraph proxy
      let n = ABC.Network g [ABC.trueLit g]
      assertEqual "test_true" [True] =<< ABC.evaluate n []
  , testCase "test_false" $ do
      ABC.SomeGraph g <- ABC.newGraph proxy
      let n = ABC.Network g [ABC.falseLit g]
      assertEqual "test_false" [False] =<< ABC.evaluate n []
  , testProperty "test_constant"$ \b -> ioProperty $do
      ABC.SomeGraph g <- ABC.newGraph proxy
      let n = ABC.Network g [ABC.constant g b]
      (==[b]) <$> ABC.evaluate n []
  , testProperty "test_not" $ \b0 -> ioProperty $ do
      ABC.SomeGraph g <- ABC.newGraph proxy
      i0 <- ABC.newInput g
      let n = ABC.Network g [ABC.not i0]
      r <- ABC.evaluate n [b0]
      return $ r == [not b0]
  , testProperty "test_and" $ \b1 b2 -> ioProperty $ do
      ABC.SomeGraph g <- ABC.newGraph proxy
      i0 <- ABC.newInput g
      i1 <- ABC.newInput g
      x <- ABC.and g i0 i1
      let n = ABC.Network g [x]
      r <- ABC.evaluate n [b1, b2]
      return $ r == [b1 && b2]
  , testProperty "test_xor" $ \b1 b2 -> ioProperty $ do
      ABC.SomeGraph g <- ABC.newGraph proxy
      i0 <- ABC.newInput g
      i1 <- ABC.newInput g
      x <- ABC.xor g i0 i1
      let n = ABC.Network g [x]
      r <- ABC.evaluate n [b1, b2]
      return $ r == [b1 /= b2]
  , testProperty "test_mux" $ \b0 b1 b2 -> ioProperty $ do
      ABC.SomeGraph g <- ABC.newGraph proxy
      i0 <- ABC.newInput g
      i1 <- ABC.newInput g
      i2 <- ABC.newInput g
      o <- ABC.mux g i0 i1 i2

      let n = ABC.Network g [o]
      r <- ABC.evaluate n [b0, b1, b2]
      return $ r == [if b0 then b1 else b2]
  , testCase "test_cec" $ do
     r <- join $ ABC.cec <$> cecNetwork proxy <*> cecNetwork' proxy
     assertEqual "test_cec" (ABC.Invalid (toEnum <$> [0,0,0,1,0,0,0])) r
  , testCase "test_aiger" $ do
      -- XXX: cwd unfriendly
      n1 <- ABC.aigerNetwork proxy "tests/eijk.S298.S.aig"
      tmpdir <- getTemporaryDirectory
      (path, hndl) <- openTempFile tmpdir "aiger.aig"
      hClose hndl
      ABC.writeAiger path n1
      n2 <- ABC.aigerNetwork proxy path
      assertEqual "test_aiger" ABC.Valid =<< ABC.cec n1 n2
      removeFile path

  , testProperty "unfold_fold" $ \litForest -> ioProperty $ do
      let maxInput = foldr max 0 $ map ABC.getMaxInput litForest

      n1@(ABC.Network g ls) <- ABC.buildNetwork proxy litForest

      litForest' <- ABC.toLitForest g ls

      -- NB: we cannot just compare litForest and litForest' for syntactic equality
      -- due to simplifications performed when building the AIG.  Also, the following
      -- commented line does not work because references to inputs may also be removed
      -- during simpification, resulting in a different number of inputs.
      --n2 <- ABC.buildNetwork proxy litForest'

      -- so do this instead...
      (ABC.SomeGraph g') <- ABC.newGraph proxy
      forM_ [0 .. maxInput] (\_ -> ABC.newInput g')
      ls' <- ABC.fromLitForest g' litForest'
      let n2 = ABC.Network g' ls'

      result <- ABC.cec n1 n2
      return $ result == ABC.Valid

  , testCase "fold_unfold" $ do
      (ABC.Network g l) <- cecNetwork proxy
      inputs <- ABC.inputCount g
      litForest <- ABC.toLitForest g l

      (ABC.SomeGraph g') <- ABC.newGraph proxy
      forM_ [0 .. inputs-1] (\_ -> ABC.newInput g')
      l' <- ABC.fromLitForest g' litForest

      assertEqual "fold_unfold" ABC.Valid =<< ABC.cec (ABC.Network g l) (ABC.Network g' l')

  , testCase "bad_aiger" $ do
      me <- tryIO $ ABC.aigerNetwork proxy "Nonexistent AIGER!"
      case me of
        Left{} -> return ()
        Right{} -> fail "Expected error when opening AIGER"
  , testCase "test_sat" $ do
     ABC.SomeGraph g <- ABC.newGraph proxy
     rt <- ABC.checkSat g (ABC.trueLit g)
     case rt of
       ABC.Sat{} -> return ()
       ABC.Unsat{} -> fail "trueLit is unsat"
       ABC.SatUnknown{} -> fail "trueLit is unknown"
     rf <- ABC.checkSat g (ABC.falseLit g)
     case rf of
       ABC.Sat{} -> fail "falseLit is sat"
       ABC.Unsat{} -> return ()
       ABC.SatUnknown{} -> fail "falseLit is unknown"

  , testCase "aiger_twice" $ do
      ABC.SomeGraph g <- ABC.newGraph proxy

      tmpdir <- getTemporaryDirectory
      (path, hndl) <- openTempFile tmpdir "aiger.aig"
      hClose hndl

      x <- ABC.newInput g

      ABC.writeAiger (path++"1") (ABC.Network g [ABC.falseLit g, ABC.falseLit g])

      y <- ABC.newInput g
      r <- ABC.and g x y

      ABC.writeAiger (path++"2") (ABC.Network g [r])

  , testCase "aiger_eval" $ do
      ABC.SomeGraph g <- ABC.newGraph proxy

      tmpdir <- getTemporaryDirectory
      (path, hndl) <- openTempFile tmpdir "aiger.aig"
      hClose hndl

      x <- fmap ABC.bvFromList $ sequence $ replicate 32 (ABC.newInput g)
      y <- ABC.zipWithM (ABC.lAnd' g) x (ABC.bvFromInteger g 32 0x12345678)

      ABC.writeAiger path (ABC.Network g (ABC.bvToList y))

      let tobool :: Int -> Bool
          tobool i = if i == 0 then False else True

      let inputs = map tobool $ reverse $
                   [ 0,1,1,0,1,0,0,0,
                     0,0,0,0,0,0,0,0,
                     0,0,0,0,0,0,0,0,
                     0,0,0,0,0,0,0,0 ]

      let outputs = fmap tobool $ reverse $
                    [ 0,0,0,0,1,0,0,0,
                      0,0,0,0,0,0,0,0,
                      0,0,0,0,0,0,0,0,
                      0,0,0,0,0,0,0,0 ]

      z <- ABC.evaluate (ABC.Network g (ABC.bvToList y)) inputs

      assertEqual "aiger_eval" outputs z

  , testCase "lit_view" $ do
       ABC.SomeGraph g <- ABC.newGraph proxy
       i  <- ABC.newInput g
       lv <- ABC.litView g i
       x  <- ABC.newInput g
       xv <- ABC.litView g x
       o  <- ABC.and g i x
       lo <- ABC.litView g o

       case lv of
         ABC.Input 0 -> return ()
         _ -> fail "expected input 0"

       case xv of
         ABC.Input 1 -> return ()
         _ -> fail "expected input 1"

       case lo of
         ABC.And a1 a2
           | a1 ABC.=== i, a2 ABC.=== x -> return ()
         _ -> fail "expected and literal"
  ]

cecNetwork :: ABC.IsAIG l g => ABC.Proxy l g -> IO (ABC.Network l g)
cecNetwork proxy = do
  ABC.SomeGraph g <- ABC.newGraph proxy
  [n2, n3, n4, n5, n6, n7, n8] <- replicateM 7 $ ABC.newInput g

  n14 <- ABC.ands g [ ABC.not n2
                    , ABC.not n3
                    , ABC.not n4
                    , n5
                    , ABC.not n6
                    , ABC.not n7
                    , ABC.not n8
                    ]
  let r = [n14] ++ replicate 6 (ABC.falseLit g)
  return (ABC.Network g r)

cecNetwork' :: ABC.IsAIG l g => ABC.Proxy l g -> IO (ABC.Network l g)
cecNetwork' proxy = do
  ABC.SomeGraph g <- ABC.newGraph proxy
  replicateM_ 7 $ ABC.newInput g
  let r = replicate 7 $ ABC.falseLit g
  return (ABC.Network g r)