-- 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/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 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 = 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 = Ptr (Cnf_Dat_t_)
{-# LINE 48 "src/Data/ABC/Internal/CNF.chs" #-}


cnfVarNums :: Cnf_Dat_t -> IO (Ptr CInt)
cnfVarNums = (\ptr -> do {peekByteOff ptr 32 ::IO (Ptr 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 
  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 
  withCString a2 $ \a2' -> 
  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 (Ptr (Cnf_Man_t_)))

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

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

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

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

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