packages feed

z3 4.3.1 → 408.0

raw patch · 13 files changed

+117/−312 lines, 13 filesdep +transformersdep −mtl

Dependencies added: transformers

Dependencies removed: mtl

Files

CHANGES.md view
@@ -1,9 +1,22 @@  # Release Notes +## 408.0++* Enabled support for Z3 4.8. (Carlo Nucera)+    - Required removing the Inteprolation API, `z3_get_parser_error` and other functions!+* Do not crash on empty lists. (M Farkas-Dyck)+* Added binding for `Z3_mk_finite_domain_sort`. (M Farkas-Dyck)+* Implemented workaround for `Z3.Base.toBool` to work on OS X. (Matthew Doty)++By the way, you have read correctly, this new version is _408.0_.+Find more details about the new version policy in the [README](README.md).+ ## 4.3.1 -* Fix compatibility with base 4.11 due to SMP (M Farkas-Dyck)+* Fixed compatibility with base 4.11 due to SMP. (M Farkas-Dyck)++NOTE: This version didn't make it into Hackage.  ## 4.3
README.md view
@@ -5,11 +5,25 @@ 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.](blob/master/CHANGES.md)+[Changelog here.](CHANGES.md) -[Examples here.](tree/master/examples)+[Examples here.](examples) -[Do you want to contribute?](blob/master/HACKING.md)+[Do you want to contribute?](HACKING.md)++## Supported versions and version policy++Z3 releases come out often and sometimes introduce backwards incompatible changes.+In order to avoid #ifdef-ery, we only try to support a reasonably recent version+of Z3, ideally the latest one.+We use semantic versioning to reflect which version(s) are supported:++    <z3-version>.<bindings-version>[.<patch-level>]++The `<z3-version>` indicates which version of Z3 is supported, it is computed as+_x*100+y_ for Z3 _x.y_. For example, versions _408.y.z_ of these bindings are+meant to support versions _4.8.*_ of Z3.+This version policy is in line with Haskell's PVP.  ## Installation
examples/Example/Monad/DataTypes.hs view
@@ -3,7 +3,7 @@ module Example.Monad.DataTypes where  import Z3.Monad-import Control.Monad.Trans (liftIO)+import Control.Monad.IO.Class (liftIO)  run :: IO () run = evalZ3 datatypeScript
− examples/Example/Monad/Interpolation.hs 
@@ -1,35 +0,0 @@--- | Compute interpolant for an unsatisfiable conjunction of formulas-module Example.Monad.Interpolation-  ( run )-  where--import Control.Monad-import Control.Monad.Trans ( liftIO )--import Z3.Monad--run :: IO ()-run = do-    env <- newItpEnv Nothing stdOpts-    evalZ3WithEnv z3 env--z3 = do-    a <- mkFreshBoolVar "a"-    b <- mkFreshBoolVar "b"--    na <- mkNot a-    nb <- mkNot b--    f1 <- mkIff a b-    f2 <- mkIff a nb--    g1 <- mkInterpolant f1-    g2 <- mkInterpolant f2-    g3 <- mkInterpolant =<< mkTrue--    params <- mkParams-    res <- flip computeInterpolant params =<< mkAnd [g1, g2, g3]--    case res of-        Just (Right itps) -> mapM_ (liftIO . putStrLn <=< astToString) itps-        otherwise         -> error "could not compute interpolants"
examples/Example/Monad/MutuallyRecursive.hs view
@@ -3,7 +3,7 @@ module Example.Monad.MutuallyRecursive where  import Z3.Monad-import Control.Monad.Trans (liftIO)+import Control.Monad.IO.Class (liftIO)  run :: IO () run = evalZ3 datatypeScript
examples/Example/Monad/QuantifierElimination.hs view
@@ -3,7 +3,7 @@   where  import Control.Monad-import Control.Monad.Trans ( liftIO )+import Control.Monad.IO.Class (liftIO)  import Z3.Monad
examples/Example/Monad/Quantifiers.hs view
@@ -3,7 +3,7 @@   where  import Control.Monad-import Control.Monad.Trans ( liftIO )+import Control.Monad.IO.Class (liftIO)  import Z3.Monad
examples/Example/Monad/ToSMTLib.hs view
@@ -5,7 +5,6 @@  import Control.Applicative import Control.Monad ( join )-import Control.Monad.Trans import Data.Maybe import qualified Data.Traversable as T
examples/Examples.hs view
@@ -10,7 +10,6 @@ import qualified Example.Monad.QuantifierElimination import qualified Example.Monad.ToSMTLib import qualified Example.Monad.Tuple-import qualified Example.Monad.Interpolation import qualified Example.Monad.ParserInterface  import System.Environment@@ -27,9 +26,6 @@     )   , ("funcModel"     , Example.Monad.FuncModel.run-    )-  , ("interpolation"-    , Example.Monad.Interpolation.run     )   , ("mutuallyRecursive"     , Example.Monad.MutuallyRecursive.run
src/Z3/Base.hs view
@@ -105,6 +105,7 @@   , mkIntSort   , mkRealSort   , mkBvSort+  , mkFiniteDomainSort   , mkArraySort   , mkTupleSort   , mkConstructor@@ -142,6 +143,7 @@   , mkAnd   , mkOr   , mkDistinct+  , mkDistinct1   -- ** Helpers   , mkBool @@ -149,6 +151,7 @@   , mkAdd   , mkMul   , mkSub+  , mkSub1   , mkUnaryMinus   , mkDiv   , mkMod@@ -372,7 +375,6 @@   -- * Parser interface   , parseSMTLib2String   , parseSMTLib2File-  , getParserError    -- * Error Handling   , Z3Error(..)@@ -394,17 +396,6 @@   , fixedpointGetAnswer   , fixedpointGetAssertions -  -- * Interpolation-  , InterpolationProblem(..)-  , mkInterpolant-  , mkInterpolationContext-  , getInterpolant-  , computeInterpolant-  , readInterpolationProblem-  , checkInterpolant-  , interpolationProfile-  , writeInterpolationProblem-   -- * Solvers   , Logic(..)   , mkSolver@@ -432,10 +423,12 @@  import Control.Applicative ( (<$>), (<*>), (<*), pure ) import Control.Exception ( Exception, bracket, throw )-import Control.Monad ( join, when, (>=>), forM )+import Control.Monad ( join, when, forM ) import Data.Fixed ( Fixed, HasResolution )+import Data.Foldable ( Foldable (..) ) import Data.Int import Data.IORef ( IORef, newIORef, atomicModifyIORef' )+import Data.List.NonEmpty (NonEmpty (..), nonEmpty) import Data.Maybe ( fromJust ) import Data.Ratio ( numerator, denominator, (%) ) import Data.Traversable ( Traversable )@@ -743,7 +736,9 @@   | i >= 0    = liftFun1 z3_mk_bv_sort c i   | otherwise = error "Z3.Base.mkBvSort: negative size" --- TODO: Z3_mk_finite_domain_sort+-- | Create a finite-domain type.+mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort+mkFiniteDomainSort = liftFun2 z3_mk_finite_domain_sort  -- | Create an array type --@@ -987,10 +982,16 @@ -- distinct. -- -- That is, @and [ args!!i /= args!!j | i <- [0..length(args)-1], j <- [i+1..length(args)-1] ]@+--+-- Requires a non-empty list. mkDistinct :: Context -> [AST] -> IO AST mkDistinct =-  liftAstN "Z3.Base.mkDistinct: empty list of expressions" z3_mk_distinct+  liftAstN_err "Z3.Base.mkDistinct: empty list of expressions" z3_mk_distinct +-- | Same as 'mkDistinct' but type-safe.+mkDistinct1 :: Context -> NonEmpty AST -> IO AST+mkDistinct1 = liftAstN1 z3_mk_distinct+ -- | Create an AST node representing /not(a)/. mkNot :: Context -> AST -> IO AST mkNot = liftFun1 z3_mk_not@@ -1013,13 +1014,11 @@  -- | Create an AST node representing args[0] and ... and args[num_args-1]. mkAnd :: Context -> [AST] -> IO AST-mkAnd ctx [] = mkTrue ctx-mkAnd ctx as = marshal z3_mk_and ctx $ marshalArrayLen as+mkAnd = liftAstN z3_mk_true z3_mk_and  -- | Create an AST node representing args[0] or ... or args[num_args-1]. mkOr :: Context -> [AST] -> IO AST-mkOr ctx [] = mkFalse ctx-mkOr ctx os = marshal z3_mk_or ctx $ marshalArrayLen os+mkOr = liftAstN z3_mk_false z3_mk_or  ------------------------------------------------- -- ** Helpers@@ -1034,16 +1033,22 @@  -- | Create an AST node representing args[0] + ... + args[num_args-1]. mkAdd :: Context -> [AST] -> IO AST-mkAdd = liftAstN "Z3.Base.mkAdd: empty list of expressions" z3_mk_add+mkAdd ctx = maybe (mkInteger ctx 0) (liftAstN1 z3_mk_add ctx) . nonEmpty  -- | Create an AST node representing args[0] * ... * args[num_args-1]. mkMul :: Context -> [AST] -> IO AST-mkMul = liftAstN "Z3.Base.mkMul: empty list of expressions" z3_mk_mul+mkMul ctx = maybe (mkInteger ctx 1) (liftAstN1 z3_mk_mul ctx) . nonEmpty  -- | Create an AST node representing args[0] - ... - args[num_args - 1].+--+-- Requires a non-empty list. mkSub :: Context -> [AST] -> IO AST-mkSub = liftAstN "Z3.Base.mkSub: empty list of expressions" z3_mk_sub+mkSub = liftAstN_err "Z3.Base.mkSub: empty list of expressions" z3_mk_sub +-- | Same as 'mkSub' but type-safe.+mkSub1 :: Context -> NonEmpty AST -> IO AST+mkSub1 = liftAstN1 z3_mk_sub+ -- | Create an AST node representing -arg. mkUnaryMinus :: Context -> AST -> IO AST mkUnaryMinus = liftFun1 z3_mk_unary_minus@@ -2445,9 +2450,6 @@       f fileName sortNum sortNameArr sortArr declNum declNameArr declArr  -getParserError :: Context -> IO String-getParserError = liftFun0 z3_get_parser_error- --------------------------------------------------------------------- -- Error handling @@ -2590,131 +2592,6 @@ -- TODO  ------------------------------------------------------------------------ Interpolation---- | Interpolation problem formulation.-data InterpolationProblem =-    InterpolationProblem {-      getConstraints    :: [AST]-    , getParents        :: Maybe [Int]-    , getTheoryTerms    :: [AST]-    }---- | Generate a Z3 context suitable for generation of interpolants.-mkInterpolationContext :: Config -> IO Context-mkInterpolationContext = mkContextWith z3_mk_interpolation_context---- | Create an AST node marking a formula position for interpolation.-mkInterpolant :: Context-              -> AST     -- ^ boolean expression-              -> IO AST-mkInterpolant = liftFun1 z3_mk_interpolant---- | Extracts interpolants from a proof of unsatisfiability.------ Interpolants are computed in pre-order for occurrences of 'mkInterpolant'--- within the second argument, which needs to be in form of a conjunction.-getInterpolant :: Context-               -> AST      -- ^ proof of /false/-               -> AST      -- ^ interpolation pattern (cf. 'mkInterpolant')-               -> Params-               -> IO [AST]-getInterpolant = liftFun3 z3_get_interpolant---- | Checks satisfiability of input conjunction.------ Returns either a model witnessing satisfiability, or a (sequence) interpolants--- between individual subformulae of the conjunction wrapped in 'mkInterpolant'.------ Result:--- /sat/     -> @Just (Left <model>)@--- /unsat/   -> @Just (Right <interp>)@--- /unknown/ -> @Nothing@-computeInterpolant :: Context -> AST -> Params-                   -> IO (Maybe (Either Model [AST]))-computeInterpolant c p ps =-  alloca $ \interp ->-  alloca $ \model ->-  h2c p $ \pat -> do-  h2c ps $ \params -> do-    res <- toHsCheckError c $ \ctx ->-      z3_compute_interpolant ctx pat params interp model-    case res of-         Sat   -> Just . Left <$> peekToHs c model-         Unsat -> Just . Right <$> peekToHs c interp-         Undef -> return Nothing---- | Read an interpolation problem from file.-readInterpolationProblem :: Context -> FilePath-                         -> IO (Either String InterpolationProblem)-readInterpolationProblem c file =-  withCString file $ \fileName ->-  alloca $ \num ->-  alloca $ \cnsts ->-  alloca $ \parents ->-  alloca $ \errorMsg ->-  alloca $ \numTheory ->-  alloca $ \theory -> do-    suc <- toHsCheckError c $ \ctx ->-      z3_read_interpolation_problem ctx num cnsts parents fileName errorMsg-                                        numTheory theory-    if suc-      then do-        n <- peekToHs c num-        constraints' <- peekArrayToHs c n cnsts-        parents' <- peekPtrArrayToHs c n `T.traverse` ptrToMaybe parents-        nt <- peekToHs c numTheory-        theory' <- peekArrayToHs c nt theory-        return $ Right $ InterpolationProblem-            { getConstraints = constraints'-            , getParents     = parents'-            , getTheoryTerms = theory' }-      else do-        Left <$> peekToHs c errorMsg---- | Check the correctness of an interpolant.------ The Z3 context must have no constraints asserted when this call is made.--- That means that after interpolating, you must first fully pop the Z3 context--- before calling this.-checkInterpolant :: Context -> InterpolationProblem -> [AST] -> IO (Result,Maybe String)-checkInterpolant c prob is =-  marshalArrayLen cs $ \num cnsts ->-  marshalMaybeArray ps $ \parents ->-  marshalArray is $ \interps ->-  alloca $ \errorMsgPtr ->-  marshalArrayLen t $ \numTheory theory -> do-    res <- toHsCheckError c $ \ctx ->-      z3_check_interpolant ctx num cnsts parents interps errorMsgPtr numTheory theory-    errorMsg <- peekToMaybeHs c errorMsgPtr-    return (res,errorMsg)-  where cs = getConstraints prob-        ps = getParents prob-        t  = getTheoryTerms prob---- | Return a string summarizing cumulative time used for interpolation.------ This string is purely for entertainment purposes and has no semantics.-interpolationProfile :: Context -> IO String-interpolationProfile = liftFun0 z3_interpolation_profile---- | Write an interpolation problem to file suitable for reading with 'readInterpolationProblem'.------ The output file is a sequence of SMT-LIB2 format commands, suitable for reading--- with command-line Z3 or other interpolating solvers.-writeInterpolationProblem :: Context -> FilePath -> InterpolationProblem -> IO ()-writeInterpolationProblem c file prob =-  marshalArrayLen cs $ \num cnsts ->-  marshalMaybeArray ps $ \parents ->-  withCString file $ \filename ->-  marshalArrayLen t $ \numTheory theory ->-  toHsCheckError c $ \ctx ->-    z3_write_interpolation_problem ctx num cnsts parents filename numTheory theory-  where cs = getConstraints prob-        ps = getParents prob-        t  = getTheoryTerms prob----------------------------------------------------------------------- -- Solvers  -- | Solvers available in Z3.@@ -2954,17 +2831,28 @@ marshalArrayLen hs f =   hs2cs hs $ \cs -> withArrayLen cs $ \n -> f (fromIntegral n) -marshalMaybeArray :: (Marshal h c, Storable c) => Maybe [h] -> (Ptr c -> IO a) -> IO a-marshalMaybeArray Nothing   f = f nullPtr-marshalMaybeArray (Just hs) f = marshalArray hs f+-- marshalMaybeArray :: (Marshal h c, Storable c) => Maybe [h] -> (Ptr c -> IO a) -> IO a+-- marshalMaybeArray Nothing   f = f nullPtr+-- marshalMaybeArray (Just hs) f = marshalArray hs f -liftAstN :: String+liftAstN_err :: String             -> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))             -> Context -> [AST] -> IO AST-liftAstN s _ _ [] = error s-liftAstN _ f c es = marshal f c $ marshalArrayLen es+liftAstN_err s _ _ [] = error s+liftAstN_err _ f c es = marshal f c $ marshalArrayLen es+{-# INLINE liftAstN_err #-}++liftAstN :: (Ptr Z3_context -> IO (Ptr Z3_ast))+         -> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))+         -> Context -> [AST] -> IO AST+liftAstN s f c = maybe (liftFun0 s c) (liftAstN1 f c) . nonEmpty {-# INLINE liftAstN #-} +liftAstN1 :: (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))+          -> Context -> NonEmpty AST -> IO AST+liftAstN1 f c = marshal f c . marshalArrayLen . toList+{-# INLINE liftAstN1 #-}+ class Marshal h c where   c2h :: Context -> c -> IO h   h2c :: h -> (c -> IO r) -> IO r@@ -2978,18 +2866,18 @@ cs2hs :: Marshal h c => Context -> [c] -> IO [h] cs2hs ctx = mapM (c2h ctx) -peekToHs :: (Marshal h c, Storable c) => Context -> Ptr c -> IO h-peekToHs c ptr = c2h c =<< peek ptr+-- peekToHs :: (Marshal h c, Storable c) => Context -> Ptr c -> IO h+-- peekToHs c ptr = c2h c =<< peek ptr -peekToMaybeHs :: (Marshal h (Ptr c), Storable c) => Context -> Ptr (Ptr c) -> IO (Maybe h)-peekToMaybeHs c = peek >=> (c2h c `T.traverse`) . ptrToMaybe+-- peekToMaybeHs :: (Marshal h (Ptr c), Storable c) => Context -> Ptr (Ptr c) -> IO (Maybe h)+-- peekToMaybeHs c = peek >=> (c2h c `T.traverse`) . ptrToMaybe  peekArrayToHs :: (Marshal h c, Storable c) => Context -> Int -> Ptr c -> IO [h] peekArrayToHs c n dPtr =   cs2hs c =<< peekArray n dPtr -peekPtrArrayToHs :: (Marshal h c, Storable c) => Context -> Int -> Ptr (Ptr c) -> IO [h]-peekPtrArrayToHs c n = peekArray n >=> mapM (peekToHs c)+-- peekPtrArrayToHs :: (Marshal h c, Storable c) => Context -> Int -> Ptr (Ptr c) -> IO [h]+-- peekPtrArrayToHs c n = peekArray n >=> mapM (peekToHs c)  toHsCheckError :: Marshal h c => Context -> (Ptr Z3_context -> IO c) -> IO h toHsCheckError c f = withContext c $ \cPtr ->@@ -3192,9 +3080,10 @@ -- 'Foreign.toBool' should be OK but this is more convenient. toBool :: Z3_bool -> Bool toBool b-    | b == z3_true  = True     | b == z3_false = False-    | otherwise     = error "Z3.Base.toBool: illegal `Z3_bool' value"+    -- As of March 2019, OS X has an issue where z3 uses other+    -- values than 'z3_true' as truthy. Our work around is to be permissive.+    | otherwise = True  -- | Convert 'Bool' to 'Z3_bool'. unBool :: Bool -> Z3_bool
src/Z3/Base/C.hsc view
@@ -243,6 +243,10 @@ foreign import ccall unsafe "Z3_mk_real_sort"     z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) +-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga62166c0e3f9a8be4ba492eee5a52ce1b>+foreign import ccall unsafe "Z3_mk_finite_domain_sort"+    z3_mk_finite_domain_sort :: Ptr Z3_context -> Ptr Z3_symbol -> CULLong -> IO (Ptr Z3_sort)+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688> foreign import ccall unsafe "Z3_mk_bv_sort"     z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort)@@ -1212,52 +1216,6 @@     z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string  ------------------------------------------------------------------------ * Interpolation---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga0d5e342cd83ed43185bcfdc583513959>-foreign import ccall unsafe "Z3_mk_interpolant"-    z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1fd3d3fe7bc4426c4787c3cc8cf92864>-foreign import ccall unsafe "Z3_mk_interpolation_context"-    z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context)---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad4417737993c62d39a6624118427f506>-foreign import ccall unsafe "Z3_get_interpolant"-    z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast-                       -> Ptr Z3_params -> IO (Ptr Z3_ast_vector)---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf62f6b456349886273e15d3cfe8656fe>-foreign import ccall unsafe "Z3_compute_interpolant"-    z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params-                           -> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model)-                           -> IO Z3_lbool---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2bf6a92d53d65fc32163792bedd5d31f>-foreign import ccall unsafe "Z3_read_interpolation_problem"-    z3_read_interpolation_problem :: Ptr Z3_context -> Ptr CUInt -> Ptr (Ptr Z3_ast)-                                  -> Ptr (Ptr CUInt) -> Ptr CChar -> Ptr Z3_string-                                  -- TODO: report "inexact" result type-                                  -> Ptr CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_bool---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gadf50d7093abe5a892593baef552bbf89>-foreign import ccall unsafe "Z3_check_interpolant"-    z3_check_interpolant :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt-                         -> Ptr (Ptr Z3_ast) -> Ptr Z3_string -> CUInt-                         -- TODO: report "inexact" result type-                         -> Ptr (Ptr Z3_ast) -> IO Z3_lbool---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad45c5746cd1eefe4f2fc6df956c9cd8e>-foreign import ccall unsafe "Z3_interpolation_profile"-    z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2a8ee59130e23e10568a1f70e387c608>-foreign import ccall unsafe "Z3_write_interpolation_problem"-    z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast)-                                   -> Ptr CUInt -> Ptr CChar -> CUInt-                                   -> Ptr (Ptr Z3_ast) -> IO ()----------------------------------------------------------------------- -- * Tactics  -- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaa4b9d53ba194d2d3a8bb2f55bec7e78e>@@ -1475,10 +1433,6 @@                         -> 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
src/Z3/Monad.hs view
@@ -24,7 +24,6 @@     -- ** Z3 enviroments   , Z3Env   , newEnv-  , newItpEnv   , evalZ3WithEnv    -- * Types@@ -64,6 +63,7 @@   , mkIntSort   , mkRealSort   , mkBvSort+  , mkFiniteDomainSort   , mkArraySort   , mkTupleSort   , mkConstructor@@ -101,6 +101,7 @@   , mkAnd   , mkOr   , mkDistinct+  , mkDistinct1   -- ** Helpers   , mkBool @@ -108,6 +109,7 @@   , mkAdd   , mkMul   , mkSub+  , mkSub1   , mkUnaryMinus   , mkDiv   , mkMod@@ -331,7 +333,6 @@   -- * Parser interface   , parseSMTLib2String   , parseSMTLib2File-  , getParserError    -- * Error Handling   , Base.Z3Error(..)@@ -352,17 +353,6 @@   , fixedpointGetAnswer   , fixedpointGetAssertions -  -- * Interpolation-  , Base.InterpolationProblem(..)-  , mkInterpolant-  , Base.mkInterpolationContext-  , getInterpolant-  , computeInterpolant-  , readInterpolationProblem-  , checkInterpolant-  , interpolationProfile-  , writeInterpolationProblem-   -- * Solvers   , solverGetHelp   , solverSetParams@@ -424,10 +414,11 @@  import Control.Applicative ( Applicative ) import Data.Fixed ( Fixed, HasResolution )-import Control.Monad.Reader ( ReaderT, runReaderT, asks )-import Control.Monad.Trans ( MonadIO, liftIO )+import Control.Monad.IO.Class ( MonadIO, liftIO )+import Control.Monad.Trans.Reader ( ReaderT, runReaderT, asks ) import Control.Monad.Fix ( MonadFix ) import Data.Int ( Int64 )+import Data.List.NonEmpty (NonEmpty) import Data.Word ( Word, Word64 ) import Data.Traversable ( Traversable ) import qualified Data.Traversable as T@@ -559,9 +550,6 @@ newEnv :: Maybe Logic -> Opts -> IO Z3Env newEnv = newEnvWith Base.mkContext -newItpEnv :: Maybe Logic -> Opts -> IO Z3Env-newItpEnv = newEnvWith Base.mkInterpolationContext- -- | Eval a Z3 script with a given environment. -- -- Environments may facilitate running many queries under the same@@ -657,6 +645,10 @@ mkBvSort :: MonadZ3 z3 => Int -> z3 Sort mkBvSort = liftFun1 Base.mkBvSort +-- | Create a finite-domain type.+mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort+mkFiniteDomainSort = liftFun2 Base.mkFiniteDomainSort+ -- | Create an array type -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>@@ -833,10 +825,16 @@ -- | The distinct construct is used for declaring the arguments pairwise -- distinct. --+-- Requires a non-empty list.+-- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7> mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST mkDistinct = liftFun1 Base.mkDistinct +-- | Same as 'mkDistinct' but type-safe.+mkDistinct1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST+mkDistinct1 = liftFun1 Base.mkDistinct1+ -- | Create an AST node representing /not(a)/. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>@@ -903,10 +901,16 @@  -- | Create an AST node representing args[0] - ... - args[num_args - 1]. --+-- Requires a non-empty list.+-- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9> mkSub :: MonadZ3 z3 => [AST] -> z3 AST mkSub = liftFun1 Base.mkSub +-- | Same as 'mkSub' but type-safe.+mkSub1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST+mkSub1 = liftFun1 Base.mkSub1+ -- | Create an AST node representing -arg. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>@@ -1988,9 +1992,6 @@                  -> z3 AST parseSMTLib2File = liftFun5 Base.parseSMTLib2File -getParserError :: MonadZ3 z3 => z3 String-getParserError = liftScalar Base.getParserError- --------------------------------------------------------------------- -- Miscellaneous @@ -2027,31 +2028,6 @@  fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST] fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions-------------------------------------------------------------------------- * Interpolation--mkInterpolant :: MonadZ3 z3 => AST -> z3 AST-mkInterpolant = liftFun1 Base.mkInterpolant--getInterpolant :: MonadZ3 z3 => AST -> AST -> Params -> z3 [AST]-getInterpolant = liftFun3 Base.getInterpolant--computeInterpolant :: MonadZ3 z3 => AST -> Params-                   -> z3 (Maybe (Either Model [AST]))-computeInterpolant = liftFun2 Base.computeInterpolant--readInterpolationProblem :: MonadZ3 z3 => FilePath -> z3 (Either String Base.InterpolationProblem)-readInterpolationProblem = liftFun1 Base.readInterpolationProblem--checkInterpolant :: MonadZ3 z3 => Base.InterpolationProblem -> [AST] -> z3 (Result, Maybe String)-checkInterpolant = liftFun2 Base.checkInterpolant--interpolationProfile :: MonadZ3 z3 => z3 String-interpolationProfile = liftScalar Base.interpolationProfile--writeInterpolationProblem :: MonadZ3 z3 => FilePath -> Base.InterpolationProblem -> z3 ()-writeInterpolationProblem = liftFun2 Base.writeInterpolationProblem  --------------------------------------------------------------------- -- * Solvers
z3.cabal view
@@ -1,5 +1,5 @@ Name:                z3-Version:             4.3.1+Version:             408.0 Synopsis:            Bindings for the Z3 Theorem Prover Description:     Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -59,7 +59,7 @@     -- Ban to mtl-2.1: modify in MonadState causes <<loop>> in mtl-2.1     Build-depends:       base >= 4.5 && <5,                          containers,-                         mtl > 2.1+                         transformers >= 0.2      Build-tools:         hsc2hs     Extensions:          FlexibleInstances@@ -93,7 +93,7 @@     Build-depends:     base >=4.5,                        z3,                        containers,-                       mtl >2.1+                       transformers >= 0.2   else     Buildable:         False @@ -104,7 +104,6 @@                        Example.Monad.Queens4All                        Example.Monad.DataTypes                        Example.Monad.FuncModel-                       Example.Monad.Interpolation                        Example.Monad.MutuallyRecursive                        Example.Monad.ParserInterface                        Example.Monad.Quantifiers