module Data.ABC.Internal.GIA (
Gia_Man_t
, Gia_Man_t_
, giaManNObjs
, giaManFanData
, Gia_Obj_t
, getGiaObjValue
, setGiaObjValue
, GiaVar(..)
, GiaLit(..)
, giaManConst0Lit
, giaManConst1Lit
, giaLitIsCompl
, giaLitVar
, giaVarLit
, giaLitNotCond
, giaManCexComb
, giaManConst0
, giaManCis
, giaManCos
, giaManCiNum
, giaManCoNum
, giaManPiNum
, giaManPoNum
, giaManAndNum
, getGiaManRegNum
, setGiaManRegNum
, giaManCiVar
, giaManCoVar
, giaManCi
, giaManCo
, giaManObj
, gia_none
, giaObjIsCo
, giaObjDiff0
, giaObjDiff1
, giaObjFaninC0
, giaObjFaninC1
, giaObjMark0
, giaObjMark1
, giaObjChild0
, giaObjChild1
, giaObjFaninId0
, giaObjFaninId1
, giaObjIsTerm
, giaObjIsAndOrConst0
, giaObjId
, giaManObjNum
, giaLitNot
, giaRegular
, giaIsComplement
, giaObjToLit
, giaObjFromLit
, giaManForEachObj1_
, giaManForEachCo
, giaManAppendCi
, giaManAppendCo
, giaManAppendAnd
, giaAigerRead
, giaAigerWrite
, giaManMiter
, giaDupLit
, giaManDupNormalize
, giaManHashAlloc
, giaManHashStart
, giaManHashStop
, giaManHashAnd
, giaManHashXor
, giaManHashMux
, giaManStart
, giaManStop
, p_giaManStop
, giaManCleanup
, giaManFillValue
, clearGiaObj
) where
import qualified Data.Bits as C2HSImp
import qualified Foreign.C.String as C2HSImp
import qualified Foreign.C.Types as C2HSImp
import qualified Foreign.Marshal.Utils as C2HSImp
import qualified Foreign.Ptr as C2HSImp
import qualified Foreign.Storable as C2HSImp
import Control.Applicative ((<$>), (<*>))
import Control.Exception
import Control.Monad
import Foreign hiding (void)
import Foreign.C
import Data.ABC.Internal.ABCGlobal
import Data.ABC.Internal.VecInt
import Data.ABC.Internal.Field
enumRange :: (Eq a, Enum a) => a -> a -> [a]
enumRange i n | i == n = []
| otherwise = i : enumRange (succ i) n
lazyAnd :: Monad m => m Bool -> m Bool -> m Bool
lazyAnd mx my = do
x <- mx
if x then my else return False
asWordPtr :: (WordPtr -> WordPtr) -> Ptr a -> Ptr b
asWordPtr f = wordPtrToPtr . f . ptrToWordPtr
data Gia_Obj_t_
type Gia_Obj_t = C2HSImp.Ptr (Gia_Obj_t_)
sizeOfGiaObj :: Int
sizeOfGiaObj = 12
giaRegular :: Gia_Obj_t -> Gia_Obj_t
giaRegular = asWordPtr (.&. complement 0x1)
giaObjDiff0 :: Gia_Obj_t -> IO CUInt
giaObjDiff0 = (\ptr -> do {val <- C2HSImp.peekByteOff ptr 0 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 29)) `C2HSImp.shiftR` (32 29)})
giaObjFaninC0 :: Gia_Obj_t -> IO Bool
giaObjFaninC0 o = toBool `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 0 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 30)) `C2HSImp.shiftR` (32 1)}) o
giaObjMark0 :: Gia_Obj_t -> IO Bool
giaObjMark0 o = toBool `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 0 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 31)) `C2HSImp.shiftR` (32 1)}) o
giaObjIsTerm :: Gia_Obj_t -> IO Bool
giaObjIsTerm o = toBool `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 0 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 32)) `C2HSImp.shiftR` (32 1)}) o
giaObjDiff1 :: Gia_Obj_t -> IO CUInt
giaObjDiff1 = (\ptr -> do {val <- C2HSImp.peekByteOff ptr 4 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 29)) `C2HSImp.shiftR` (32 29)})
giaObjFaninC1 :: Gia_Obj_t -> IO Bool
giaObjFaninC1 o = toBool `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 4 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 30)) `C2HSImp.shiftR` (32 1)}) o
giaObjMark1 :: Gia_Obj_t -> IO Bool
giaObjMark1 o = toBool `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 4 :: IO C2HSImp.CUInt; return $ (val `C2HSImp.shiftL` (32 31)) `C2HSImp.shiftR` (32 1)}) o
getGiaObjValue :: Gia_Obj_t -> IO CUInt
getGiaObjValue = (\ptr -> do {C2HSImp.peekByteOff ptr 8 :: IO C2HSImp.CUInt})
setGiaObjValue :: Gia_Obj_t -> CUInt -> IO ()
setGiaObjValue = (\ptr val -> do {C2HSImp.pokeByteOff ptr 8 (val :: C2HSImp.CUInt)})
gia_none :: CUInt
gia_none = 0x1FFFFFFF
giaObjIsAndOrConst0 :: Gia_Obj_t -> IO Bool
giaObjIsAndOrConst0 o = not <$> giaObjIsTerm o
giaObjDiff0Assigned :: Gia_Obj_t -> IO Bool
giaObjDiff0Assigned o = (/= gia_none) <$> giaObjDiff0 o
giaIsComplement :: Gia_Obj_t -> Bool
giaIsComplement o = ptrToWordPtr o `testBit` 0
giaNot :: Gia_Obj_t -> Gia_Obj_t
giaNot = asWordPtr (xor 1)
giaNotCond :: Gia_Obj_t -> Bool -> Gia_Obj_t
giaNotCond o b = if b then giaNot o else o
giaObjIsCo :: Gia_Obj_t -> IO Bool
giaObjIsCo o = lazyAnd (giaObjIsTerm o) (giaObjDiff0Assigned o)
incObjPtr :: Gia_Obj_t -> CInt -> Gia_Obj_t
incObjPtr o i = o `plusPtr` (sizeOfGiaObj * fromIntegral i)
decObjPtr :: Gia_Obj_t -> CUInt -> Gia_Obj_t
decObjPtr o i = incObjPtr o (negate (fromIntegral i))
objDiff :: Gia_Obj_t -> Gia_Obj_t -> Int
objDiff p q = (p `minusPtr` q) `div` sizeOfGiaObj
giaObjFanin0 :: Gia_Obj_t -> IO Gia_Obj_t
giaObjFanin0 o = decObjPtr o <$> giaObjDiff0 o
giaObjFanin1 :: Gia_Obj_t -> IO Gia_Obj_t
giaObjFanin1 o = decObjPtr o <$> giaObjDiff1 o
giaObjChild0 :: Gia_Obj_t -> IO Gia_Obj_t
giaObjChild0 o = giaNotCond <$> giaObjFanin0 o <*> giaObjFaninC0 o
giaObjChild1 :: Gia_Obj_t -> IO Gia_Obj_t
giaObjChild1 o = giaNotCond <$> giaObjFanin1 o <*> giaObjFaninC1 o
giaObjFaninId0 :: Gia_Obj_t -> GiaVar -> IO GiaVar
giaObjFaninId0 o (GiaVar v) = (\d -> GiaVar (v fromIntegral d)) <$> giaObjDiff0 o
giaObjFaninId1 :: Gia_Obj_t -> GiaVar -> IO GiaVar
giaObjFaninId1 o (GiaVar v) = (\d -> GiaVar (v fromIntegral d)) <$> giaObjDiff1 o
newtype GiaVar = GiaVar { unGiaVar :: CInt } deriving (Eq, Ord, Storable)
newtype GiaLit = GiaLit { unGiaLit :: CInt } deriving (Eq, Ord, Storable)
giaManConst0Lit :: GiaLit
giaManConst0Lit = GiaLit 0
giaManConst1Lit :: GiaLit
giaManConst1Lit = GiaLit 1
giaLitIsCompl :: GiaLit -> Bool
giaLitIsCompl l = unGiaLit l `testBit` 0
giaLitVar :: GiaLit -> GiaVar
giaLitVar (GiaLit l) = GiaVar (l `shiftR` 1)
giaVarLit :: GiaVar -> GiaLit
giaVarLit (GiaVar v) = GiaLit (v `shiftL` 1)
giaLitNot :: GiaLit -> GiaLit
giaLitNot = GiaLit . xor 1 . unGiaLit
giaLitNotCond :: GiaLit -> Bool -> GiaLit
giaLitNotCond (GiaLit l) b = GiaLit (l `xor` (if b then 1 else 0))
data Gia_Man_t_
type Gia_Man_t = C2HSImp.Ptr (Gia_Man_t_)
giaManCexComb :: Gia_Man_t -> IO Abc_Cex_t
giaManCexComb = (\ptr -> do {C2HSImp.peekByteOff ptr 248 :: IO (Abc_Cex_t)})
giaManNObjs :: Field Gia_Man_t CInt
giaManNObjs = fieldFromOffset (24)
giaManObjs :: Field Gia_Man_t Gia_Obj_t
giaManObjs = fieldFromOffset (32)
giaManConst0 :: Gia_Man_t -> IO Gia_Obj_t
giaManConst0 = readAt giaManObjs
giaManCis :: Gia_Man_t -> IO Vec_Int_t
giaManCis = (\ptr -> do {C2HSImp.peekByteOff ptr 64 :: IO (Vec_Int_t)})
giaManCos :: Gia_Man_t -> IO Vec_Int_t
giaManCos = (\ptr -> do {C2HSImp.peekByteOff ptr 72 :: IO (Vec_Int_t)})
giaManFanData :: Gia_Man_t -> IO (Ptr CInt)
giaManFanData = (\ptr -> do {C2HSImp.peekByteOff ptr 184 :: IO (C2HSImp.Ptr C2HSImp.CInt)})
giaManObjNum :: Gia_Man_t -> IO CInt
giaManObjNum = readAt giaManNObjs
giaManCiNum :: Gia_Man_t -> IO CInt
giaManCiNum = vecIntSize <=< giaManCis
giaManCoNum :: Gia_Man_t -> IO CInt
giaManCoNum = vecIntSize <=< giaManCos
getGiaManRegNum :: Gia_Man_t -> IO CInt
getGiaManRegNum = (\ptr -> do {C2HSImp.peekByteOff ptr 16 :: IO C2HSImp.CInt})
setGiaManRegNum :: Gia_Man_t -> CInt -> IO ()
setGiaManRegNum = (\ptr val -> do {C2HSImp.pokeByteOff ptr 16 (val :: C2HSImp.CInt)})
giaManPiNum :: Gia_Man_t -> IO CInt
giaManPiNum m = () <$> giaManCiNum m <*> getGiaManRegNum m
giaManPoNum :: Gia_Man_t -> IO CInt
giaManPoNum m = () <$> giaManCoNum m <*> getGiaManRegNum m
giaManAndNum :: Gia_Man_t -> IO CInt
giaManAndNum m = fn <$> giaManObjNum m <*> giaManCiNum m <*> giaManCoNum m
where fn t i o = t i o 1
giaManForEachObj1_ :: Gia_Man_t -> (Gia_Obj_t -> GiaVar -> IO b) -> IO ()
giaManForEachObj1_ fp action = do
nMax <- giaManObjNum fp
forM_ (enumRange 1 nMax) $ \i -> do
let var = GiaVar (fromIntegral i)
pObj <- giaManObj fp var
void $ action pObj var
giaManForEachCo :: Gia_Man_t -> (Gia_Obj_t -> Int -> IO b) -> IO [b]
giaManForEachCo fp action = do
nMax <- giaManCoNum fp
forM (enumRange 0 nMax) $ \i -> do
pObj <- giaManCo fp i
action pObj (fromIntegral i)
foreign import ccall unsafe "AbcBridge_Gia_ManAppendCi"
giaManAppendCi_ :: Gia_Man_t -> IO CInt
giaManAppendCi :: Gia_Man_t -> IO GiaLit
giaManAppendCi m = GiaLit <$> giaManAppendCi_ m
foreign import ccall unsafe "AbcBridge_Gia_ManAppendAnd"
giaManAppendAnd_ :: Gia_Man_t -> CInt -> CInt -> IO CInt
giaManAppendAnd :: Gia_Man_t -> GiaLit -> GiaLit -> IO GiaLit
giaManAppendAnd m (GiaLit x) (GiaLit y) =
GiaLit <$> giaManAppendAnd_ m x y
foreign import ccall unsafe "AbcBridge_Gia_ManAppendCo"
giaManAppendCo_ :: Gia_Man_t -> CInt -> IO CInt
giaManAppendCo :: Gia_Man_t -> GiaLit -> IO GiaLit
giaManAppendCo m (GiaLit l) = GiaLit <$> giaManAppendCo_ m l
giaManObj :: Gia_Man_t -> GiaVar -> IO Gia_Obj_t
giaManObj m (GiaVar v) = do
cnt <- giaManObjNum m
assert (0 <= v && v < cnt) $ do
(`incObjPtr` v) <$> giaManConst0 m
giaManCiVar :: Gia_Man_t -> CInt -> IO GiaVar
giaManCiVar m i = do
v <- giaManCis m
GiaVar <$> vecIntEntry v i
giaManCi :: Gia_Man_t -> CInt -> IO Gia_Obj_t
giaManCi m i = giaManObj m =<< giaManCiVar m i
giaManCoVar :: Gia_Man_t -> CInt -> IO GiaVar
giaManCoVar m i = do
v <- giaManCos m
GiaVar <$> vecIntEntry v i
giaManCo :: Gia_Man_t -> CInt -> IO Gia_Obj_t
giaManCo m i = giaManObj m =<< giaManCoVar m i
giaObjId :: Gia_Man_t -> Gia_Obj_t -> IO GiaVar
giaObjId p pObj = do
objs <- giaManConst0 p
nObjs <- readAt giaManNObjs p
assert (objs <= pObj && pObj < objs `incObjPtr` nObjs) $ do
return $ GiaVar $ fromIntegral $ pObj `objDiff` objs
giaObjToLit :: (Gia_Man_t) -> (Gia_Obj_t) -> IO ((GiaLit))
giaObjToLit a1 a2 =
let {a1' = id a1} in
let {a2' = id a2} in
giaObjToLit'_ a1' a2' >>= \res ->
let {res' = GiaLit res} in
return (res')
giaObjFromLit :: (Gia_Man_t) -> (GiaLit) -> IO ((Gia_Obj_t))
giaObjFromLit a1 a2 =
let {a1' = id a1} in
let {a2' = unGiaLit a2} in
giaObjFromLit'_ a1' a2' >>= \res ->
let {res' = id res} in
return (res')
giaAigerRead :: (String)
-> (Bool)
-> (Bool)
-> IO ((Gia_Man_t))
giaAigerRead a1 a2 a3 =
C2HSImp.withCString a1 $ \a1' ->
let {a2' = C2HSImp.fromBool a2} in
let {a3' = C2HSImp.fromBool a3} in
giaAigerRead'_ a1' a2' a3' >>= \res ->
let {res' = id res} in
return (res')
giaAigerWrite :: (Gia_Man_t) -> (String)
-> (Bool)
-> (Bool)
-> IO ()
giaAigerWrite a1 a2 a3 a4 =
let {a1' = id a1} in
C2HSImp.withCString a2 $ \a2' ->
let {a3' = C2HSImp.fromBool a3} in
let {a4' = C2HSImp.fromBool a4} in
giaAigerWrite'_ a1' a2' a3' a4' >>
return ()
giaManMiter :: (Gia_Man_t)
-> (Gia_Man_t)
-> (Int)
-> (Bool)
-> (Bool)
-> (Bool)
-> (Bool)
-> IO ((Gia_Man_t))
giaManMiter a1 a2 a3 a4 a5 a6 a7 =
let {a1' = id a1} in
let {a2' = id a2} in
let {a3' = fromIntegral a3} in
let {a4' = C2HSImp.fromBool a4} in
let {a5' = C2HSImp.fromBool a5} in
let {a6' = C2HSImp.fromBool a6} in
let {a7' = C2HSImp.fromBool a7} in
giaManMiter'_ a1' a2' a3' a4' a5' a6' a7' >>= \res ->
let {res' = id res} in
return (res')
foreign import ccall unsafe "Gia_ManDupNormalize" giaManDupNormalize
:: Gia_Man_t -> IO Gia_Man_t
giaDupLit :: Gia_Man_t -> Gia_Man_t -> GiaLit -> IO GiaLit
giaDupLit pNew p (GiaLit l) = GiaLit <$> giaDupLit' pNew p l
foreign import ccall unsafe "AbcBridge_Gia_DupLit" giaDupLit'
:: Gia_Man_t -> Gia_Man_t -> CInt -> IO CInt
foreign import ccall unsafe "Gia_ManHashAlloc" giaManHashAlloc
:: Gia_Man_t -> IO ()
foreign import ccall unsafe "Gia_ManHashStart" giaManHashStart
:: Gia_Man_t -> IO ()
foreign import ccall unsafe "Gia_ManHashStop" giaManHashStop
:: Gia_Man_t -> IO ()
giaManHashAnd :: (Gia_Man_t)
-> (GiaLit)
-> (GiaLit)
-> IO ((GiaLit))
giaManHashAnd a1 a2 a3 =
let {a1' = id a1} in
let {a2' = unGiaLit a2} in
let {a3' = unGiaLit a3} in
giaManHashAnd'_ a1' a2' a3' >>= \res ->
let {res' = GiaLit res} in
return (res')
giaManHashXor :: (Gia_Man_t)
-> (GiaLit)
-> (GiaLit)
-> IO ((GiaLit))
giaManHashXor a1 a2 a3 =
let {a1' = id a1} in
let {a2' = unGiaLit a2} in
let {a3' = unGiaLit a3} in
giaManHashXor'_ a1' a2' a3' >>= \res ->
let {res' = GiaLit res} in
return (res')
giaManHashMux :: (Gia_Man_t)
-> (GiaLit)
-> (GiaLit)
-> (GiaLit)
-> IO ((GiaLit))
giaManHashMux a1 a2 a3 a4 =
let {a1' = id a1} in
let {a2' = unGiaLit a2} in
let {a3' = unGiaLit a3} in
let {a4' = unGiaLit a4} in
giaManHashMux'_ a1' a2' a3' a4' >>= \res ->
let {res' = GiaLit res} in
return (res')
foreign import ccall unsafe "Gia_ManStop"
giaManStop :: Gia_Man_t -> IO ()
foreign import ccall unsafe "gia.h &Gia_ManStop"
p_giaManStop :: FunPtr (Gia_Man_t -> IO ())
foreign import ccall unsafe "AbcBridge_Gia_ClearGiaObj"
clearGiaObj :: Gia_Obj_t -> IO ()
giaManStart :: (CInt) -> IO ((Gia_Man_t))
giaManStart a1 =
let {a1' = id a1} in
giaManStart'_ a1' >>= \res ->
let {res' = id res} in
return (res')
giaManCleanup :: (Gia_Man_t)
-> IO ((Gia_Man_t))
giaManCleanup a1 =
let {a1' = id a1} in
giaManCleanup'_ a1' >>= \res ->
let {res' = id res} in
return (res')
giaManFillValue :: (Gia_Man_t)
-> IO ()
giaManFillValue a1 =
let {a1' = id a1} in
giaManFillValue'_ a1' >>
return ()
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h AbcBridge_Gia_ObjToLit"
giaObjToLit'_ :: ((Gia_Man_t) -> ((Gia_Obj_t) -> (IO C2HSImp.CInt)))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h AbcBridge_Gia_ObjFromLit"
giaObjFromLit'_ :: ((Gia_Man_t) -> (C2HSImp.CInt -> (IO (Gia_Obj_t))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_AigerRead"
giaAigerRead'_ :: ((C2HSImp.Ptr C2HSImp.CChar) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO (Gia_Man_t)))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_AigerWrite"
giaAigerWrite'_ :: ((Gia_Man_t) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO ())))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManMiter"
giaManMiter'_ :: ((Gia_Man_t) -> ((Gia_Man_t) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO (Gia_Man_t)))))))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManHashAnd"
giaManHashAnd'_ :: ((Gia_Man_t) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO C2HSImp.CInt))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManHashXor"
giaManHashXor'_ :: ((Gia_Man_t) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO C2HSImp.CInt))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManHashMux"
giaManHashMux'_ :: ((Gia_Man_t) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO C2HSImp.CInt)))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManStart"
giaManStart'_ :: (C2HSImp.CInt -> (IO (Gia_Man_t)))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManCleanup"
giaManCleanup'_ :: ((Gia_Man_t) -> (IO (Gia_Man_t)))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManFillValue"
giaManFillValue'_ :: ((Gia_Man_t) -> (IO ()))