diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,1 +1,2 @@
-module Main (main) where import Distribution.Simple ; main = defaultMain
+import Distribution.Simple
+main = defaultMain
diff --git a/obdd.cabal b/obdd.cabal
--- a/obdd.cabal
+++ b/obdd.cabal
@@ -1,5 +1,5 @@
 Name:                obdd
-Version:             0.2.3
+Version:             0.2.5
 Cabal-Version:       >= 1.6
 Build-type: Simple
 Synopsis:            Ordered Reduced Binary Decision Diagrams
@@ -15,6 +15,7 @@
     Build-Depends:       base==4.*, random, mtl, containers
     Hs-Source-Dirs:	     src
     Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property
+    Other-Modules:	     OBDD.IntIntMap, OBDD.VarIntIntMap
     ghc-options: -funbox-strict-fields
 
 
diff --git a/src/OBDD/Data.hs b/src/OBDD/Data.hs
--- a/src/OBDD/Data.hs
+++ b/src/OBDD/Data.hs
@@ -23,6 +23,15 @@
 
 where
 
+import Data.IntMap.Strict ( IntMap )
+import qualified Data.IntMap.Strict as IM
+
+import OBDD.IntIntMap (IntIntMap)
+import qualified OBDD.IntIntMap as IIM
+
+import OBDD.VarIntIntMap (VarIntIntMap)
+import qualified OBDD.VarIntIntMap as VIIM
+
 import Data.Map.Strict ( Map )
 import qualified Data.Map.Strict as M
 
@@ -35,20 +44,28 @@
 import Prelude hiding ( null )
 import qualified Prelude
 
-newtype Index = Index { unIndex :: Int }
-   deriving ( Eq, Ord, Num, Enum, Show )
+-- newtype Index = Index { unIndex :: Int }
+--   deriving ( Eq, Ord, Num, Enum, Show )
 
+type Index = Int ; unIndex = id
+
 -- | assumes total ordering on variables
 data OBDD v = OBDD
-	    { core :: !(Map Index ( Node v Index ))
-	    , icore :: !(Map ( Node v Index ) Index)
-	    , counter :: Map Index Integer -- ^ number of assignments
+	    { core :: !(IntMap ( Node v Index ))
+	    
+            -- , icore :: !(Map ( Node v Index ) Index)
+            , icore :: !(VarIntIntMap v Index)
 	    , next :: !Index
 	    , top :: !Index
-	    , cache :: ! (Map ( Index, Index ) Index) -- ^ inputs and output for binary op
-		    -- (unary will be simulated by binary)
+	    
+            , cache ::  !(IntIntMap Index) 
+               -- ^ inputs and output for binary op
+               -- (unary will be simulated by binary)
 	    }
 
+icore_false = 0 :: Index  
+icore_true = 1 :: Index  
+              
 size = unIndex . next
 
 -- | Number of satisfying assignments with  given set of variables.
@@ -72,51 +89,50 @@
                              xr <- fun r post
                              let xlr = xl + xr
                              m <- get
-                             put $ M.insert ( top o ) xlr m
+                             put $! M.insert ( top o ) xlr m
                              return $ ( 2 ^ length pre ) * xlr
     in evalState ( fun o $ reverse $ S.toAscList vs ) M.empty
     
 
 empty :: OBDD v
 empty = OBDD 
-      { core = M.empty
-      , icore = M.empty
-      , counter = M.empty
-      , next = 0
-      , top = -42 -- error "OBDD.Data.empty"
-      , cache = M.empty
+      { core = IM.empty
+      , icore = VIIM.empty
+      , next = 2
+      , top = 0
+      , cache = IIM.empty
       }
 
 data Node v i = Leaf !Bool
 	    | Branch !v !i !i
     deriving ( Eq, Ord )
 
-{-! for Node derive: ToDoc !-}
-
 access :: OBDD v -> Node v ( OBDD v )
-access s = case M.lookup ( top s ) ( core s ) of
-    Nothing -> error "OBDD.Data.access"
-    Just n  -> case n of
-        Leaf p -> Leaf p
-	Branch v l r -> 
-          Branch v ( s { top = l } ) ( s { top = r } )
-
-count :: OBDD v -> Index -> Integer
-count s i = case M.lookup i ( counter s ) of
-    Nothing -> error "OBDD.Data.count"
-    Just n  -> n
+access s = case top s of
+    0 -> Leaf False
+    1 -> Leaf True
+    t -> case IM.lookup ( top s ) ( core s ) of
+        Nothing -> error "OBDD.Data.access"
+        Just n  -> case n of
+            Leaf p -> error "Leaf in core"
+	    Branch v l r -> 
+                Branch v ( s { top = l } ) 
+                         ( s { top = r } )
 
 -- | does the OBDD have any models?
 satisfiable :: OBDD v -> Bool
-satisfiable s = 0 < count s ( top s )
+satisfiable = not . null
 
 -- | does the OBDD not have any models?
 null :: OBDD v -> Bool
-null s = 0 == count s ( top s )
-
+null s = case access s of
+      Leaf False -> True 
+      _ -> False
 
 -- | randomly select one model, if possible
-some_model :: Ord v => OBDD v -> IO ( Maybe  ( Map v Bool ) )
+some_model :: Ord v 
+           => OBDD v 
+           -> IO ( Maybe  ( Map v Bool ) )
 some_model s = case access s of
     Leaf True -> return $ Just $ M.empty
     Leaf False -> return Nothing
@@ -131,7 +147,8 @@
         Just m <- some_model t
         return $ Just $ M.insert v p m 
 
--- | list of all models (WARNING not using variables that had been deleted)
+-- | list of all models (WARNING not using 
+-- variables that had been deleted)
 all_models :: Ord v => OBDD v -> [ Map v Bool ]
 all_models s = case access s of
     Leaf True -> return  M.empty
@@ -162,7 +179,7 @@
 fresh = do
     s <- get
     let i = next s
-    put $ s { next = succ i }
+    put $! s { next = succ i }
     return i
 
 cached :: Ord v
@@ -171,32 +188,31 @@
 	-> State ( OBDD v ) Index
 cached (l,r) action = do
     s <- get
-    case M.lookup (l,r) $ cache s of
+    case IIM.lookup (l, r) $ cache s of
         Just i -> return i
 	Nothing -> do
 	    i <- action
 	    s <- get
-	    put $ s { cache = M.insert ( l,r) i $ cache s }
+	    put $! s { cache = IIM.insert (l, r) i 
+                              $ cache s }
 	    return i
 
 register :: Ord v
 	 => Node v Index
        -> State ( OBDD v ) Index
-register n = do
-    s <- get
-    case M.lookup n ( icore s ) of
+register n = case n of
+    Leaf False -> return 0
+    Leaf True -> return 1
+    Branch v l r -> if l == r then return l else do
+      s <- get    
+      case VIIM.lookup (v, l, r) ( icore s ) of
         Just i -> return i
-	Nothing -> case n of
-            Branch v l r | l == r -> return l -- TRICK (?)
-            _ -> do
+	Nothing -> do
 	        i <- fresh
 	        s <- get
-	        let c = case n of
-		        Leaf p -> if p then 1 else 0
-		        Branch v l r -> count s l + count s r 
-	        put $ s 
-		    { core = M.insert i n $ core s
-		    , icore = M.insert n i $ icore s
-		    , counter = M.insert i c $ counter s
+	        put $! s 
+		    { core = IM.insert i n $ core s
+		    , icore = VIIM.insert (v, l, r) i 
+                            $ icore s
 		    }
 	        return i  
diff --git a/src/OBDD/IntIntMap.hs b/src/OBDD/IntIntMap.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/IntIntMap.hs
@@ -0,0 +1,31 @@
+module OBDD.IntIntMap 
+       
+( IntIntMap ()       
+, empty, lookup, insert, singleton
+)  
+       
+where
+
+import Prelude hiding ( lookup )  
+  
+import Data.IntMap (IntMap)
+import qualified Data.IntMap.Strict as M
+
+newtype IntIntMap v = IntIntMap (IntMap (IntMap v))
+
+empty = IntIntMap M.empty
+
+singleton (i, j) v = 
+    IntIntMap $ M.singleton i (M.singleton j v) 
+
+lookup (i, j) (IntIntMap mm) = do
+    m <- M.lookup i mm
+    M.lookup j m
+
+insert (i, j) v (IntIntMap mm) = 
+    case M.lookup i mm of
+        Nothing -> IntIntMap 
+                   $ M.insert i (M.singleton j v) mm 
+        Just m -> IntIntMap           
+                   $ M.insert i (M.insert j v m) mm 
+                   
diff --git a/src/OBDD/Operation.hs b/src/OBDD/Operation.hs
--- a/src/OBDD/Operation.hs
+++ b/src/OBDD/Operation.hs
@@ -19,7 +19,8 @@
 import Data.Set ( Set )
 import qualified Data.Set as S
 
-import Data.List ( foldl' )
+-- import Data.List ( foldl' )
+-- don't use, see below
 
 import Prelude hiding ( (&&), (||), and, or, not )
 import qualified Prelude
@@ -30,11 +31,15 @@
 ( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v
 ( || ) = binary ( Prelude.|| )
 
+
+
 and :: Ord v => [ OBDD v ] -> OBDD v
-and = foldl' ( && ) ( constant True ) 
+and = foldr ( && ) ( constant True ) 
+-- writing foldl or fold' here 
+-- makes performance MUCH worse!
 
 or :: Ord v => [ OBDD v ] -> OBDD v
-or = foldl' ( || ) ( constant False ) 
+or = foldr ( || ) ( constant False ) 
 
 
 -- | FIXME this is a silly implementation. Negation should be done
diff --git a/src/OBDD/Property.hs b/src/OBDD/Property.hs
--- a/src/OBDD/Property.hs
+++ b/src/OBDD/Property.hs
@@ -3,6 +3,7 @@
 ( null, satisfiable
 , number_of_models
 , some_model, all_models
+, size
 )
 
 where
diff --git a/src/OBDD/VarIntIntMap.hs b/src/OBDD/VarIntIntMap.hs
new file mode 100644
--- /dev/null
+++ b/src/OBDD/VarIntIntMap.hs
@@ -0,0 +1,23 @@
+module OBDD.VarIntIntMap where
+
+import qualified OBDD.IntIntMap as I
+import qualified Data.Map.Strict as M
+import Prelude hiding ( lookup )  
+  
+
+newtype VarIntIntMap k v = 
+    VarIntIntMap ( M.Map k ( I.IntIntMap v ))
+    
+empty = VarIntIntMap M.empty
+
+lookup (k, i, j) (VarIntIntMap mm) = do
+    m <- M.lookup k mm
+    I.lookup (i, j) m
+
+insert (k, i, j) v (VarIntIntMap mm) = 
+    case M.lookup k mm of
+        Nothing -> VarIntIntMap 
+                   $ M.insert k (I.singleton (i, j) v) mm
+        Just m -> VarIntIntMap           
+                   $ M.insert k (I.insert (i, j) v m) mm
+