diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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, diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -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 - diff --git a/src/Z3/Base/C.hsc b/src/Z3/Base/C.hsc --- a/src/Z3/Base/C.hsc +++ b/src/Z3/Base/C.hsc @@ -249,6 +249,10 @@ -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_sort) + +-- | Reference: +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: +foreign import ccall unsafe "Z3_mk_empty_set" + z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) + +-- | Reference: +foreign import ccall unsafe "Z3_mk_full_set" + z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) + +-- | Reference: +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: +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: +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: +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: +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: +foreign import ccall unsafe "Z3_mk_set_complement" + z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Reference: +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: +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: -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: +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: foreign import ccall unsafe "Z3_is_as_array" diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: +-- +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: +mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST +mkEmptySet = liftFun1 Base.mkEmptySet + +-- | Create the full set. +-- +-- Reference: +mkFullSet :: MonadZ3 z3 => Sort -> z3 AST +mkFullSet = liftFun1 Base.mkFullSet + +-- | Add an element to a set. +-- +-- Reference: +mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST +mkSetAdd = liftFun2 Base.mkSetAdd + +-- | Remove an element from a set. +-- +-- Reference: +mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST +mkSetDel = liftFun2 Base.mkSetDel + +-- | Take the union of a list of sets. +-- +-- Reference: +mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST +mkSetUnion = liftFun1 Base.mkSetUnion + +-- | Take the intersection of a list of sets. +-- +-- Reference: +mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST +mkSetIntersect = liftFun1 Base.mkSetIntersect + +-- | Take the set difference between two sets. +-- +-- Reference: +mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST +mkSetDifference = liftFun2 Base.mkSetDifference + +-- | Take the complement of a set. +-- +-- Reference: +mkSetComplement :: MonadZ3 z3 => AST -> z3 AST +mkSetComplement = liftFun1 Base.mkSetComplement + +-- | Check for set membership. +-- +-- Reference: +mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST +mkSetMember = liftFun2 Base.mkSetMember + +-- | Check if the first set is a subset of the second set. +-- +-- Reference: +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 diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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 diff --git a/test/Z3/Base/Spec.hs b/test/Z3/Base/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Z3/Base/Spec.hs @@ -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 + diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -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