diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/examples/Examples.hs b/examples/Examples.hs --- a/examples/Examples.hs +++ b/examples/Examples.hs @@ -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 ) ] diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -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 ? 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 @@ -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: -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: 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: foreign import ccall unsafe "Z3_mk_tuple_sort" @@ -654,11 +659,18 @@ -- | Reference: 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: 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: foreign import ccall unsafe "Z3_mk_const_array" @@ -686,7 +698,7 @@ -- | 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) @@ -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: 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: -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: 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: +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 +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 +foreign import ccall unsafe "Z3_get_parser_error" + z3_get_parser_error :: Ptr Z3_context -> IO Z3_string + +--------------------------------------------------------------------- -- * Error Handling -- | Reference: @@ -1408,3 +1509,43 @@ -- | Reference: 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 diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: @@ -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 diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -11,9 +11,9 @@ . * "Z3.Monad" provides a convenient monadic wrapper for the common usage scenario. . - Examples: + Examples: . - Changelog: + Changelog: . 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 , @@ -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