     --     {#call unsafe cudd_bddIte#} ddmanager ip tp ep
     --       >>= addBDDfinalizer
 
-bddConstant :: (DDManager -> IO (Ptr BDD)) -> BDD
-bddConstant f = unsafePerformIO $ f ddmanager >>= addBDDnullFinalizer
+cudd_constant :: (DDManager -> IO (Ptr BDD)) -> BDD
+cudd_constant f = unsafePerformIO $ f ddmanager >>= addBDDnullFinalizer
+{-# INLINE cudd_constant #-}
 
 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
+{-# INLINE bddBinOp #-}
 
 instance QBF BDD where
-    data Group BDD = MkGroup BDD
+    data Group BDD = MkGroup !BDD
 
     mkGroup = MkGroup . conjoin -- FIXME maybe use Cudd_bddComputeCube
     exists = cudd_exists


cToNum :: (Num i, Integral e) => e -> i
cToNum  = fromIntegral . toInteger

cFromEnum :: (Integral i, Enum e) => e -> i
cFromEnum  = fromIntegral . fromEnum

-------------------------------------------------------------------
-- Types.

  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
