     rel_product = cudd_rel_product
 
 instance Substitution BDD where
-    data Subst BDD = MkSubst [(BDD, BDD)]
-
-    mkSubst = MkSubst
-    rename = cudd_rename
-    substitute = error "CUDD substitute" -- cudd_substitute
+  -- Cache substitution arrays.
+  data Subst BDD = MkSubst {-# UNPACK #-} !Int
+                           {-# UNPACK #-} !(ForeignPtr (Ptr BDD))
+                           {-# UNPACK #-} !(ForeignPtr (Ptr BDD))
+
+  mkSubst = cudd_mkSubst
+  rename = cudd_rename
+  substitute = error "CUDD substitute" -- cudd_substitute
+
+cudd_mkSubst :: [(BDD, BDD)] -> Subst BDD
+cudd_mkSubst subst = unsafePerformIO $
+    do arrayx  <- mallocArray len
+       arrayx' <- mallocArray len
+       zipWithM_ (pokeSubst arrayx arrayx') subst [0..]
+       fpx  <- newForeignPtr finalizerFree arrayx
+       fpx' <- newForeignPtr finalizerFree arrayx'
+       return (MkSubst len fpx fpx')
+  where
+    pokeSubst :: Ptr (Ptr BDD) -> Ptr (Ptr BDD) -> (BDD, BDD) -> Int -> IO ()
+    pokeSubst arrayx arrayx' (v, v') i =
+      do withBDD v  $ pokeElemOff arrayx  i
+         withBDD v' $ pokeElemOff arrayx' i
+
+    len = length subst
+{-# INLINE cudd_mkSubst #-}
 
 instance BDDOps BDD where
     bif bdd = unsafePerformIO $


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

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

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

                                   Just v  -> v

instance Boolean BDD where
    true  = cudd_constant {#call unsafe Cudd_ReadOne as _cudd_ReadOne#}
    false = cudd_constant {#call unsafe Cudd_ReadLogicZero as _cudd_ReadLogicZero#}

    (/\)  = bddBinOp AND
    neg x = unsafePerformIO $ withBDD x $ \xp ->
