z3 4.0.0 → 4.1.0
raw patch · 8 files changed
+338/−61 lines, 8 filesdep ~z3
Dependency ranges changed: z3
Files
- CHANGES.md +11/−0
- README.md +1/−1
- src/Z3/Base.hs +120/−46
- src/Z3/Base/C.hsc +54/−8
- src/Z3/Monad.hs +88/−3
- test/Spec.hs +11/−1
- test/Z3/Base/Spec.hs +49/−0
- z3.cabal +4/−2
CHANGES.md view
@@ -1,6 +1,17 @@ # Release Notes +## 4.1.0++Small maintenance release that however introduces one API breaking change.++* Added bindings for the _Set_ API. (Nadia Polikarpova)+* Fix #4: Replace the now deprecated Z3_eval with Z3_model_eval.+* Fix #5: Check error codes right after an API call. (David Castro)++To fix #4 we had to change the type of ```modelEval```, which now takes+an extra ```Bool``` parameter (to force model completion).+ ## 4.0.0 This release brings support for the new Z3 4.x API,
README.md view
@@ -9,7 +9,7 @@ [Examples here.](https://bitbucket.org/iago/z3-haskell/src/tip/examples) -[Do you want to contribute?](https://bitbucket.org/iago/z3-haskell/src/tip/CHANGES.md)+[Do you want to contribute?](https://bitbucket.org/iago/z3-haskell/src/tip/HACKING.md) ## Installation
src/Z3/Base.hs view
@@ -105,6 +105,7 @@ , mkTupleSort , mkConstructor , mkDatatype+ , mkSetSort -- * Constants and Applications , mkFuncDecl@@ -212,6 +213,18 @@ , mkMap , mkArrayDefault + -- * Sets+ , mkEmptySet+ , mkFullSet+ , mkSetAdd+ , mkSetDel+ , mkSetUnion+ , mkSetIntersect+ , mkSetDifference+ , mkSetComplement+ , mkSetMember+ , mkSetSubset+ -- * Numerals , mkNumeral , mkReal@@ -636,9 +649,9 @@ marshalArray sorts $ \ sortsPtr -> alloca $ \ outConstrPtr -> allocaArray n $ \ outProjsPtr -> do- srtPtr <- z3_mk_tuple_sort cPtr symPtr- (fromIntegral n) symsPtr sortsPtr- outConstrPtr outProjsPtr+ srtPtr <- checkError cPtr $ z3_mk_tuple_sort cPtr symPtr+ (fromIntegral n) symsPtr sortsPtr+ outConstrPtr outProjsPtr outConstr <- peek outConstrPtr outProjs <- peekArray n outProjsPtr sort <- c2h c srtPtr@@ -677,11 +690,14 @@ -> Symbol -> [Constructor] -> IO Sort-mkDatatype c sym consList = withContextError c $ \cPtr ->- marshalArrayLen consList $ \ n consPtrs -> checkError cPtr $ do- sortPtr <- z3_mk_datatype cPtr (unSymbol sym) n consPtrs- c2h c sortPtr+mkDatatype c sym consList = marshalArrayLen consList $ \ n consPtrs -> do+ toHsCheckError c $ \cPtr -> z3_mk_datatype cPtr (unSymbol sym) n consPtrs +-- | Create an set type with a given domain type+mkSetSort :: Context -> Sort -> IO Sort+mkSetSort = liftFun1 z3_mk_set_sort++ -- TODO: from Z3_mk_constructor_list on ---------------------------------------------------------------------@@ -1189,8 +1205,71 @@ --------------------------------------------------------------------- -- Sets --- TODO: Sets+-- | Create the empty set.+mkEmptySet :: Context+ -> Sort -- ^ Domain sort of the set.+ -> IO AST+mkEmptySet = liftFun1 z3_mk_empty_set +-- | Create the full set.+mkFullSet :: Context+ -> Sort -- ^ Domain sort of the set.+ -> IO AST+mkFullSet = liftFun1 z3_mk_full_set++-- | Add an element to a set.+mkSetAdd :: Context+ -> AST -- ^ Set.+ -> AST -- ^ Element.+ -> IO AST+mkSetAdd = liftFun2 z3_mk_set_add++-- | Remove an element from a set.+mkSetDel :: Context+ -> AST -- ^ Set.+ -> AST -- ^ Element.+ -> IO AST+mkSetDel = liftFun2 z3_mk_set_del++-- | Take the union of a list of sets.+mkSetUnion :: Context -> [AST] -> IO AST+mkSetUnion ctx args = marshal z3_mk_set_union ctx $ \f ->+ marshalArrayLen args $ \argsNum argsArr ->+ f argsNum argsArr++-- | Take the intersection of a list of sets.+mkSetIntersect :: Context -> [AST] -> IO AST+mkSetIntersect ctx args = marshal z3_mk_set_intersect ctx $ \f ->+ marshalArrayLen args $ \argsNum argsArr ->+ f argsNum argsArr++-- | Take the set difference between two sets.+mkSetDifference :: Context+ -> AST -- ^ First set.+ -> AST -- ^ Second set.+ -> IO AST+mkSetDifference = liftFun2 z3_mk_set_difference++-- | Take the complement of a set.+mkSetComplement :: Context+ -> AST -- ^ Set.+ -> IO AST+mkSetComplement = liftFun1 z3_mk_set_complement++-- | Check for set membership.+mkSetMember :: Context+ -> AST -- ^ Element.+ -> AST -- ^ Set.+ -> IO AST+mkSetMember = liftFun2 z3_mk_set_member++-- | Check if the first set is a subset of the second set.+mkSetSubset :: Context+ -> AST -- ^ First set.+ -> AST -- ^ Second set.+ -> IO AST+mkSetSubset = liftFun2 z3_mk_set_subset+ --------------------------------------------------------------------- -- * Numerals @@ -1467,12 +1546,11 @@ getDatatypeSortConstructors c dtSort = withContextError c $ \cPtr -> h2c dtSort $ \dtSortPtr -> do- numCons <- z3_get_datatype_sort_num_constructors cPtr dtSortPtr- T.mapM (getConstructor cPtr dtSortPtr) [0..(numCons-1)]+ numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr+ T.mapM (getConstructor dtSortPtr) [0..(numCons-1)] where- getConstructor cPtr dtSortPtr idx = do- funcDeclPtr <- z3_get_datatype_sort_constructor cPtr dtSortPtr idx- c2h c funcDeclPtr+ getConstructor dtSortPtr idx = do+ toHsCheckError c $ \cPtr -> z3_get_datatype_sort_constructor cPtr dtSortPtr idx -- TODO: Needs proper review -- | Get list of recognizers for datatype.@@ -1482,13 +1560,12 @@ getDatatypeSortRecognizers c dtSort = withContextError c $ \cPtr -> h2c dtSort $ \dtSortPtr -> do- numCons <- z3_get_datatype_sort_num_constructors cPtr dtSortPtr- T.mapM (getConstructor cPtr dtSortPtr) [0..(numCons-1)]+ numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr+ T.mapM (getConstructor dtSortPtr) [0..(numCons-1)] where -- TODO: Maybe this should be renamed to getRecognizer :-)- getConstructor cPtr dtSortPtr idx = do- funcDeclPtr <- z3_get_datatype_sort_recognizer cPtr dtSortPtr idx- c2h c funcDeclPtr+ getConstructor dtSortPtr idx = do+ toHsCheckError c $ \cPtr -> z3_get_datatype_sort_recognizer cPtr dtSortPtr idx -- TODO: Z3_get_datatype_sort_constructor_accessor @@ -1504,9 +1581,8 @@ -- | Return the constant declaration name as a symbol. getDeclName :: Context -> FuncDecl -> IO Symbol-getDeclName c decl = withContextError c $ \cPtr ->- h2c decl $ \declPtr ->- Symbol <$> z3_get_decl_name cPtr declPtr+getDeclName c decl = h2c decl $ \declPtr ->+ Symbol <$> withContextError c (\cPtr -> z3_get_decl_name cPtr declPtr) -- TODO: Z3_get_decl_kind @@ -1556,9 +1632,8 @@ -- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF -- otherwise. getBoolValue :: Context -> AST -> IO (Maybe Bool)-getBoolValue c a = withContextError c $ \cPtr ->- h2c a $ \astPtr ->- castLBool <$> z3_get_bool_value cPtr astPtr+getBoolValue c a = h2c a $ \astPtr ->+ castLBool <$> withContextError c (\cPtr -> z3_get_bool_value cPtr astPtr) where castLBool :: Z3_lbool -> Maybe Bool castLBool lb | lb == z3_l_true = Just True@@ -1710,14 +1785,16 @@ modelEval :: Context -> Model -- ^ Model /m/. -> AST -- ^ Expression to evaluate /t/.+ -> Bool -- ^ Model completion? -> IO (Maybe AST)-modelEval ctx m a =+modelEval ctx m a b = withContext ctx $ \ctxPtr -> alloca $ \aptr2 -> h2c a $ \astPtr -> h2c m $ \mPtr ->- checkError ctxPtr $- z3_eval ctxPtr mPtr astPtr aptr2 >>= peekAST aptr2 . toBool+ h2c b $ \b' ->+ checkError ctxPtr+ (z3_model_eval ctxPtr mPtr astPtr b' aptr2) >>= peekAST aptr2 . toBool where peekAST :: Ptr (Ptr Z3_ast) -> Bool -> IO (Maybe AST) peekAST _p False = return Nothing peekAST p True = fmap Just . c2h ctx =<< peek p@@ -1829,9 +1906,9 @@ -- reasons, see 'modelEval'. type EvalAst a = Model -> AST -> IO (Maybe a) --- | An alias for 'modelEval'.+-- | An alias for 'modelEval' with model completion enabled. eval :: Context -> EvalAst AST-eval = modelEval+eval ctx m a = modelEval ctx m a True -- | Evaluate an AST node of sort /bool/ in the given model. --@@ -2225,9 +2302,8 @@ mkSimpleSolver = liftFun0 z3_mk_simple_solver mkSolverForLogic :: Context -> Logic -> IO Solver-mkSolverForLogic c logic = withContextError c $ \cPtr ->- do sym <- mkStringSymbol c (show logic)- c2h c =<< z3_mk_solver_for_logic cPtr (unSymbol sym)+mkSolverForLogic c logic = mkStringSymbol c (show logic) >>= \sym ->+ toHsCheckError c $ \cPtr -> z3_mk_solver_for_logic cPtr $ unSymbol sym -- | Return a string describing all solver available parameters. solverGetHelp :: Context -> Solver -> IO String@@ -2342,6 +2418,10 @@ c2h :: Context -> c -> IO h h2c :: h -> (c -> IO r) -> IO r +toHsCheckError :: Marshal h c => Context -> (Ptr Z3_context -> IO c) -> IO h+toHsCheckError c f = withContext c $ \cPtr ->+ c2h c =<< checkError cPtr (f cPtr)+ hs2cs :: Marshal h c => [h] -> ([c] -> IO r) -> IO r hs2cs [] f = f [] hs2cs (h:hs) f =@@ -2486,37 +2566,32 @@ marshal :: Marshal rh rc => (Ptr Z3_context -> t) -> Context -> (t -> IO rc) -> IO rh-marshal f c cont = withContextError c $ \cPtr ->- cont (f cPtr) >>= c2h c+marshal f c cont = toHsCheckError c $ \cPtr -> cont $ f cPtr liftFun0 :: Marshal rh rc => (Ptr Z3_context -> IO rc) -> Context -> IO rh-liftFun0 f c = withContextError c $ \cPtr ->- c2h c =<< f cPtr+liftFun0 = flip toHsCheckError {-# INLINE liftFun0 #-} liftFun1 :: (Marshal ah ac, Marshal rh rc) => (Ptr Z3_context -> ac -> IO rc) -> Context -> ah -> IO rh-liftFun1 f c x = withContextError c $ \cPtr ->- h2c x $ \a ->- c2h c =<< f cPtr a+liftFun1 f c x = h2c x $ \a ->+ toHsCheckError c $ \cPtr -> f cPtr a {-# INLINE liftFun1 #-} liftFun2 :: (Marshal ah ac, Marshal bh bc, Marshal rh rc) => (Ptr Z3_context -> ac -> bc -> IO rc) -> Context -> ah -> bh -> IO rh-liftFun2 f c x y = withContextError c $ \cPtr ->- h2c x $ \a -> h2c y $ \b ->- c2h c =<< f cPtr a b+liftFun2 f c x y = h2c x $ \a -> h2c y $ \b ->+ toHsCheckError c $ \cPtr -> f cPtr a b {-# INLINE liftFun2 #-} liftFun3 :: (Marshal ah ac, Marshal bh bc, Marshal ch cc, Marshal rh rc) => (Ptr Z3_context -> ac -> bc -> cc -> IO rc) -> Context -> ah -> bh -> ch -> IO rh-liftFun3 f c x y z = withContextError c $ \cPtr ->- h2c x $ \x1 -> h2c y $ \y1 -> h2c z $ \z1 ->- c2h c =<< f cPtr x1 y1 z1+liftFun3 f c x y z = h2c x $ \x1 -> h2c y $ \y1 -> h2c z $ \z1 ->+ toHsCheckError c $ \cPtr -> f cPtr x1 y1 z1 {-# INLINE liftFun3 #-} ---------------------------------------------------------------------@@ -2548,4 +2623,3 @@ ptrToMaybe :: Ptr a -> Maybe (Ptr a) ptrToMaybe ptr | ptr == nullPtr = Nothing | otherwise = Just ptr-
src/Z3/Base/C.hsc view
@@ -249,6 +249,10 @@ -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_sort)+ +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b>+foreign import ccall unsafe "Z3_mk_set_sort"+ z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) -- TODO Sorts: from Z3_mk_array_sort on @@ -613,8 +617,49 @@ foreign import ccall unsafe "Z3_mk_array_default" z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- TODO Sets+--------------------------------------------------------------------------------+-- * Sets +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga358b6b80509a567148f1c0ca9252118c>+foreign import ccall unsafe "Z3_mk_empty_set"+ z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2>+foreign import ccall unsafe "Z3_mk_full_set"+ z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175>+foreign import ccall unsafe "Z3_mk_set_add"+ z3_mk_set_add :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)+ +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d>+foreign import ccall unsafe "Z3_mk_set_del"+ z3_mk_set_del :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4050162a13d539b8913200963bb4743c>+foreign import ccall unsafe "Z3_mk_set_union"+ z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d>+foreign import ccall unsafe "Z3_mk_set_intersect"+ z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1>+foreign import ccall unsafe "Z3_mk_set_difference"+ z3_mk_set_difference :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5c57143c9229cdf730c5103ff696590f>+foreign import ccall unsafe "Z3_mk_set_complement"+ z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063>+foreign import ccall unsafe "Z3_mk_set_member"+ z3_mk_set_member :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a>+foreign import ccall unsafe "Z3_mk_set_subset"+ z3_mk_set_subset :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)+ --------------------------------------------------------------------- -- * Numerals @@ -806,13 +851,14 @@ -> Ptr Z3_model -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga47d3655283564918c85bda0b423b7f67>-foreign import ccall unsafe "Z3_eval"- z3_eval :: Ptr Z3_context- -> Ptr Z3_model- -> Ptr Z3_ast- -> Ptr (Ptr Z3_ast)- -> IO Z3_bool+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86670c291a16640b932e7892176a9d1b>+foreign import ccall unsafe "Z3_model_eval"+ z3_model_eval :: Ptr Z3_context+ -> Ptr Z3_model+ -> Ptr Z3_ast+ -> Z3_bool+ -> Ptr (Ptr Z3_ast)+ -> IO Z3_bool -- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa> foreign import ccall unsafe "Z3_is_as_array"
src/Z3/Monad.hs view
@@ -66,6 +66,7 @@ , mkTupleSort , mkConstructor , mkDatatype+ , mkSetSort -- * Constants and Applications , mkFuncDecl@@ -173,6 +174,18 @@ , mkMap , mkArrayDefault + -- * Sets+ , mkEmptySet+ , mkFullSet+ , mkSetAdd+ , mkSetDel+ , mkSetUnion+ , mkSetIntersect+ , mkSetDifference+ , mkSetComplement+ , mkSetMember+ , mkSetSubset+ -- * Numerals , mkNumeral , mkInt@@ -547,6 +560,13 @@ -> z3 Sort mkDatatype = liftFun2 Base.mkDatatype +-- | Create a set type+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b>+--+mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort+mkSetSort = liftFun1 Base.mkSetSort+ --------------------------------------------------------------------- -- Constants and Applications @@ -1150,6 +1170,69 @@ mkArrayDefault = liftFun1 Base.mkArrayDefault ---------------------------------------------------------------------+-- Sets++-- | Create the empty set.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga358b6b80509a567148f1c0ca9252118c>+mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST+mkEmptySet = liftFun1 Base.mkEmptySet++-- | Create the full set.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2>+mkFullSet :: MonadZ3 z3 => Sort -> z3 AST+mkFullSet = liftFun1 Base.mkFullSet++-- | Add an element to a set.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175>+mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST+mkSetAdd = liftFun2 Base.mkSetAdd++-- | Remove an element from a set.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d>+mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST+mkSetDel = liftFun2 Base.mkSetDel++-- | Take the union of a list of sets.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4050162a13d539b8913200963bb4743c>+mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST+mkSetUnion = liftFun1 Base.mkSetUnion++-- | Take the intersection of a list of sets.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d>+mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST+mkSetIntersect = liftFun1 Base.mkSetIntersect++-- | Take the set difference between two sets.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1>+mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST+mkSetDifference = liftFun2 Base.mkSetDifference++-- | Take the complement of a set.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5c57143c9229cdf730c5103ff696590f>+mkSetComplement :: MonadZ3 z3 => AST -> z3 AST+mkSetComplement = liftFun1 Base.mkSetComplement++-- | Check for set membership.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063>+mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST+mkSetMember = liftFun2 Base.mkSetMember++-- | Check if the first set is a subset of the second set.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a>+mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST+mkSetSubset = liftFun2 Base.mkSetSubset++--------------------------------------------------------------------- -- * Numerals -- | Create a numeral of a given sort.@@ -1348,8 +1431,10 @@ -- * /t/ contains a quantifier. -- * the model /m/ is partial. -- * /t/ is type incorrect.-modelEval :: MonadZ3 z3 => Model -> AST -> z3 (Maybe AST)-modelEval = liftFun2 Base.modelEval+modelEval :: MonadZ3 z3 => Model -> AST+ -> Bool -- ^ Model completion?+ -> z3 (Maybe AST)+modelEval = liftFun3 Base.modelEval -- | Get array as a list of argument/value pairs, if it is -- represented as a function (ie, using as-array).@@ -1440,7 +1525,7 @@ -- reasons, see 'modelEval'. type EvalAst m a = Model -> AST -> m (Maybe a) --- | An alias for 'modelEval'.+-- | An alias for 'modelEval' with model completion enabled. eval :: MonadZ3 z3 => EvalAst z3 AST eval = liftFun2 Base.eval
test/Spec.hs view
@@ -1,1 +1,11 @@-{-# OPTIONS_GHC -F -pgmF hspec-discover #-}++import Test.Hspec++import qualified Z3.Base.Spec++main :: IO ()+main = hspec spec++spec :: Spec+spec = do+ describe "Z3.Base" Z3.Base.Spec.spec
+ test/Z3/Base/Spec.hs view
@@ -0,0 +1,49 @@+-- TODO: Create a context for all the tests, use push; ...; pop to rollback++module Z3.Base.Spec+ ( spec )+ where++import Test.Hspec+import Test.QuickCheck ( property )+import Test.QuickCheck.Monadic++import qualified Z3.Base as Z3++withContext :: ActionWith Z3.Context -> IO ()+withContext k = do+ ctx <- Z3.withConfig Z3.mkContext+ k ctx++anyZ3Error :: Selector Z3.Z3Error+anyZ3Error = const True++spec :: Spec+spec = around withContext $ do++ context "Propositional Logic and Equality" $ do++ specify "mkBool" $ \ctx -> property $ \b ->+ monadicIO $ do+ x::Maybe Bool <- run $ do+ ast <- Z3.mkBool ctx b+ Z3.getBoolValue ctx ast+ assert $ x == Just b++ context "Numerals" $ do++ specify "mkInt" $ \ctx -> property $ \(i :: Integer) ->+ monadicIO $ do+ x::Integer <- run $ do+ ast <- Z3.mkInteger ctx i;+ Z3.getInt ctx ast;+ assert $ x == i++ context "Bit-vectors" $ do++ specify "mkBvmul" $ \ctx ->+ let bad = do+ x <- Z3.mkFreshIntVar ctx "x";+ Z3.mkBvmul ctx x x+ in bad `shouldThrow` anyZ3Error+
z3.cabal view
@@ -1,5 +1,5 @@ Name: z3-Version: 4.0.0+Version: 4.1.0 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the (now open source!) Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -110,7 +110,9 @@ Main-is: Spec.hs + Other-modules: Z3.Base.Spec+ Build-depends: base >= 4.5,- z3 >= 0.4,+ z3 == 4.*, hspec >= 2.1, QuickCheck >= 2.5.1