-- GENERATED by C->Haskell Compiler, version 0.28.1 Switcheroo, 1 April 2016 (Haskell)
-- Edit the ORIGNAL .chs file instead!


{-# LINE 1 "src/Data/ABC/Internal/CNF.chs" #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
{- |
Module      : Data.ABC.Internal.CNF
Copyright   : Galois, Inc. 2010-2014
License     : BSD3
Maintainer  : jhendrix@galois.com
Stability   : experimental
Portability : non-portable (c2hs, language extensions)
-}
module Data.ABC.Internal.CNF
  ( Cnf_Dat_t
  , cnfVarNums
  , withCnfDerive
  , cnfDataWriteIntoFile
  , Cnf_Man_t
  , Cnf_Man_t_
  , cnfManStart
  , cnfDeriveWithMan
  , cnfDataFree
  , cnfDataWriteIntoFileWithHeader
  ) where
import qualified Foreign.C.String as C2HSImp
import qualified Foreign.C.Types as C2HSImp
import qualified Foreign.ForeignPtr as C2HSImp
import qualified Foreign.Ptr as C2HSImp
import qualified Foreign.Storable as C2HSImp



import Control.Exception (bracket)
import Data.ABC.Internal.AIG
import Foreign
import Foreign.C



data Cnf_Man_t_


{-# LINE 32 "src/Data/ABC/Internal/CNF.chs" #-}


type Cnf_Man_t = C2HSImp.ForeignPtr (Cnf_Man_t_)
{-# LINE 34 "src/Data/ABC/Internal/CNF.chs" #-}


foreign import ccall unsafe "&Cnf_ManStop"
    p_cnfManStop :: FunPtr (Ptr Cnf_Man_t_ -> IO ())

newCnfMan :: Ptr Cnf_Man_t_ -> IO Cnf_Man_t
newCnfMan = newForeignPtr p_cnfManStop

-- | Create a new CNF manager.
cnfManStart :: IO ((Cnf_Man_t))
cnfManStart =
  cnfManStart'_ >>= \res ->
  newCnfMan res >>= \res' ->
  return (res')

{-# LINE 44 "src/Data/ABC/Internal/CNF.chs" #-}


data Cnf_Dat_t_

type Cnf_Dat_t = C2HSImp.Ptr (Cnf_Dat_t_)
{-# LINE 48 "src/Data/ABC/Internal/CNF.chs" #-}


cnfVarNums :: Cnf_Dat_t -> IO (Ptr CInt)
cnfVarNums = (\ptr -> do {C2HSImp.peekByteOff ptr 32 :: IO (C2HSImp.Ptr C2HSImp.CInt)})
{-# LINE 51 "src/Data/ABC/Internal/CNF.chs" #-}


cnfDerive :: (Aig_Man_t) -> (CInt) -> IO ((Cnf_Dat_t))
cnfDerive a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  cnfDerive'_ a1' a2' >>= \res ->
  let {res' = id res} in
  return (res')

{-# LINE 57 "src/Data/ABC/Internal/CNF.chs" #-}


-- | Use results on cnfDerive in a comptuation, then free them.
withCnfDerive :: Aig_Man_t -> CInt -> (Cnf_Dat_t -> IO a) -> IO a
withCnfDerive mgr outputCount h =
  bracket (cnfDerive mgr outputCount) cnfDataFree h

cnfDeriveWithMan :: (Cnf_Man_t) -> (Aig_Man_t) -> (CInt) -> IO ((Cnf_Dat_t))
cnfDeriveWithMan a1 a2 a3 =
  withForeignPtr a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  cnfDeriveWithMan'_ a1' a2' a3' >>= \res ->
  let {res' = id res} in
  return (res')

{-# LINE 68 "src/Data/ABC/Internal/CNF.chs" #-}


cnfDataWriteIntoFile :: (Cnf_Dat_t) -> (String) -> (Int) -> (Ptr ()) -> (Ptr ()) -> IO ()
cnfDataWriteIntoFile a1 a2 a3 a4 a5 =
  let {a1' = id a1} in 
  C2HSImp.withCString a2 $ \a2' -> 
  let {a3' = fromIntegral a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  cnfDataWriteIntoFile'_ a1' a2' a3' a4' a5' >>
  return ()

{-# LINE 76 "src/Data/ABC/Internal/CNF.chs" #-}


cnfDataWriteIntoFileWithHeader :: (Cnf_Dat_t) -> (String) -- Filename
 -> (String) -- Header
 -> (Int) -> IO ()
cnfDataWriteIntoFileWithHeader a1 a2 a3 a4 =
  let {a1' = id a1} in 
  C2HSImp.withCString a2 $ \a2' -> 
  C2HSImp.withCString a3 $ \a3' -> 
  let {a4' = fromIntegral a4} in 
  cnfDataWriteIntoFileWithHeader'_ a1' a2' a3' a4' >>
  return ()

{-# LINE 83 "src/Data/ABC/Internal/CNF.chs" #-}


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

{-# LINE 87 "src/Data/ABC/Internal/CNF.chs" #-}


foreign import ccall safe "Data/ABC/Internal/CNF.chs.h Cnf_ManStart"
  cnfManStart'_ :: (IO (C2HSImp.Ptr (Cnf_Man_t_)))

foreign import ccall safe "Data/ABC/Internal/CNF.chs.h Cnf_Derive"
  cnfDerive'_ :: ((Aig_Man_t) -> (C2HSImp.CInt -> (IO (Cnf_Dat_t))))

foreign import ccall safe "Data/ABC/Internal/CNF.chs.h Cnf_DeriveWithMan"
  cnfDeriveWithMan'_ :: ((C2HSImp.Ptr (Cnf_Man_t_)) -> ((Aig_Man_t) -> (C2HSImp.CInt -> (IO (Cnf_Dat_t)))))

foreign import ccall safe "Data/ABC/Internal/CNF.chs.h Cnf_DataWriteIntoFile"
  cnfDataWriteIntoFile'_ :: ((Cnf_Dat_t) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (C2HSImp.CInt -> ((C2HSImp.Ptr ()) -> ((C2HSImp.Ptr ()) -> (IO ()))))))

foreign import ccall safe "Data/ABC/Internal/CNF.chs.h Cnf_DataWriteIntoFileWithHeader"
  cnfDataWriteIntoFileWithHeader'_ :: ((Cnf_Dat_t) -> ((C2HSImp.Ptr C2HSImp.CChar) -> ((C2HSImp.Ptr C2HSImp.CChar) -> (C2HSImp.CInt -> (IO C2HSImp.CInt)))))

foreign import ccall safe "Data/ABC/Internal/CNF.chs.h Cnf_DataFree"
  cnfDataFree'_ :: ((Cnf_Dat_t) -> (IO ()))