 
 cToNum :: (Num i, Integral e) => e -> i
 cToNum  = fromIntegral . toInteger
+{-# INLINE cToNum #-}
 
 cFromEnum :: (Integral i, Enum e) => e -> i
 cFromEnum  = fromIntegral . fromEnum
+{-# INLINE cFromEnum #-}
 
 -------------------------------------------------------------------
 -- Types.

    --     {#call unsafe cudd_bddIte#} ddmanager ip tp ep
    --       >>= addBDDfinalizer

bddConstant :: (DDManager -> IO (Ptr BDD)) -> BDD
bddConstant f = unsafePerformIO $ f ddmanager >>= addBDDnullFinalizer

bddBinOp :: CuddBinOp -> BDD -> BDD -> BDD
bddBinOp op x y = unsafePerformIO $
  withBDD x $ \xp -> withBDD y $ \yp ->
    {#call unsafe cudd_BinOp#} ddmanager (cFromEnum op) xp yp >>= addBDDfinalizer

instance QBF BDD where
    data Group BDD = MkGroup BDD

    mkGroup = MkGroup . conjoin -- FIXME maybe use Cudd_bddComputeCube
    exists = cudd_exists

  withGroup group $ \groupp -> withBDD bdd $ \bddp ->
    {#call unsafe cudd_bddExistAbstract#} ddmanager bddp groupp
      >>= addBDDfinalizer
{-# INLINE cudd_exists #-}

cudd_forall :: Group BDD -> BDD -> BDD
cudd_forall group bdd = unsafePerformIO $ bdd `seq`
  withGroup group $ \groupp -> withBDD bdd $ \bddp ->
    {#call unsafe cudd_bddUnivAbstract#} ddmanager bddp groupp
      >>= addBDDfinalizer
{-# INLINE cudd_forall #-}

cudd_rel_product :: Group BDD -> BDD -> BDD -> BDD
cudd_rel_product group f g = unsafePerformIO $
  withGroup group $ \groupp -> withBDD f $ \fp -> withBDD g $ \gp ->
    {#call unsafe cudd_bddAndAbstract#} ddmanager fp gp groupp
      >>= addBDDfinalizer
{-# INLINE cudd_rel_product #-}

-- | This function swaps variables, as it uses
-- @cudd_bddSwapVariables@. This is not exactly a "rename" behaviour.
cudd_rename :: Subst BDD -> BDD -> BDD
cudd_rename (MkSubst len fpx fpx') f = unsafePerformIO $
  withBDD f $ \fp ->
    withForeignPtr fpx $ \arrayx -> withForeignPtr fpx' $ \arrayx' ->
      {#call unsafe cudd_bddSwapVariables#} ddmanager fp arrayx arrayx' (fromIntegral len)
        >>= addBDDfinalizer
{-# INLINE cudd_rename #-}

-- FIXME verify implementation.
cudd_reduce :: BDD -> BDD -> BDD
