diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2016 Zhen Zhang
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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/src/Z3/Assertion.hs b/src/Z3/Assertion.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Assertion.hs
@@ -0,0 +1,63 @@
+-- |
+-- 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/Class.hs b/src/Z3/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Class.hs
@@ -0,0 +1,223 @@
+-- |
+-- 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
new file mode 100644
--- /dev/null
+++ b/src/Z3/Context.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- | A concrete context implement SMT provided *for convenience*
+
+module Z3.Context (Z3SMT) where
+
+import Z3.Monad
+import Z3.Class
+import Z3.Encoding
+
+import Control.Monad.State
+import Control.Monad.Except
+import qualified Data.Map as M
+
+data SMTContext e = SMTContext {
+    -- | Bind local variables introduced by qualifiers to de brujin index in Z3
+    _qualifierContext :: M.Map String (AST, Sort),
+    -- | From type name to Z3 sort
+    _datatypeCtx :: M.Map String Sort,
+    -- | Counter used to generate globally unique ID
+    _counter :: Int,
+    -- | Extra field reserved for extension
+    _extra :: e
+} deriving (Show, Eq)
+
+newtype Z3SMT e a = Z3SMT { unZ3SMT :: ExceptT String (StateT (SMTContext e) Z3) a }
+    deriving (Monad, Applicative, Functor, MonadState (SMTContext e), MonadIO, MonadError String)
+
+instance MonadZ3 (Z3SMT e) where
+  getSolver  = Z3SMT (lift (lift getSolver))
+  getContext = Z3SMT (lift (lift getContext))
+
+instance SMT Z3SMT e where
+    genFreshId = do
+        i <- _counter <$> get
+        modify (\ctx -> ctx { _counter = i + 1 })
+        return i
+
+    runSMT 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 }
+                smt
+
+            -- XXX: not sure what does this option mean
+            opts = opt "MODEL" True
+            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) }
+
+    getQualifierCtx = _qualifierContext <$> get
+
+    getDataTypeCtx = _datatypeCtx <$> get
+
+    getExtra = _extra <$> get
+
+    modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }
diff --git a/src/Z3/Encoding.hs b/src/Z3/Encoding.hs
new file mode 100644
--- /dev/null
+++ b/src/Z3/Encoding.hs
@@ -0,0 +1,52 @@
+-- |
+-- 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
new file mode 100644
--- /dev/null
+++ b/src/Z3/Logic.hs
@@ -0,0 +1,18 @@
+-- | 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/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,9 @@
+import qualified Z3.Test
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = do
+  describe "Z3" Z3.Test.spec
diff --git a/test/Z3/Demo.hs b/test/Z3/Demo.hs
new file mode 100644
--- /dev/null
+++ b/test/Z3/Demo.hs
@@ -0,0 +1,123 @@
+-- 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
new file mode 100644
--- /dev/null
+++ b/test/Z3/Test.hs
@@ -0,0 +1,79 @@
+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 Control.Monad (forM_)
+import Control.Monad.IO.Class (liftIO)
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Test.Hspec
+
+tests :: [(Z3Pred, Either String Result)]
+tests = [
+    (PTrue, Right Sat),
+    (PFalse, Right Unsat),
+    (PConj PTrue PFalse, Right Unsat),
+    (PConj PTrue PTrue, Right Sat),
+    (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),
+    (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),
+    (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),
+    (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)
+    ]
+
+checkPre :: Z3Pred -> Z3SMT () (Result, Maybe Model)
+checkPre pre = local $ do
+    ast <- encode pre
+    local (assert ast >> getModel)
+
+test :: (Z3Pred, Either String Result) -> IO ()
+test (p, expected) = do
+    let adts = [("optionInt", [("none", []),
+                               ("just", [("val", TyInt)])])]
+    ret <- runSMT adts () $ do
+        (r, _mm) <- checkPre p
+        case r of
+            Unsat -> do
+                core <- getUnsatCore
+                liftIO $ sequence_ (map print core)
+                return r
+            other -> return other
+    ret `shouldBe` expected
+
+spec :: Spec
+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
new file mode 100644
--- /dev/null
+++ b/z3-encoding.cabal
@@ -0,0 +1,56 @@
+-- Initial z3-encoding.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                z3-encoding
+version:             0.2.1.1
+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
+-- copyright:           
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.10
+
+source-repository head
+  type:     git
+  location: https://github.com/izgzhen/z3-encoding
+
+library
+  exposed-modules:     Z3.Class
+                       Z3.Logic
+                       Z3.Encoding
+                       Z3.Assertion
+                       Z3.Context
+  -- other-modules:       
+  -- other-extensions: 
+  build-depends:       base >=4.9 && <4.10,
+                       mtl >=2.2 && <2.3,
+                       containers >=0.5 && <0.6,
+                       z3 >=4.1.0
+  hs-source-dirs:      src
+  default-extensions:  FlexibleInstances
+                       FlexibleContexts
+                       ScopedTypeVariables
+                       MultiParamTypeClasses
+                       RankNTypes
+                       GADTs
+  default-language:    Haskell2010
+  ghc-options:         -Wall
+
+test-suite z3-encoding-test
+  type:                exitcode-stdio-1.0
+  other-modules:       Z3.Test, Z3.Demo
+  hs-source-dirs:      test
+  main-is:             Spec.hs
+  build-depends:       base >=4.9 && <4.10
+                     , z3 >=4.1.0
+                     , z3-encoding
+                     , hspec >= 1.3
+                     , containers >=0.5 && <0.6
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N -Wall
+  default-extensions:  StandaloneDeriving
+  default-language:    Haskell2010