diff --git a/bin/rtree-c/Main.hs b/bin/rtree-c/Main.hs
index 278c3a8b798745f54aac40ad85cdc4a3b796c08c..ba16a49850b0034fe324d75d6682c505a31109e6 100644
--- a/bin/rtree-c/Main.hs
+++ b/bin/rtree-c/Main.hs
@@ -13,10 +13,17 @@ import ReduceC
 import Colog
 import Control.Applicative
 import Control.Monad
+import Control.Monad.State
 import Control.Monad.Trans
+import Data.Bool (bool)
 import Data.Foldable
 import Data.Functor
+import Data.List (intercalate)
+import Data.Map.Strict qualified as Map
 import Data.Text qualified as Text
+import Data.Time (getCurrentTime)
+import Data.Time qualified as Time
+import Data.Vector qualified as V
 import GHC.Stack
 import Language.C qualified as C
 import Options.Applicative
@@ -56,6 +63,14 @@ run = do
         , help "run in exponential mode"
         ]
 
+  checkmode <-
+    flag False True
+      $ fold
+        [ long "dry-run"
+        , short 'n'
+        , help "don't do any reduction"
+        ]
+
   validity <-
     optional
       $ strOption
@@ -83,9 +98,22 @@ run = do
 
   file <- strArgument $ fold [metavar "FILE"]
 
-  pure
-    $ usingLoggerT (cmap fmtMessage logTextStdout)
-    $ do
+  pure do
+    t <- getCurrentTime
+    let
+      fmt m = do
+        t' <- getCurrentTime
+        pure
+          ( Text.pack
+              ( Time.formatTime
+                  Time.defaultTimeLocale
+                  "%_3m:%04ES "
+                  (t' `Time.diffUTCTime` t)
+              )
+              <> fmtMessage m
+          )
+
+    usingLoggerT (cmapM fmt logTextStderr) do
       let
         test f = process D ("test " <> Text.pack f) do
           err <- liftIO $ runProcess cmd
@@ -103,24 +131,44 @@ run = do
           let x = P.render (C.pretty (c $> C.undefNode))
           liftIO $ writeFile f x
 
-        check' f val c = do
-          logInfo "Checking predictate"
-          when debug do
-            pPrint [(void k, v) | (k, v) <- Val.toPairs val]
-            pPrint (void c)
-          when pedandic do
-            liftIO $ copyFile file (file <.> "last")
-          output f c
-          v <- validiate f
-          if v
-            then test f
-            else do
-              logWarning "Produced invalid code"
-              liftIO $ when pedandic do
-                copyFile file (file <.> "fail")
-                copyFile (file <.> "last") file
-                exitFailure
+        cleanup f = do
+          logError "Cleaning up"
+          liftIO do
+            copyFile (f <.> "bak") f
+            removeFile (f <.> "bak")
+          liftIO exitFailure
+
+        check' f (ReState ch i val) mc = process I "Checking predictate" do
+          logDebug . Text.pack $ map (\j -> maybe '*' (bool '0' '1') (ch V.!? j)) [0 .. i]
+          logDebug
+            . Text.pack
+            $ intercalate
+              ", "
+              [C.identToString k | (k, v) <- Val.toPairs val, v]
+          logDebug
+            . Text.pack
+            $ intercalate
+              ", "
+              ["!" <> C.identToString k | (k, v) <- Val.toPairs val, not v]
+          case mc of
+            Nothing -> do
+              logDebug "Empty input"
               pure False
+            Just c -> do
+              when debug do
+                pPrint (void c)
+              when pedandic do
+                liftIO $ copyFile f (f <.> "last")
+              output f c
+              v <- validiate f
+              if v
+                then test f
+                else do
+                  logWarning "Produced invalid code"
+                  when pedandic do
+                    liftIO $ copyFile f (f <.> "fail")
+                    cleanup f
+                  pure False
 
       let bak = file <.> "bak"
 
@@ -153,20 +201,32 @@ run = do
           liftIO do
             withFile "error.1.hs" WriteMode (`pHPrint` void c)
             withFile "error.2.hs" WriteMode (`pHPrint` void c')
-          logError "Outputted a different file than i read... Please report original file and error.{1,2}.hs"
+          logError "Outputted a different file than I read... Please report original file and error.{1,2}.hs"
           liftIO exitFailure
 
         t <- test file
         unless t do
-          liftIO exitFailure
+          logError "file did not satisfy predicate"
+          cleanup file
+
+      when checkmode do
+        liftIO exitSuccess
 
       l <-
-        (if expmode then ireduceExp else ireduce)
+        (if expmode then ireduceExpT (`evalStateT` Map.empty) else ireduceT (`evalStateT` Map.empty))
           (check' file)
           (Val.singleton (Val.is $ C.internalIdent "main"))
           (ReduceC.reduceC c)
 
-      output file l
+      when pedandic do
+        liftIO $ copyFile file (file <.> "last")
+
+      case l of
+        Just l' ->
+          output file l'
+        Nothing -> do
+          logError "Was unable to produce any output"
+          cleanup file
  where
   parseCFile file = do
     res <- liftIO $ C.parseCFilePre file
diff --git a/bin/rtree-c/ReduceC.hs b/bin/rtree-c/ReduceC.hs
index e6174f3dcf2c7269d78ac0a889b4b507c858a4b2..6ba2a1058d8e77f04972fa9003926746a410731c 100644
--- a/bin/rtree-c/ReduceC.hs
+++ b/bin/rtree-c/ReduceC.hs
@@ -1,7 +1,12 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 
@@ -12,273 +17,239 @@ import Control.Monad.Reduce
 import qualified Data.Valuation as Val
 
 import Control.Applicative
-import Control.Monad.Trans
+import Control.Monad.State
 import Control.Monad.Trans.Maybe
-import Data.Foldable
+import Data.Data
+import Data.Function
 import Data.Functor
-import Data.Maybe
+import qualified Data.Map.Strict as Map
+import Data.Maybe (catMaybes)
 import qualified Language.C as C
 
 type Lab = C.Ident
 
-reduceC :: (MonadReduce Lab m) => C.CTranslUnit -> m C.CTranslUnit
+data LabInfo
+  = Type [C.CDeclarationSpecifier C.NodeInfo]
+
+type CState = Map.Map Lab LabInfo
+
+reduceC :: (MonadReduce Lab m, MonadState CState m) => C.CTranslUnit -> m C.CTranslUnit
 reduceC (C.CTranslUnit es ni) = do
-  es' <- collect mrCExternalDeclaration es
+  es' <- collect reduceCExternalDeclaration es
   pure $ C.CTranslUnit es' ni
+ where
+  reduceCExternalDeclaration = \case
+    C.CFDefExt fun -> do
+      C.CFDefExt <$> reduce @C.CFunctionDef fun
+    C.CDeclExt decl ->
+      C.CDeclExt <$> reduce @C.CDeclaration decl
+    a -> error (show a)
 
-mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo)
-mrCExternalDeclaration = \case
-  C.CFDefExt fun -> do
-    C.CFDefExt <$> mrCFunctionDef fun
-  C.CDeclExt decl ->
-    C.CDeclExt <$> mrCDeclaration decl
-  a -> error (show a)
-
-mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo)
-mrCDeclaration = \case
-  C.CDecl spc decl ni -> do
-    mapM_ cCDeclarationSpecifier spc
-    decl' <- lift $ collect mrCDeclarationItem decl
-    case decl' of
-      [] -> empty
-      decl'' -> pure $ C.CDecl spc decl'' ni
-  a -> error (show a)
+identifiers :: forall a. (Data a) => a -> [Lab]
+identifiers d = case cast d of
+  Just l -> [l]
+  Nothing -> concat $ gmapQ identifiers d
 
-mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo)
-mrCDeclarationItem = \case
-  C.CDeclarationItem d i e -> do
-    i' <- mtry $ munder i mrCInitializer
-    e' <- mtry $ munder e mrCExpression
-    cCDeclr d
-    pure (C.CDeclarationItem d i' e')
-  a -> error (show a)
+type Reducer m a = a -> m a
 
-cCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m ()
-cCDeclarationItem = \case
-  C.CDeclarationItem d i e -> do
-    munder i cCInitializer
-    munder e cCExpression
-    cCDeclr d
-  a -> error (show a)
+class CReducible c where
+  reduce :: (MonadReducePlus Lab m, MonadState CState m) => Reducer m (c C.NodeInfo)
 
-cCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m ()
-cCDeclaration = \case
-  C.CDecl spc decl _ -> do
-    forM_ spc cCDeclarationSpecifier
-    mapM_ cCDeclarationItem decl
-  a -> error (show a)
+cDeclaratorIdentifiers :: C.CDeclarator C.NodeInfo -> (Maybe Lab, [Lab])
+cDeclaratorIdentifiers (C.CDeclr mi dd _ la _) =
+  (mi, identifiers dd <> identifiers la)
 
-cCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m ()
-cCExpression e =
-  -- TODO not optimal, create version that only checks for identifiers  .
-  void $ mrCExpression e
+instance CReducible C.CFunctionDef where
+  reduce (C.CFunDef spc dec cdecls smt ni) = do
+    let (fn, ids) = cDeclaratorIdentifiers dec
+    let requirements = identifiers spc <> identifiers cdecls <> ids
+    case fn of
+      Just fn' ->
+        conditionalGivenThat requirements (Val.is fn')
+      Nothing ->
+        mapM_ (givenThat . Val.is) requirements
+    smt' <- reduce @C.CStatement smt
+    pure $ C.CFunDef spc dec cdecls smt' ni
 
-cCDeclarationSpecifier :: (MonadReduce Lab m) => C.CDeclarationSpecifier C.NodeInfo -> MaybeT m ()
-cCDeclarationSpecifier = \case
-  C.CTypeSpec t -> cCTypeSpecifier t
-  C.CStorageSpec _ -> pure ()
-  C.CTypeQual t -> cCTypeQualifier t
-  C.CFunSpec _ -> pure ()
-  C.CAlignSpec (C.CAlignAsType t _) -> cCDeclaration t
-  C.CAlignSpec (C.CAlignAsExpr t _) -> cCExpression t
+instance CReducible C.CDeclaration where
+  reduce = \case
+    C.CDecl spc@(C.CStorageSpec (C.CTypedef _) : rst) decl ni -> do
+      decl' <-
+        decl & collectNonEmpty' \case
+          C.CDeclarationItem d Nothing Nothing -> do
+            let (x, _) = cDeclaratorIdentifiers d
+            case x of
+              Just x' ->
+                splitOn
+                  (Val.is x')
+                  ( do
+                      modify (Map.insert x' (Type rst))
+                      mzero
+                  )
+                  (pure $ C.CDeclarationItem d Nothing Nothing)
+              Nothing ->
+                pure $ C.CDeclarationItem d Nothing Nothing
+          a -> error (show a)
+      pure (C.CDecl spc decl' ni)
+    C.CDecl spc decl ni -> do
+      decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers spc) decl
+      pure $ C.CDecl spc decl' ni
+    a -> error (show a)
+   where
+    reduceCDeclarationItem rq' = \case
+      C.CDeclarationItem d i e -> do
+        let (fn, reqs) = cDeclaratorIdentifiers d
+        case fn of
+          Just fn' ->
+            conditionalGivenThat (rq' <> reqs) (Val.is fn')
+          Nothing ->
+            mapM_ (givenThat . Val.is) (rq' <> reqs)
 
-cCTypeQualifier :: (MonadReduce Lab m) => C.CTypeQualifier C.NodeInfo -> MaybeT m ()
-cCTypeQualifier = \case
-  C.CAttrQual a -> cCAttr a
-  _ -> pure ()
+        i' <- optional do
+          liftMaybe i >>= reduce @C.CInitializer
+        e' <- optional do
+          liftMaybe e >>= reduce @C.CExpression
 
-cCTypeSpecifier :: (MonadReduce Lab m) => C.CTypeSpecifier C.NodeInfo -> MaybeT m ()
-cCTypeSpecifier = \case
-  C.CVoidType _ -> pure ()
-  C.CCharType _ -> pure ()
-  C.CShortType _ -> pure ()
-  C.CIntType _ -> pure ()
-  C.CLongType _ -> pure ()
-  C.CFloatType _ -> pure ()
-  C.CDoubleType _ -> pure ()
-  C.CSignedType _ -> pure ()
-  C.CUnsigType _ -> pure ()
-  C.CBoolType _ -> pure ()
-  C.CComplexType _ -> pure ()
-  C.CInt128Type _ -> pure ()
-  -- C.CUInt128Type a -> pure ()
-  C.CFloatNType{} -> pure ()
-  C.CTypeDef i _ -> do
-    givenThat (Val.is i)
-    pure ()
-  (C.CTypeOfExpr e _) -> cCExpression e
-  (C.CTypeOfType t _) -> cCDeclaration t
-  (C.CAtomicType t _) -> cCDeclaration t
-  a@(C.CSUType _ _) -> error (show a)
-  a@(C.CEnumType _ _) -> error (show a)
+        pure (C.CDeclarationItem d i' e')
+      a -> error (show a)
 
-cCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m ()
-cCInitializer = void . mrCInitializer
+instance CReducible C.CInitializer where
+  reduce = \case
+    C.CInitExpr e ni -> reduce @C.CExpression e <&> \e' -> C.CInitExpr e' ni
+    C.CInitList (C.CInitializerList items) ni -> do
+      collectNonEmpty' rmCInitializerListItem items <&> \items' ->
+        C.CInitList (C.CInitializerList items') ni
+   where
+    rmCInitializerListItem (pds, is) = do
+      pds' <- collect rmCPartDesignator pds
+      is' <- reduce is
+      pure (pds', is')
 
-mrCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m (C.CInitializer C.NodeInfo)
-mrCInitializer = \case
-  C.CInitExpr e ni -> mrCExpression e <&> \e' -> C.CInitExpr e' ni
-  C.CInitList (C.CInitializerList items) ni -> do
-    collectNonEmpty' rmCInitializerListItem items <&> \items' ->
-      C.CInitList (C.CInitializerList items') ni
- where
-  rmCInitializerListItem (pds, is) = do
-    pds' <- lift $ collect rmCPartDesignator pds
-    is' <- mrCInitializer is
-    pure (pds', is')
+    rmCPartDesignator = \case
+      a -> error (show a)
 
-  rmCPartDesignator :: (MonadReduce Lab m) => C.CPartDesignator C.NodeInfo -> m (C.CPartDesignator C.NodeInfo)
-  rmCPartDesignator = \case
+instance CReducible C.CStatement where
+  reduce = \case
+    C.CCompound is cbi ni -> do
+      cbi' <- collect (reduce @C.CCompoundBlockItem) cbi
+      pure $ C.CCompound is cbi' ni
+    C.CExpr e ni -> do
+      e' <- optional do
+        e' <- liftMaybe e
+        reduce @C.CExpression e'
+      pure $ C.CExpr e' ni
+    C.CIf e s els ni -> do
+      s' <- reduce s
+      e' <- optional do
+        reduce @C.CExpression e
+      els' <- optional do
+        els' <- liftMaybe els
+        given >> reduce els'
+      case (e', els') of
+        (Nothing, Nothing) -> pure s'
+        (Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
+        (Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
+        (Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
+    C.CFor e1 e2 e3 s ni -> do
+      reduce s <| do
+        e1' <- reduce @C.CForInit e1
+        e2' <- optional $ liftMaybe e2 >>= reduce @C.CExpression
+        e3' <- optional $ liftMaybe e3 >>= reduce @C.CExpression
+        s' <- reduce s
+        pure $ C.CFor e1' e2' e3' s' ni
+    C.CReturn e ni -> do
+      e' <- traverse (fmap orZero reduce) e
+      pure $ C.CReturn e' ni
+    C.CBreak ni -> pure (C.CBreak ni)
+    C.CCont ni -> pure (C.CCont ni)
+    C.CLabel i s [] ni -> do
+      -- todo fix attrs
+      s' <- reduce s
+      withFallback s' do
+        givenThat (Val.is i)
+        pure $ C.CLabel i s' [] ni
+    C.CGoto i ni ->
+      withFallback (C.CExpr Nothing ni) do
+        givenThat (Val.is i)
+        pure $ C.CGoto i ni
+    C.CWhile e s dow ni -> do
+      e' <- orZero (reduce @C.CExpression e)
+      s' <- reduce s
+      pure $ C.CWhile e' s' dow ni
     a -> error (show a)
 
-mrCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> MaybeT m (C.CFunctionDef C.NodeInfo)
-mrCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do
-  smt' <- lift $ rCStatement smt
-  mapM_ cCDeclaration cdecls
-  mapM_ cCDeclarationSpecifier spc
-  cCDeclr dec
-  pure $ C.CFunDef spc dec cdecls smt' ni
-
-cCDeclr :: (MonadReduce Lab m) => C.CDeclarator C.NodeInfo -> MaybeT m ()
-cCDeclr (C.CDeclr x dd _ _ _) = do
-  mapM_ cCDerivedDeclarator dd
-  givenWith (Val.is <$> x)
- where
-  cCDerivedDeclarator = \case
-    C.CPtrDeclr ts _ -> mapM_ cCTypeQualifier ts
-    C.CArrDeclr ts as _ -> do
-      mapM_ cCTypeQualifier ts
-      case as of
-        C.CNoArrSize _ -> pure ()
-        C.CArrSize _ e -> cCExpression e
-    C.CFunDeclr f attr _ -> do
-      mapM_ cCAttr attr
-      cCFunParams f
-  cCFunParams = \case
-    C.CFunParamsOld o -> mapM_ (givenThat . Val.is) o
-    C.CFunParamsNew o _ -> mapM_ cCDeclaration o
-
-cCAttr :: (MonadReduce Lab m) => C.CAttribute C.NodeInfo -> MaybeT m ()
-cCAttr (C.CAttr i e _) = do
-  mapM_ cCExpression e
-  givenThat (Val.is i)
-
-rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo)
-rCStatement = \case
-  C.CCompound is cbi ni -> do
-    cbi' <- collect mrCCompoundBlockItem cbi
-    pure $ C.CCompound is cbi' ni
-  C.CExpr e ni -> do
-    e' <- runMaybeT $ munder e mrCExpression
-    pure $ C.CExpr e' ni
-  C.CIf e s els ni -> do
-    e' <- runMaybeT $ mrCExpression e
-    s' <- rCStatement s
-    els' <- case els of
-      Just els' -> do
-        pure Nothing <| Just <$> rCStatement els'
-      Nothing -> pure Nothing
-    case (e', els') of
-      (Nothing, Nothing) -> pure s'
-      (Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
-      (Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
-      (Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
-  C.CFor e1 e2 e3 s ni -> do
-    rCStatement s <| do
-      e1' <- rCForInit e1
-      e2' <- runMaybeT $ munder e2 mrCExpression
-      e3' <- runMaybeT $ munder e3 mrCExpression
-      s' <- rCStatement s
-      pure $ C.CFor e1' e2' e3' s' ni
-  C.CReturn e ni -> do
-    e' <- case e of
-      Nothing -> pure Nothing
-      Just e' -> Just <$> zrCExpression e'
-    pure $ C.CReturn e' ni
-  C.CBreak ni -> pure (C.CBreak ni)
-  C.CCont ni -> pure (C.CCont ni)
-  C.CLabel i s [] ni ->
-    -- todo fix attrs
-    splitOn (Val.is i) (rCStatement s) do
-      s' <- rCStatement s
-      pure $ C.CLabel i s' [] ni
-  C.CGoto i ni ->
-    -- todo fix attrs
-    splitOn (Val.is i) (pure $ C.CExpr Nothing ni) do
-      pure $ C.CGoto i ni
-  C.CWhile e s dow ni -> do
-    e' <- zrCExpression e
-    s' <- rCStatement s
-    pure $ C.CWhile e' s' dow ni
-  a -> error (show a)
- where
-  rCForInit = \case
-    C.CForDecl decl -> do
-      m <- runMaybeT $ mrCDeclaration decl
-      pure $ case m of
-        Nothing -> C.CForInitializing Nothing
-        Just d' -> C.CForDecl d'
+instance CReducible C.CForInit where
+  reduce = \case
+    C.CForDecl decl -> withFallback (C.CForInitializing Nothing) do
+      C.CForDecl <$> reduce @C.CDeclaration decl
     C.CForInitializing n -> do
-      C.CForInitializing <$> runMaybeT (munder n mrCExpression)
+      C.CForInitializing <$> optional do
+        n' <- liftMaybe n
+        reduce @C.CExpression n'
 
-orZero :: Maybe (C.CExpression C.NodeInfo) -> C.CExpression C.NodeInfo
-orZero = fromMaybe zeroExp
+instance CReducible C.CExpression where
+  reduce = \case
+    C.CVar i ni -> do
+      givenThat (Val.is i)
+      pure $ C.CVar i ni
+    C.CCall e es ni -> do
+      e' <- reduce e
+      es' <- traverse (fmap orZero reduce) es
+      pure $ C.CCall e' es' ni
+    C.CCond ec et ef ni -> do
+      ec' <- reduce ec
+      ef' <- reduce ef
+      et' <- optional do
+        et' <- liftMaybe et
+        reduce et'
+      pure $ C.CCond ec' et' ef' ni
+    C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs ->
+      pure $ C.CBinary o lhs rhs ni
+    C.CUnary o elhs ni -> do
+      lhs <- reduce elhs
+      pure $ C.CUnary o lhs ni
+    C.CConst c -> do
+      -- TODO fix
+      pure $ C.CConst c
+    C.CCast cd e ni -> do
+      -- TODO fix
+      cd' <- reduce @C.CDeclaration cd
+      e' <- reduce e
+      pure $ C.CCast cd' e' ni
+    C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
+      pure $ C.CAssign op e1' e2' ni
+    C.CIndex e1 e2 ni -> do
+      e1' <- reduce e1
+      e2' <- orZero (reduce e2)
+      pure $ C.CIndex e1' e2' ni
+    C.CMember e i b ni -> do
+      givenThat (Val.is i)
+      e' <- reduce e
+      pure $ C.CMember e' i b ni
+    C.CComma items ni -> do
+      C.CComma <$> collectNonEmpty' reduce items <*> pure ni
+    e -> error (show e)
+   where
+    onBothExpr elhs erhs = onBoth (reduce elhs) (reduce erhs)
 
 zeroExp :: C.CExpression C.NodeInfo
 zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
 
-zrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> m (C.CExpression C.NodeInfo)
-zrCExpression e = orZero <$> runMaybeT (mrCExpression e)
+withFallback :: (Alternative m) => a -> m a -> m a
+withFallback a ma = ma <|> pure a
 
-mrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m (C.CExpression C.NodeInfo)
-mrCExpression = \case
-  C.CVar i ni -> do
-    givenThat (Val.is i)
-    pure $ C.CVar i ni
-  C.CCall e es ni -> do
-    e' <- mrCExpression e
-    es' <- lift $ traverse zrCExpression es
-    pure $ C.CCall e' es' ni
-  C.CCond ec et ef ni -> do
-    ec' <- mrCExpression ec
-    ef' <- mrCExpression ef
-    et' <- mtry $ munder et mrCExpression
-    pure $ C.CCond ec' et' ef' ni
-  C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs ->
-    pure $ C.CBinary o lhs rhs ni
-  C.CUnary o elhs ni -> do
-    lhs <- mrCExpression elhs
-    pure $ C.CUnary o lhs ni
-  C.CConst c -> do
-    -- TODO fix
-    pure $ C.CConst c
-  C.CCast cd e ni -> do
-    -- TODO fix
-    cd' <- mrCDeclaration cd
-    e' <- mrCExpression e
-    pure $ C.CCast cd' e' ni
-  C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
-    pure $ C.CAssign op e1' e2' ni
-  C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
-    pure $ C.CIndex e1' e2' ni
-  C.CMember e i b ni -> do
-    givenThat (Val.is i)
-    e' <- mrCExpression e
-    pure $ C.CMember e' i b ni
-  C.CComma items ni -> do
-    C.CComma <$> collectNonEmpty' mrCExpression items <*> pure ni
-  e -> error (show e)
- where
-  onBothExpr elhs erhs = onBoth (mrCExpression elhs) (mrCExpression erhs)
+orZero :: (Alternative m) => m (C.CExpression C.NodeInfo) -> m (C.CExpression C.NodeInfo)
+orZero = withFallback zeroExp
 
-mrCCompoundBlockItem
-  :: (MonadReduce Lab m)
-  => C.CCompoundBlockItem C.NodeInfo
-  -> MaybeT m (C.CCompoundBlockItem C.NodeInfo)
-mrCCompoundBlockItem = \case
-  C.CBlockStmt s -> empty <| lift (C.CBlockStmt <$> rCStatement s)
-  C.CBlockDecl d -> C.CBlockDecl <$> mrCDeclaration d
-  a -> error (show a)
+instance CReducible C.CCompoundBlockItem where
+  reduce = \case
+    C.CBlockStmt s ->
+      C.CBlockStmt <$> do
+        given >> reduce @C.CStatement s
+    C.CBlockDecl d ->
+      C.CBlockDecl <$> do
+        reduce @C.CDeclaration d
+    a -> error (show a)
 
 mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a)
 mtry (MaybeT mt) = MaybeT (Just <$> mt)
diff --git a/package.yaml b/package.yaml
index 084d3cec27da819839cf1cf76a27bd18add0a72f..8f266d55c204a2388d6b1b71dfd29e4fe0b48816 100644
--- a/package.yaml
+++ b/package.yaml
@@ -11,6 +11,7 @@ dependencies:
   - base >= 4.9 && < 5
   - transformers
   - free
+  - vector
   - data-fix
   - mtl
   - directory
diff --git a/rtree.cabal b/rtree.cabal
index 3e6c2e839d275d720fc2c0b400709570a01b71a2..af80d3de6fa72079820a31a4c8b3fc8499e35e95 100644
--- a/rtree.cabal
+++ b/rtree.cabal
@@ -28,6 +28,7 @@ library
     , pretty-simple
     , text
     , transformers
+    , vector
   default-language: Haskell2010
 
 executable rtree-c
@@ -56,6 +57,7 @@ executable rtree-c
     , time
     , transformers
     , typed-process
+    , vector
   default-language: Haskell2010
 
 test-suite rtree-test
@@ -77,4 +79,5 @@ test-suite rtree-test
     , rtree
     , text
     , transformers
+    , vector
   default-language: Haskell2010
diff --git a/src/Control/Monad/Reduce.hs b/src/Control/Monad/Reduce.hs
index 72bb47eb77b31272d3c95a3a2d5747aacc489ef2..9fec4e0ef0f1b1ae0d693649d1ad359108d97440 100644
--- a/src/Control/Monad/Reduce.hs
+++ b/src/Control/Monad/Reduce.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -25,9 +26,11 @@ module Control.Monad.Reduce (
   givenWith,
   check,
   checkThat,
+  conditionalGivenThat,
 
   -- * Combinators
   collect,
+  collectReverse,
   collectNonEmpty,
   collectNonEmpty',
 
@@ -39,8 +42,10 @@ module Control.Monad.Reduce (
   exponentialSearch,
 
   -- * Helpers
+  MonadReducePlus,
   onBoth,
   liftMaybe,
+  liftMaybeT,
 ) where
 
 import Control.Applicative
@@ -49,7 +54,9 @@ import Control.Monad.Trans.Maybe
 import qualified Data.List.NonEmpty as NE
 import Data.Maybe
 
+import Control.Monad.State
 import Data.Valuation (Truth (..))
+import qualified Data.Valuation as Val
 
 -- {- | A reducer should extract itself
 -- @
@@ -61,7 +68,7 @@ import Data.Valuation (Truth (..))
 
 -- | The Monad Reduce class.
 class (Monad m) => MonadReduce l m | m -> l where
-  {-# MINIMAL splitWith | checkWith #-}
+  {-# MINIMAL (splitWith | checkWith), bottom #-}
 
   -- | Split the world into the a reduced world (left) without an element and a world
   -- with that element (right). Optionally, labeled with l.
@@ -78,6 +85,10 @@ class (Monad m) => MonadReduce l m | m -> l where
   checkWith l = splitWith l (pure False) (pure True)
   {-# INLINE checkWith #-}
 
+  -- | An unrecoverable bottom, which claims that the predicate would always fail on this
+  -- input.
+  bottom :: m ()
+
 -- | Split with no label.
 split :: (MonadReduce l m) => m i -> m i -> m i
 split = splitWith Nothing
@@ -113,17 +124,17 @@ checkThat l = checkWith (Just l)
 {-# INLINE checkThat #-}
 
 -- | Continues if the fact is true.
-given :: (MonadReduce l m) => MaybeT m ()
+given :: (MonadReducePlus l m) => m ()
 given = givenWith Nothing
 {-# INLINE given #-}
 
 -- | Continues if the labeled fact is true.
-givenWith :: (MonadReduce l m, MonadPlus m) => Maybe (Truth l) -> m ()
+givenWith :: (MonadReducePlus l m) => Maybe (Truth l) -> m ()
 givenWith l = splitWith l mzero (pure ())
 {-# INLINE givenWith #-}
 
 -- | Continues if the labeled fact is true.
-givenThat :: (MonadReduce l m, MonadPlus m) => Truth l -> m ()
+givenThat :: (MonadReducePlus l m) => Truth l -> m ()
 givenThat l = givenWith (Just l)
 {-# INLINE givenThat #-}
 
@@ -132,25 +143,44 @@ collect :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> m [b]
 collect fn = fmap catMaybes . traverse (runMaybeT . fn)
 {-# INLINE collect #-}
 
+-- | Given a list of item try to remove each of them from the list, but from the other direction
+collectReverse :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> m [b]
+collectReverse fn = fmap (reverse . catMaybes) . traverse (runMaybeT . fn) . reverse
+{-# INLINE collectReverse #-}
+
 -- | Given a list of item try to remove each of them, but keep atleast one.
-collectNonEmpty' :: (MonadReduce l m, MonadPlus m) => (a -> MaybeT m b) -> [a] -> m [b]
+collectNonEmpty' :: (MonadReducePlus l m) => (a -> m b) -> [a] -> m [b]
 collectNonEmpty' fn as =
   NE.toList <$> collectNonEmpty fn as
 {-# INLINE collectNonEmpty' #-}
 
 -- | Given a list of item try to remove each of them, but keep atleast one.
-collectNonEmpty :: (MonadReduce l m, MonadPlus m) => (a -> MaybeT m b) -> [a] -> m (NE.NonEmpty b)
+collectNonEmpty :: (MonadReducePlus l m) => (a -> m b) -> [a] -> m (NE.NonEmpty b)
 collectNonEmpty fn as = do
-  as' <- fmap catMaybes . traverse (runMaybeT . fn) $ as
+  as' <- fmap catMaybes . traverse (optional . fn) $ as
   maybe mzero pure $ NE.nonEmpty as'
 {-# INLINE collectNonEmpty #-}
 
+conditionalGivenThat :: (MonadReducePlus l m) => [l] -> Truth l -> m ()
+conditionalGivenThat [] t = givenThat t
+conditionalGivenThat (a : as) t = do
+  splitOn
+    (Val.is a)
+    (splitOn (Val.not t) bottom mzero)
+    (conditionalGivenThat as t)
+
+type MonadReducePlus l m = (MonadReduce l m, MonadPlus m)
+
 instance (MonadReduce l m) => MonadReduce l (MaybeT m) where
+  bottom = MaybeT{runMaybeT = Just <$> bottom}
   splitWith m (MaybeT lhs) (MaybeT rhs) = MaybeT (splitWith m lhs rhs)
 
 -- | Helper that lifts a maybe into MonadPlus (or MaybeT)
-liftMaybe :: (MonadPlus m) => Maybe a -> m a
-liftMaybe = maybe mzero pure
+liftMaybe :: (Alternative m) => Maybe a -> m a
+liftMaybe = maybe empty pure
+
+liftMaybeT :: (MonadPlus m) => MaybeT m e -> m e
+liftMaybeT m = runMaybeT m >>= liftMaybe
 
 -- | Returns either of the maybes or combines them if both have values.
 onBoth :: (MonadPlus m) => m a -> m a -> (a -> a -> m a) -> m a
diff --git a/src/Control/RTree.hs b/src/Control/RTree.hs
index 506ecccd40cf5a8c0d365b7147ea34af45c24a38..32caea37143b4e589412166150be0c22db13bdf3 100644
--- a/src/Control/RTree.hs
+++ b/src/Control/RTree.hs
@@ -19,6 +19,7 @@ module Control.RTree (
   RTree (..),
   extract,
   reduce,
+  reduceMaybe,
   -- # IRTree
   IRTree,
   iextract,
@@ -38,23 +39,30 @@ import Control.Monad.Reader
 import Control.Monad.State.Strict
 import Data.Functor.Identity
 
+import qualified Data.Vector as V
+
 import Control.Monad.Reduce
+import Control.Monad.Trans.Maybe
+import Data.Bits
+import Data.Maybe
 import qualified Data.Valuation as Val
 
 type Valuation = Val.Valuation
 type Truth = Val.Truth
 
 data RTree l i
-  = SplitWith (Maybe (Truth l)) (RTree l i) !(RTree l i)
+  = Bottom
   | Done i
+  | SplitWith (Maybe (Truth l)) (RTree l i) !(RTree l i)
   deriving (Functor)
 
-extract :: (Ord l) => Valuation l -> RTree l i -> i
+extract :: (Ord l) => Valuation l -> RTree l i -> Maybe i
 extract v = \case
+  Bottom -> Nothing
   SplitWith ml lhs rhs -> case ml >>= Val.condition v of
     Just v' -> extract v' rhs
     _ -> extract v lhs
-  Done i -> i
+  Done i -> Just i
 
 instance Applicative (RTree l) where
   pure = Done
@@ -62,23 +70,29 @@ instance Applicative (RTree l) where
 
 instance Monad (RTree l) where
   ma >>= f = case ma of
+    Bottom -> Bottom
     Done i -> f i
     SplitWith ml lhs rhs -> SplitWith ml (lhs >>= f) (rhs >>= f)
 
 instance MonadReduce l (RTree l) where
   splitWith = SplitWith
+  bottom = Bottom
 
 reduce
   :: forall m l i
    . (Alternative m, Ord l)
-  => (i -> m ())
+  => (Valuation l -> i -> m ())
   -> Valuation l
   -> RTree l i
   -> m i
 reduce p = checkgo
  where
-  checkgo v r = p (extract v r) *> go v r
+  checkgo v r =
+    case extract v r of
+      Nothing -> empty
+      Just e -> p v e *> go v r
   go v = \case
+    Bottom -> empty
     Done i -> pure i
     SplitWith (Just l) lhs rhs -> case Val.truthValue v (Val.label l) of
       Just t
@@ -88,48 +102,70 @@ reduce p = checkgo
     SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
 {-# INLINE reduce #-}
 
+reduceMaybe
+  :: forall m l i
+   . (Monad m, Ord l)
+  => (Valuation l -> i -> m Bool)
+  -> Valuation l
+  -> RTree l i
+  -> m (Maybe i)
+reduceMaybe p v rt =
+  runMaybeT
+    $ reduce
+      ( \v' i -> do
+          t <- lift (p v' i)
+          unless t empty
+      )
+      v
+      rt
+
 data ReState l = ReState
-  { choices :: [Bool]
+  { choices :: V.Vector Bool
+  , progress :: Int
   , valuation :: !(Valuation l)
   }
 
 type IRTree l = IRTreeT l Identity
 
-newtype IRTreeT l m i = IRTreeT {runIRTreeT :: StateT (ReState l) m i}
-  deriving (Functor, Applicative, Monad) via (StateT (ReState l) m)
-  deriving (MonadTrans) via (StateT (ReState l))
+newtype IRTreeT l m i = IRTreeT {runIRTreeT :: MaybeT (StateT (ReState l) m) i}
+  deriving (Functor, Applicative, Alternative, Monad, MonadPlus) via (MaybeT (StateT (ReState l) m))
+
+instance MonadTrans (IRTreeT l) where
+  lift m = IRTreeT (lift (lift m))
+
+instance (MonadState s m) => MonadState s (IRTreeT l m) where
+  state s = lift (state s)
 
 instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
+  bottom = mzero
   checkWith =
-    IRTreeT . StateT . \case
+    IRTreeT . MaybeT . StateT . \case
       Nothing -> \case
-        ReState (uncons -> (a, as)) v ->
-          pure (a, ReState as v)
+        ReState ch i v ->
+          pure (Just (fromMaybe True (ch V.!? i)), ReState ch (i + 1) v)
       Just l -> \case
-        ReState as v@((`Val.truthValue` Val.label l) -> Just x) ->
-          pure (x, ReState as v)
-        ReState (uncons -> (a, as)) v ->
-          pure (a, ReState as (Val.withTruth v (if a then l else Val.not l)))
-   where
-    uncons [] = (True, [])
-    uncons (a : as) = (a, as)
+        ReState ch i v@((`Val.truthValue` Val.label l) -> Just t) ->
+          pure (Just (t == Val.truth l), ReState ch i v)
+        ReState ch i v ->
+          let a = fromMaybe True (ch V.!? i)
+           in pure (Just a, ReState ch (i + 1) (Val.withTruth v (if a then l else Val.not l)))
   {-# INLINE checkWith #-}
 
-iextract :: (Ord l) => Valuation l -> IRTree l a -> a
+iextract :: (Ord l) => Valuation l -> IRTree l a -> Maybe a
 iextract v t = runIdentity $ iextractT v t
 {-# INLINE iextract #-}
 
-iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m i
-iextractT v (IRTreeT m) = evalStateT m (ReState [] v)
+iextractT :: (Ord l, Monad m) => Valuation l -> IRTreeT l m i -> m (Maybe i)
+iextractT v (IRTreeT m) = evalStateT (runMaybeT m) (ReState V.empty 0 v)
 {-# INLINE iextractT #-}
 
 ireduce
   :: forall m l i
    . (Monad m, Ord l)
-  => (Valuation l -> i -> m Bool)
+  => (ReState l -> Maybe i -> m Bool)
   -> Valuation l
   -> IRTree l i
-  -> m i
+  -> m (Maybe i)
 ireduce = ireduceT (pure . runIdentity)
 {-# INLINE ireduce #-}
 
@@ -139,28 +175,33 @@ ireduceT
    . (Monad m, Monad t, Ord l)
   => (forall a. m a -> t a)
   -- ^ a lift of monad m into t (normally @id@ or @lift@)
-  -> (Valuation l -> i -> t Bool)
+  -> (ReState l -> Maybe i -> t Bool)
   -> Valuation l
   -> IRTreeT l m i
-  -> t i
-ireduceT lift_ p v (IRTreeT m) = go []
+  -> t (Maybe i)
+ireduceT lift_ p v (IRTreeT m) = go V.empty
  where
-  go pth =
-    lift_ (runStateT m (ReState pth v)) >>= \case
-      (i, ReState [] v') -> do
-        t <- p v' i
+  go pth = do
+    -- Try to run the false branch.
+    let pth' = pth <> V.singleton False
+    result <- lift_ (runStateT (runMaybeT m) (ReState pth' 0 v))
+    case result of
+      (mi, ReState _ i v') | i >= V.length pth' -> do
+        t <- p (ReState pth' i v') mi
         -- if the predicate is true, we can reduce to the false branch.
-        go (pth <> [not t])
-      (i, _) -> pure i
+        go (pth <> V.singleton (not t))
+
+      -- if we no more choices are needed, stop.
+      (mi, _) -> pure mi
 {-# INLINE ireduceT #-}
 
 ireduceExp
   :: forall m l i
    . (Monad m, Ord l)
-  => (Valuation l -> i -> m Bool)
+  => (ReState l -> Maybe i -> m Bool)
   -> Valuation l
   -> IRTree l i
-  -> m i
+  -> m (Maybe i)
 ireduceExp = ireduceExpT (pure . runIdentity)
 {-# INLINE ireduceExp #-}
 
@@ -170,28 +211,23 @@ ireduceExpT
    . (Monad m, Monad t, Ord l)
   => (forall a. m a -> t a)
   -- ^ a lift of monad m into t (normally @id@ or @lift@)
-  -> (Valuation l -> i -> t Bool)
+  -> (ReState l -> Maybe i -> t Bool)
   -> Valuation l
   -> IRTreeT l m i
-  -> t i
-ireduceExpT lift_ p v (IRTreeT (StateT m)) = go 0 []
+  -> t (Maybe i)
+ireduceExpT lift_ p v (IRTreeT m) = go 0 V.empty
  where
   -- here n is the number of explorative elements
-  go n pth =
-    lift_ (m $ ReState pth v) >>= \case
-      (i, ReState [] v') -> do
-        p v' i >>= \case
-          True -> do
-            let n' = next n
-            go n' (pth <> replicate n' False)
-          False -> do
-            case n of
-              0 -> go 0 (pth <> [True])
-              n' -> go n' $ take (length pth - prev n') pth
-      (i, _) -> pure i
-
-  next 0 = 1
-  next n = n * 2
-
-  prev 1 = 0
-  prev n = n `quot` 2
+  go n pth = do
+    let depth = shiftL 1 n
+    let pth' = pth <> V.replicate depth False
+    result <- lift_ (runStateT (runMaybeT m) $ ReState pth' 0 v)
+    case result of
+      (mi, ReState _ i v') | i >= length pth' - depth + 1 -> do
+        t <- p (ReState pth' i v') mi
+        if t
+          then go (n + 1) pth'
+          else case n of
+            0 -> go 0 (pth <> V.singleton True)
+            n' -> go (n' - 1) pth
+      (mi, _) -> pure mi
diff --git a/test/data/.gitignore b/test/data/.gitignore
index 74345629919684fb947bcfb72f363716baa1d1c1..b86ba2e4d0922a2d3345241809e3e2e5d05a4a18 100644
--- a/test/data/.gitignore
+++ b/test/data/.gitignore
@@ -1 +1,2 @@
 file2.c
+*.bak
diff --git a/test/data/typedef.c b/test/data/typedef.c
new file mode 100644
index 0000000000000000000000000000000000000000..98d10336a42d3a501d4f3033515aeeee61a2f655
--- /dev/null
+++ b/test/data/typedef.c
@@ -0,0 +1,6 @@
+typedef const int size_t;
+void main()
+{
+    size_t a = 0;
+    return 0;
+}
\ No newline at end of file