diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -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 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 @@ -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: +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: +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: foreign import ccall unsafe "Z3_get_as_array_func_decl" z3_get_as_array_func_decl :: Ptr Z3_context @@ -1451,11 +1462,7 @@ -- | Reference: foreign import ccall unsafe "Z3_get_error_msg" - z3_get_error_msg :: Z3_error_code -> IO Z3_string - --- | Reference: -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 () diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: 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 diff --git a/test/Z3/Base/Spec.hs b/test/Z3/Base/Spec.hs --- a/test/Z3/Base/Spec.hs +++ b/test/Z3/Base/Spec.hs @@ -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 - diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -30,7 +30,7 @@ Author: Iago Abal , David Castro Maintainer: Iago Abal -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