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 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 = 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 <- peekByteOff ptr 0 ::IO CUInt; return $ (val `shiftL` (32 29)) `shiftR` (32 29)})
giaObjFaninC0 :: Gia_Obj_t -> IO Bool
giaObjFaninC0 o = toBool `fmap` (\ptr -> do {val <- peekByteOff ptr 0 ::IO CUInt; return $ (val `shiftL` (32 30)) `shiftR` (32 1)}) o
giaObjMark0 :: Gia_Obj_t -> IO Bool
giaObjMark0 o = toBool `fmap` (\ptr -> do {val <- peekByteOff ptr 0 ::IO CUInt; return $ (val `shiftL` (32 31)) `shiftR` (32 1)}) o
giaObjIsTerm :: Gia_Obj_t -> IO Bool
giaObjIsTerm o = toBool `fmap` (\ptr -> do {val <- peekByteOff ptr 0 ::IO CUInt; return $ (val `shiftL` (32 32)) `shiftR` (32 1)}) o
giaObjDiff1 :: Gia_Obj_t -> IO CUInt
giaObjDiff1 = (\ptr -> do {val <- peekByteOff ptr 4 ::IO CUInt; return $ (val `shiftL` (32 29)) `shiftR` (32 29)})
giaObjFaninC1 :: Gia_Obj_t -> IO Bool
giaObjFaninC1 o = toBool `fmap` (\ptr -> do {val <- peekByteOff ptr 4 ::IO CUInt; return $ (val `shiftL` (32 30)) `shiftR` (32 1)}) o
giaObjMark1 :: Gia_Obj_t -> IO Bool
giaObjMark1 o = toBool `fmap` (\ptr -> do {val <- peekByteOff ptr 4 ::IO CUInt; return $ (val `shiftL` (32 31)) `shiftR` (32 1)}) o
getGiaObjValue :: Gia_Obj_t -> IO CUInt
getGiaObjValue = (\ptr -> do {peekByteOff ptr 8 ::IO CUInt})
setGiaObjValue :: Gia_Obj_t -> CUInt -> IO ()
setGiaObjValue = (\ptr val -> do {pokeByteOff ptr 8 (val::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 = Ptr (Gia_Man_t_)
giaManCexComb :: Gia_Man_t -> IO Abc_Cex_t
giaManCexComb = (\ptr -> do {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 {peekByteOff ptr 64 ::IO (Vec_Int_t)})
giaManCos :: Gia_Man_t -> IO Vec_Int_t
giaManCos = (\ptr -> do {peekByteOff ptr 72 ::IO (Vec_Int_t)})
giaManFanData :: Gia_Man_t -> IO (Ptr CInt)
giaManFanData = (\ptr -> do {peekByteOff ptr 184 ::IO (Ptr 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 {peekByteOff ptr 16 ::IO CInt})
setGiaManRegNum :: Gia_Man_t -> CInt -> IO ()
setGiaManRegNum = (\ptr val -> do {pokeByteOff ptr 16 (val::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 =
withCString a1 $ \a1' ->
let {a2' = fromBool a2} in
let {a3' = 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
withCString a2 $ \a2' ->
let {a3' = fromBool a3} in
let {a4' = 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' = fromBool a4} in
let {a5' = fromBool a5} in
let {a6' = fromBool a6} in
let {a7' = 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 CInt)))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h AbcBridge_Gia_ObjFromLit"
giaObjFromLit'_ :: ((Gia_Man_t) -> (CInt -> (IO (Gia_Obj_t))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_AigerRead"
giaAigerRead'_ :: ((Ptr CChar) -> (CInt -> (CInt -> (IO (Gia_Man_t)))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_AigerWrite"
giaAigerWrite'_ :: ((Gia_Man_t) -> ((Ptr CChar) -> (CInt -> (CInt -> (IO ())))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManMiter"
giaManMiter'_ :: ((Gia_Man_t) -> ((Gia_Man_t) -> (CInt -> (CInt -> (CInt -> (CInt -> (CInt -> (IO (Gia_Man_t)))))))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManHashAnd"
giaManHashAnd'_ :: ((Gia_Man_t) -> (CInt -> (CInt -> (IO CInt))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManHashXor"
giaManHashXor'_ :: ((Gia_Man_t) -> (CInt -> (CInt -> (IO CInt))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManHashMux"
giaManHashMux'_ :: ((Gia_Man_t) -> (CInt -> (CInt -> (CInt -> (IO CInt)))))
foreign import ccall safe "Data/ABC/Internal/GIA.chs.h Gia_ManStart"
giaManStart'_ :: (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 ()))