module Data.ABC.Internal.CEC (
Cec_ParCec_t_(..)
, Cec_ParSat_t_(..)
, cecManVerify
, cecManSatDefaultParams
, cecManCecDefaultParams
, cecManSatSolving
, Cec_ManPat_t_
, Cec_ManPat_t
, cecManPatStart
, cecManPatStop
, cecManPatPatCount
, cecManPatPrintStats
, cecManSatSolve
) where
import qualified Foreign.C.Types as C2HSImp
import qualified Foreign.Ptr as C2HSImp
import qualified Foreign.Storable as C2HSImp
import Control.Applicative
import Foreign
import Foreign.C (CInt(..))
import qualified System.IO.Unsafe as Unsafe
import Data.ABC.Internal.GIA
type Cec_ParSat_t = C2HSImp.Ptr (Cec_ParSat_t_)
type Cec_ParCec_t = Ptr Cec_ParCec_t_
data Cec_ManPat_t_
type Cec_ManPat_t = C2HSImp.Ptr (Cec_ManPat_t_)
data Cec_ParSat_t_ = Cec_ParSat_t_
{ nBTLimit'Cec_ParSat :: CInt
, nSatVarMax'Cec_ParSat :: CInt
, nCallsRecycle'Cec_ParSat :: CInt
, fNonChrono'Cec_ParSat :: Bool
, fPolarFlip'Cec_ParSat :: Bool
, fCheckMiter'Cec_ParSat :: Bool
, fLearnCls'Cec_ParSat :: Bool
, fVerbose'Cec_ParSat :: Bool
} deriving (Show, Read, Eq)
instance Storable Cec_ParSat_t_ where
sizeOf _ = 32
alignment _ = alignment (undefined :: CInt)
peek p = Cec_ParSat_t_
<$> pInt (\ptr -> do {C2HSImp.peekByteOff ptr 0 :: IO C2HSImp.CInt})
<*> pInt (\ptr -> do {C2HSImp.peekByteOff ptr 4 :: IO C2HSImp.CInt})
<*> pInt (\ptr -> do {C2HSImp.peekByteOff ptr 8 :: IO C2HSImp.CInt})
<*> pBool (\ptr -> do {C2HSImp.peekByteOff ptr 12 :: IO C2HSImp.CInt})
<*> pBool (\ptr -> do {C2HSImp.peekByteOff ptr 16 :: IO C2HSImp.CInt})
<*> pBool (\ptr -> do {C2HSImp.peekByteOff ptr 20 :: IO C2HSImp.CInt})
<*> pBool (\ptr -> do {C2HSImp.peekByteOff ptr 24 :: IO C2HSImp.CInt})
<*> pBool (\ptr -> do {C2HSImp.peekByteOff ptr 28 :: IO C2HSImp.CInt})
where pInt :: (Cec_ParSat_t -> IO CInt) -> IO CInt
pInt f = f p
pBool :: (Cec_ParSat_t -> IO CInt) -> IO Bool
pBool f = (/= 0) <$> f p
poke p x = do
pokeInt (\ptr val -> do {C2HSImp.pokeByteOff ptr 0 (val :: C2HSImp.CInt)}) nBTLimit'Cec_ParSat
pokeInt (\ptr val -> do {C2HSImp.pokeByteOff ptr 4 (val :: C2HSImp.CInt)}) nSatVarMax'Cec_ParSat
pokeInt (\ptr val -> do {C2HSImp.pokeByteOff ptr 8 (val :: C2HSImp.CInt)}) nCallsRecycle'Cec_ParSat
pokeBool (\ptr val -> do {C2HSImp.pokeByteOff ptr 12 (val :: C2HSImp.CInt)}) fNonChrono'Cec_ParSat
pokeBool (\ptr val -> do {C2HSImp.pokeByteOff ptr 16 (val :: C2HSImp.CInt)}) fPolarFlip'Cec_ParSat
pokeBool (\ptr val -> do {C2HSImp.pokeByteOff ptr 20 (val :: C2HSImp.CInt)}) fCheckMiter'Cec_ParSat
pokeBool (\ptr val -> do {C2HSImp.pokeByteOff ptr 24 (val :: C2HSImp.CInt)}) fLearnCls'Cec_ParSat
pokeBool (\ptr val -> do {C2HSImp.pokeByteOff ptr 28 (val :: C2HSImp.CInt)}) fVerbose'Cec_ParSat
where pokeInt :: (Cec_ParSat_t -> CInt -> IO ()) -> (Cec_ParSat_t_ -> CInt) -> IO ()
pokeInt w f = w p (f x)
pokeBool :: (Cec_ParSat_t -> CInt -> IO ()) -> (Cec_ParSat_t_ -> Bool) -> IO ()
pokeBool w f = w p (if f x then 1 else 0)
data Cec_ParCec_t_ = Cec_ParCec_t_
{ nBTLimit'Cec_ParCec :: Int
, nTimeLimit'Cec_ParCec :: Int
, fUseSmartCnf'Cec_ParCec :: Bool
, fRewriting'Cec_ParCec :: Bool
, fNaive'Cec_ParCec :: Bool
, fVeryVerbose'Cec_ParCec :: Bool
, fVerbose'Cec_ParCec :: Bool
, iOutFail'Cec_ParCec :: Int
} deriving (Show, Read, Eq)
instance Storable Cec_ParCec_t_ where
sizeOf _ = 32
alignment _ = alignment (undefined :: CInt)
peek p = Cec_ParCec_t_
<$> fmap fromIntegral ((\ptr -> do {C2HSImp.peekByteOff ptr 0 :: IO C2HSImp.CInt}) p)
<*> fmap fromIntegral ((\ptr -> do {C2HSImp.peekByteOff ptr 4 :: IO C2HSImp.CInt}) p)
<*> fmap toBool ((\ptr -> do {C2HSImp.peekByteOff ptr 8 :: IO C2HSImp.CInt}) p)
<*> fmap toBool ((\ptr -> do {C2HSImp.peekByteOff ptr 12 :: IO C2HSImp.CInt}) p)
<*> fmap toBool ((\ptr -> do {C2HSImp.peekByteOff ptr 16 :: IO C2HSImp.CInt}) p)
<*> fmap toBool ((\ptr -> do {C2HSImp.peekByteOff ptr 20 :: IO C2HSImp.CInt}) p)
<*> fmap toBool ((\ptr -> do {C2HSImp.peekByteOff ptr 24 :: IO C2HSImp.CInt}) p)
<*> fmap fromIntegral ((\ptr -> do {C2HSImp.peekByteOff ptr 28 :: IO C2HSImp.CInt}) p)
poke p x = do
(\ptr val -> do {C2HSImp.pokeByteOff ptr 0 (val :: C2HSImp.CInt)}) p (fromIntegral $ nBTLimit'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 4 (val :: C2HSImp.CInt)}) p (fromIntegral $ nTimeLimit'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 8 (val :: C2HSImp.CInt)}) p (fromBool $ fUseSmartCnf'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 12 (val :: C2HSImp.CInt)}) p (fromBool $ fRewriting'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 16 (val :: C2HSImp.CInt)}) p (fromBool $ fNaive'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 20 (val :: C2HSImp.CInt)}) p (fromBool $ fVeryVerbose'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 24 (val :: C2HSImp.CInt)}) p (fromBool $ fVerbose'Cec_ParCec x)
(\ptr val -> do {C2HSImp.pokeByteOff ptr 28 (val :: C2HSImp.CInt)}) p (fromIntegral $ iOutFail'Cec_ParCec x)
cecManSatDefaultParams :: Cec_ParSat_t_
cecManSatDefaultParams = Unsafe.unsafePerformIO $ do
alloca $ \p -> do
cecManSatSetDefaultParams p
peek p
foreign import ccall unsafe "Cec_ManSatSetDefaultParams"
cecManSatSetDefaultParams :: Cec_ParSat_t -> IO ()
cecManCecDefaultParams :: Cec_ParCec_t_
cecManCecDefaultParams = Unsafe.unsafePerformIO $ do
alloca $ \p -> do
cecManCecSetDefaultParams p
peek p
foreign import ccall unsafe "Cec_ManCecSetDefaultParams"
cecManCecSetDefaultParams :: Cec_ParCec_t -> IO ()
cecManPatStart :: IO ((Cec_ManPat_t))
cecManPatStart =
cecManPatStart'_ >>= \res ->
let {res' = id res} in
return (res')
cecManPatStop :: (Cec_ManPat_t) -> IO ()
cecManPatStop a1 =
let {a1' = id a1} in
cecManPatStop'_ a1' >>
return ()
cecManPatPrintStats :: (Cec_ManPat_t) -> IO ()
cecManPatPrintStats a1 =
let {a1' = id a1} in
cecManPatPrintStats'_ a1' >>
return ()
cecManPatPatCount :: Cec_ManPat_t -> IO CInt
cecManPatPatCount = (\ptr -> do {C2HSImp.peekByteOff ptr 28 :: IO C2HSImp.CInt})
cecManSatSolve :: (Cec_ManPat_t)
-> (Gia_Man_t)
-> (Cec_ParSat_t)
-> IO ()
cecManSatSolve a1 a2 a3 =
let {a1' = id a1} in
let {a2' = id a2} in
let {a3' = id a3} in
cecManSatSolve'_ a1' a2' a3' >>
return ()
cecManSatSolving :: Gia_Man_t -> Cec_ParSat_t_ -> IO Gia_Man_t
cecManSatSolving aig pars = do
with pars $ \p -> cecManSatSolving' aig p
foreign import ccall unsafe "Cec_ManSatSolving"
cecManSatSolving' :: Gia_Man_t -> Cec_ParSat_t -> IO Gia_Man_t
cecManVerify :: Gia_Man_t -> Cec_ParCec_t_ -> IO CInt
cecManVerify m pars = with pars $ \p -> cecManVerify' m p
foreign import ccall unsafe "Cec_ManVerify"
cecManVerify' :: Gia_Man_t -> Cec_ParCec_t -> IO CInt
foreign import ccall safe "Data/ABC/Internal/CEC.chs.h Cec_ManPatStart"
cecManPatStart'_ :: (IO (Cec_ManPat_t))
foreign import ccall safe "Data/ABC/Internal/CEC.chs.h Cec_ManPatStop"
cecManPatStop'_ :: ((Cec_ManPat_t) -> (IO ()))
foreign import ccall safe "Data/ABC/Internal/CEC.chs.h Cec_ManPatPrintStats"
cecManPatPrintStats'_ :: ((Cec_ManPat_t) -> (IO ()))
foreign import ccall safe "Data/ABC/Internal/CEC.chs.h Cec_ManSatSolve"
cecManSatSolve'_ :: ((Cec_ManPat_t) -> ((Gia_Man_t) -> ((Cec_ParSat_t) -> (IO ()))))