z3 4.2.0 → 4.3
raw patch · 7 files changed
+472/−29 lines, 7 filesdep ~z3
Dependency ranges changed: z3
Files
- CHANGES.md +17/−0
- README.md +3/−3
- examples/Examples.hs +4/−0
- src/Z3/Base.hs +135/−5
- src/Z3/Base/C.hsc +152/−11
- src/Z3/Monad.hs +153/−3
- z3.cabal +8/−7
CHANGES.md view
@@ -1,6 +1,23 @@ # Release Notes +## 4.3++### Fixes++* Fixed memory leak due to typo in ```Z3.Base.C```. (Deian Stefan)++### New API support++* Added partial support for _Fixedpoint_ API. (David Heath)+* Added more bindings to the _Models_ API. (Daniel Gröber)+* Added _Parser interface_ API. (Tristan Knoth)++### Misc++* After many requests, I have moved the repository to GitHub: https://github.com/IagoAbal/haskell-z3.+* From now on the revision number (aka patch level) 0 will be omitted (so x.y instead of x.y.0).+ ## 4.2.0 This release removes support for SMT-LIB 1.x in order to be compatible with Z3 4.6.
README.md view
@@ -5,11 +5,11 @@ We don't provide any high-level interface (e.g. in the form of a Haskell eDSL) here, these bindings are targeted to those who want to build verification tools on top of Z3 in Haskell. -[Changelog here.](https://bitbucket.org/iago/z3-haskell/src/tip/CHANGES.md)+[Changelog here.](blob/master/CHANGES.md) -[Examples here.](https://bitbucket.org/iago/z3-haskell/src/tip/examples)+[Examples here.](tree/master/examples) -[Do you want to contribute?](https://bitbucket.org/iago/z3-haskell/src/tip/HACKING.md)+[Do you want to contribute?](blob/master/HACKING.md) ## Installation
examples/Examples.hs view
@@ -11,6 +11,7 @@ import qualified Example.Monad.ToSMTLib import qualified Example.Monad.Tuple import qualified Example.Monad.Interpolation+import qualified Example.Monad.ParserInterface import System.Environment @@ -44,6 +45,9 @@ ) , ("tuple" , Example.Monad.Tuple.run+ )+ , ("parserInterface"+ , Example.Monad.ParserInterface.run ) ]
src/Z3/Base.hs view
@@ -308,8 +308,18 @@ -- * Models , modelEval , evalArray+ , getConstInterp , getFuncInterp+ , hasInterp+ , numConsts+ , numFuncs+ , getConstDecl+ , getFuncDecl+ , getConsts+ , getFuncs , isAsArray+ , addFuncInterp+ , addConstInterp , getAsArrayFuncDecl , funcInterpGetNumEntries , funcInterpGetEntry@@ -359,6 +369,11 @@ , funcDeclToString , benchmarkToSMTLibString + -- * Parser interface+ , parseSMTLib2String+ , parseSMTLib2File+ , getParserError+ -- * Error Handling , Z3Error(..) , Z3ErrorCode(..)@@ -367,6 +382,18 @@ , Version(..) , getVersion + -- * Fixedpoint+ , Fixedpoint (..)+ , mkFixedpoint+ , fixedpointPush+ , fixedpointPop+ , fixedpointAddRule+ , fixedpointSetParams+ , fixedpointRegisterRelation+ , fixedpointQueryRelations+ , fixedpointGetAnswer+ , fixedpointGetAssertions+ -- * Interpolation , InterpolationProblem(..) , mkInterpolant@@ -405,7 +432,7 @@ import Control.Applicative ( (<$>), (<*>), (<*), pure ) import Control.Exception ( Exception, bracket, throw )-import Control.Monad ( join, when, (>=>) )+import Control.Monad ( join, when, (>=>), forM ) import Data.Fixed ( Fixed, HasResolution ) import Data.Int import Data.IORef ( IORef, newIORef, atomicModifyIORef' )@@ -2039,10 +2066,37 @@ peekAST _p False = return Nothing peekAST p True = fmap Just . c2h ctx =<< peek p --- TODO: Z3_model_get_const_interp+getConstInterp :: Context -> Model -> FuncDecl -> IO (Maybe AST)+getConstInterp ctx m fd = marshal z3_model_get_const_interp ctx $ \f ->+ h2c m $ \mPtr ->+ h2c fd $ \fdPtr ->+ f mPtr fdPtr --- TODO: Z3_model_has_interp+hasInterp :: Context -> Model -> FuncDecl -> IO Bool+hasInterp = liftFun2 z3_model_has_interp +numConsts :: Context -> Model -> IO Word+numConsts = liftFun1 z3_model_get_num_consts++numFuncs :: Context -> Model -> IO Word+numFuncs = liftFun1 z3_model_get_num_funcs++getConstDecl :: Context -> Model -> Word -> IO FuncDecl+getConstDecl = liftFun2 z3_model_get_const_decl++getFuncDecl :: Context -> Model -> Word -> IO FuncDecl+getFuncDecl = liftFun2 z3_model_get_func_decl++getConsts :: Context -> Model -> IO [FuncDecl]+getConsts ctx m = do+ n <- numConsts ctx m+ forM [0..n-1] $ \i -> getConstDecl ctx m i++getFuncs :: Context -> Model -> IO [FuncDecl]+getFuncs ctx m = do+ n <- numFuncs ctx m+ forM [0..n-1] $ \i -> getFuncDecl ctx m i+ -- | Evaluate an array as a function, if possible. evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel) evalArray ctx model array =@@ -2071,7 +2125,13 @@ isAsArray :: Context -> AST -> IO Bool isAsArray = liftFun1 z3_is_as_array +addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp+addFuncInterp = liftFun3 z3_add_func_interp +addConstInterp :: Context -> Model -> FuncDecl -> AST -> IO ()+addConstInterp = liftFun3 z3_add_const_interp++ getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)] getMapFromInterp ctx interp = do n <- funcInterpGetNumEntries ctx interp@@ -2352,8 +2412,42 @@ --------------------------------------------------------------------- -- Parser interface --- TODO+parseSMTLib2String :: Context+ -> String -- ^ string to parse+ -> [Symbol] -- ^ sort names+ -> [Sort] -- ^ sorts+ -> [Symbol] -- ^ declaration names+ -> [FuncDecl] -- ^ declarations+ -> IO AST+parseSMTLib2String ctx str sortNames sorts declNames decls =+ marshal z3_parse_smtlib2_string ctx $ \f ->+ withCString str $ \cstr ->+ marshalArrayLen sorts $ \sortNum sortArr ->+ marshalArray sortNames $ \sortNameArr ->+ marshalArrayLen decls $ \declNum declArr ->+ marshalArray declNames $ \declNameArr ->+ f cstr sortNum sortNameArr sortArr declNum declNameArr declArr +parseSMTLib2File :: Context+ -> String -- ^ file name+ -> [Symbol] -- ^ sort names+ -> [Sort] -- ^ sorts+ -> [Symbol] -- ^ declaration names+ -> [FuncDecl] -- ^ declarations+ -> IO AST+parseSMTLib2File ctx file sortNames sorts declNames decls =+ marshal z3_parse_smtlib2_string ctx $ \f ->+ withCString file $ \fileName ->+ marshalArrayLen sorts $ \sortNum sortArr ->+ marshalArray sortNames $ \sortNameArr ->+ marshalArrayLen decls $ \declNum declArr ->+ marshalArray declNames $ \declNameArr ->+ f fileName sortNum sortNameArr sortArr declNum declNameArr declArr+++getParserError :: Context -> IO String+getParserError = liftFun0 z3_get_parser_error+ --------------------------------------------------------------------- -- Error handling @@ -2443,7 +2537,43 @@ --------------------------------------------------------------------- -- Fixedpoint facilities --- TODO+newtype Fixedpoint = Fixedpoint { unFixedpoint :: ForeignPtr Z3_fixedpoint }+ deriving Eq++instance Marshal Fixedpoint (Ptr Z3_fixedpoint) where+ c2h = mkC2hRefCount Fixedpoint z3_fixedpoint_inc_ref z3_fixedpoint_dec_ref+ h2c fp = withForeignPtr (unFixedpoint fp)++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++fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO ()+fixedpointSetParams = liftFun2 z3_fixedpoint_set_params++fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO ()+fixedpointRegisterRelation = liftFun2 z3_fixedpoint_register_relation++fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result+fixedpointQueryRelations ctx fixedpoint fds =+ marshal z3_fixedpoint_query_relations ctx $ \f ->+ h2c fixedpoint $ \fixedpointPtr ->+ marshalArrayLen fds $ \fdsNum fdsArr ->+ f fixedpointPtr fdsNum fdsArr++fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST+fixedpointGetAnswer = liftFun1 z3_fixedpoint_get_answer++fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST]+fixedpointGetAssertions = liftFun1 z3_fixedpoint_get_assertions -- AST vectors ?
src/Z3/Base/C.hsc view
@@ -66,6 +66,8 @@ data Z3_func_entry +data Z3_fixedpoint+ data Z3_solver data Z3_params@@ -202,7 +204,7 @@ z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga9cd52225142c085630495044acc68bd2>-foreign import ccall unsafe "Z3_inc_ref"+foreign import ccall unsafe "Z3_dec_ref" z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () ---------------------------------------------------------------------@@ -247,7 +249,10 @@ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafe617994cce1b516f46128e448c84445> foreign import ccall unsafe "Z3_mk_array_sort"- z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort)+ z3_mk_array_sort :: Ptr Z3_context+ -> Ptr Z3_sort -- ^ domain+ -> Ptr Z3_sort -- ^ range+ -> IO (Ptr Z3_sort) -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1> foreign import ccall unsafe "Z3_mk_tuple_sort"@@ -654,11 +659,18 @@ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67> foreign import ccall unsafe "Z3_mk_select"- z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)+ z3_mk_select :: Ptr Z3_context+ -> Ptr Z3_ast -- ^ aray+ -> Ptr Z3_ast -- ^ index+ -> IO (Ptr Z3_ast) -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593> foreign import ccall unsafe "Z3_mk_store"- z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)+ z3_mk_store :: Ptr Z3_context+ -> Ptr Z3_ast -- ^ array+ -> Ptr Z3_ast -- ^ index+ -> Ptr Z3_ast -- ^ value to store at array[index]+ -> IO (Ptr Z3_ast) -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d> foreign import ccall unsafe "Z3_mk_const_array"@@ -686,7 +698,7 @@ -- | Reference: <http://z3prover.github.io/api/html/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://z3prover.github.io/api/html/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)@@ -996,6 +1008,55 @@ -> Ptr (Ptr Z3_ast) -> IO Z3_bool +-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga01bc2993f3eb358f7bd3b2d2d4cf5e51+foreign import ccall unsafe "Z3_model_get_const_interp"+ z3_model_get_const_interp :: Ptr Z3_context+ -> Ptr Z3_model+ -> Ptr Z3_func_decl+ -> IO (Ptr Z3_ast)+++-- | Reference: https://z3prover.github.io/api/html/group__capi.html#gaf5e9adb229e98b29cbeb7cebf41433a3+foreign import ccall unsafe "Z3_model_get_func_interp"+ z3_model_get_func_interp :: Ptr Z3_context+ -> Ptr Z3_model+ -> Ptr Z3_func_decl+ -> IO (Ptr Z3_func_interp)+++-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga3c7f8f6ce7c9f30710d3b73fa091f6b3+foreign import ccall unsafe "Z3_model_has_interp"+ z3_model_has_interp :: Ptr Z3_context+ -> Ptr Z3_model+ -> Ptr Z3_func_decl+ -> IO Z3_bool++-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga3ff26c1c0f55d17ebf2c152a74eac743+foreign import ccall unsafe "Z3_model_get_num_consts"+ z3_model_get_num_consts :: Ptr Z3_context+ -> Ptr Z3_model+ -> IO CUInt++-- | Reference: https://z3prover.github.io/api/html/group__capi.html#gaab062a06c0789b432885f4813dd9633b+foreign import ccall unsafe "Z3_model_get_num_funcs"+ z3_model_get_num_funcs :: Ptr Z3_context+ -> Ptr Z3_model+ -> IO CUInt++-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga8e70ac56fe6748301b7776191395184a+foreign import ccall unsafe "Z3_model_get_const_decl"+ z3_model_get_const_decl :: Ptr Z3_context+ -> Ptr Z3_model+ -> CUInt+ -> IO (Ptr Z3_func_decl)++-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga2a1a4524289574ae34ce2eecdade84d7+foreign import ccall unsafe "Z3_model_get_func_decl"+ z3_model_get_func_decl :: Ptr Z3_context+ -> Ptr Z3_model+ -> CUInt+ -> IO (Ptr Z3_func_decl)+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4674da67d226bfb16861829b9f129cfa> foreign import ccall unsafe "Z3_is_as_array" z3_is_as_array :: Ptr Z3_context@@ -1008,13 +1069,22 @@ -> Ptr Z3_ast -> IO (Ptr Z3_func_decl) --- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>-foreign import ccall unsafe "Z3_model_get_func_interp"- z3_model_get_func_interp :: Ptr Z3_context- -> Ptr Z3_model- -> Ptr Z3_func_decl- -> IO (Ptr Z3_func_interp)+-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga1f30176bce864257bebb1fb30a103779+foreign import ccall unsafe "Z3_add_func_interp"+ z3_add_func_interp :: Ptr Z3_context+ -> Ptr Z3_model+ -> Ptr Z3_func_decl+ -> Ptr Z3_ast+ -> IO (Ptr Z3_func_interp) +-- | Reference: https://z3prover.github.io/api/html/group__capi.html#ga73b1de0ec17bb4f2e47d256a7628925c+foreign import ccall unsafe "Z3_add_const_interp"+ z3_add_const_interp :: Ptr Z3_context+ -> Ptr Z3_model+ -> Ptr Z3_func_decl+ -> Ptr Z3_ast+ -> IO ()+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga80218e1d50bdc4dac5ba18bd13a8ddfb> foreign import ccall unsafe "Z3_func_interp_inc_ref" z3_func_interp_inc_ref :: Ptr Z3_context@@ -1380,6 +1450,37 @@ -> IO Z3_string ---------------------------------------------------------------------+-- * Parser Interface++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga74e6e5107c4143be3929e80bdaf73d6d>+foreign import ccall unsafe "Z3_parse_smtlib2_string"+ z3_parse_smtlib2_string :: Ptr Z3_context+ -> Z3_string+ -> CUInt+ -> Ptr (Ptr Z3_symbol)+ -> Ptr (Ptr Z3_sort)+ -> CUInt+ -> Ptr (Ptr Z3_symbol)+ -> Ptr (Ptr Z3_func_decl)+ -> IO (Ptr Z3_ast)++-- | Referece <http://z3prover.github.io/api/html/group__capi.html#ga6168be4babb03fbbccff1fa7df451300>+foreign import ccall unsafe "Z3_parse_smtlib2_file"+ z3_parse_smtlib2_file :: Ptr Z3_context+ -> Z3_string+ -> CUInt+ -> Ptr (Ptr Z3_symbol)+ -> Ptr (Ptr Z3_sort)+ -> CUInt+ -> Ptr (Ptr Z3_symbol)+ -> Ptr (Ptr Z3_func_decl)+ -> IO (Ptr Z3_ast)++-- | Referece <http://z3prover.github.io/api/html/group__capi.html#ga96b11da43464071c4ec35418d1cc3483>+foreign import ccall unsafe "Z3_get_parser_error"+ z3_get_parser_error :: Ptr Z3_context -> IO Z3_string++--------------------------------------------------------------------- -- * Error Handling -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8ac771e68b28d2c86f40aa84889b3807>@@ -1408,3 +1509,43 @@ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga45fcd18a00379b13a536c5b6117190ae> foreign import ccall unsafe "Z3_get_version" z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO ()++---------------------------------------------------------------------+-- * Fixedpoint facilities++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 ()++foreign import ccall unsafe "Z3_fixedpoint_dec_ref"+ z3_fixedpoint_dec_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()++foreign import ccall unsafe "Z3_fixedpoint_set_params"+ z3_fixedpoint_set_params :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_params -> IO ()++foreign import ccall unsafe "Z3_fixedpoint_add_rule"+ z3_fixedpoint_add_rule :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_ast -> Ptr Z3_symbol -> IO ()++foreign import ccall unsafe "Z3_fixedpoint_register_relation"+ z3_fixedpoint_register_relation :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_func_decl -> IO ()++foreign import ccall unsafe "Z3_fixedpoint_get_answer"+ z3_fixedpoint_get_answer :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_fixedpoint_get_assertions"+ z3_fixedpoint_get_assertions :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast_vector)++foreign import ccall unsafe "Z3_fixedpoint_query_relations"+ z3_fixedpoint_query_relations :: Ptr Z3_context+ -> Ptr Z3_fixedpoint+ -> CUInt+ -> Ptr (Ptr Z3_func_decl)+ -> IO Z3_lbool
src/Z3/Monad.hs view
@@ -267,8 +267,18 @@ -- * Models , modelEval , evalArray+ , getConstInterp , getFuncInterp+ , hasInterp+ , numConsts+ , numFuncs+ , getConstDecl+ , getFuncDecl+ , getConsts+ , getFuncs , isAsArray+ , addFuncInterp+ , addConstInterp , getAsArrayFuncDecl , funcInterpGetNumEntries , funcInterpGetEntry@@ -318,6 +328,11 @@ , funcDeclToString , benchmarkToSMTLibString + -- * Parser interface+ , parseSMTLib2String+ , parseSMTLib2File+ , getParserError+ -- * Error Handling , Base.Z3Error(..) , Base.Z3ErrorCode(..)@@ -326,6 +341,17 @@ , Version(..) , getVersion + -- * Fixedpoint+ , Fixedpoint+ , fixedpointPush+ , fixedpointPop+ , fixedpointAddRule+ , fixedpointSetParams+ , fixedpointRegisterRelation+ , fixedpointQueryRelations+ , fixedpointGetAnswer+ , fixedpointGetAssertions+ -- * Interpolation , Base.InterpolationProblem(..) , mkInterpolant@@ -387,6 +413,7 @@ , Version(..) , Params , Solver+ , Fixedpoint , SortKind(..) , ASTKind(..) , Tactic@@ -433,6 +460,12 @@ -> a -> b -> c -> d -> z3 e liftFun4 f a b c d = getContext >>= \ctx -> liftIO (f ctx a b c d) +liftFun5 :: MonadZ3 z3 =>+ (Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> IO b)+ -> a1 -> a2 -> a3 -> a4 -> a5-> z3 b+liftFun5 f x1 x2 x3 x4 x5 =+ getContext >>= \ctx -> liftIO (f ctx x1 x2 x3 x4 x5)+ liftFun6 :: MonadZ3 z3 => (Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO b) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> z3 b@@ -460,6 +493,27 @@ slv <- getSolver liftIO $ f ctx slv a b +liftFixedpoint0 :: MonadFixedpoint z3 =>+ (Base.Context -> Base.Fixedpoint -> IO b)+ -> z3 b+liftFixedpoint0 f_s =+ do ctx <- getContext+ liftIO . f_s ctx =<< getFixedpoint++liftFixedpoint1 :: MonadFixedpoint z3 =>+ (Base.Context -> Base.Fixedpoint -> a -> IO b)+ -> a -> z3 b+liftFixedpoint1 f_s a =+ do ctx <- getContext+ liftIO . (\s -> f_s ctx s a) =<< getFixedpoint++liftFixedpoint2 :: MonadFixedpoint z3 => (Base.Context -> Base.Fixedpoint -> a -> b -> IO c)+ -> a -> b -> z3 c+liftFixedpoint2 f a b = do+ ctx <- getContext+ slv <- getFixedpoint+ liftIO $ f ctx slv a b+ ------------------------------------------------- -- A simple Z3 monad. @@ -469,14 +523,18 @@ -- | Z3 environment. data Z3Env = Z3Env {- envSolver :: Base.Solver- , envContext :: Base.Context+ envSolver :: Base.Solver+ , envContext :: Base.Context+ , envFixedpoint :: Base.Fixedpoint } instance MonadZ3 Z3 where getSolver = Z3 $ asks envSolver getContext = Z3 $ asks envContext +instance MonadFixedpoint Z3 where+ getFixedpoint = Z3 $ asks envFixedpoint+ -- | Eval a Z3 script. evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a evalZ3With mbLogic opts (Z3 s) = do@@ -494,7 +552,8 @@ setOpts cfg opts ctx <- mkContext cfg solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic- return $ Z3Env solver ctx+ fixedpoint <- Base.mkFixedpoint ctx+ return $ Z3Env solver ctx fixedpoint -- | Create a new Z3 environment. newEnv :: Maybe Logic -> Opts -> IO Z3Env@@ -1647,6 +1706,9 @@ evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel) evalArray = liftFun2 Base.evalArray +getConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe AST)+getConstInterp = liftFun2 Base.getConstInterp+ -- | Return the interpretation of the function f in the model m. -- Return NULL, if the model does not assign an interpretation for f. -- That should be interpreted as: the f does not matter.@@ -1655,6 +1717,27 @@ getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp) getFuncInterp = liftFun2 Base.getFuncInterp +hasInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 Bool+hasInterp = liftFun2 Base.hasInterp++numConsts :: MonadZ3 z3 => Model -> z3 Word+numConsts = liftFun1 Base.numConsts++numFuncs :: MonadZ3 z3 => Model -> z3 Word+numFuncs = liftFun1 Base.numFuncs++getConstDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl+getConstDecl = liftFun2 Base.getConstDecl++getFuncDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl+getFuncDecl = liftFun2 Base.getFuncDecl++getConsts :: MonadZ3 z3 => Model -> z3 [FuncDecl]+getConsts = liftFun1 Base.getConsts++getFuncs :: MonadZ3 z3 => Model -> z3 [FuncDecl]+getFuncs = liftFun1 Base.getFuncs+ -- | The (_ as-array f) AST node is a construct for assigning interpretations -- for arrays in Z3. It is the array such that forall indices i we have that -- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE@@ -1664,6 +1747,13 @@ isAsArray :: MonadZ3 z3 => AST -> z3 Bool isAsArray = liftFun1 Base.isAsArray +addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp+addFuncInterp = liftFun3 Base.addFuncInterp++addConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 ()+addConstInterp = liftFun3 Base.addConstInterp++ -- | Return the function declaration f associated with a (_ as_array f) node. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>@@ -1870,13 +1960,73 @@ -> z3 String benchmarkToSMTLibString = liftFun6 Base.benchmarkToSMTLibString + ---------------------------------------------------------------------+-- Parser interface++-- | Parse SMT expressions from a string+--+-- The sort and declaration arguments allow parsing in a context in which variables and functions have already been declared. They are almost never used.+parseSMTLib2String :: MonadZ3 z3 =>+ String -- ^ string to parse+ -> [Symbol] -- ^ sort names+ -> [Sort] -- ^ sorts+ -> [Symbol] -- ^ declaration names+ -> [FuncDecl] -- ^ declarations+ -> z3 AST+parseSMTLib2String = liftFun5 Base.parseSMTLib2String++-- | Parse SMT expressions from a file+--+-- The sort and declaration arguments allow parsing in a context in which variables and functions have already been declared. They are almost never used.+parseSMTLib2File :: MonadZ3 z3 =>+ String -- ^ string to parse+ -> [Symbol] -- ^ sort names+ -> [Sort] -- ^ sorts+ -> [Symbol] -- ^ declaration names+ -> [FuncDecl] -- ^ declarations+ -> z3 AST+parseSMTLib2File = liftFun5 Base.parseSMTLib2File++getParserError :: MonadZ3 z3 => z3 String+getParserError = liftScalar Base.getParserError++--------------------------------------------------------------------- -- Miscellaneous -- | Return Z3 version number information. getVersion :: MonadZ3 z3 => z3 Version getVersion = liftIO Base.getVersion +---------------------------------------------------------------------+-- Fixedpoint++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++fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 ()+fixedpointSetParams = liftFixedpoint1 Base.fixedpointSetParams++fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 ()+fixedpointRegisterRelation = liftFixedpoint1 Base.fixedpointRegisterRelation++fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result+fixedpointQueryRelations = liftFixedpoint1 Base.fixedpointQueryRelations++fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST+fixedpointGetAnswer = liftFixedpoint0 Base.fixedpointGetAnswer++fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST]+fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions --------------------------------------------------------------------- -- * Interpolation
z3.cabal view
@@ -1,5 +1,5 @@ Name: z3-Version: 4.2.0+Version: 4.3 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -11,9 +11,9 @@ . * "Z3.Monad" provides a convenient monadic wrapper for the common usage scenario. .- Examples: <https://bitbucket.org/iago/z3-haskell/src/tip/examples>+ Examples: <https://github.com/IagoAbal/haskell-z3/tree/master/examples> .- Changelog: <https://bitbucket.org/iago/z3-haskell/src/tip/CHANGES.md>+ Changelog: <https://github.com/IagoAbal/haskell-z3/blob/master/CHANGES.md> . Installation: .@@ -23,7 +23,8 @@ . (Hackage reports a build failure because Z3's library is missing.) -Homepage: http://bitbucket.org/iago/z3-haskell+Homepage: https://github.com/IagoAbal/haskell-z3+Bug-reports: https://github.com/IagoAbal/haskell-z3/issues License: BSD3 License-file: LICENSE Author: Iago Abal <mail@iagoabal.eu>,@@ -37,8 +38,8 @@ Extra-source-files: README.md CHANGES.md HACKING.md source-repository head- type: mercurial- location: https://bitbucket.org/iago/z3-haskell+ type: git+ location: git@github.com:IagoAbal/haskell-z3.git Library hs-source-dirs: src@@ -89,7 +90,7 @@ if flag(examples) Buildable: True Build-depends: base >=4.5,- z3 >=0.4,+ z3, containers, mtl >2.1 else