diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# Revision history for expressions-z3
+
+## 0.1.0
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2017, Jakub Daniel
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Jakub Daniel nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/expressions-z3.cabal b/expressions-z3.cabal
new file mode 100644
--- /dev/null
+++ b/expressions-z3.cabal
@@ -0,0 +1,73 @@
+name:                expressions-z3
+version:             0.1.0
+synopsis:            Encode and Decode expressions from Z3 ASTs
+description:
+  A simple interface for converting expressions back and forth between pure
+  representation and an AST within a Z3 context.
+  .
+  Assume
+  .
+  > λ> :m + Control.Monad Data.Expression Data.Expression.Z3 Z3.Monad Data.Singletons
+  > λ> :t f
+  > f :: MonadZ3 z3 => AST -> z3 AST
+  .
+  Then
+  .
+  > λ> let g :: ( MonadZ3 z3, IFromZ3 f, IToZ3 f, SingI s ) => IFix f s -> z3 (IFix f s); g = fromZ3 <=< f <=< toZ3
+  > λ> :t g (var "a" :: Lia 'BooleanSort)
+  > g (var "a" :: Lia 'BooleanSort) :: MonadZ3 z3 => z3 (Lia 'BooleanSort)
+  .
+  For example
+  .
+  > λ> let f b = mkStringSymbol "a" >>= mkIntVar >>= toApp >>= \a' -> mkForallConst [] [a'] b
+  > λ> let g :: ( MonadZ3 z3, IFromZ3 f, IToZ3 f ) => IFix f 'BooleanSort -> z3 (IFix f 'BooleanSort); g = fromZ3 <=< g <=< toZ3
+  > λ> evalZ3 $ g (var "a" .+. cnst 1 .=. var "b" :: Lia 'BooleanSort)
+  > (forall ((a : int)) (= (+ 1 (a : int)) (b : int)))
+  .
+  Or more interestingly
+  .
+  > λ> :{
+  > |  let f :: ( MonadZ3 z3, IFromZ3 f, IToZ3 f, SingI s ) => IFix f s -> z3 (IFix f s)
+  > |      f a = do
+  > |      a' <- toZ3 a
+  > |      r <- getModel
+  > |      case r of
+  > |          (Sat, Just m) -> do
+  > |              v <- modelEval m a' True
+  > |              case v of
+  > |                Just v' -> fromZ3 v'
+  > |                _ -> error "..."
+  > |          _ -> error "..."
+  > :}
+  > λ> evalZ3 $ f (var "a" :: Lia 'BooleanSort)
+  > false
+  > λ> evalZ3 $ f (var "a" :: Lia 'IntegralSort)
+  > 0
+  > λ> evalZ3 $ f (var "a" .+. cnst 1:: Lia 'IntegralSort)
+  > 1
+
+license:             BSD3
+license-file:        LICENSE
+author:              Jakub Daniel
+maintainer:          jakub.daniel@protonmail.com
+copyright:           Copyright (C) 2017 Jakub Daniel
+category:            Data, Logic, Math
+build-type:          Simple
+extra-source-files:  ChangeLog.md
+cabal-version:       >=1.10
+
+source-repository head
+  type:     git
+  location: https://github.com/jakubdaniel/expressions-z3.git
+
+library
+  exposed-modules:     Data.Expression.Z3
+  build-depends:       base >=4.9 && <4.11,
+                       containers >=0.5 && <0.5.11,
+                       expressions >=0.1 && <0.2,
+                       singletons >=2.2 && <2.4,
+                       transformers >=0.5.2 && <0.5.5,
+                       z3 >=4.1.2 && <4.2
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall
diff --git a/src/Data/Expression/Z3.hs b/src/Data/Expression/Z3.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Expression/Z3.hs
@@ -0,0 +1,368 @@
+{-# LANGUAGE DataKinds
+           , FlexibleContexts
+           , FlexibleInstances
+           , GADTs
+           , GeneralizedNewtypeDeriving
+           , KindSignatures
+           , MultiParamTypeClasses
+           , RankNTypes
+           , ScopedTypeVariables
+           , TypeOperators
+           , UndecidableInstances #-}
+
+module Data.Expression.Z3 ( IToZ3, toZ3, IFromZ3, fromZ3 ) where
+
+import Control.Applicative hiding (Const)
+import Control.Monad
+import Control.Monad.IO.Class
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.List
+import Control.Monad.Trans.State
+import Data.Expression
+import Data.List hiding (and, or)
+import Data.Maybe
+import Data.Proxy
+import Data.Singletons
+import Data.Singletons.Decide
+import Prelude hiding (and, or, not)
+
+import qualified Data.Functor.Const as F
+import qualified Data.Map as M
+import qualified Z3.Monad as Z3
+
+type Cache g = M.Map Z3.AST (DynamicallySorted g)
+
+newtype Decoder g a b = Decoder { unwrap :: StateT (Cache g) (ListT a) b } deriving ( Functor, Applicative, Alternative, Monad, MonadIO )
+
+instance Z3.MonadZ3 z3 => Z3.MonadZ3 (Decoder f z3) where
+    getSolver  = Decoder . lift . lift $ Z3.getSolver
+    getContext = Decoder . lift . lift $ Z3.getContext
+
+class IFunctor f => IToZ3 f where
+    itoZ3 :: forall (s :: Sort) z3. Z3.MonadZ3 z3 => f (F.Const (z3 Z3.AST)) s -> F.Const (z3 Z3.AST) s
+
+sortToZ3 :: forall (s :: Sort) z3. Z3.MonadZ3 z3 => Sing s -> z3 Z3.Sort
+sortToZ3  SBooleanSort    = Z3.mkBoolSort
+sortToZ3  SIntegralSort   = Z3.mkIntSort
+sortToZ3 (SArraySort i e) = do
+    z3i <- sortToZ3 i
+    z3e <- sortToZ3 e
+    Z3.mkArraySort z3i z3e
+
+instance IToZ3 VarF where
+    itoZ3 (Var n s) = F.Const $ do
+        z3n <- Z3.mkStringSymbol n
+        z3s <- sortToZ3 s
+        Z3.mkVar z3n z3s
+
+instance IToZ3 ConjunctionF where
+    itoZ3 (And as) = F.Const $ Z3.mkAnd =<< mapM F.getConst as
+
+instance IToZ3 DisjunctionF where
+    itoZ3 (Or os) = F.Const $ Z3.mkOr =<< mapM F.getConst os
+
+instance IToZ3 NegationF where
+    itoZ3 (Not n) = F.Const $ Z3.mkNot =<< F.getConst n
+
+instance IToZ3 (UniversalF v) where
+    itoZ3 (Forall vs a) = F.Const $ do
+        z3vs <- mapM (Z3.toApp <=< toZ3) vs
+        Z3.mkForallConst [] z3vs =<< F.getConst a
+
+instance IToZ3 (ExistentialF v) where
+    itoZ3 (Exists vs a) = F.Const $ do
+        z3vs <- mapM (Z3.toApp <=< toZ3) vs
+        Z3.mkExistsConst [] z3vs =<< F.getConst a
+
+instance IToZ3 EqualityF where
+    itoZ3 (Equals _ a b) = F.Const . join $ liftM2 Z3.mkEq (F.getConst a) (F.getConst b)
+
+instance IToZ3 ArithmeticF where
+    itoZ3 (Const c)      = F.Const $ Z3.mkInt c =<< Z3.mkIntSort
+    itoZ3 (Add as)       = F.Const $ Z3.mkAdd =<< mapM F.getConst as
+    itoZ3 (Mul ms)       = F.Const $ Z3.mkMul =<< mapM F.getConst ms
+    itoZ3 (Divides c a)  = F.Const $ do
+        z3c <- Z3.mkInt c =<< Z3.mkIntSort
+        z30 <- Z3.mkInt 0 =<< Z3.mkIntSort
+        z3a <- F.getConst a
+        Z3.mkEq z30 =<< Z3.mkMod z3a z3c
+    itoZ3 (LessThan a b) = F.Const . join $ liftM2 Z3.mkLt (F.getConst a) (F.getConst b)
+
+instance IToZ3 IfThenElseF where
+    itoZ3 (IfThenElse _ i t e) = F.Const . join $ liftM3 Z3.mkIte (F.getConst i) (F.getConst t) (F.getConst e)
+
+instance IToZ3 ArrayF where
+    itoZ3 (Select _ _ a i)   = F.Const . join $ liftM2 Z3.mkSelect (F.getConst a) (F.getConst i)
+    itoZ3 (Store  _ _ a i v) = F.Const . join $ liftM3 Z3.mkStore  (F.getConst a) (F.getConst i) (F.getConst v)
+
+instance ( IToZ3 f, IToZ3 g ) => IToZ3 (f :+: g) where
+    itoZ3 (InL a) = itoZ3 a
+    itoZ3 (InR b) = itoZ3 b
+
+toZ3 :: forall f (s :: Sort) z3. ( IToZ3 f, Z3.MonadZ3 z3 ) => IFix f s -> z3 Z3.AST
+toZ3 = F.getConst . icata itoZ3
+
+class IFromZ3Into (f :: (Sort -> *) -> Sort -> *) (g :: (Sort -> *) -> Sort -> *) where
+    ifromZ3App        :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> String -> Z3.App           -> Decoder g z3 (DynamicallySorted g)
+    ifromZ3Quantifier :: Z3.MonadZ3 z3 => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> Bool -> [Z3.AST] -> Z3.AST -> Decoder g z3 (DynamicallySorted g)
+    ifromZ3Numeral    :: Z3.MonadZ3 z3 => Proxy f ->                                                   Int                        -> Decoder g z3 (DynamicallySorted g)
+
+    ifromZ3App        _ _ _ _   = empty
+    ifromZ3Quantifier _ _ _ _ _ = empty
+    ifromZ3Numeral    _ _       = empty
+
+class IFromZ3Into f f => IFromZ3 f
+
+sortFromZ3 :: Z3.MonadZ3 z3 => Z3.Sort -> z3 DynamicSort
+sortFromZ3 s = do
+    k <- Z3.getSortKind s
+    case k of
+        Z3.Z3_BOOL_SORT  -> return (DynamicSort SBooleanSort)
+        Z3.Z3_INT_SORT   -> return (DynamicSort SIntegralSort)
+        Z3.Z3_ARRAY_SORT -> do
+            DynamicSort i <- sortFromZ3 =<< Z3.getArraySortDomain s
+            DynamicSort e <- sortFromZ3 =<< Z3.getArraySortRange s
+            return (DynamicSort $ SArraySort i e)
+        _ -> error "unrecognized sort"
+
+instance IFromZ3 VarF
+instance VarF :<: g => IFromZ3Into VarF g where
+    ifromZ3App _ _ name app = do
+        guard . null =<< Z3.getAppArgs app
+        DynamicSort s <- sortFromZ3 =<< Z3.getSort =<< Z3.appToAst app
+        return $ DynamicallySorted s (inject (Var name s))
+
+instance IFromZ3 ConjunctionF
+instance ConjunctionF :<: g => IFromZ3Into ConjunctionF g where
+    ifromZ3App _ _ "true" app = do
+        guard . null =<< Z3.getAppArgs app
+        return . DynamicallySorted SBooleanSort $ true
+    ifromZ3App _ r "and" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just as -> return . DynamicallySorted SBooleanSort $ and as
+            _ -> empty
+    ifromZ3App _ _ _ _ = empty
+
+instance IFromZ3 DisjunctionF
+instance DisjunctionF :<: g => IFromZ3Into DisjunctionF g where
+    ifromZ3App _ _ "false" app = do
+        guard . null =<< Z3.getAppArgs app
+        return . DynamicallySorted SBooleanSort $ false
+    ifromZ3App _ r "or" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just os -> return . DynamicallySorted SBooleanSort $ or os
+            _ -> empty
+    ifromZ3App _ _ _ _ = empty
+
+instance IFromZ3 NegationF
+instance NegationF :<: g => IFromZ3Into NegationF g where
+    ifromZ3App _ r "not" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        guard (length args == 1)
+        case toStaticallySorted (head args) of
+            Just n -> return . DynamicallySorted SBooleanSort $ not n
+            _ -> empty
+    ifromZ3App _ _ _ _ = empty
+
+varFromZ3 :: Z3.MonadZ3 z3 => Z3.AST -> Decoder VarF z3 (DynamicallySorted VarF)
+varFromZ3 = ifromZ3 (Proxy :: Proxy (VarF :: (Sort -> *) -> Sort -> *)) varFromZ3
+
+local :: Z3.MonadZ3 z3 => Decoder VarF z3 a -> Decoder g z3 a
+local = Decoder . lift . flip evalStateT M.empty . unwrap
+
+instance SingI v => IFromZ3 (UniversalF v)
+instance ( UniversalF v :<: g, SingI v ) => IFromZ3Into (UniversalF v) g where
+    ifromZ3Quantifier _ r True as f = do
+        vs <- mapM (local . varFromZ3) as
+        let (vvs, rest) = partition (isVSorted . fst) $ zip vs as
+
+        if null vvs then empty else do
+            let (vs', bound) = unzip vvs
+
+            vs'' <- mapM (Z3.toApp . snd) rest
+            a'   <- if null vs'' then return f else Z3.mkForallConst [] vs'' f
+            b    <- r =<< Z3.substituteVars a' bound
+
+            case toStaticallySorted b of
+                Just b'' -> return . DynamicallySorted SBooleanSort $ forall (fromJust . mapM toStaticallySorted $ vs' :: [IFix VarF v]) b''
+                _ -> empty
+        where
+
+            isVSorted :: DynamicallySorted VarF -> Bool
+            isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )
+
+    ifromZ3Quantifier _ _ _ _ _ = empty
+
+instance SingI v => IFromZ3 (ExistentialF v)
+instance ( ExistentialF v :<: g, SingI v ) => IFromZ3Into (ExistentialF v) g where
+    ifromZ3Quantifier _ r False as f = do
+        vs <- mapM (local . varFromZ3) as
+        let (vvs, rest) = partition (isVSorted . fst) $ zip vs as
+
+        if null vvs then empty else do
+            let (vs', bound) = unzip vvs
+
+            vs'' <- mapM (Z3.toApp . snd) rest
+            a'   <- if null vs'' then return f else Z3.mkExistsConst [] vs'' f
+            b    <- r =<< Z3.substituteVars a' bound
+
+            case toStaticallySorted b of
+                Just b'' -> return . DynamicallySorted SBooleanSort $ exists (fromJust . mapM toStaticallySorted $ vs' :: [IFix VarF v]) b''
+                _ -> empty
+        where
+
+            isVSorted :: DynamicallySorted VarF -> Bool
+            isVSorted = isJust . ( toStaticallySorted :: DynamicallySorted VarF -> Maybe (IFix VarF v) )
+
+    ifromZ3Quantifier _ _ _ _ _ = empty
+
+instance IFromZ3 EqualityF
+instance EqualityF :<: g => IFromZ3Into EqualityF g where
+    ifromZ3App _ r name app = case name of
+        "="   -> ifromZ3'' =<< mapM r =<< Z3.getAppArgs app
+        "iff" -> ifromZ3'' =<< mapM r =<< Z3.getAppArgs app
+        _ -> empty
+
+        where
+
+            ifromZ3'' :: Z3.MonadZ3 z3 => [DynamicallySorted g] -> Decoder g z3 (DynamicallySorted g)
+            ifromZ3'' [DynamicallySorted s1 a, DynamicallySorted s2 b] = case s1 %~ s2 of
+                Proved Refl -> return . DynamicallySorted SBooleanSort $ inject (Equals s1 a b)
+                Disproved _ -> empty
+            ifromZ3'' _ = empty
+
+instance IFromZ3 ArithmeticF
+instance ArithmeticF :<: g => IFromZ3Into ArithmeticF g where
+    ifromZ3Numeral _ c = return . DynamicallySorted SIntegralSort $ cnst c
+    ifromZ3App _ r "+" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just as -> return . DynamicallySorted SIntegralSort $ add as
+            _ -> empty
+    ifromZ3App _ r "*" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just ms -> return . DynamicallySorted SIntegralSort $ mul ms
+            _ -> empty
+    ifromZ3App _ r "<" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just [k, l] -> return . DynamicallySorted SBooleanSort $ k .<. l
+            _ -> empty
+    ifromZ3App _ r ">" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just [k, l] -> return . DynamicallySorted SBooleanSort $ l .<. k
+            _ -> empty
+    ifromZ3App _ r "<=" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just [k, l] -> return . DynamicallySorted SBooleanSort $ k .<. l .+. cnst 1
+            _ -> empty
+    ifromZ3App _ r ">=" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case mapM toStaticallySorted args of
+            Just [k, l] -> return . DynamicallySorted SBooleanSort $ l .<. k .+. cnst 1
+            _ -> empty
+    ifromZ3App _ r "=" app = do
+        args <- Z3.getAppArgs app
+        case args of
+            [m, n] -> modulo m n <|> modulo n m
+            _ -> empty
+
+        where
+
+            modulo k l = do
+                ka <- Z3.getAstKind k
+                kb <- Z3.getAstKind l
+                case (ka, kb) of
+                    (Z3.Z3_NUMERAL_AST, Z3.Z3_APP_AST) -> do
+                        z    <- Z3.getInt k
+                        app'  <- Z3.toApp l
+                        name <- Z3.getSymbolString =<< Z3.getDeclName =<< Z3.getAppDecl app'
+                        case (z, name) of
+                            (0, "mod") -> do
+                                args <- Z3.getAppArgs app'
+                                case args of
+                                    [n, c] -> do
+                                        kc <- Z3.getAstKind c
+                                        case kc of
+                                            Z3.Z3_NUMERAL_AST -> do
+                                                c' <- fromIntegral <$> Z3.getInt c
+                                                n' <- r n
+                                                case toStaticallySorted n' of
+                                                    Just n'' -> return . DynamicallySorted SBooleanSort $ c' .\. n''
+                                                    _ -> empty
+                                            _ -> empty
+                                    _ -> empty
+                            _ -> empty
+                    _ -> empty
+    ifromZ3App _ _ _ _ = empty
+
+instance IFromZ3 IfThenElseF
+instance IfThenElseF :<: g => IFromZ3Into IfThenElseF g where
+    ifromZ3App _ r "if" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case args of
+            [DynamicallySorted SBooleanSort i, DynamicallySorted ts t, DynamicallySorted es e] -> case ts %~ es of
+                Proved Refl -> return . DynamicallySorted ts $ inject (IfThenElse ts i t e)
+                Disproved _ -> empty
+            _ -> empty
+    ifromZ3App _ _ _ _ = empty
+
+instance IFromZ3 ArrayF
+instance ArrayF :<: g => IFromZ3Into ArrayF g where
+    ifromZ3App _ r "select" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case args of
+            [DynamicallySorted (SArraySort is1 es) a, DynamicallySorted is2 i] -> case is1 %~ is2 of
+                Proved Refl -> return . DynamicallySorted es $ inject (Select is1 es a i)
+                Disproved _ -> empty
+            _ -> empty
+    ifromZ3App _ r "store" app = do
+        args <- mapM r =<< Z3.getAppArgs app
+        case args of
+            [DynamicallySorted as@(SArraySort _ _) a, DynamicallySorted is i, DynamicallySorted es v] -> case as %~ SArraySort is es of
+                Proved Refl -> return . DynamicallySorted as $ inject (Store is es a i v)
+                Disproved _ -> empty
+            _ -> empty
+    ifromZ3App _ _ _ _ = empty
+
+instance ( IFromZ3Into f (f :+: g), IFromZ3Into g (f :+: g) ) => IFromZ3 (f :+: g)
+instance ( IFromZ3Into f h, IFromZ3Into g h ) => IFromZ3Into (f :+: g) h where
+    ifromZ3App        _ r name app = ifromZ3App (Proxy :: Proxy f) r name app <|> ifromZ3App (Proxy :: Proxy g) r name app
+    ifromZ3Quantifier _ r q vs b   = ifromZ3Quantifier (Proxy :: Proxy f) r q vs b <|> ifromZ3Quantifier (Proxy :: Proxy g) r q vs b
+    ifromZ3Numeral    _ c          = ifromZ3Numeral (Proxy :: Proxy f) c <|> ifromZ3Numeral (Proxy :: Proxy g) c
+
+ifromZ3 :: forall (f :: (Sort -> *) -> Sort -> *)
+                  (g :: (Sort -> *) -> Sort -> *)
+                  z3.
+           ( IFromZ3Into f g, Z3.MonadZ3 z3 )
+         => Proxy f -> (Z3.AST -> Decoder g z3 (DynamicallySorted g)) -> Z3.AST -> Decoder g z3 (DynamicallySorted g)
+ifromZ3 p r a = do
+    c <- Decoder $ get
+    if a `M.member` c then do
+        return (c M.! a)
+    else do
+        k <- Z3.getAstKind a
+        e <- case k of
+            Z3.Z3_NUMERAL_AST -> ifromZ3Numeral p . fromIntegral =<< Z3.getInt a
+            Z3.Z3_APP_AST -> do
+                app <- Z3.toApp a
+                name <- Z3.getSymbolString =<< Z3.getDeclName =<< Z3.getAppDecl app
+                ifromZ3App p r name app
+            Z3.Z3_QUANTIFIER_AST -> do
+                t  <- Z3.isQuantifierForall a
+                vs <- Z3.getQuantifierBoundVars a
+                b  <- Z3.getQuantifierBody a
+                ifromZ3Quantifier p r t vs b
+            _ -> empty
+        Decoder $ modify (M.insert a e)
+        return e
+
+fromZ3 :: forall (f :: (Sort -> *) -> Sort -> *) (s :: Sort) z3. ( IFromZ3 f, Z3.MonadZ3 z3, SingI s ) => Z3.AST -> z3 (IFix f s)
+fromZ3 a = let r = ifromZ3 (Proxy :: Proxy f) r in head' <=< fmap (mapMaybe toStaticallySorted) . runListT . flip evalStateT M.empty . unwrap . r $ a where
+    head' (h : _) = return h
+    head' _       = Z3.astToString a >>= \s -> error ("couldn't re-encode Z3 AST: " ++ s)