-- 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/ABC.chs" #-}
{-# LANGUAGE ForeignFunctionInterface, EmptyDataDecls #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
{- |
Module      : Data.ABC.Internal.ABC
Copyright   : Galois, Inc. 2010-2014
License     : BSD3
Maintainer  : jhendrix@galois.com
Stability   : experimental
Portability : non-portable (c2hs, language extensions)

/Incomplete./ Binding of @base\/base\/abc.h@ for manipulating and
running algorithms on the original ABC datatypes.

This current incomplete binding focuses on functions for manipulating
and-inverter graphs (AIGs).
-}

module Data.ABC.Internal.ABC
    (
    -- * Types
    -- ** Enums
      Abc_NtkType_t(..)
    , Abc_NtkFunc_t(..)
    , Abc_ObjType_t(..)
    -- ** Opague types
    , Abc_Ntk_t_
    , Abc_Obj_t_

    -- ** Pointer types
    , Abc_Ntk_t
    , Abc_Obj_t
    -- * Base
    -- ** Network getters
    , abcNtkFunc
    , abcNtkManName
    , abcNtkObjs
    , abcNtkPis
    , abcNtkPos
    , abcNtkCos
    , abcNtkCis
    , abcNtkObj
    , abcNtkManFunc
    , abcNtkModel
    , abcNtkExdc
    -- ** Counting objects
    , abcNtkPiNum
    , abcNtkPoNum
    , abcNtkCiNum
    , abcNtkCoNum
    , abcNtkLatchNum
    -- ** Creating simple objects
    , abcNtkCreateObj
    , abcObjNot
      -- ** Name manager
    , Nm_Man_t_
    , Nm_Man_t
    , nmManCreate
    , nmManFree

    -- ** Object getters
    , abcObjIsComplement
    , abcObjRegular
    , abcObjId
    , abcObjType
    , abcObjFanins
    , abcObjIsAnd
    , abcObjLit0
    , abcObjLit1
    , abcAigAnd
    , abcAigXor
    , abcAigMux
    , abcAigConst1
    , abcAigCleanup
    -- ** abcFanio.c
    -- | Functions for manipulating fanins and fanouts of a node.
    , abcObjAddFanin
    -- ** abcMiter.c
    -- | Functions for manipulating miters, a combination of two
    -- circuits that outputs @1@ if the outputs of the two original
    -- circuits would have been different.
    , abcNtkMiter
    , abcNtkMiterIsConstant
    -- ** abcNames.c
    -- | Functions for manipulating the names attached to distinguished
    -- nodes.  Many functions in ABC require that networks being
    -- combined be named equivalently, so adopting the canonical form
    -- by 'abcNtkShortNames' helps avoid name mismatch errors.
    , abcNtkShortNames
    -- ** abcNtk.c
    -- | Functions for allocating and deleting networks, each of which
    -- manages the memory of all nodes and other locations attached to it.
    , abcNtkAlloc
    , abcNtkDup
    , abcNtkDelete
    , p_abcNtkDelete
    -- ** abcObj.c
    -- | Functions for manipulating objects in networks.
    , abcNtkDeleteObj
    , abcNtkDeleteObjPo
    -- ** abcProve.c
    -- | Functions for performing SAT solving.
    , abcNtkIvyProve
    -- ** abcVerify.c
    -- | Functions for creating and testing counterexample models.
    , abcNtkVerifySimulatePattern
    -- ** abcBrdige_qbf
    , abcNtkQbf
    ) where
import qualified Data.Bits as C2HSImp
import qualified Foreign.C.Types as C2HSImp
import qualified Foreign.Marshal.Utils as C2HSImp
import qualified Foreign.Ptr as C2HSImp
import qualified Foreign.Storable as C2HSImp



import Control.Monad
import Foreign
import Foreign.C

import Data.ABC.Internal.VecInt
{-# LINE 114 "src/Data/ABC/Internal/ABC.chs" #-}

import Data.ABC.Internal.VecPtr
{-# LINE 115 "src/Data/ABC/Internal/ABC.chs" #-}


import Data.ABC.Internal.Field




data Nm_Man_t_

type Nm_Man_t = C2HSImp.Ptr (Nm_Man_t_)
{-# LINE 124 "src/Data/ABC/Internal/ABC.chs" #-}


nmManCreate :: (CInt) -- nSize
 -> IO ((Nm_Man_t))
nmManCreate a1 =
  let {a1' = id a1} in 
  nmManCreate'_ a1' >>= \res ->
  let {res' = id res} in
  return (res')

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


nmManFree :: (Nm_Man_t) -- p
 -> IO ()
nmManFree a1 =
  let {a1' = id a1} in 
  nmManFree'_ a1' >>
  return ()

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


cintEnum :: (Integral a, Enum b) => a -> b
cintEnum v = toEnum (fromIntegral v)

enumCInt :: Enum a => a -> CInt
enumCInt v = fromIntegral (fromEnum v)

data Abc_NtkType_t = AbcNtkNone
                   | AbcNtkNetlist
                   | AbcNtkLogic
                   | AbcNtkStrash
                   | AbcNtkOther
  deriving (Show,Eq)
instance Enum Abc_NtkType_t where
  succ AbcNtkNone = AbcNtkNetlist
  succ AbcNtkNetlist = AbcNtkLogic
  succ AbcNtkLogic = AbcNtkStrash
  succ AbcNtkStrash = AbcNtkOther
  succ AbcNtkOther = error "Abc_NtkType_t.succ: AbcNtkOther has no successor"

  pred AbcNtkNetlist = AbcNtkNone
  pred AbcNtkLogic = AbcNtkNetlist
  pred AbcNtkStrash = AbcNtkLogic
  pred AbcNtkOther = AbcNtkStrash
  pred AbcNtkNone = error "Abc_NtkType_t.pred: AbcNtkNone has no predecessor"

  enumFromTo from to = go from
    where
      end = fromEnum to
      go v = case compare (fromEnum v) end of
                 LT -> v : go (succ v)
                 EQ -> [v]
                 GT -> []

  enumFrom from = enumFromTo from AbcNtkOther

  fromEnum AbcNtkNone = 0
  fromEnum AbcNtkNetlist = 1
  fromEnum AbcNtkLogic = 2
  fromEnum AbcNtkStrash = 3
  fromEnum AbcNtkOther = 4

  toEnum 0 = AbcNtkNone
  toEnum 1 = AbcNtkNetlist
  toEnum 2 = AbcNtkLogic
  toEnum 3 = AbcNtkStrash
  toEnum 4 = AbcNtkOther
  toEnum unmatched = error ("Abc_NtkType_t.toEnum: Cannot match " ++ show unmatched)

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

data Abc_NtkFunc_t = AbcFuncNone
                   | AbcFuncSop
                   | AbcFuncBdd
                   | AbcFuncAig
                   | AbcFuncMap
                   | AbcFuncBlifmv
                   | AbcFuncBlackbox
                   | AbcFuncOther
  deriving (Show,Eq)
instance Enum Abc_NtkFunc_t where
  succ AbcFuncNone = AbcFuncSop
  succ AbcFuncSop = AbcFuncBdd
  succ AbcFuncBdd = AbcFuncAig
  succ AbcFuncAig = AbcFuncMap
  succ AbcFuncMap = AbcFuncBlifmv
  succ AbcFuncBlifmv = AbcFuncBlackbox
  succ AbcFuncBlackbox = AbcFuncOther
  succ AbcFuncOther = error "Abc_NtkFunc_t.succ: AbcFuncOther has no successor"

  pred AbcFuncSop = AbcFuncNone
  pred AbcFuncBdd = AbcFuncSop
  pred AbcFuncAig = AbcFuncBdd
  pred AbcFuncMap = AbcFuncAig
  pred AbcFuncBlifmv = AbcFuncMap
  pred AbcFuncBlackbox = AbcFuncBlifmv
  pred AbcFuncOther = AbcFuncBlackbox
  pred AbcFuncNone = error "Abc_NtkFunc_t.pred: AbcFuncNone has no predecessor"

  enumFromTo from to = go from
    where
      end = fromEnum to
      go v = case compare (fromEnum v) end of
                 LT -> v : go (succ v)
                 EQ -> [v]
                 GT -> []

  enumFrom from = enumFromTo from AbcFuncOther

  fromEnum AbcFuncNone = 0
  fromEnum AbcFuncSop = 1
  fromEnum AbcFuncBdd = 2
  fromEnum AbcFuncAig = 3
  fromEnum AbcFuncMap = 4
  fromEnum AbcFuncBlifmv = 5
  fromEnum AbcFuncBlackbox = 6
  fromEnum AbcFuncOther = 7

  toEnum 0 = AbcFuncNone
  toEnum 1 = AbcFuncSop
  toEnum 2 = AbcFuncBdd
  toEnum 3 = AbcFuncAig
  toEnum 4 = AbcFuncMap
  toEnum 5 = AbcFuncBlifmv
  toEnum 6 = AbcFuncBlackbox
  toEnum 7 = AbcFuncOther
  toEnum unmatched = error ("Abc_NtkFunc_t.toEnum: Cannot match " ++ show unmatched)

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

data Abc_ObjType_t = AbcObjNone
                   | AbcObjConst1
                   | AbcObjPi
                   | AbcObjPo
                   | AbcObjBi
                   | AbcObjBo
                   | AbcObjNet
                   | AbcObjNode
                   | AbcObjLatch
                   | AbcObjWhitebox
                   | AbcObjBlackbox
                   | AbcObjNumber
  deriving (Show,Eq)
instance Enum Abc_ObjType_t where
  succ AbcObjNone = AbcObjConst1
  succ AbcObjConst1 = AbcObjPi
  succ AbcObjPi = AbcObjPo
  succ AbcObjPo = AbcObjBi
  succ AbcObjBi = AbcObjBo
  succ AbcObjBo = AbcObjNet
  succ AbcObjNet = AbcObjNode
  succ AbcObjNode = AbcObjLatch
  succ AbcObjLatch = AbcObjWhitebox
  succ AbcObjWhitebox = AbcObjBlackbox
  succ AbcObjBlackbox = AbcObjNumber
  succ AbcObjNumber = error "Abc_ObjType_t.succ: AbcObjNumber has no successor"

  pred AbcObjConst1 = AbcObjNone
  pred AbcObjPi = AbcObjConst1
  pred AbcObjPo = AbcObjPi
  pred AbcObjBi = AbcObjPo
  pred AbcObjBo = AbcObjBi
  pred AbcObjNet = AbcObjBo
  pred AbcObjNode = AbcObjNet
  pred AbcObjLatch = AbcObjNode
  pred AbcObjWhitebox = AbcObjLatch
  pred AbcObjBlackbox = AbcObjWhitebox
  pred AbcObjNumber = AbcObjBlackbox
  pred AbcObjNone = error "Abc_ObjType_t.pred: AbcObjNone has no predecessor"

  enumFromTo from to = go from
    where
      end = fromEnum to
      go v = case compare (fromEnum v) end of
                 LT -> v : go (succ v)
                 EQ -> [v]
                 GT -> []

  enumFrom from = enumFromTo from AbcObjNumber

  fromEnum AbcObjNone = 0
  fromEnum AbcObjConst1 = 1
  fromEnum AbcObjPi = 2
  fromEnum AbcObjPo = 3
  fromEnum AbcObjBi = 4
  fromEnum AbcObjBo = 5
  fromEnum AbcObjNet = 6
  fromEnum AbcObjNode = 7
  fromEnum AbcObjLatch = 8
  fromEnum AbcObjWhitebox = 9
  fromEnum AbcObjBlackbox = 10
  fromEnum AbcObjNumber = 11

  toEnum 0 = AbcObjNone
  toEnum 1 = AbcObjConst1
  toEnum 2 = AbcObjPi
  toEnum 3 = AbcObjPo
  toEnum 4 = AbcObjBi
  toEnum 5 = AbcObjBo
  toEnum 6 = AbcObjNet
  toEnum 7 = AbcObjNode
  toEnum 8 = AbcObjLatch
  toEnum 9 = AbcObjWhitebox
  toEnum 10 = AbcObjBlackbox
  toEnum 11 = AbcObjNumber
  toEnum unmatched = error ("Abc_ObjType_t.toEnum: Cannot match " ++ show unmatched)

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

data Abc_InitType_t = AbcInitNone
                    | AbcInitZero
                    | AbcInitOne
                    | AbcInitDc
                    | AbcInitOther
  deriving (Show,Eq)
instance Enum Abc_InitType_t where
  succ AbcInitNone = AbcInitZero
  succ AbcInitZero = AbcInitOne
  succ AbcInitOne = AbcInitDc
  succ AbcInitDc = AbcInitOther
  succ AbcInitOther = error "Abc_InitType_t.succ: AbcInitOther has no successor"

  pred AbcInitZero = AbcInitNone
  pred AbcInitOne = AbcInitZero
  pred AbcInitDc = AbcInitOne
  pred AbcInitOther = AbcInitDc
  pred AbcInitNone = error "Abc_InitType_t.pred: AbcInitNone has no predecessor"

  enumFromTo from to = go from
    where
      end = fromEnum to
      go v = case compare (fromEnum v) end of
                 LT -> v : go (succ v)
                 EQ -> [v]
                 GT -> []

  enumFrom from = enumFromTo from AbcInitOther

  fromEnum AbcInitNone = 0
  fromEnum AbcInitZero = 1
  fromEnum AbcInitOne = 2
  fromEnum AbcInitDc = 3
  fromEnum AbcInitOther = 4

  toEnum 0 = AbcInitNone
  toEnum 1 = AbcInitZero
  toEnum 2 = AbcInitOne
  toEnum 3 = AbcInitDc
  toEnum 4 = AbcInitOther
  toEnum unmatched = error ("Abc_InitType_t.toEnum: Cannot match " ++ show unmatched)

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


data Abc_Ntk_t_
data Abc_Obj_t_
data Abc_Aig_t_

-- | 'Abc_Obj_t' pointer that can have it's lower bit complemented,
-- and thus needs to be converted into an 'Abc_Obj_t' before you
-- can dereference it.

type Abc_Ntk_t = C2HSImp.Ptr (Abc_Ntk_t_)
{-# LINE 153 "src/Data/ABC/Internal/ABC.chs" #-}

type Abc_Obj_t = C2HSImp.Ptr (Abc_Obj_t_)
{-# LINE 154 "src/Data/ABC/Internal/ABC.chs" #-}

type Abc_Aig_t = C2HSImp.Ptr (Abc_Aig_t_)
{-# LINE 155 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Default foreign pointer constructor that just calls free() on the
-- pointer when it is no longer being used.
-- XXX move this somewhere common
newDefaultForeignPtr :: Ptr a -> IO (ForeignPtr a)
newDefaultForeignPtr = newForeignPtr p_abcPrimFree

foreign import ccall unsafe "stdlib.h &free"
    p_abcPrimFree :: FunPtr (Ptr a -> IO ())

abcNtkCreateObj :: Abc_Ntk_t -> Abc_ObjType_t -> IO Abc_Obj_t
abcNtkCreateObj ntk tp = abcNtkCreateObj' ntk (enumCInt tp)

foreign import ccall unsafe "Abc_NtkCreateObj"
  abcNtkCreateObj' :: Abc_Ntk_t -> CInt -> IO Abc_Obj_t

-- inline definitions

abcNtkFunc :: Abc_Ntk_t -> IO Abc_NtkFunc_t
abcNtkFunc ntk = cintEnum `fmap` (\ptr -> do {C2HSImp.peekByteOff ptr 4 :: IO C2HSImp.CInt}) ntk

-- | Network name manager.
abcNtkManName :: Field Abc_Ntk_t Nm_Man_t
abcNtkManName = fieldFromOffset (24)
{-# LINE 179 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Return array of all objects.
abcNtkObjs :: Abc_Ntk_t -> IO Vec_Ptr_t
abcNtkObjs = (\ptr -> do {C2HSImp.peekByteOff ptr 32 :: IO (Vec_Ptr_t)})
{-# LINE 183 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Return primary inputs.
abcNtkPis :: Abc_Ntk_t -> IO Vec_Ptr_t
abcNtkPis = (\ptr -> do {C2HSImp.peekByteOff ptr 40 :: IO (Vec_Ptr_t)})
{-# LINE 187 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Return primary outputs.
abcNtkPos :: Abc_Ntk_t -> IO Vec_Ptr_t
abcNtkPos = (\ptr -> do {C2HSImp.peekByteOff ptr 48 :: IO (Vec_Ptr_t)})
{-# LINE 191 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Return combinational inputs (PIs, latches)
abcNtkCis :: Abc_Ntk_t -> IO Vec_Ptr_t
abcNtkCis = (\ptr -> do {C2HSImp.peekByteOff ptr 56 :: IO (Vec_Ptr_t)})
{-# LINE 195 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Return combinational outputs (POs, asserts, latches).
abcNtkCos :: Abc_Ntk_t -> IO Vec_Ptr_t
abcNtkCos = (\ptr -> do {C2HSImp.peekByteOff ptr 64 :: IO (Vec_Ptr_t)})
{-# LINE 199 "src/Data/ABC/Internal/ABC.chs" #-}


-- | The functionality manager varies between 'AbcNtkFunc'.  In the case
-- of 'AbcFuncAig', this pointer is guaranteed to be an 'Abc_Aig_t'.
abcNtkManFunc :: Abc_Ntk_t -> IO (Ptr ())
abcNtkManFunc = (\ptr -> do {C2HSImp.peekByteOff ptr 256 :: IO (C2HSImp.Ptr ())})
{-# LINE 204 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Return pointer to model associated with network.
abcNtkModel :: Abc_Ntk_t -> IO (Ptr CInt)
abcNtkModel = (\ptr -> do {C2HSImp.peekByteOff ptr 304 :: IO (C2HSImp.Ptr C2HSImp.CInt)})
{-# LINE 208 "src/Data/ABC/Internal/ABC.chs" #-}


-- | The EXDC network.
abcNtkExdc :: Field Abc_Ntk_t Abc_Ntk_t
abcNtkExdc = fieldFromOffset (328)
{-# LINE 212 "src/Data/ABC/Internal/ABC.chs" #-}


abcNtkObj :: Abc_Ntk_t -> Int -> IO Abc_Obj_t
abcNtkObj ntk i = do
  v <- abcNtkObjs ntk
  vecPtrEntry v i

abcNtkPiNum :: Abc_Ntk_t -> IO Int
abcNtkPiNum = vecPtrSize <=< abcNtkPis

abcNtkPoNum :: Abc_Ntk_t -> IO Int
abcNtkPoNum = vecPtrSize <=< abcNtkPos

abcNtkCiNum :: Abc_Ntk_t -> IO Int
abcNtkCiNum = vecPtrSize <=< abcNtkCis

abcNtkCoNum :: Abc_Ntk_t -> IO Int
abcNtkCoNum = vecPtrSize <=< abcNtkCos

abcNtkObjCounts :: Abc_Ntk_t -> Ptr CInt
abcNtkObjCounts = (`plusPtr` (96))

abcNtkObjCount :: Abc_Ntk_t -> Abc_ObjType_t -> IO CInt
abcNtkObjCount p tp = peekElemOff (abcNtkObjCounts p) (fromEnum tp)

abcNtkLatchNum :: Abc_Ntk_t -> IO CInt
abcNtkLatchNum = (`abcNtkObjCount` AbcObjLatch)

-- | Object network
abcObjNtk :: Abc_Obj_t -> IO Abc_Ntk_t
abcObjNtk = (\ptr -> do {C2HSImp.peekByteOff ptr 0 :: IO (Abc_Ntk_t)})
{-# LINE 242 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Object identifier.
abcObjId :: Abc_Obj_t -> IO CInt
abcObjId = (\ptr -> do {C2HSImp.peekByteOff ptr 16 :: IO C2HSImp.CInt})
{-# LINE 246 "src/Data/ABC/Internal/ABC.chs" #-}


-- | Object type.
abcObjType :: Abc_Obj_t -> IO Abc_ObjType_t
abcObjType o = cintEnum `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 20 :: IO C2HSImp.CUInt{-:4-}; return $ (val `C2HSImp.shiftL` (32 - 4)) `C2HSImp.shiftR` (32 - 4)}) o

-- | Indicates if first fanin of object is complemented.
abcObjCompl0 :: Abc_Obj_t -> IO Bool
abcObjCompl0 o = cintEnum `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 20 :: IO C2HSImp.CUInt{-:1-}; return $ (val `C2HSImp.shiftL` (32 - 11)) `C2HSImp.shiftR` (32 - 1)}) o

-- | Indicates if second fanin of object is complemented.
abcObjCompl1 :: Abc_Obj_t -> IO Bool
abcObjCompl1 o = cintEnum `fmap` (\ptr -> do {val <- C2HSImp.peekByteOff ptr 20 :: IO C2HSImp.CUInt{-:1-}; return $ (val `C2HSImp.shiftL` (32 - 12)) `C2HSImp.shiftR` (32 - 1)}) o

-- | Get object fanins.
abcObjFanins :: Abc_Obj_t -> Vec_Int_t
abcObjFanins = (`plusPtr` (24))


abcObjFaninIdx :: Abc_Obj_t -> Int -> IO Int
abcObjFaninIdx o i = do
  fromIntegral `fmap` vecIntEntry (abcObjFanins o) (fromIntegral i)

-- | Return true if this an and gate.
abcObjIsAnd :: Abc_Obj_t -> IO Bool
abcObjIsAnd o = do
  fanin_count <- vecIntSize (abcObjFanins o)
  return (fanin_count == 2)

-- | Return fanin obj at given index.
abcFaninObj :: Abc_Ntk_t -> Abc_Obj_t -> Int -> IO Abc_Obj_t
abcFaninObj ntk o i = do
  objs <- abcNtkObjs ntk
  idx <- abcObjFaninIdx o i
  vecPtrEntry objs idx

abcObjNotIf :: Abc_Obj_t -> Bool -> Abc_Obj_t
abcObjNotIf o b = wordPtrToPtr $ ptrToWordPtr o `xor` (if b then 1 else 0)

abcObjLit0 :: Abc_Obj_t -> IO Abc_Obj_t
abcObjLit0 o = do
  ntk <- abcObjNtk o
  o0 <- abcFaninObj ntk o 0
  c0 <- abcObjCompl0 o
  return (o0 `abcObjNotIf` c0)

abcObjLit1 :: Abc_Obj_t -> IO Abc_Obj_t
abcObjLit1 o = do
  ntk <- abcObjNtk o
  o1 <- abcFaninObj ntk o 1
  c1 <- abcObjCompl1 o
  return (o1 `abcObjNotIf` c1)

-- | Return true if object is complemented.
abcObjIsComplement :: Abc_Obj_t -> Bool
abcObjIsComplement o = ptrToWordPtr o `testBit` 0

-- | Return  normalized object.
abcObjRegular :: Abc_Obj_t -> Abc_Obj_t
abcObjRegular o = wordPtrToPtr $ ptrToWordPtr o `clearBit` 0

-- | Negate object.
abcObjNot :: Abc_Obj_t -> Abc_Obj_t
abcObjNot o = wordPtrToPtr $ ptrToWordPtr o `xor` 1

-- abcAig.c

foreign import ccall unsafe "Abc_AigAnd"
  abcAigAnd :: Abc_Aig_t -> Abc_Obj_t -> Abc_Obj_t -> IO Abc_Obj_t

foreign import ccall unsafe "Abc_AigXor"
  abcAigXor :: Abc_Aig_t -> Abc_Obj_t -> Abc_Obj_t -> IO Abc_Obj_t

foreign import ccall unsafe "Abc_AigMux"
  abcAigMux :: Abc_Aig_t -> Abc_Obj_t -> Abc_Obj_t -> Abc_Obj_t -> IO Abc_Obj_t

abcAigConst1 :: (Abc_Ntk_t) -> IO ((Abc_Obj_t))
abcAigConst1 a1 =
  let {a1' = id a1} in 
  abcAigConst1'_ a1' >>= \res ->
  let {res' = id res} in
  return (res')

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


foreign import ccall unsafe "Abc_AigCleanup"
  abcAigCleanup :: Abc_Aig_t -> IO CInt

-- abcFanio.c

abcObjAddFanin :: (Abc_Obj_t) -- pObj
 -> (Abc_Obj_t) -- pFanin
 -> IO ()
abcObjAddFanin a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  abcObjAddFanin'_ a1' a2' >>
  return ()

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


-- abcMiter.c

abcNtkMiter :: (Abc_Ntk_t) -> (Abc_Ntk_t) -> (Bool) -- fComb
 -> (Int) -- nPartSize
 -> (Bool) -- fImplic
 -> (Bool) -- fMulti
 -> IO ((Abc_Ntk_t))
abcNtkMiter a1 a2 a3 a4 a5 a6 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  let {a3' = C2HSImp.fromBool a3} in 
  let {a4' = fromIntegral a4} in 
  let {a5' = C2HSImp.fromBool a5} in 
  let {a6' = C2HSImp.fromBool a6} in 
  abcNtkMiter'_ a1' a2' a3' a4' a5' a6' >>= \res ->
  let {res' = id res} in
  return (res')

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


abcNtkMiterIsConstant :: (Abc_Ntk_t) -> IO ((Int))
abcNtkMiterIsConstant a1 =
  let {a1' = id a1} in 
  abcNtkMiterIsConstant'_ a1' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

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


-- abcNames.c

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

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


-- abcNtk.c

abcNtkAlloc :: (Abc_NtkType_t) -> (Abc_NtkFunc_t) -> (Bool) -- fUseMemMan
 -> IO ((Abc_Ntk_t))
abcNtkAlloc a1 a2 a3 =
  let {a1' = enumCInt a1} in 
  let {a2' = enumCInt a2} in 
  let {a3' = C2HSImp.fromBool a3} in 
  abcNtkAlloc'_ a1' a2' a3' >>= \res ->
  let {res' = id res} in
  return (res')

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


-- | Duplicate a network, allocating memory for the new network.  This
-- procedure does not preserve the @Id@ of objects.
abcNtkDup :: (Abc_Ntk_t) -> IO ((Abc_Ntk_t))
abcNtkDup a1 =
  let {a1' = id a1} in 
  abcNtkDup'_ a1' >>= \res ->
  let {res' = id res} in
  return (res')

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


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

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



foreign import ccall unsafe "&Abc_NtkDelete"
    p_abcNtkDelete :: FunPtr (Abc_Ntk_t -> IO ())

-- abcObj.c

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

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


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

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


-- abcProve.c

abcNtkIvyProve :: (Ptr Abc_Ntk_t) -> (Ptr ()) -> IO ((Int))
abcNtkIvyProve a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  abcNtkIvyProve'_ a1' a2' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

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


-- abcVerify.c

abcNtkVerifySimulatePattern :: (Abc_Ntk_t) -> (Ptr CInt) -> IO ((ForeignPtr CInt))
abcNtkVerifySimulatePattern a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  abcNtkVerifySimulatePattern'_ a1' a2' >>= \res ->
  newDefaultForeignPtr res >>= \res' ->
  return (res')

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


-- abcBridge_qbv.c

abcNtkQbf :: (Abc_Ntk_t) -- Network
 -> (Int) -- Number of parameters
 -> (CInt) -- Maximum number of iterations.
 -> (Vec_Int_t) -- Vector for storing result.
 -> IO ((Int))
abcNtkQbf a1 a2 a3 a4 =
  let {a1' = id a1} in 
  let {a2' = fromIntegral a2} in 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  abcNtkQbf'_ a1' a2' a3' a4' >>= \res ->
  let {res' = fromIntegral res} in
  return (res')

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

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Nm_ManCreate"
  nmManCreate'_ :: (C2HSImp.CInt -> (IO (Nm_Man_t)))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Nm_ManFree"
  nmManFree'_ :: ((Nm_Man_t) -> (IO ()))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_AigConst1"
  abcAigConst1'_ :: ((Abc_Ntk_t) -> (IO (Abc_Obj_t)))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_ObjAddFanin"
  abcObjAddFanin'_ :: ((Abc_Obj_t) -> ((Abc_Obj_t) -> (IO ())))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkMiter"
  abcNtkMiter'_ :: ((Abc_Ntk_t) -> ((Abc_Ntk_t) -> (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO (Abc_Ntk_t))))))))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkMiterIsConstant"
  abcNtkMiterIsConstant'_ :: ((Abc_Ntk_t) -> (IO C2HSImp.CInt))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkShortNames"
  abcNtkShortNames'_ :: ((Abc_Ntk_t) -> (IO ()))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkAlloc"
  abcNtkAlloc'_ :: (C2HSImp.CInt -> (C2HSImp.CInt -> (C2HSImp.CInt -> (IO (Abc_Ntk_t)))))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkDup"
  abcNtkDup'_ :: ((Abc_Ntk_t) -> (IO (Abc_Ntk_t)))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkDelete"
  abcNtkDelete'_ :: ((Abc_Ntk_t) -> (IO ()))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkDeleteObj"
  abcNtkDeleteObj'_ :: ((Abc_Obj_t) -> (IO ()))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkDeleteObjPo"
  abcNtkDeleteObjPo'_ :: ((Abc_Obj_t) -> (IO ()))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkIvyProve"
  abcNtkIvyProve'_ :: ((C2HSImp.Ptr (Abc_Ntk_t)) -> ((C2HSImp.Ptr ()) -> (IO C2HSImp.CInt)))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkVerifySimulatePattern"
  abcNtkVerifySimulatePattern'_ :: ((Abc_Ntk_t) -> ((C2HSImp.Ptr C2HSImp.CInt) -> (IO (C2HSImp.Ptr C2HSImp.CInt))))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h AbcBridge_NtkQbf"
  abcNtkQbf'_ :: ((Abc_Ntk_t) -> (C2HSImp.CInt -> (C2HSImp.CInt -> ((Vec_Int_t) -> (IO C2HSImp.CInt)))))