z3 408.0 → 408.1
raw patch · 7 files changed
+99/−34 lines, 7 filesdep +semigroups
Dependencies added: semigroups
Files
- CHANGES.md +9/−0
- README.md +12/−0
- src/Z3/Base.hs +16/−9
- src/Z3/Base/C.hsc +12/−11
- src/Z3/Monad.hs +11/−11
- test/Z3/Base/Spec.hs +35/−1
- z3.cabal +4/−2
CHANGES.md view
@@ -1,6 +1,15 @@ # Release Notes +## 408.1++* Added bindings to `substitute` and `isEqAST`. (Hengchu Zhang)+* Added `MonadFail` instance for `Z3`, required by GHC >=8.6. (Conal Elliott)+* Updated `Z3_get_error_msg` signature (Z3 C API 4.8.7). (Kevin Quick)+* Removed bindings to `Z3_fixedpoint_push` and `Z3_fixedpoint_pop` (Z3 C API 4.8.5). (Eric Walkingshaw)+* Replaced `z3_get_error_msg_ex` with `z3_get_error_msg` (Z3 C API 4.8.5). (Alexander Knauth)+* Added semigroups to dependencies for GHC <= 7. (Hogeyama)+ ## 408.0 * Enabled support for Z3 4.8. (Carlo Nucera)
README.md view
@@ -11,6 +11,18 @@ [Do you want to contribute?](HACKING.md) +## State of maintenance++The library is currently "maintained", meaning that I try to be responsive to new+issues and pull requests.+Unfortunately I do not have time to investigate issues or to do major work myself.+I do try to help those who want to contribute.++If someone demonstrates willingness to maintain the library more actively+in the long run, then I will be very happy to give the required permissions+to become a co-maintainer.+In the meantime I will do my best to keep it alive.+ ## Supported versions and version policy Z3 releases come out often and sometimes introduce backwards incompatible changes.
src/Z3/Base.hs view
@@ -307,6 +307,7 @@ -- * Modifiers , substituteVars+ , substitute -- * Models , modelEval@@ -321,6 +322,7 @@ , getConsts , getFuncs , isAsArray+ , isEqAST , addFuncInterp , addConstInterp , getAsArrayFuncDecl@@ -387,8 +389,6 @@ -- * Fixedpoint , Fixedpoint (..) , mkFixedpoint- , fixedpointPush- , fixedpointPop , fixedpointAddRule , fixedpointSetParams , fixedpointRegisterRelation@@ -2044,6 +2044,16 @@ marshalArrayLen vars $ \varsNum varsArr -> f aPtr varsNum varsArr +substitute :: Context -> AST -> [(AST, AST)] -> IO AST+substitute ctx a substs =+ let froms = map fst substs+ tos = map snd substs+ in marshal z3_substitute ctx $ \f ->+ h2c a $ \aPtr ->+ marshalArrayLen froms $ \fromsLen fromsArr ->+ marshalArray tos $ \ tosArr ->+ f aPtr fromsLen fromsArr tosArr+ --------------------------------------------------------------------- -- Models @@ -2130,6 +2140,9 @@ isAsArray :: Context -> AST -> IO Bool isAsArray = liftFun1 z3_is_as_array +isEqAST :: Context -> AST -> AST -> IO Bool+isEqAST = liftFun2 z3_is_eq_ast+ addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp addFuncInterp = liftFun3 z3_add_func_interp @@ -2498,7 +2511,7 @@ checkError :: Ptr Z3_context -> IO a -> IO a checkError cPtr m = do m <* (z3_get_error_code cPtr >>= throwZ3Exn)- where getErrStr i = peekCString =<< z3_get_error_msg_ex cPtr i+ where getErrStr i = peekCString =<< z3_get_error_msg cPtr i throwZ3Exn i = when (i /= z3_ok) $ getErrStr i >>= z3Error (toZ3Error i) ---------------------------------------------------------------------@@ -2548,12 +2561,6 @@ mkFixedpoint :: Context -> IO Fixedpoint mkFixedpoint = liftFun0 z3_mk_fixedpoint--fixedpointPush :: Context -> Fixedpoint -> IO ()-fixedpointPush = liftFun1 z3_fixedpoint_push--fixedpointPop :: Context -> Fixedpoint -> IO ()-fixedpointPop = liftFun1 z3_fixedpoint_pop fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO () fixedpointAddRule = liftFun3 z3_fixedpoint_add_rule
src/Z3/Base/C.hsc view
@@ -969,6 +969,10 @@ foreign import ccall unsafe "Z3_substitute_vars" z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) +-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga0f8ba9b735388e010044b8a1d39c6af0>+foreign import ccall unsafe "Z3_substitute"+ z3_substitute :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)+ --------------------------------------------------------------------- -- * AST vectors @@ -1067,6 +1071,13 @@ -> Ptr Z3_ast -> IO Z3_bool +-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gabc6d17e7862f2db40c778409152e931f>+foreign import ccall unsafe "Z3_is_eq_ast"+ z3_is_eq_ast :: Ptr Z3_context+ -> Ptr Z3_ast+ -> Ptr Z3_ast+ -> IO Z3_bool+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda> foreign import ccall unsafe "Z3_get_as_array_func_decl" z3_get_as_array_func_decl :: Ptr Z3_context@@ -1451,11 +1462,7 @@ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6> foreign import ccall unsafe "Z3_get_error_msg"- z3_get_error_msg :: Z3_error_code -> IO Z3_string---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92>-foreign import ccall unsafe "Z3_get_error_msg_ex"- z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string+ z3_get_error_msg :: Ptr Z3_context -> Z3_error_code -> IO Z3_string --------------------------------------------------------------------- -- * Miscellaneous@@ -1469,12 +1476,6 @@ foreign import ccall unsafe "Z3_mk_fixedpoint" z3_mk_fixedpoint :: Ptr Z3_context -> IO (Ptr Z3_fixedpoint)--foreign import ccall unsafe "Z3_fixedpoint_push"- z3_fixedpoint_push :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()--foreign import ccall unsafe "Z3_fixedpoint_pop"- z3_fixedpoint_pop :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () foreign import ccall unsafe "Z3_fixedpoint_inc_ref" z3_fixedpoint_inc_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
src/Z3/Monad.hs view
@@ -1,4 +1,3 @@- {-# LANGUAGE GeneralizedNewtypeDeriving #-} -- |@@ -265,6 +264,7 @@ -- * Modifiers , substituteVars+ , substitute -- * Models , modelEval@@ -279,6 +279,7 @@ , getConsts , getFuncs , isAsArray+ , isEqAST , addFuncInterp , addConstInterp , getAsArrayFuncDecl@@ -344,8 +345,6 @@ -- * Fixedpoint , Fixedpoint- , fixedpointPush- , fixedpointPop , fixedpointAddRule , fixedpointSetParams , fixedpointRegisterRelation@@ -414,6 +413,7 @@ import Control.Applicative ( Applicative ) import Data.Fixed ( Fixed, HasResolution )+import Control.Monad.Fail import Control.Monad.IO.Class ( MonadIO, liftIO ) import Control.Monad.Trans.Reader ( ReaderT, runReaderT, asks ) import Control.Monad.Fix ( MonadFix )@@ -509,7 +509,7 @@ -- A simple Z3 monad. newtype Z3 a = Z3 { _unZ3 :: ReaderT Z3Env IO a }- deriving (Functor, Applicative, Monad, MonadIO, MonadFix)+ deriving (Functor, Applicative, Monad, MonadIO, MonadFix, MonadFail) -- | Z3 environment. data Z3Env@@ -1292,7 +1292,7 @@ mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST mkSelect = liftFun2 Base.mkSelect --- | Array update. +-- | Array update. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593> mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST@@ -1690,6 +1690,9 @@ substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST substituteVars = liftFun2 Base.substituteVars +substitute :: MonadZ3 z3 => AST -> [(AST, AST)] -> z3 AST+substitute = liftFun2 Base.substitute+ --------------------------------------------------------------------- -- Models @@ -1751,6 +1754,9 @@ isAsArray :: MonadZ3 z3 => AST -> z3 Bool isAsArray = liftFun1 Base.isAsArray +isEqAST :: MonadZ3 z3 => AST -> AST -> z3 Bool+isEqAST = liftFun2 Base.isEqAST+ addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp addFuncInterp = liftFun3 Base.addFuncInterp @@ -2004,12 +2010,6 @@ class MonadZ3 m => MonadFixedpoint m where getFixedpoint :: m Base.Fixedpoint--fixedpointPush :: MonadFixedpoint z3 => z3 ()-fixedpointPush = liftFixedpoint0 Base.fixedpointPush--fixedpointPop :: MonadFixedpoint z3 => z3 ()-fixedpointPop = liftFixedpoint0 Base.fixedpointPush fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 () fixedpointAddRule = liftFixedpoint2 Base.fixedpointAddRule
test/Z3/Base/Spec.hs view
@@ -39,6 +39,41 @@ Z3.getInt ctx ast; assert $ x == i + context "AST Equality and Substitution" $ do+ specify "isEqAST" $ \ctx ->+ monadicIO $ do+ (r1, r2) <- run $ do+ x1 <- Z3.mkFreshIntVar ctx "x1"+ x2 <- Z3.mkFreshIntVar ctx "x2"+ x3 <- Z3.mkFreshIntVar ctx "x3"++ s <- Z3.mkAdd ctx [x1, x2]+ s' <- Z3.mkAdd ctx [x1, x2]+ s23 <- Z3.mkAdd ctx [x2, x3]++ r1 <- Z3.isEqAST ctx s s'+ r2 <- Z3.isEqAST ctx s s23++ return (r1, r2)+ assert r1+ assert (not r2)++ specify "substitute" $ \ctx ->+ monadicIO $ do+ r <- run $ do+ x1 <- Z3.mkFreshIntVar ctx "x1"+ x2 <- Z3.mkFreshIntVar ctx "x2"+ x3 <- Z3.mkFreshIntVar ctx "x3"+ x4 <- Z3.mkFreshIntVar ctx "x4"++ s12 <- Z3.mkAdd ctx [x1, x2]+ s34 <- Z3.mkAdd ctx [x3, x4]++ s34' <- Z3.substitute ctx s12 [(x1, x3), (x2, x4)]++ Z3.isEqAST ctx s34 s34'+ assert r+ context "Bit-vectors" $ do specify "mkBvmul" $ \ctx ->@@ -46,4 +81,3 @@ x <- Z3.mkFreshIntVar ctx "x"; Z3.mkBvmul ctx x x in bad `shouldThrow` anyZ3Error-
z3.cabal view
@@ -1,5 +1,5 @@ Name: z3-Version: 408.0+Version: 408.1 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -30,7 +30,7 @@ Author: Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> Maintainer: Iago Abal <mail@iagoabal.eu>-Copyright: 2012-2018, Iago Abal, David Castro+Copyright: 2012-2019, Iago Abal, David Castro Category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors Build-type: Simple Cabal-version: >= 1.8@@ -60,6 +60,8 @@ Build-depends: base >= 4.5 && <5, containers, transformers >= 0.2+ if impl(ghc < 8)+ Build-depends: semigroups >= 0.5 Build-tools: hsc2hs Extensions: FlexibleInstances