-- GENERATED by C->Haskell Compiler, version 0.20.1 The shapeless maps, 31 Oct 2014 (Haskell)
-- Edit the ORIGNAL .chs file instead!


{-# LINE 1 "src/Data/ABC/Internal/CEC.chs" #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}

{- |
Module      : Data.ABC.Internal.CEC
Copyright   : Galois, Inc. 2010-2014
License     : BSD3
Maintainer  : jhendrix@galois.com
Stability   : experimental
Portability : non-portable (c2hs, language extensions)

Comprehensive binding of @aig\/cec\/cec.h@ for performing combinational
equivalence checking of scalable and-inverter graphs (GIA).

-}

module Data.ABC.Internal.CEC (
    -- * Types
    -- ** Storable types
      Cec_ParCec_t_(..)
    , Cec_ParSat_t_(..)
    -- * Functions
    -- ** cecCec.c
    , cecManVerify
    -- ** cecCore.c
    , cecManSatDefaultParams
    , cecManCecDefaultParams
    , cecManSatSolving
    , Cec_ManPat_t_
    , Cec_ManPat_t
    , cecManPatStart
    , cecManPatStop
    , cecManPatPatCount
    , cecManPatPrintStats
    , cecManSatSolve
    ) where





import Control.Applicative
import Foreign
import Foreign.C (CInt(..))
import qualified System.IO.Unsafe as Unsafe

import Data.ABC.Internal.GIA
{-# LINE 48 "src/Data/ABC/Internal/CEC.chs" #-}


type Cec_ParSat_t = Ptr (Cec_ParSat_t_)
{-# LINE 50 "src/Data/ABC/Internal/CEC.chs" #-}

type Cec_ParCec_t = Ptr Cec_ParCec_t_

data Cec_ManPat_t_
type Cec_ManPat_t = Ptr (Cec_ManPat_t_)
{-# LINE 54 "src/Data/ABC/Internal/CEC.chs" #-}


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
{-# LINE 68 "src/Data/ABC/Internal/CEC.chs" #-}

  alignment _ = alignment (undefined :: CInt)
  peek p = Cec_ParSat_t_
      <$> pInt  (\ptr -> do {peekByteOff ptr 0 ::IO CInt})
{-# LINE 71 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pInt  (\ptr -> do {peekByteOff ptr 4 ::IO CInt})
{-# LINE 72 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pInt  (\ptr -> do {peekByteOff ptr 8 ::IO CInt})
{-# LINE 73 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pBool (\ptr -> do {peekByteOff ptr 12 ::IO CInt})
{-# LINE 74 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pBool (\ptr -> do {peekByteOff ptr 16 ::IO CInt})
{-# LINE 75 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pBool (\ptr -> do {peekByteOff ptr 20 ::IO CInt})
{-# LINE 76 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pBool (\ptr -> do {peekByteOff ptr 24 ::IO CInt})
{-# LINE 77 "src/Data/ABC/Internal/CEC.chs" #-}

      <*> pBool (\ptr -> do {peekByteOff ptr 28 ::IO CInt})
{-# LINE 78 "src/Data/ABC/Internal/CEC.chs" #-}

    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 {pokeByteOff ptr 0 (val::CInt)}) nBTLimit'Cec_ParSat
      pokeInt  (\ptr val -> do {pokeByteOff ptr 4 (val::CInt)}) nSatVarMax'Cec_ParSat
      pokeInt  (\ptr val -> do {pokeByteOff ptr 8 (val::CInt)}) nCallsRecycle'Cec_ParSat
      pokeBool (\ptr val -> do {pokeByteOff ptr 12 (val::CInt)})   fNonChrono'Cec_ParSat
      pokeBool (\ptr val -> do {pokeByteOff ptr 16 (val::CInt)})   fPolarFlip'Cec_ParSat
      pokeBool (\ptr val -> do {pokeByteOff ptr 20 (val::CInt)})   fCheckMiter'Cec_ParSat
      pokeBool (\ptr val -> do {pokeByteOff ptr 24 (val::CInt)})     fLearnCls'Cec_ParSat
      pokeBool (\ptr val -> do {pokeByteOff ptr 28 (val::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      -- ^ conflict limit at a node
    , nTimeLimit'Cec_ParCec :: Int    -- ^ the runtime limit in seconds (added prefix @n@)
    , fUseSmartCnf'Cec_ParCec :: Bool -- ^ use smart CNF computation
    , fRewriting'Cec_ParCec :: Bool   -- ^ enables AIG rewriting
    , fVeryVerbose'Cec_ParCec :: Bool -- ^ very verbose stats
    , fVerbose'Cec_ParCec :: Bool     -- ^ verbose stats
    , iOutFail'Cec_ParCec :: Int      -- ^ the number of failed output
    } deriving (Show, Read, Eq)

instance Storable Cec_ParCec_t_ where
    sizeOf _ = 28
{-# LINE 108 "src/Data/ABC/Internal/CEC.chs" #-}

    alignment _ = alignment (undefined :: CInt)
    peek p = Cec_ParCec_t_
        <$> fmap fromIntegral ((\ptr -> do {peekByteOff ptr 0 ::IO CInt}) p)
        <*> fmap fromIntegral ((\ptr -> do {peekByteOff ptr 4 ::IO CInt}) p)
        <*> fmap toBool ((\ptr -> do {peekByteOff ptr 8 ::IO CInt}) p)
        <*> fmap toBool ((\ptr -> do {peekByteOff ptr 12 ::IO CInt}) p)
        <*> fmap toBool ((\ptr -> do {peekByteOff ptr 16 ::IO CInt}) p)
        <*> fmap toBool ((\ptr -> do {peekByteOff ptr 20 ::IO CInt}) p)
        <*> fmap fromIntegral ((\ptr -> do {peekByteOff ptr 24 ::IO CInt}) p)
    poke p x = do
        (\ptr val -> do {pokeByteOff ptr 0 (val::CInt)})      p (fromIntegral $ nBTLimit'Cec_ParCec x)
        (\ptr val -> do {pokeByteOff ptr 4 (val::CInt)})     p (fromIntegral $ nTimeLimit'Cec_ParCec x)
        (\ptr val -> do {pokeByteOff ptr 8 (val::CInt)})  p (fromBool $ fUseSmartCnf'Cec_ParCec x)
        (\ptr val -> do {pokeByteOff ptr 12 (val::CInt)})    p (fromBool $ fRewriting'Cec_ParCec x)
        (\ptr val -> do {pokeByteOff ptr 16 (val::CInt)})  p (fromBool $ fVeryVerbose'Cec_ParCec x)
        (\ptr val -> do {pokeByteOff ptr 20 (val::CInt)})      p (fromBool $ fVerbose'Cec_ParCec x)
        (\ptr val -> do {pokeByteOff ptr 24 (val::CInt)})      p (fromIntegral $ iOutFail'Cec_ParCec x)


-- cecCore.c

{-# NOINLINE cecManSatDefaultParams #-}
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 ()

{-# NOINLINE cecManCecDefaultParams #-}
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')

{-# LINE 150 "src/Data/ABC/Internal/CEC.chs" #-}


cecManPatStop :: (Cec_ManPat_t) -> IO ()
cecManPatStop a1 =
  let {a1' = id a1} in 
  cecManPatStop'_ a1' >>
  return ()

{-# LINE 152 "src/Data/ABC/Internal/CEC.chs" #-}


cecManPatPrintStats :: (Cec_ManPat_t) -> IO ()
cecManPatPrintStats a1 =
  let {a1' = id a1} in 
  cecManPatPrintStats'_ a1' >>
  return ()

{-# LINE 154 "src/Data/ABC/Internal/CEC.chs" #-}


cecManPatPatCount :: Cec_ManPat_t -> IO CInt
cecManPatPatCount = (\ptr -> do {peekByteOff ptr 28 ::IO CInt})
{-# LINE 157 "src/Data/ABC/Internal/CEC.chs" #-}


cecManSatSolve :: (Cec_ManPat_t) -- pPat
 -> (Gia_Man_t) -- pAig
 -> (Cec_ParSat_t) -- pPars
 -> 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 ()

{-# LINE 163 "src/Data/ABC/Internal/CEC.chs" #-}



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 ()))))