diff --git a/src/Z3/Assertion.hs b/src/Z3/Assertion.hs
deleted file mode 100644
--- a/src/Z3/Assertion.hs
+++ /dev/null
@@ -1,63 +0,0 @@
--- |
--- Assertions provided by libraries *for convenience*
--- It is not hard-coded into Z3.Logic.Pred
---
-
-module Z3.Assertion (Assertion(..)) where
-
-import Z3.Class
-import Z3.Encoding()
-import Z3.Monad
-
-import qualified Data.Map as M
-import qualified Data.Set as S
-
-data Assertion where
-    -- | k is mapped to v in (m :: M.Map k v)
-    -- XXX: m should be any "term", too strong now
-    InMap    :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion
-    -- | v is in s
-    -- XXX: s should be any "term", too strong now
-    InSet    :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion
-    -- | All below are binary relationships
-    -- XXX: Should make sure v1 ~ v2, too weak now
-    Equal    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
-    LessE    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
-    GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
-    Less     :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
-    Greater  :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
-
-instance Z3Encoded Assertion where
-    encode (InMap k v m) = do
-        kTm <- encode k
-        vTm <- encode v
-        mTm <- encode m
-        lhs <- mkSelect mTm kTm
-        mkEq lhs vTm
-    encode (InSet e s) = do
-        eTm <- encode e
-        sTm <- encode s
-        lhs <- mkSelect sTm eTm
-        -- XXX: magic number
-        one <- (mkIntSort >>= mkInt 1)
-        mkEq one lhs
-    encode (Equal t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkEq a1 a2
-    encode (LessE t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkLe a1 a2
-    encode (GreaterE t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkGe a1 a2
-    encode (Less t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkLt a1 a2
-    encode (Greater t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkGt a1 a2
diff --git a/src/Z3/Base/Atom.hs b/src/Z3/Base/Atom.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Base/Atom.hs
@@ -0,0 +1,61 @@
+-- |
+-- Atomic predicates
+--
+
+module Z3.Base.Atom (Atom(..)) where
+
+import Z3.Base.Class
+import Z3.Monad
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+data Atom where
+    -- | k is mapped to v in (m :: M.Map k v)
+    -- XXX: m should be any "term", too strong now
+    InMap    :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Atom
+    -- | v is in s
+    -- XXX: s should be any "term", too strong now
+    InSet    :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Atom
+    -- | All below are binary relationships
+    -- XXX: Should make sure v1 ~ v2, too weak now
+    Equal    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
+    LessE    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
+    GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
+    Less     :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
+    Greater  :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
+
+instance Z3Encoded Atom where
+    encode (InMap k v m) = do
+        kTm <- encode k
+        vTm <- encode v
+        mTm <- encode m
+        lhs <- mkSelect mTm kTm
+        mkEq lhs vTm
+    encode (InSet e s) = do
+        eTm <- encode e
+        sTm <- encode s
+        lhs <- mkSelect sTm eTm
+        -- XXX: magic number
+        one <- (mkIntSort >>= mkInt 1)
+        mkEq one lhs
+    encode (Equal t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkEq a1 a2
+    encode (LessE t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkLe a1 a2
+    encode (GreaterE t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkGe a1 a2
+    encode (Less t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkLt a1 a2
+    encode (Greater t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkGt a1 a2
diff --git a/src/Z3/Base/Class.hs b/src/Z3/Base/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Base/Class.hs
@@ -0,0 +1,195 @@
+-- |
+-- Type classes and built-in implementation for primitive Haskell types
+-- 
+
+module Z3.Base.Class (
+    -- ** Types whose values are encodable to Z3 internal AST
+    Z3Encoded(..),
+    -- ** Types representable as Z3 Sort
+    -- XXX: Unsound now
+    -- XXX: Too flexible, can be used to encode Type ADT
+    Z3Sorted(..),
+    -- ** Type proxy helper, used with Z3Sorted
+    Z3Sort(..),
+    -- ** Types with reserved value for Z3 encoding use
+    -- XXX: Magic value for built-in types
+    Z3Reserved(..),
+    -- ** Monad which can be instantiated into a concrete context
+    SMT(..),
+    Datatypes,
+    ValBindings,
+    emptyValBindings,
+    -- ** Heterogenous list, a hack to encode different "term" into a list
+    -- Used to encode function argument list
+    HeteroList(..),
+    mapH
+) where
+
+import Z3.Monad
+
+import Control.Monad.Except
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+data Z3Sort a = Z3Sort
+
+class Z3Encoded a where
+    encode :: SMT m e => a -> m e AST
+
+type Datatypes ty = [(String, [(String, [(String, ty)])])]
+type ValBindings = ([String], HeteroList)
+
+emptyValBindings :: ValBindings
+emptyValBindings = ([], Nil)
+
+
+-- | XXX: Unsound
+class Z3Sorted a where
+    -- | Map a value to Sort, the value should be a type-level thing
+    sortOf :: SMT m e => a -> m e Sort
+    sortOf _ = sortPhantom (Z3Sort :: Z3Sort a)
+
+    -- | Map a Haskell type to Sort
+    sortPhantom :: SMT m e => Z3Sort a -> m e Sort
+    sortPhantom _ = smtError "sort error"
+
+class Z3Encoded a => Z3Reserved a where
+    def :: a
+
+class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where
+    -- | Globally unique id
+    genFreshId :: m e Int
+
+    -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad
+    runSMT :: Z3Sorted ty => ValBindings -> Datatypes ty -> e -> m e a -> IO (Either String a)
+
+    bindVals :: ([String], HeteroList) -> m e ()
+    bindVals (x:xs, Cons v vs) = do
+        ast <- encode v
+        st <- sortOf v
+        bindVal x ast st
+        bindVals (xs, vs)
+    bindVals _ = return ()
+
+    modifyValBindCtx :: ValBindings -> m e ()
+
+    -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort
+    bindVal :: String -> AST -> Sort -> m e ()
+
+    getValBindMaybe :: String -> m e (Maybe (AST, Sort))
+
+    getValBind :: String -> m e (AST, Sort)
+    getValBind x = getValBindMaybe x >>= \case
+        Just p  -> return p
+        Nothing -> smtError $ "no such variable: " ++ x
+
+    getDataTypeMaybe :: String -> m e (Maybe Sort)
+
+    getDataType :: String -> m e Sort
+    getDataType x = getDataTypeMaybe x >>= \case
+        Just p  -> return p
+        Nothing -> smtError $ "no such type variable: " ++ x
+
+    -- | Get extra
+    getExtra :: m e e
+
+    -- | Set extra
+    modifyExtra :: (e -> e) -> m e ()
+
+    -- | User don't have to import throwError
+    smtError :: String -> m e a
+    smtError = throwError
+
+instance Z3Reserved Int where
+    def = -1 -- XXX: Magic number
+
+instance Z3Sorted Int where
+    sortPhantom _ = mkIntSort
+
+instance Z3Encoded Int where
+    encode i = mkIntSort >>= mkInt i
+
+instance Z3Reserved Double where
+    def = -1.0 -- XXX: Magic number
+
+instance Z3Sorted Double where
+    sortPhantom _ = mkRealSort
+
+instance Z3Encoded Double where
+    encode = mkRealNum
+
+instance Z3Reserved Bool where
+    def = False -- XXX: Magic number
+
+instance Z3Sorted Bool where
+    sortPhantom _ = mkBoolSort
+
+instance Z3Encoded Bool where
+    encode = mkBool
+
+-- The basic idea:
+-- For each (k, v), assert in Z3 that if we select k from array we will get
+-- the same value v
+-- HACK: to set a default value for rest fields (or else we always get the last asserted value
+--       as default, which is certainly not complying to finite map's definition), thus the
+--       user should guarantee that he/she will never never think this value as a vaid one,
+--       if not, he/she might get "a valid value mapped to a invalid key" semantics
+instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where
+    encode m = do
+        fid <- genFreshId
+        arrSort <- sortOf m
+        arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort
+        mapM_ (\(k, v) -> do
+            kast <- encode k
+            vast <- encode v
+            sel <- mkSelect arr kast
+            mkEq sel vast >>= assert) (M.toList m)
+        arrValueDef <- mkArrayDefault arr
+        vdef <- encode (def :: v)
+        mkEq arrValueDef vdef >>= assert
+        return arr
+
+instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where
+    sortPhantom _ = do
+        sk <- sortPhantom  (Z3Sort :: Z3Sort k)
+        sv <- sortPhantom  (Z3Sort :: Z3Sort v)
+        mkArraySort sk sv
+
+-- Basic idea:
+-- Set v =def= Map v {0, 1}
+-- Thank god, this is much more sound
+instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where
+    encode s = do
+        setSort <- sortOf s
+        fid <- genFreshId
+        arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort
+        mapM_ (\e -> do
+            ast <- encode e
+            sel <- mkSelect arr ast
+            one <- (mkIntSort >>= mkInt 1)
+            mkEq sel one >>= assert) (S.toList s)
+        arrValueDef <- mkArrayDefault arr
+        zero <- (mkIntSort >>= mkInt 0)
+        mkEq zero arrValueDef >>= assert
+        return arr
+
+instance Z3Sorted v => Z3Sorted (S.Set v) where
+    sortPhantom _ = do
+        sortElem <- sortPhantom (Z3Sort :: Z3Sort v)
+        intSort <- mkIntSort
+        mkArraySort sortElem intSort
+
+
+data HeteroList where
+    Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList
+    Nil :: HeteroList
+
+instance Eq HeteroList where
+  Nil == Nil = True
+  Cons _ h1 == Cons _ h2 = h1 == h2
+  _ == _ = False
+
+mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]
+mapH _ Nil = []
+mapH f (Cons a l) = f a : mapH f l
diff --git a/src/Z3/Base/Logic.hs b/src/Z3/Base/Logic.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Base/Logic.hs
@@ -0,0 +1,95 @@
+-- | Predicates
+
+module Z3.Base.Logic (Pred(..)) where
+
+import Z3.Monad
+import Z3.Base.Class
+import Z3.Base.Atom
+
+data Pred t ty a where
+    PTrue   :: Pred t ty a
+    PFalse  :: Pred t ty a
+    PConj   :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PDisj   :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PXor    :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PNeg    :: Pred t ty a -> Pred t ty a
+    PForAll :: String -> ty -> Pred t ty a -> Pred t ty a
+    PExists :: String -> ty -> Pred t ty a -> Pred t ty a
+    PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a
+    PImpli  :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PIff    :: Pred t ty a -> Pred t ty a -> Pred t ty a
+    PAtom   :: Atom -> Pred t ty a
+    -- User-extension
+    PExt    :: a -> Pred t ty a
+
+instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where
+    encode PTrue = mkTrue
+    encode PFalse = mkFalse
+    encode (PConj p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkAnd [a1, a2]
+
+    encode (PDisj p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkOr [a1, a2]
+
+    encode (PXor p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkXor a1 a2
+
+    encode (PNeg p) = encode p >>= mkNot
+
+    encode (PForAll x ty p) = do
+        sym <- mkStringSymbol x
+        xsort <- sortOf ty
+        -- "0" is de brujin idx for current binder
+        -- it is passed to Z3 which returns an intenal (idx :: AST)
+        -- This (idx :: AST) will be used to replace the variable
+        -- in the abstraction body when encountered, thus it is stored
+        -- in context by bindVal we provide
+        -- XXX: we should save and restore qualifier context here
+        idx <- mkBound 0 xsort
+        local $ do
+            bindVal x idx xsort
+            body <- encode p
+            -- The first [] is [Pattern], which is not really useful here
+            mkForall [] [sym] [xsort] body
+
+    encode (PExists x ty p) = do
+        sym <- mkStringSymbol x
+        xsort <- sortOf ty
+        idx <- mkBound 0 xsort
+        local $ do
+            bindVal x idx xsort
+            a <- encode p
+            mkExists [] [sym] [xsort] a
+
+    -- HACK
+    encode (PExists2 x y ty p) = do
+        sym1 <- mkStringSymbol x
+        sym2 <- mkStringSymbol y
+        xsort <- sortOf ty
+        idx1 <- mkBound 0 xsort
+        idx2 <- mkBound 1 xsort
+        local $ do
+            bindVal x idx1 xsort
+            bindVal y idx2 xsort
+            a <- encode p
+            mkExists [] [sym1, sym2] [xsort, xsort] a
+
+    encode (PImpli p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkImplies a1 a2
+
+    encode (PIff p1 p2) = do
+        a1 <- encode p1
+        a2 <- encode p2
+        mkIff a1 a2
+
+    encode (PAtom a)  = encode a
+
+    encode (PExt ext) = encode ext
diff --git a/src/Z3/Class.hs b/src/Z3/Class.hs
deleted file mode 100644
--- a/src/Z3/Class.hs
+++ /dev/null
@@ -1,223 +0,0 @@
--- |
--- Type classes and built-in implementation for primitive Haskell types
--- 
-
-module Z3.Class (
-    -- ** Types whose values are encodable to Z3 internal AST
-    Z3Encoded(..),
-    -- ** Types representable as Z3 Sort
-    -- XXX: Unsound now
-    -- XXX: Too flexible, can be used to encode Type ADT
-    Z3Sorted(..),
-    -- ** Type proxy helper, used with Z3Sorted
-    Z3Sort(..),
-    -- ** Types with reserved value for Z3 encoding use
-    -- XXX: Magic value for built-in types
-    Z3Reserved(..),
-    -- ** Monad which can be instantiated into a concrete context
-    SMT(..)
-) where
-
-import Z3.Monad
-import Z3.Logic
-
-import Control.Monad.Except
-
-import qualified Data.Map as M
-import qualified Data.Set as S
-
-data Z3Sort a = Z3Sort
-
-class Z3Encoded a where
-    encode :: SMT m e => a -> m e AST
-
--- | XXX: Unsound
-class Z3Sorted a where
-    -- | Map a value to Sort, the value should be a type-level thing
-    sort :: SMT m e => a -> m e Sort
-    sort _ = sortPhantom (Z3Sort :: Z3Sort a)
-
-    -- | Map a Haskell type to Sort
-    sortPhantom :: SMT m e => Z3Sort a -> m e Sort
-    sortPhantom _ = smtError "sort error"
-
-class Z3Encoded a => Z3Reserved a where
-    def :: a
-
-class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where
-    -- | Globally unique id
-    genFreshId :: m e Int
-
-    -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad
-    runSMT :: Z3Sorted ty => [(String, [(String, [(String, ty)])])] -> e -> m e a -> IO (Either String a)
-
-    -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort
-    bindQualified :: String -> AST -> Sort -> m e ()
-
-    -- | Get the above AST
-    -- FIXME: The context management need extra -- we need to make sure that old binding wouldn't be destoryed
-    -- XXX: We shouldn't expose a Map here. A fallible query interface is better
-    getQualifierCtx :: m e (M.Map String (AST, Sort))
-
-    -- | Get the preprocessed datatype context, a map from ADT's type name to its Z3 Sort
-    -- XXX: We shouldn't expose a Map here. A fallible query interface is better
-    getDataTypeCtx :: m e (M.Map String Sort)
-
-    -- | Get extra
-    getExtra :: m e e
-
-    -- | Set extra
-    modifyExtra :: (e -> e) -> m e ()
-
-    -- | User don't have to import throwError
-    smtError :: String -> m e a
-    smtError = throwError
-
-instance Z3Reserved Int where
-    def = -1 -- XXX: Magic number
-
-instance Z3Sorted Int where
-    sortPhantom _ = mkIntSort
-
-instance Z3Encoded Int where
-    encode i = mkIntSort >>= mkInt i
-
-instance Z3Reserved Double where
-    def = -1.0 -- XXX: Magic number
-
-instance Z3Sorted Double where
-    sortPhantom _ = mkRealSort
-
-instance Z3Encoded Double where
-    encode = mkRealNum
-
-instance Z3Reserved Bool where
-    def = False -- XXX: Magic number
-
-instance Z3Sorted Bool where
-    sortPhantom _ = mkBoolSort
-
-instance Z3Encoded Bool where
-    encode = mkBool
-
--- The basic idea:
--- For each (k, v), assert in Z3 that if we select k from array we will get
--- the same value v
--- HACK: to set a default value for rest fields (or else we always get the last asserted value
---       as default, which is certainly not complying to finite map's definition), thus the
---       user should guarantee that he/she will never never think this value as a vaid one,
---       if not, he/she might get "a valid value mapped to a invalid key" semantics
-instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where
-    encode m = do
-        fid <- genFreshId
-        arrSort <- sort m
-        arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort
-        mapM_ (\(k, v) -> do
-            kast <- encode k
-            vast <- encode v
-            sel <- mkSelect arr kast
-            mkEq sel vast >>= assert) (M.toList m)
-        arrValueDef <- mkArrayDefault arr
-        vdef <- encode (def :: v)
-        mkEq arrValueDef vdef >>= assert
-        return arr
-
-instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where
-    sortPhantom _ = do
-        sk <- sortPhantom  (Z3Sort :: Z3Sort k)
-        sv <- sortPhantom  (Z3Sort :: Z3Sort v)
-        mkArraySort sk sv
-
--- Basic idea:
--- Set v =def= Map v {0, 1}
--- Thank god, this is much more sound
-instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where
-    encode s = do
-        setSort <- sort s
-        fid <- genFreshId
-        arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort
-        mapM_ (\e -> do
-            ast <- encode e
-            sel <- mkSelect arr ast
-            one <- (mkIntSort >>= mkInt 1)
-            mkEq sel one >>= assert) (S.toList s)
-        arrValueDef <- mkArrayDefault arr
-        zero <- (mkIntSort >>= mkInt 0)
-        mkEq zero arrValueDef >>= assert
-        return arr
-
-instance Z3Sorted v => Z3Sorted (S.Set v) where
-    sortPhantom _ = do
-        sortElem <- sortPhantom (Z3Sort :: Z3Sort v)
-        intSort <- mkIntSort
-        mkArraySort sortElem intSort
-
-instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where
-    encode PTrue = mkTrue
-    encode PFalse = mkFalse
-    encode (PConj p1 p2) = do
-        a1 <- encode p1
-        a2 <- encode p2
-        mkAnd [a1, a2]
-
-    encode (PDisj p1 p2) = do
-        a1 <- encode p1
-        a2 <- encode p2
-        mkOr [a1, a2]
-
-    encode (PXor p1 p2) = do
-        a1 <- encode p1
-        a2 <- encode p2
-        mkXor a1 a2
-
-    encode (PNeg p) = encode p >>= mkNot
-
-    encode (PForAll x ty p) = do
-        sym <- mkStringSymbol x
-        xsort <- sort ty
-        -- "0" is de brujin idx for current binder
-        -- it is passed to Z3 which returns an intenal (idx :: AST)
-        -- This (idx :: AST) will be used to replace the variable
-        -- in the abstraction body when encountered, thus it is stored
-        -- in context by bindQualified we provide
-        -- XXX: we should save and restore qualifier context here
-        idx <- mkBound 0 xsort
-        local $ do
-            bindQualified x idx xsort
-            body <- encode p
-            -- The first [] is [Pattern], which is not really useful here
-            mkForall [] [sym] [xsort] body
-
-    encode (PExists x ty p) = do
-        sym <- mkStringSymbol x
-        xsort <- sort ty
-        idx <- mkBound 0 xsort
-        local $ do
-            bindQualified x idx xsort
-            a <- encode p
-            mkExists [] [sym] [xsort] a
-
-    -- HACK
-    encode (PExists2 x y ty p) = do
-        sym1 <- mkStringSymbol x
-        sym2 <- mkStringSymbol y
-        xsort <- sort ty
-        idx1 <- mkBound 0 xsort
-        idx2 <- mkBound 1 xsort
-        local $ do
-            bindQualified x idx1 xsort
-            bindQualified y idx2 xsort
-            a <- encode p
-            mkExists [] [sym1, sym2] [xsort, xsort] a
-
-    encode (PImpli p1 p2) = do
-        a1 <- encode p1
-        a2 <- encode p2
-        mkImplies a1 a2
-
-    encode (PIff p1 p2) = do
-        a1 <- encode p1
-        a2 <- encode p2
-        mkIff a1 a2
-
-    encode (PAssert a) = encode a
diff --git a/src/Z3/Context.hs b/src/Z3/Context.hs
--- a/src/Z3/Context.hs
+++ b/src/Z3/Context.hs
@@ -2,11 +2,11 @@
 
 -- | A concrete context implement SMT provided *for convenience*
 
-module Z3.Context (Z3SMT) where
+module Z3.Context (Z3SMT, localSMT) where
 
 import Z3.Monad
-import Z3.Class
-import Z3.Encoding
+import Z3.Base.Class
+import Z3.Datatypes
 
 import Control.Monad.State
 import Control.Monad.Except
@@ -14,7 +14,7 @@
 
 data SMTContext e = SMTContext {
     -- | Bind local variables introduced by qualifiers to de brujin index in Z3
-    _qualifierContext :: M.Map String (AST, Sort),
+    _valBindCtx :: M.Map String (AST, Sort),
     -- | From type name to Z3 sort
     _datatypeCtx :: M.Map String Sort,
     -- | Counter used to generate globally unique ID
@@ -36,12 +36,13 @@
         modify (\ctx -> ctx { _counter = i + 1 })
         return i
 
-    runSMT datatypes e smt = evalZ3With Nothing opts m
+    runSMT initialBindings datatypes e smt = evalZ3With Nothing opts m
         where
             smt' = do
                 sorts <- mapM encodeDataType datatypes
                 let datatypeCtx = M.fromList (zip (map fst datatypes) sorts)
                 modify $ \ctx -> ctx { _datatypeCtx = datatypeCtx }
+                bindVals initialBindings
                 smt
 
             -- XXX: not sure what does this option mean
@@ -49,13 +50,29 @@
             m = evalStateT (runExceptT (unZ3SMT smt'))
                            (SMTContext M.empty M.empty 0 e)
 
-    bindQualified x idx s = modify $ \ctx ->
-            ctx { _qualifierContext = M.insert x (idx, s) (_qualifierContext ctx) }
+    bindVal x ast st = modify $ \ctx ->
+            ctx { _valBindCtx = M.insert x (ast, st) (_valBindCtx ctx) }
 
-    getQualifierCtx = _qualifierContext <$> get
+    modifyValBindCtx bindings = do
+        modify $ \ctx -> ctx { _valBindCtx = M.empty }
+        bindVals bindings
 
-    getDataTypeCtx = _datatypeCtx <$> get
+    getValBindMaybe x = do
+        ctx <- _valBindCtx <$> get
+        return $ M.lookup x ctx
 
+    getDataTypeMaybe x = do
+        ctx <- _datatypeCtx <$> get
+        return $ M.lookup x ctx
+
     getExtra = _extra <$> get
 
     modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }
+
+
+localSMT :: Z3SMT e a -> Z3SMT e a
+localSMT m = do
+    s <- get
+    ret <- local m
+    put s
+    return ret
diff --git a/src/Z3/Datatypes.hs b/src/Z3/Datatypes.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Datatypes.hs
@@ -0,0 +1,36 @@
+-- |
+-- Z3 encoding for datatypes
+--
+
+module Z3.Datatypes (
+  -- ** encode constructor application
+  encodeCons,
+  -- ** encode datatype definition
+  encodeDataType
+) where
+
+import Z3.Base.Class
+import Z3.Monad hiding (mkMap, App)
+
+encodeCons :: SMT m e => String -> HeteroList -> Sort -> m e AST
+encodeCons fname args retSort = do
+    paramSorts <- sequence $ mapH sortOf args
+    sym <- mkStringSymbol fname
+    decl <- mkFuncDecl sym paramSorts retSort
+    argASTs <- sequence $ mapH encode args
+    mkApp decl argASTs
+
+encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort
+encodeDataType (tyName, alts) = do
+    constrs <- mapM (\(consName, fields) -> do
+                        consSym <- mkStringSymbol consName
+                        -- recognizer. e.g. is_None None = True, is_None (Some _) = False
+                        recogSym <- mkStringSymbol ("is_" ++ consName)
+                        flds <- flip mapM fields $ \(fldName, fldTy) -> do
+                            symFld <- mkStringSymbol fldName
+                            s <- sortOf fldTy
+                            return (symFld, Just s, -1) -- XXX: non-rec
+                        mkConstructor consSym recogSym flds
+                    ) alts
+    sym <- mkStringSymbol tyName
+    mkDatatype sym constrs
diff --git a/src/Z3/Encoding.hs b/src/Z3/Encoding.hs
deleted file mode 100644
--- a/src/Z3/Encoding.hs
+++ /dev/null
@@ -1,52 +0,0 @@
--- |
--- Prviding some Z3 encoding for certain language constructs
--- Require a Class.SMT context to work
-
-module Z3.Encoding (
-  -- ** Heterogenous list, a hack to encode different "term" into a list
-  -- Used to encode function argument list
-  HeteroList(..),
-  -- ** encode function application
-  encodeApp,
-  -- ** encode datatype definition
-  encodeDataType
-) where
-
-import Z3.Class
-import Z3.Monad hiding (mkMap, App)
-
-data HeteroList where
-    Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList
-    Nil :: HeteroList
-
-instance Eq HeteroList where
-  Nil == Nil = True
-  Cons _ h1 == Cons _ h2 = h1 == h2
-  _ == _ = False
-
-mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]
-mapH _ Nil = []
-mapH f (Cons a l) = f a : mapH f l
-
-encodeApp :: SMT m e => String -> HeteroList -> Sort -> m e AST
-encodeApp fname args retSort = do
-    paramSorts <- sequence $ mapH sort args
-    sym <- mkStringSymbol fname
-    decl <- mkFuncDecl sym paramSorts retSort
-    argASTs <- sequence $ mapH encode args
-    mkApp decl argASTs
-
-encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort
-encodeDataType (tyName, alts) = do
-    constrs <- mapM (\(consName, fields) -> do
-                        consSym <- mkStringSymbol consName
-                        -- recognizer. e.g. is_None None = True, is_None (Some _) = False
-                        recogSym <- mkStringSymbol ("is_" ++ consName)
-                        flds <- flip mapM fields $ \(fldName, fldTy) -> do
-                            symFld <- mkStringSymbol fldName
-                            s <- sort fldTy
-                            return (symFld, Just s, -1) -- XXX: non-rec
-                        mkConstructor consSym recogSym flds
-                    ) alts
-    sym <- mkStringSymbol tyName
-    mkDatatype sym constrs
diff --git a/src/Z3/Logic.hs b/src/Z3/Logic.hs
deleted file mode 100644
--- a/src/Z3/Logic.hs
+++ /dev/null
@@ -1,18 +0,0 @@
--- | Predicates
-
-module Z3.Logic (Pred(..)) where
-
-data Pred t ty a where
-    PTrue   :: Pred t ty a
-    PFalse  :: Pred t ty a
-    PConj   :: Pred t ty a -> Pred t ty a -> Pred t ty a
-    PDisj   :: Pred t ty a -> Pred t ty a -> Pred t ty a
-    PXor    :: Pred t ty a -> Pred t ty a -> Pred t ty a
-    PNeg    :: Pred t ty a -> Pred t ty a
-    PForAll :: String -> ty -> Pred t ty a -> Pred t ty a
-    PExists :: String -> ty -> Pred t ty a -> Pred t ty a
-    PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a
-    PImpli  :: Pred t ty a -> Pred t ty a -> Pred t ty a
-    PIff    :: Pred t ty a -> Pred t ty a -> Pred t ty a
-    PAssert :: a -> Pred t ty a
-    deriving (Show)
diff --git a/src/Z3/Z3Pred.hs b/src/Z3/Z3Pred.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Z3Pred.hs
@@ -0,0 +1,136 @@
+{-
+  Sealed AST for out-of-box use
+
+  The design choice is to fix all possible *primitive*
+  types as an AST, so a sound type checking is possible here.
+
+  Question: How to handle TmApp (which is only instantiated as
+  constructors) and potential user functions here? Do we have to
+  provide an extra field or user can make up a Encoded Expr which
+  layers on top of Term here (while preserving (expected) type soundness
+  provided in this module)?
+
+-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Z3.Z3Pred where
+
+import Z3.Base.Logic
+import Z3.Base.Class
+import Z3.Base.Atom
+import Z3.Context
+import Z3.Datatypes
+import Z3.Monad
+
+data Term = -- XXX: Verify that TmVar can serve at the same time as
+            --      qualified var, bounded var, and zero-arity constructor
+            TmVar   String
+          | TmInt   Int
+          | TmDouble Double
+          | TmBool  Bool
+          | TmString String
+          | TmLE    Term Term
+          | TmGE    Term Term
+          | TmSub   Term Term
+          | TmAdd   Term Term
+          | TmMul   Term Term
+          | TmDiv   Term Term
+          | TmMod   Term Term
+          | TmRem   Term Term
+          | TmMinus Term
+          | TmIf    Term Term Term
+          | TmCons String HeteroList Type
+
+deriving instance Eq Term
+
+data Type = TyBool
+          | TyInt
+          | TyDouble
+          | TyString
+          | TyMap Type Type
+          | TySet Type
+          | TyADT String
+
+deriving instance Eq Type
+
+type Z3Pred tm = Pred tm Type ()
+
+instance Z3Encoded Term where
+    encode (TmVar x) = fst <$> getValBind x
+    encode (TmInt n) = encode n
+    encode (TmBool b) = encode b
+    encode (TmLE t1 t2) = encode (LessE t1 t2)
+    encode (TmGE t1 t2) = encode (GreaterE t1 t2)
+    encode (TmAdd t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkAdd [a1, a2]
+    encode (TmSub t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkSub [a1, a2]
+    encode (TmMul t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkMul [a1, a2]
+    encode (TmDiv t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkDiv a1 a2
+    encode (TmMod t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkMod a1 a2
+    encode (TmRem t1 t2) = do
+        a1 <- encode t1
+        a2 <- encode t2
+        mkRem a1 a2
+    encode (TmMinus t) = do
+        a <- encode t
+        mkUnaryMinus a
+    encode (TmIf p c a) = do
+        a1 <- encode p
+        a2 <- encode c
+        a3 <- encode a
+        mkIte a1 a2 a3
+    encode (TmCons fname args retty) = do
+      retSort <- sortOf retty
+      encodeCons fname args retSort
+
+-- XXX: Maybe if we have type checking this can be neater
+instance Z3Sorted Term where
+    sortOf (TmVar x) = snd <$> getValBind x
+    sortOf (TmInt _) = mkIntSort
+    sortOf (TmBool _) = mkBoolSort
+    sortOf (TmLE _ _) = mkBoolSort
+    sortOf (TmGE _ _) = mkBoolSort
+    sortOf (TmAdd _ _) = mkIntSort
+    sortOf (TmSub _ _) = mkIntSort
+    sortOf (TmMul _ _) = mkIntSort
+    sortOf (TmDiv _ _) = mkIntSort
+    sortOf (TmMod _ _) = mkIntSort
+    sortOf (TmRem _ _) = mkIntSort
+    sortOf (TmMinus _) = mkIntSort
+    sortOf (TmIf _ c _) = sortOf c
+    sortOf (TmCons _ _ retty) = sortOf retty
+
+instance Z3Sorted Type where
+    sortOf TyBool     = mkBoolSort
+    sortOf TyInt      = mkIntSort
+    sortOf TyDouble   = mkRealSort
+    sortOf (TyMap ty1 ty2) = do
+        s1 <- sortOf ty1
+        s2 <- sortOf ty2
+        mkArraySort s1 s2
+    sortOf (TySet ty) = do
+        s <- sortOf ty
+        intSort <- mkIntSort
+        mkArraySort s intSort
+    sortOf (TyADT tyName) = getDataType tyName
+
+instance Z3Encoded () where
+
+checkPre :: Z3Sorted tm => Z3Pred tm -> Z3SMT e (Result, Maybe Model)
+checkPre pre = local $ do
+    ast <- encode pre
+    local (assert ast >> getModel)
diff --git a/test/Z3/Demo.hs b/test/Z3/Demo.hs
deleted file mode 100644
--- a/test/Z3/Demo.hs
+++ /dev/null
@@ -1,123 +0,0 @@
--- Demo of how to instantiate the Pred
-
-module Z3.Demo where
-
-import Z3.Logic
-import Z3.Class
-import Z3.Encoding
-import Z3.Assertion
-import Z3.Monad
-
-import qualified Data.Map as M
-
-data Term = TmVar   String
-          | TmNum   Int
-          | TmBool  Bool
-          | TmLE    Term Term
-          | TmGE    Term Term
-          | TmSub   Term Term
-          | TmAdd   Term Term
-          | TmMul   Term Term
-          | TmDiv   Term Term
-          | TmMod   Term Term
-          | TmRem   Term Term
-          | TmMinus Term
-          | TmIf    Term Term Term
-          | TmApp   String HeteroList Type
-
-deriving instance Eq Term
-
-data Type = TyBool
-          | TyInt
-          | TyDouble
-          | TyMap Type Type
-          | TySet Type
-          | TyADT String
-
-deriving instance Eq Type
-
-type Z3Pred = Pred Term Type Assertion
-
-instance Z3Encoded Term where
-    encode (TmVar x) = do
-        ctx <- getQualifierCtx
-        case M.lookup x ctx of
-            Just (idx, _) -> return idx
-            Nothing -> smtError $ "Can't find variable " ++ x
-    encode (TmNum n) = mkIntSort >>= mkInt n
-    encode (TmBool b) = mkBool b
-    encode (TmLE t1 t2) = encode (LessE t1 t2)
-    encode (TmGE t1 t2) = encode (GreaterE t1 t2)
-    encode (TmAdd t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkAdd [a1, a2]
-    encode (TmSub t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkSub [a1, a2]
-    encode (TmMul t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkMul [a1, a2]
-    encode (TmDiv t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkDiv a1 a2
-    encode (TmMod t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkMod a1 a2
-    encode (TmRem t1 t2) = do
-        a1 <- encode t1
-        a2 <- encode t2
-        mkRem a1 a2
-    encode (TmMinus t) = do
-        a <- encode t
-        mkUnaryMinus a
-    encode (TmIf p c a) = do
-        a1 <- encode p
-        a2 <- encode c
-        a3 <- encode a
-        mkIte a1 a2 a3
-    encode (TmApp fname args retty) = do
-      retSort <- sort retty
-      encodeApp fname args retSort
-
-instance Z3Sorted Term where
-    sort (TmVar x) = do
-        ctx <- getQualifierCtx
-        case M.lookup x ctx of
-            Just (_, s) -> return s
-            Nothing -> smtError $ "Can't find variable " ++ x
-    sort (TmNum _) = mkIntSort
-    sort (TmBool _) = mkBoolSort
-    sort (TmLE _ _) = mkBoolSort
-    sort (TmGE _ _) = mkBoolSort
-    sort (TmAdd _ _) = mkIntSort
-    sort (TmSub _ _) = mkIntSort
-    sort (TmMul _ _) = mkIntSort
-    sort (TmDiv _ _) = mkIntSort
-    sort (TmMod _ _) = mkIntSort
-    sort (TmRem _ _) = mkIntSort
-    sort (TmMinus _) = mkIntSort
-    sort (TmIf _ c _) = sort c
-    sort (TmApp _ _ retty) = sort retty
-
-instance Z3Sorted Type where
-    sort TyBool     = mkBoolSort
-    sort TyInt      = mkIntSort
-    sort TyDouble   = mkRealSort
-    sort (TyMap ty1 ty2) = do
-        s1 <- sort ty1
-        s2 <- sort ty2
-        mkArraySort s1 s2
-    sort (TySet ty) = do
-        s <- sort ty
-        intSort <- mkIntSort
-        mkArraySort s intSort
-    sort (TyADT tyName)  = do
-      ctx <- getDataTypeCtx
-      case M.lookup tyName ctx of
-          Just s  -> return s
-          Nothing -> smtError $ "Undefined type: " ++ tyName
diff --git a/test/Z3/Test.hs b/test/Z3/Test.hs
--- a/test/Z3/Test.hs
+++ b/test/Z3/Test.hs
@@ -1,13 +1,15 @@
 module Z3.Test (spec) where
 
-import Z3.Class
-import Z3.Logic
-import Z3.Demo
-import Z3.Encoding
-import Z3.Context
-import Z3.Assertion
 import Z3.Monad hiding (mkMap)
 
+import Z3.Base.Class
+import Z3.Base.Logic
+import Z3.Base.Atom
+
+import Z3.Z3Pred
+import Z3.Datatypes
+import Z3.Context
+
 import Control.Monad (forM_)
 import Control.Monad.IO.Class (liftIO)
 import qualified Data.Map as M
@@ -15,7 +17,7 @@
 
 import Test.Hspec
 
-tests :: [(Z3Pred, Either String Result)]
+tests :: [(Z3Pred Term, Either String Result)]
 tests = [
     (PTrue, Right Sat),
     (PFalse, Right Unsat),
@@ -24,45 +26,40 @@
     (PDisj PTrue PFalse, Right Sat),
     (PDisj PFalse PFalse, Right Unsat),
     (PNeg PFalse, Right Sat),
-    (PAssert (Equal (1 :: Int) (1 :: Int)), Right Sat),
-    (PAssert (Equal True False), Right Unsat),
+    (PAtom (Equal (1 :: Int) (1 :: Int)), Right Sat),
+    (PAtom (Equal True False), Right Unsat),
     (PForAll "x" TyInt PTrue, Right Sat),
-    (PExists "x" TyInt (PAssert (Equal (TmVar "x") (1 :: Int))), Right Sat),
-    (PForAll "x" TyInt (PImpli (PAssert (Less (TmVar "x") (0 :: Int)))
-                               (PAssert (Less (TmVar "x") (1 :: Int)))), Right Sat),
-    (PForAll "x" TyInt (PImpli (PAssert (Less (TmVar "x") (1 :: Int)))
-                               (PAssert (Less (TmVar "x") (0 :: Int)))), Right Unsat),
+    (PExists "x" TyInt (PAtom (Equal (TmVar "x") (1 :: Int))), Right Sat),
+    (PForAll "x" TyInt (PImpli (PAtom (Less (TmVar "x") (0 :: Int)))
+                               (PAtom (Less (TmVar "x") (1 :: Int)))), Right Sat),
+    (PForAll "x" TyInt (PImpli (PAtom (Less (TmVar "x") (1 :: Int)))
+                               (PAtom (Less (TmVar "x") (0 :: Int)))), Right Unsat),
     (PForAll "x" TyInt (PImpli PTrue PFalse), Right Unsat),
-    (PAssert (InMap (1 :: Int) (1 :: Int) (M.singleton (1 :: Int) 1)), Right Sat),
-    (PAssert (InSet (10 :: Int) (S.singleton (10 :: Int))), Right Sat),
-    (PAssert (Equal (TmApp "none" Nil (TyADT "optionInt"))
-                    (TmApp "none" Nil (TyADT "optionInt"))), Right Sat),
+    (PAtom (InMap (1 :: Int) (1 :: Int) (M.singleton (1 :: Int) 1)), Right Sat),
+    (PAtom (InSet (10 :: Int) (S.singleton (10 :: Int))), Right Sat),
+    (PAtom (Equal (TmCons "none" Nil (TyADT "optionInt"))
+                    (TmCons "none" Nil (TyADT "optionInt"))), Right Sat),
     (PForAll "x" (TyADT "optionInt") PTrue, Right Sat),
-    (PAssert (Equal (TmApp "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))
-                    (TmApp "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))), Right Sat),
-    (PExists "x" TyInt $ PConj (PAssert $ GreaterE (TmSub (TmVar "x") (TmNum 1)) (3 :: Int))
-                               (PAssert $ GreaterE (TmSub (TmSub (TmVar "x") (TmNum 2)) (TmNum 1)) (0 :: Int)), Right Sat),
-    (PExists "x" TyInt $ PConj (PAssert $ Less (TmVar "x") (TmNum 0))
-                               (PNeg $ PAssert $ LessE (TmVar "x") (TmNum 0)), Right Unsat),
-    (PExists2 "x" "y" TyInt $ PConj (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")
-                                    (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat),
-    (PExists2 "x" "y" TyInt $ PConj (PConj (PAssert $ LessE (TmVar "x") $ TmNum 3)
-                                           (PAssert $ LessE (TmVar "y") $ TmNum 3))
-                                    (PAssert $ GreaterE (TmAdd (TmVar "x") (TmVar "y")) $ TmNum 9), Right Unsat),
-    (PExists2 "x" "y" TyInt $ PNeg $ PConj (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")
-                                           (PAssert $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat)
+    (PAtom (Equal (TmCons "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))
+                    (TmCons "just" (Cons (1 :: Int) Nil) (TyADT "optionInt"))), Right Sat),
+    (PExists "x" TyInt $ PConj (PAtom $ GreaterE (TmSub (TmVar "x") (TmInt 1)) (3 :: Int))
+                               (PAtom $ GreaterE (TmSub (TmSub (TmVar "x") (TmInt 2)) (TmInt 1)) (0 :: Int)), Right Sat),
+    (PExists "x" TyInt $ PConj (PAtom $ Less (TmVar "x") (TmInt 0))
+                               (PNeg $ PAtom $ LessE (TmVar "x") (TmInt 0)), Right Unsat),
+    (PExists2 "x" "y" TyInt $ PConj (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")
+                                    (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat),
+    (PExists2 "x" "y" TyInt $ PConj (PConj (PAtom $ LessE (TmVar "x") $ TmInt 3)
+                                           (PAtom $ LessE (TmVar "y") $ TmInt 3))
+                                    (PAtom $ GreaterE (TmAdd (TmVar "x") (TmVar "y")) $ TmInt 9), Right Unsat),
+    (PExists2 "x" "y" TyInt $ PNeg $ PConj (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "x")
+                                           (PAtom $ GreaterE (TmIf (TmLE (TmVar "x") (TmVar "y")) (TmVar "x") (TmVar "y")) $ TmVar "y"), Right Sat)
     ]
 
-checkPre :: Z3Pred -> Z3SMT () (Result, Maybe Model)
-checkPre pre = local $ do
-    ast <- encode pre
-    local (assert ast >> getModel)
-
-test :: (Z3Pred, Either String Result) -> IO ()
+test :: (Z3Pred Term, Either String Result) -> IO ()
 test (p, expected) = do
     let adts = [("optionInt", [("none", []),
                                ("just", [("val", TyInt)])])]
-    ret <- runSMT adts () $ do
+    ret <- runSMT emptyValBindings adts () $ do
         (r, _mm) <- checkPre p
         case r of
             Unsat -> do
@@ -76,4 +73,3 @@
 spec = forM_ tests $ (\pair@(p, expected) -> do
          it {-(show p ++ " → " ++ show expected )-}"no show" $
            test pair)
-
diff --git a/z3-encoding.cabal b/z3-encoding.cabal
--- a/z3-encoding.cabal
+++ b/z3-encoding.cabal
@@ -2,14 +2,14 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                z3-encoding
-version:             0.2.1.1
+version:             0.3.0.0
 synopsis:            High-level assertion encoding to Z3 solver
 description:
   A library targeting at providing high-level, extensible, easy to use Haskell interface to Z3 solver.
 license:             MIT
 license-file:        LICENSE
-author:              Zhen Zhang
-maintainer:          izgzhen@gmail.com
+author:              Zhen Zhang <izgzhen@gmail.com>
+maintainer:          Zhen Zhang <izgzhen@gmail.com>
 -- copyright:           
 category:            Language
 build-type:          Simple
@@ -20,11 +20,12 @@
   location: https://github.com/izgzhen/z3-encoding
 
 library
-  exposed-modules:     Z3.Class
-                       Z3.Logic
-                       Z3.Encoding
-                       Z3.Assertion
+  exposed-modules:     Z3.Base.Class
+                       Z3.Base.Logic
+                       Z3.Base.Atom
+                       Z3.Datatypes
                        Z3.Context
+                       Z3.Z3Pred
   -- other-modules:       
   -- other-extensions: 
   build-depends:       base >=4.9 && <4.10,
@@ -37,13 +38,14 @@
                        ScopedTypeVariables
                        MultiParamTypeClasses
                        RankNTypes
+                       LambdaCase
                        GADTs
   default-language:    Haskell2010
   ghc-options:         -Wall
 
 test-suite z3-encoding-test
   type:                exitcode-stdio-1.0
-  other-modules:       Z3.Test, Z3.Demo
+  other-modules:       Z3.Test
   hs-source-dirs:      test
   main-is:             Spec.hs
   build-depends:       base >=4.9 && <4.10
@@ -52,5 +54,5 @@
                      , hspec >= 1.3
                      , containers >=0.5 && <0.6
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N -Wall
-  default-extensions:  StandaloneDeriving
+--  default-extensions:  StandaloneDeriving
   default-language:    Haskell2010