diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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: + + .[.] + +The `` 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 diff --git a/examples/Example/Monad/DataTypes.hs b/examples/Example/Monad/DataTypes.hs --- a/examples/Example/Monad/DataTypes.hs +++ b/examples/Example/Monad/DataTypes.hs @@ -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 diff --git a/examples/Example/Monad/Interpolation.hs b/examples/Example/Monad/Interpolation.hs deleted file mode 100644 --- a/examples/Example/Monad/Interpolation.hs +++ /dev/null @@ -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" diff --git a/examples/Example/Monad/MutuallyRecursive.hs b/examples/Example/Monad/MutuallyRecursive.hs --- a/examples/Example/Monad/MutuallyRecursive.hs +++ b/examples/Example/Monad/MutuallyRecursive.hs @@ -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 diff --git a/examples/Example/Monad/QuantifierElimination.hs b/examples/Example/Monad/QuantifierElimination.hs --- a/examples/Example/Monad/QuantifierElimination.hs +++ b/examples/Example/Monad/QuantifierElimination.hs @@ -3,7 +3,7 @@ where import Control.Monad -import Control.Monad.Trans ( liftIO ) +import Control.Monad.IO.Class (liftIO) import Z3.Monad diff --git a/examples/Example/Monad/Quantifiers.hs b/examples/Example/Monad/Quantifiers.hs --- a/examples/Example/Monad/Quantifiers.hs +++ b/examples/Example/Monad/Quantifiers.hs @@ -3,7 +3,7 @@ where import Control.Monad -import Control.Monad.Trans ( liftIO ) +import Control.Monad.IO.Class (liftIO) import Z3.Monad diff --git a/examples/Example/Monad/ToSMTLib.hs b/examples/Example/Monad/ToSMTLib.hs --- a/examples/Example/Monad/ToSMTLib.hs +++ b/examples/Example/Monad/ToSMTLib.hs @@ -5,7 +5,6 @@ import Control.Applicative import Control.Monad ( join ) -import Control.Monad.Trans import Data.Maybe import qualified Data.Traversable as T diff --git a/examples/Examples.hs b/examples/Examples.hs --- a/examples/Examples.hs +++ b/examples/Examples.hs @@ -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 diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -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 )@ --- /unsat/ -> @Just (Right )@ --- /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 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 @@ -243,6 +243,10 @@ foreign import ccall unsafe "Z3_mk_real_sort" z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) +-- | Reference: +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: 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: -foreign import ccall unsafe "Z3_mk_interpolant" - z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) - --- | Reference: -foreign import ccall unsafe "Z3_mk_interpolation_context" - z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context) - --- | Reference: -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: -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: -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: -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: -foreign import ccall unsafe "Z3_interpolation_profile" - z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string - --- | Reference: -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: @@ -1475,10 +1433,6 @@ -> 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 diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: @@ -833,10 +825,16 @@ -- | The distinct construct is used for declaring the arguments pairwise -- distinct. -- +-- Requires a non-empty list. +-- -- Reference: 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: @@ -903,10 +901,16 @@ -- | Create an AST node representing args[0] - ... - args[num_args - 1]. -- +-- Requires a non-empty list. +-- -- Reference: 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: @@ -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 diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -59,7 +59,7 @@ -- Ban to mtl-2.1: modify in MonadState causes <> 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