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

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

type Abc_Aig_t = 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 {peekByteOff ptr 4 ::IO 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 {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 {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 {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 {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 {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 {peekByteOff ptr 256 ::IO (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 {peekByteOff ptr 304 ::IO (Ptr 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 {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 {peekByteOff ptr 16 ::IO 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 <- peekByteOff ptr 20 ::IO CUInt{-:4-}; return $ (val `shiftL` (32 - 4)) `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 <- peekByteOff ptr 20 ::IO CUInt{-:1-}; return $ (val `shiftL` (32 - 11)) `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 <- peekByteOff ptr 20 ::IO CUInt{-:1-}; return $ (val `shiftL` (32 - 12)) `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' = fromBool a3} in 
  let {a4' = fromIntegral a4} in 
  let {a5' = fromBool a5} in 
  let {a6' = 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' = 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'_ :: (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) -> (CInt -> (CInt -> (CInt -> (CInt -> (IO (Abc_Ntk_t))))))))

foreign import ccall safe "Data/ABC/Internal/ABC.chs.h Abc_NtkMiterIsConstant"
  abcNtkMiterIsConstant'_ :: ((Abc_Ntk_t) -> (IO 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'_ :: (CInt -> (CInt -> (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'_ :: ((Ptr (Abc_Ntk_t)) -> ((Ptr ()) -> (IO CInt)))

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

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