packages feed

z3-encoding (empty) → 0.2.1.1

raw patch · 11 files changed

+706/−0 lines, 11 filesdep +basedep +containersdep +hspecsetup-changed

Dependencies added: base, containers, hspec, mtl, z3, z3-encoding

Files

+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Z3/Assertion.hs view
@@ -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
+ src/Z3/Class.hs view
@@ -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
+ src/Z3/Context.hs view
@@ -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) }
+ src/Z3/Encoding.hs view
@@ -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
+ src/Z3/Logic.hs view
@@ -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)
+ test/Spec.hs view
@@ -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
+ test/Z3/Demo.hs view
@@ -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
+ test/Z3/Test.hs view
@@ -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)+
+ z3-encoding.cabal view
@@ -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