diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,9 +1,43 @@ # Release Notes +## 408.2 + +Tested (sort of) with Z3 4.8.8. + +* Added Optimization API. (David Cao) +* Added Sequences and regular expressions API. (Carlo Nucera) +* Added z3_solver_get_proof. ("0xd34df00d") +* Added MonadZ3 instance for ReaderT. ("0xd34df00d") +* Fixed two typos in docs. (Mauro Bringolf) + +## 408.1 + +Tested (sort of) with Z3 4.8.4. + +* Added bindings to `substitute` and `isEqAST`. (Hengchu Zhang) +* Added `MonadFail` instance for `Z3`, required by GHC >=8.6. (Conal Elliott) +* Updated `Z3_get_error_msg` signature (Z3 C API 4.8.7). (Kevin Quick) +* Removed bindings to `Z3_fixedpoint_push` and `Z3_fixedpoint_pop` (Z3 C API 4.8.5). (Eric Walkingshaw) +* Replaced `z3_get_error_msg_ex` with `z3_get_error_msg` (Z3 C API 4.8.5). (Alexander Knauth) +* Added semigroups to dependencies for GHC <= 7. (Hogeyama) + +## 408.0 + +* Enabled support for Z3 4.8. (Carlo Nucera) + - 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,37 @@ 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) + +## State of maintenance + +The library is currently "maintained", meaning that I try to be responsive to new +issues and pull requests. +Unfortunately I do not have time to investigate issues or to do major work myself. +I do try to help those who want to contribute. + +If someone demonstrates willingness to maintain the library more actively +in the long run, then I will be very happy to give the required permissions +to become a co-maintainer. +In the meantime I will do my best to keep it alive. + +## Supported versions and version policy + +Z3 releases come out often and sometimes introduce backwards incompatible changes. +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 @@ -247,6 +250,43 @@ , mkBitvector , mkBvNum + -- * Sequences and regular expressions + , mkSeqSort + , isSeqSort + , mkReSort + , isReSort + , mkStringSort + , isStringSort + , mkString + , isString + , getString + , mkSeqEmpty + , mkSeqUnit + , mkSeqConcat + , mkSeqPrefix + , mkSeqSuffix + , mkSeqContains + , mkSeqExtract + , mkSeqReplace + , mkSeqAt + , mkSeqLength + , mkSeqIndex + , mkStrToInt + , mkIntToStr + , mkSeqToRe + , mkSeqInRe + , mkRePlus + , mkReStar + , mkReOption + , mkReUnion + , mkReConcat + , mkReRange + , mkReLoop + , mkReIntersect + , mkReComplement + , mkReEmpty + , mkReFull + -- * Quantifiers , mkPattern , mkBound @@ -304,6 +344,7 @@ -- * Modifiers , substituteVars + , substitute -- * Models , modelEval @@ -318,6 +359,7 @@ , getConsts , getFuncs , isAsArray + , isEqAST , addFuncInterp , addConstInterp , getAsArrayFuncDecl @@ -372,7 +414,6 @@ -- * Parser interface , parseSMTLib2String , parseSMTLib2File - , getParserError -- * Error Handling , Z3Error(..) @@ -385,8 +426,6 @@ -- * Fixedpoint , Fixedpoint (..) , mkFixedpoint - , fixedpointPush - , fixedpointPop , fixedpointAddRule , fixedpointSetParams , fixedpointRegisterRelation @@ -394,16 +433,31 @@ , fixedpointGetAnswer , fixedpointGetAssertions - -- * Interpolation - , InterpolationProblem(..) - , mkInterpolant - , mkInterpolationContext - , getInterpolant - , computeInterpolant - , readInterpolationProblem - , checkInterpolant - , interpolationProfile - , writeInterpolationProblem + -- * Optimization + , Optimize (..) + , mkOptimize + , optimizeAssert + , optimizeAssertAndTrack + , optimizeAssertSoft + , optimizeMaximize + , optimizeMinimize + , optimizePush + , optimizePop + , optimizeCheck + , optimizeGetReasonUnknown + , optimizeGetModel + , optimizeGetUnsatCore + , optimizeSetParams + , optimizeGetLower + , optimizeGetUpper + , optimizeGetUpperAsVector + , optimizeGetLowerAsVector + , optimizeToString + , optimizeFromString + , optimizeFromFile + , optimizeGetHelp + , optimizeGetAssertions + , optimizeGetObjectives -- * Solvers , Logic(..) @@ -421,6 +475,7 @@ , solverCheck , solverCheckAssumptions , solverGetModel + , solverGetProof , solverGetUnsatCore , solverGetReasonUnknown , solverToString @@ -432,10 +487,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 +800,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 +1046,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 +1078,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 +1097,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 @@ -1523,6 +1592,208 @@ mkBvNum ctx s n = mkIntegral ctx n =<< mkBvSort ctx s --------------------------------------------------------------------- +-- Sequences and regular expressions + +-- | Create a sequence sort out of the sort for the elements. +mkSeqSort :: Context -> Sort -> IO Sort +mkSeqSort = liftFun1 z3_mk_seq_sort + +-- | Check if s is a sequence sort. +isSeqSort :: Context -> Sort -> IO Bool +isSeqSort = liftFun1 z3_is_seq_sort + +-- | Create a regular expression sort out of a sequence sort. +mkReSort :: Context -> Sort -> IO Sort +mkReSort = liftFun1 z3_mk_re_sort + +-- | Check if s is a regular expression sort. +isReSort :: Context -> Sort -> IO Bool +isReSort = liftFun1 z3_is_re_sort + +-- | Create a sort for 8 bit strings. This function creates a sort for ASCII +-- strings. Each character is 8 bits. +mkStringSort :: Context -> IO Sort +mkStringSort = liftFun0 z3_mk_string_sort + +-- | Check if s is a string sort. +isStringSort :: Context -> Sort -> IO Bool +isStringSort = liftFun1 z3_is_string_sort + +-- | Create a string constant out of the string that is passed in. +mkString :: Context -> String -> IO AST +mkString = liftFun1 z3_mk_string + +-- | Determine if s is a string constant. +isString :: Context -> AST -> IO Bool +isString = liftFun1 z3_is_string + +-- | Retrieve the string constant stored in s. +getString :: Context -> AST -> IO String +getString = liftFun1 z3_get_string + +-- | Create an empty sequence of the sequence sort seq. +mkSeqEmpty :: Context -> Sort -> IO AST +mkSeqEmpty = liftFun1 z3_mk_seq_empty + +-- | Create a unit sequence of a. +mkSeqUnit :: Context -> AST -> IO AST +mkSeqUnit = liftFun1 z3_mk_seq_unit + +-- | Concatenate sequences. +mkSeqConcat :: (Integral int) => Context -> int -> [AST] -> IO AST +mkSeqConcat c i as + | i < 0 = error "Z3.Base.mkSeqConcat: negative size" + | i >= 0 && null as = error "Z3.Base.mkSeqConcet: empty list of expressions" + | otherwise = marshal z3_mk_seq_concat c $ marshalArrayLen as + +-- | Check if prefix is a prefix of s. +mkSeqPrefix :: Context + -> AST -- ^ prefix + -> AST -- ^ s + -> IO AST +mkSeqPrefix = liftFun2 z3_mk_seq_prefix + +-- | Check if suffix is a suffix of s. +mkSeqSuffix :: Context + -> AST -- ^ suffix + -> AST -- ^ s + -> IO AST +mkSeqSuffix = liftFun2 z3_mk_seq_suffix + +-- | Check if container contains containee. +mkSeqContains :: Context + -> AST -- ^ container + -> AST -- ^ containee + -> IO AST +mkSeqContains = liftFun2 z3_mk_seq_contains + +-- | Extract subsequence starting at offset of length. +mkSeqExtract :: Context + -> AST -- ^ s + -> AST -- ^ offset + -> AST -- ^ length + -> IO AST +mkSeqExtract = liftFun3 z3_mk_seq_extract + +-- | Replace the first occurrence of src with dst in s. +mkSeqReplace :: Context + -> AST -- ^ s + -> AST -- ^ src + -> AST -- ^ dst + -> IO AST +mkSeqReplace = liftFun3 z3_mk_seq_replace + +-- | Retrieve from s the unit sequence positioned at position index. +mkSeqAt :: Context + -> AST -- ^ s + -> AST -- ^ index + -> IO AST +mkSeqAt = liftFun2 z3_mk_seq_at + +-- | Return the length of the sequence s. +mkSeqLength :: Context + -> AST -- ^ s + -> IO AST +mkSeqLength = liftFun1 z3_mk_seq_length + +-- | Return index of first occurrence of substr in s starting from offset +-- offset. If s does not contain substr, then the value is -1, if offset is the +-- length of s, then the value is -1 as well. The function is under-specified if +-- offset is negative or larger than the length of s. +mkSeqIndex :: Context + -> AST -- ^ s + -> AST -- ^ substr + -> AST -- ^ offset + -> IO AST +mkSeqIndex = liftFun3 z3_mk_seq_index + +-- | Convert string to integer. +mkStrToInt :: Context -> AST -> IO AST +mkStrToInt = liftFun1 z3_mk_str_to_int + +-- | Integer to string conversion. +mkIntToStr :: Context -> AST -> IO AST +mkIntToStr = liftFun1 z3_mk_int_to_str + +-- | Create a regular expression that accepts the sequence. +mkSeqToRe :: Context -> AST -> IO AST +mkSeqToRe = liftFun1 z3_mk_seq_to_re + +-- | Check if seq is in the language generated by the regular expression re. +mkSeqInRe :: Context + -> AST -- ^ seq + -> AST -- ^ re + -> IO AST +mkSeqInRe = liftFun2 z3_mk_seq_in_re + +-- | Create the regular language re+. +mkRePlus :: Context -> AST -> IO AST +mkRePlus = liftFun1 z3_mk_re_plus + +-- | Create the regular language re*. +mkReStar :: Context -> AST -> IO AST +mkReStar = liftFun1 z3_mk_re_star + +-- | Create the regular language [re]. +mkReOption :: Context -> AST -> IO AST +mkReOption = liftFun1 z3_mk_re_option + +-- | Create the union of the regular languages. +mkReUnion :: (Integral int) => Context -> int -> [AST] -> IO AST +mkReUnion c i as + | i < 0 = error "Z3.Base.mkReUnion: negative size" + | i >= 0 && null as = error "Z3.Base.mkReUnion: empty list of expressions" + | otherwise = marshal z3_mk_re_union c $ marshalArrayLen as + +-- | Create the concatenation of the regular languages. +mkReConcat :: (Integral int) => Context -> int -> [AST] -> IO AST +mkReConcat c i as + | i < 0 = error "Z3.Base.mkReConcat: negative size" + | i >= 0 && null as = error "Z3.Base.mkReConcat: empty list of expressions" + | otherwise = marshal z3_mk_re_concat c $ marshalArrayLen as + +-- | Create the range regular expression over two sequences of length 1. +mkReRange :: Context + -> AST -- ^ lo + -> AST -- ^ hi + -> IO AST +mkReRange = liftFun2 z3_mk_re_range + +-- | Create a regular expression loop. The supplied regular expression r is +-- repeated between lo and hi times. The lo should be below hi with one +-- exception: when supplying the value hi as 0, the meaning is to repeat the +-- argument r at least lo number of times, and with an unbounded upper bound. +mkReLoop :: (Integral int) + => Context + -> AST -- ^ r + -> int -- ^ lo + -> int -- ^ hi + -> IO AST +mkReLoop c a i j + | i < 0 = error "Z3.Base.mkReLoop: negative size" + | i < 0 = error "Z3.Base.mkReLoop: empty list of expressions" + | otherwise = liftFun3 z3_mk_re_loop c a i j + +-- | Create the intersection of the regular languages. +mkReIntersect :: (Integral int) => Context -> int -> [AST] -> IO AST +mkReIntersect c i as + | i < 0 = error "Z3.Base.mkReIntersect: negative size" + | i >= 0 && null as = error "Z3.Base.mkReIntersect: empty list of expressions" + | otherwise = marshal z3_mk_re_intersect c $ marshalArrayLen as + +-- | Create the complement of the regular language. +mkReComplement :: Context -> AST -> IO AST +mkReComplement = liftFun1 z3_mk_re_complement + +-- | Create an empty regular expression of sort re. +mkReEmpty :: Context -> Sort -> IO AST +mkReEmpty = liftFun1 z3_mk_re_empty + +-- | Create an universal regular expression of sort re. +mkReFull :: Context -> Sort -> IO AST +mkReFull = liftFun1 z3_mk_re_full + + --------------------------------------------------------------------- -- Quantifiers -- | Create a pattern for quantifier instantiation. @@ -2039,6 +2310,16 @@ marshalArrayLen vars $ \varsNum varsArr -> f aPtr varsNum varsArr +substitute :: Context -> AST -> [(AST, AST)] -> IO AST +substitute ctx a substs = + let froms = map fst substs + tos = map snd substs + in marshal z3_substitute ctx $ \f -> + h2c a $ \aPtr -> + marshalArrayLen froms $ \fromsLen fromsArr -> + marshalArray tos $ \ tosArr -> + f aPtr fromsLen fromsArr tosArr + --------------------------------------------------------------------- -- Models @@ -2125,6 +2406,9 @@ isAsArray :: Context -> AST -> IO Bool isAsArray = liftFun1 z3_is_as_array +isEqAST :: Context -> AST -> AST -> IO Bool +isEqAST = liftFun2 z3_is_eq_ast + addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp addFuncInterp = liftFun3 z3_add_func_interp @@ -2445,9 +2729,6 @@ f fileName sortNum sortNameArr sortArr declNum declNameArr declArr -getParserError :: Context -> IO String -getParserError = liftFun0 z3_get_parser_error - --------------------------------------------------------------------- -- Error handling @@ -2496,7 +2777,7 @@ checkError :: Ptr Z3_context -> IO a -> IO a checkError cPtr m = do m <* (z3_get_error_code cPtr >>= throwZ3Exn) - where getErrStr i = peekCString =<< z3_get_error_msg_ex cPtr i + where getErrStr i = peekCString =<< z3_get_error_msg cPtr i throwZ3Exn i = when (i /= z3_ok) $ getErrStr i >>= z3Error (toZ3Error i) --------------------------------------------------------------------- @@ -2547,12 +2828,6 @@ mkFixedpoint :: Context -> IO Fixedpoint mkFixedpoint = liftFun0 z3_mk_fixedpoint -fixedpointPush :: Context -> Fixedpoint -> IO () -fixedpointPush = liftFun1 z3_fixedpoint_push - -fixedpointPop :: Context -> Fixedpoint -> IO () -fixedpointPop = liftFun1 z3_fixedpoint_pop - fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO () fixedpointAddRule = liftFun3 z3_fixedpoint_add_rule @@ -2575,146 +2850,109 @@ fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST] fixedpointGetAssertions = liftFun1 z3_fixedpoint_get_assertions --- AST vectors ? +--------------------------------------------------------------------- +-- Optimization facilities --- AST maps ? +newtype Optimize = Optimize { unOptimize :: ForeignPtr Z3_optimize } + deriving Eq ---------------------------------------------------------------------- --- Goals +instance Marshal Optimize (Ptr Z3_optimize) where + c2h = mkC2hRefCount Optimize z3_optimize_inc_ref z3_optimize_dec_ref + h2c fp = withForeignPtr (unOptimize fp) --- TODO +mkOptimize :: Context -> IO Optimize +mkOptimize = liftFun0 z3_mk_optimize ---------------------------------------------------------------------- --- Tactics and Probes +optimizeAssert :: Context -> Optimize -> AST -> IO () +optimizeAssert = liftFun2 z3_optimize_assert --- TODO +optimizeAssertAndTrack :: Context -> Optimize -> AST -> AST -> IO () +optimizeAssertAndTrack = liftFun3 z3_optimize_assert_and_track ---------------------------------------------------------------------- --- Interpolation +optimizeAssertSoft :: Context -> Optimize -> AST -> String -> Symbol -> IO Int +optimizeAssertSoft ctx opt ast str sym = + marshal z3_optimize_assert_soft ctx $ \f -> + h2c opt $ \optPtr -> + h2c ast $ \astPtr -> + withCString str $ \strPtr -> + h2c sym $ \symPtr -> + f optPtr astPtr strPtr symPtr --- | Interpolation problem formulation. -data InterpolationProblem = - InterpolationProblem { - getConstraints :: [AST] - , getParents :: Maybe [Int] - , getTheoryTerms :: [AST] - } +optimizeMaximize :: Context -> Optimize -> AST -> IO Int +optimizeMaximize = liftFun2 z3_optimize_maximize --- | Generate a Z3 context suitable for generation of interpolants. -mkInterpolationContext :: Config -> IO Context -mkInterpolationContext = mkContextWith z3_mk_interpolation_context +optimizeMinimize :: Context -> Optimize -> AST -> IO Int +optimizeMinimize = liftFun2 z3_optimize_minimize --- | Create an AST node marking a formula position for interpolation. -mkInterpolant :: Context - -> AST -- ^ boolean expression - -> IO AST -mkInterpolant = liftFun1 z3_mk_interpolant +optimizePush :: Context -> Optimize -> IO () +optimizePush = liftFun1 z3_optimize_push --- | 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 +optimizePop :: Context -> Optimize -> IO () +optimizePop = liftFun1 z3_optimize_pop --- | 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 +optimizeCheck :: Context -> Optimize -> [AST] -> IO Result +optimizeCheck ctx opt ss = marshal z3_optimize_check ctx $ \f -> + h2c opt $ \optPtr -> + marshalArrayLen ss $ \ssNum ssPtr -> + f optPtr ssNum ssPtr --- | 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 +optimizeGetReasonUnknown :: Context -> Optimize -> IO String +optimizeGetReasonUnknown = liftFun1 z3_optimize_get_reason_unknown --- | 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 +optimizeGetModel :: Context -> Optimize -> IO Model +optimizeGetModel = liftFun1 z3_optimize_get_model --- | 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 +optimizeGetUnsatCore :: Context -> Optimize -> IO [AST] +optimizeGetUnsatCore = liftFun1 z3_optimize_get_unsat_core --- | 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 +optimizeSetParams :: Context -> Optimize -> Params -> IO () +optimizeSetParams = liftFun2 z3_optimize_set_params +optimizeGetLower :: Context -> Optimize -> Int -> IO AST +optimizeGetLower = liftFun2 z3_optimize_get_lower + +optimizeGetUpper :: Context -> Optimize -> Int -> IO AST +optimizeGetUpper = liftFun2 z3_optimize_get_upper + +optimizeGetUpperAsVector :: Context -> Optimize -> Int -> IO [AST] +optimizeGetUpperAsVector = liftFun2 z3_optimize_get_upper_as_vector + +optimizeGetLowerAsVector :: Context -> Optimize -> Int -> IO [AST] +optimizeGetLowerAsVector = liftFun2 z3_optimize_get_lower_as_vector + +optimizeToString :: Context -> Optimize -> IO String +optimizeToString = liftFun1 z3_optimize_to_string + +optimizeFromString :: Context -> Optimize -> String -> IO () +optimizeFromString = liftFun2 z3_optimize_from_string + +optimizeFromFile :: Context -> Optimize -> String -> IO () +optimizeFromFile = liftFun2 z3_optimize_from_file + +optimizeGetHelp :: Context -> Optimize -> IO String +optimizeGetHelp = liftFun1 z3_optimize_get_help + +optimizeGetAssertions :: Context -> Optimize -> IO [AST] +optimizeGetAssertions = liftFun1 z3_optimize_get_assertions + +optimizeGetObjectives :: Context -> Optimize -> IO [AST] +optimizeGetObjectives = liftFun1 z3_optimize_get_objectives + +-- AST vectors ? + +-- AST maps ? + --------------------------------------------------------------------- +-- Goals + +-- TODO + +--------------------------------------------------------------------- +-- Tactics and Probes + +-- TODO + +--------------------------------------------------------------------- -- Solvers -- | Solvers available in Z3. @@ -2901,6 +3139,14 @@ h2c solver $ \solverPtr -> f solverPtr +-- | Retrieve the proof for the last 'solverCheck' or 'solverCheckAssumptions'. +-- +-- The error handler is invoked if a proof is not available because +-- the commands above were not invoked for the given solver, +-- or if the result was different from 'Unsat' (so 'Sat' does not have a proof). +solverGetProof :: Context -> Solver -> IO AST +solverGetProof = liftFun1 z3_solver_get_proof + -- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions solverGetUnsatCore :: Context -> Solver -> IO [AST] solverGetUnsatCore = liftFun1 z3_solver_get_unsat_core @@ -2954,17 +3200,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 +3235,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 -> @@ -3007,9 +3264,7 @@ withContext ctx $ \ctxPtr -> do incRef ctxPtr xPtr contextIncRef ctx - let xFinalizer = do - decRef ctxPtr xPtr - contextDecRef ctxPtr (refCount ctx) + let xFinalizer = do decRef ctxPtr xPtr; contextDecRef ctxPtr (refCount ctx) mk <$> newForeignPtr xPtr xFinalizer dummy_inc_ref :: Z3IncRefFun c @@ -3192,9 +3447,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 @@ -68,6 +68,8 @@ data Z3_fixedpoint +data Z3_optimize + data Z3_solver data Z3_params @@ -243,6 +245,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) @@ -755,6 +761,114 @@ z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --------------------------------------------------------------------- +-- * Sequences and regular expressions + +foreign import ccall unsafe "Z3_mk_seq_sort" + z3_mk_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) + +foreign import ccall unsafe "Z3_is_seq_sort" + z3_is_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool + +foreign import ccall unsafe "Z3_mk_re_sort" + z3_mk_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) + +foreign import ccall unsafe "Z3_is_re_sort" + z3_is_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool + +foreign import ccall unsafe "Z3_mk_string_sort" + z3_mk_string_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) + +foreign import ccall unsafe "Z3_is_string_sort" + z3_is_string_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool + +foreign import ccall unsafe "Z3_mk_string" + z3_mk_string :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_is_string" + z3_is_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool + +foreign import ccall unsafe "Z3_get_string" + z3_get_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string + +foreign import ccall unsafe "Z3_mk_seq_empty" + z3_mk_seq_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_unit" + z3_mk_seq_unit :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_concat" + z3_mk_seq_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_prefix" + z3_mk_seq_prefix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_suffix" + z3_mk_seq_suffix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_contains" + z3_mk_seq_contains :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_extract" + z3_mk_seq_extract :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_replace" + z3_mk_seq_replace :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_at" + z3_mk_seq_at :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_length" + z3_mk_seq_length :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_index" + z3_mk_seq_index :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_str_to_int" + z3_mk_str_to_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_int_to_str" + z3_mk_int_to_str :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_to_re" + z3_mk_seq_to_re :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_seq_in_re" + z3_mk_seq_in_re :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_plus" + z3_mk_re_plus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_star" + z3_mk_re_star :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_option" + z3_mk_re_option :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_union" + z3_mk_re_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_concat" + z3_mk_re_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_range" + z3_mk_re_range :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_loop" + z3_mk_re_loop :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> CUInt -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_intersect" + z3_mk_re_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_complement" + z3_mk_re_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_empty" + z3_mk_re_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_mk_re_full" + z3_mk_re_full :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) + +--------------------------------------------------------------------- -- * Quantifiers -- | Reference: @@ -965,6 +1079,10 @@ foreign import ccall unsafe "Z3_substitute_vars" z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) +-- | Reference: +foreign import ccall unsafe "Z3_substitute" + z3_substitute :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) + --------------------------------------------------------------------- -- * AST vectors @@ -1063,6 +1181,13 @@ -> Ptr Z3_ast -> IO Z3_bool +-- | Reference: +foreign import ccall unsafe "Z3_is_eq_ast" + z3_is_eq_ast :: Ptr Z3_context + -> Ptr Z3_ast + -> Ptr Z3_ast + -> IO Z3_bool + -- | Reference: foreign import ccall unsafe "Z3_get_as_array_func_decl" z3_get_as_array_func_decl :: Ptr Z3_context @@ -1212,52 +1337,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: @@ -1401,6 +1480,10 @@ foreign import ccall unsafe "Z3_solver_get_model" z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) +-- | Reference: +foreign import ccall unsafe "Z3_solver_get_proof" + z3_solver_get_proof :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast) + -- | Reference: foreign import ccall unsafe "Z3_solver_get_unsat_core" z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector) @@ -1476,10 +1559,6 @@ -> 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 @@ -1497,11 +1576,7 @@ -- | Reference: foreign import ccall unsafe "Z3_get_error_msg" - z3_get_error_msg :: Z3_error_code -> IO Z3_string - --- | Reference: -foreign import ccall unsafe "Z3_get_error_msg_ex" - z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string + z3_get_error_msg :: Ptr Z3_context -> Z3_error_code -> IO Z3_string --------------------------------------------------------------------- -- * Miscellaneous @@ -1516,12 +1591,6 @@ foreign import ccall unsafe "Z3_mk_fixedpoint" z3_mk_fixedpoint :: Ptr Z3_context -> IO (Ptr Z3_fixedpoint) -foreign import ccall unsafe "Z3_fixedpoint_push" - z3_fixedpoint_push :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () - -foreign import ccall unsafe "Z3_fixedpoint_pop" - z3_fixedpoint_pop :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () - foreign import ccall unsafe "Z3_fixedpoint_inc_ref" z3_fixedpoint_inc_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO () @@ -1549,3 +1618,139 @@ -> CUInt -> Ptr (Ptr Z3_func_decl) -> IO Z3_lbool + +--------------------------------------------------------------------- +-- * Optimization facilities + +foreign import ccall unsafe "Z3_mk_optimize" + z3_mk_optimize :: Ptr Z3_context -> IO (Ptr Z3_optimize) + +foreign import ccall unsafe "Z3_optimize_inc_ref" + z3_optimize_inc_ref :: Ptr Z3_context -> Ptr Z3_optimize -> IO () + +foreign import ccall unsafe "Z3_optimize_dec_ref" + z3_optimize_dec_ref :: Ptr Z3_context -> Ptr Z3_optimize -> IO () + +foreign import ccall unsafe "Z3_optimize_assert" + z3_optimize_assert :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO () + +foreign import ccall unsafe "Z3_optimize_assert_and_track" + z3_optimize_assert_and_track :: Ptr Z3_context + -> Ptr Z3_optimize + -> Ptr Z3_ast + -> Ptr Z3_ast + -> IO () + +foreign import ccall unsafe "Z3_optimize_assert_soft" + z3_optimize_assert_soft :: Ptr Z3_context + -> Ptr Z3_optimize + -> Ptr Z3_ast + -> Z3_string + -> Ptr Z3_symbol + -> IO CUInt + +foreign import ccall unsafe "Z3_optimize_maximize" + z3_optimize_maximize :: Ptr Z3_context + -> Ptr Z3_optimize + -> Ptr Z3_ast + -> IO CUInt + +foreign import ccall unsafe "Z3_optimize_minimize" + z3_optimize_minimize :: Ptr Z3_context + -> Ptr Z3_optimize + -> Ptr Z3_ast + -> IO CUInt + +foreign import ccall unsafe "Z3_optimize_push" + z3_optimize_push :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO () + +foreign import ccall unsafe "Z3_optimize_pop" + z3_optimize_pop :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO () + +foreign import ccall unsafe "Z3_optimize_check" + z3_optimize_check :: Ptr Z3_context + -> Ptr Z3_optimize + -> CUInt + -> Ptr (Ptr Z3_ast) + -> IO Z3_lbool + +foreign import ccall unsafe "Z3_optimize_get_reason_unknown" + z3_optimize_get_reason_unknown :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO Z3_string + +foreign import ccall unsafe "Z3_optimize_get_model" + z3_optimize_get_model :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO (Ptr Z3_model) + +foreign import ccall unsafe "Z3_optimize_get_unsat_core" + z3_optimize_get_unsat_core :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO (Ptr Z3_ast_vector) + +foreign import ccall unsafe "Z3_optimize_set_params" + z3_optimize_set_params :: Ptr Z3_context + -> Ptr Z3_optimize + -> Ptr Z3_params + -> IO () + +foreign import ccall unsafe "Z3_optimize_get_lower" + z3_optimize_get_lower :: Ptr Z3_context + -> Ptr Z3_optimize + -> CUInt + -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_optimize_get_upper" + z3_optimize_get_upper :: Ptr Z3_context + -> Ptr Z3_optimize + -> CUInt + -> IO (Ptr Z3_ast) + +foreign import ccall unsafe "Z3_optimize_get_lower_as_vector" + z3_optimize_get_lower_as_vector :: Ptr Z3_context + -> Ptr Z3_optimize + -> CUInt + -> IO (Ptr Z3_ast_vector) + +foreign import ccall unsafe "Z3_optimize_get_upper_as_vector" + z3_optimize_get_upper_as_vector :: Ptr Z3_context + -> Ptr Z3_optimize + -> CUInt + -> IO (Ptr Z3_ast_vector) + +foreign import ccall unsafe "Z3_optimize_to_string" + z3_optimize_to_string :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO Z3_string + +foreign import ccall unsafe "Z3_optimize_from_string" + z3_optimize_from_string :: Ptr Z3_context + -> Ptr Z3_optimize + -> Z3_string + -> IO () + +foreign import ccall unsafe "Z3_optimize_from_file" + z3_optimize_from_file :: Ptr Z3_context + -> Ptr Z3_optimize + -> Z3_string + -> IO () + +foreign import ccall unsafe "Z3_optimize_get_help" + z3_optimize_get_help :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO Z3_string + +foreign import ccall unsafe "Z3_optimize_get_assertions" + z3_optimize_get_assertions :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO (Ptr Z3_ast_vector) + +foreign import ccall unsafe "Z3_optimize_get_objectives" + z3_optimize_get_objectives :: Ptr Z3_context + -> Ptr Z3_optimize + -> IO (Ptr Z3_ast_vector) diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -1,4 +1,3 @@ - {-# LANGUAGE GeneralizedNewtypeDeriving #-} -- | @@ -24,7 +23,6 @@ -- ** Z3 enviroments , Z3Env , newEnv - , newItpEnv , evalZ3WithEnv -- * Types @@ -64,6 +62,7 @@ , mkIntSort , mkRealSort , mkBvSort + , mkFiniteDomainSort , mkArraySort , mkTupleSort , mkConstructor @@ -101,6 +100,7 @@ , mkAnd , mkOr , mkDistinct + , mkDistinct1 -- ** Helpers , mkBool @@ -108,6 +108,7 @@ , mkAdd , mkMul , mkSub + , mkSub1 , mkUnaryMinus , mkDiv , mkMod @@ -206,6 +207,43 @@ , mkBitvector , mkBvNum + -- * Sequences and regular expressions + , mkSeqSort + , isSeqSort + , mkReSort + , isReSort + , mkStringSort + , isStringSort + , mkString + , isString + , getString + , mkSeqEmpty + , mkSeqUnit + , mkSeqConcat + , mkSeqPrefix + , mkSeqSuffix + , mkSeqContains + , mkSeqExtract + , mkSeqReplace + , mkSeqAt + , mkSeqLength + , mkSeqIndex + , mkStrToInt + , mkIntToStr + , mkSeqToRe + , mkSeqInRe + , mkRePlus + , mkReStar + , mkReOption + , mkReUnion + , mkReConcat + , mkReRange + , mkReLoop + , mkReIntersect + , mkReComplement + , mkReEmpty + , mkReFull + -- * Quantifiers , mkPattern , mkBound @@ -263,6 +301,7 @@ -- * Modifiers , substituteVars + , substitute -- * Models , modelEval @@ -277,6 +316,7 @@ , getConsts , getFuncs , isAsArray + , isEqAST , addFuncInterp , addConstInterp , getAsArrayFuncDecl @@ -331,7 +371,6 @@ -- * Parser interface , parseSMTLib2String , parseSMTLib2File - , getParserError -- * Error Handling , Base.Z3Error(..) @@ -342,9 +381,8 @@ , getVersion -- * Fixedpoint + , MonadFixedpoint(..) , Fixedpoint - , fixedpointPush - , fixedpointPop , fixedpointAddRule , fixedpointSetParams , fixedpointRegisterRelation @@ -352,16 +390,31 @@ , fixedpointGetAnswer , fixedpointGetAssertions - -- * Interpolation - , Base.InterpolationProblem(..) - , mkInterpolant - , Base.mkInterpolationContext - , getInterpolant - , computeInterpolant - , readInterpolationProblem - , checkInterpolant - , interpolationProfile - , writeInterpolationProblem + -- * Optimization + , MonadOptimize(..) + , Optimize + , optimizeAssert + , optimizeAssertAndTrack + , optimizeAssertSoft + , optimizeMaximize + , optimizeMinimize + , optimizePush + , optimizePop + , optimizeCheck + , optimizeGetReasonUnknown + , optimizeGetModel + , optimizeGetUnsatCore + , optimizeSetParams + , optimizeGetLower + , optimizeGetUpper + , optimizeGetUpperAsVector + , optimizeGetLowerAsVector + , optimizeToString + , optimizeFromString + , optimizeFromFile + , optimizeGetHelp + , optimizeGetAssertions + , optimizeGetObjectives -- * Solvers , solverGetHelp @@ -375,6 +428,7 @@ , solverCheck , solverCheckAssumptions , solverGetModel + , solverGetProof , solverGetUnsatCore , solverGetReasonUnknown , solverToString @@ -414,6 +468,7 @@ , Params , Solver , Fixedpoint + , Optimize , SortKind(..) , ASTKind(..) , Tactic @@ -424,10 +479,12 @@ 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.Fail +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 @@ -439,6 +496,10 @@ getSolver :: m Base.Solver getContext :: m Base.Context +instance MonadZ3 m => MonadZ3 (ReaderT r m) where + getSolver = ReaderT $ const getSolver + getContext = ReaderT $ const getContext + ------------------------------------------------- -- Lifting @@ -514,11 +575,32 @@ slv <- getFixedpoint liftIO $ f ctx slv a b +liftOptimize0 :: MonadOptimize z3 => + (Base.Context -> Base.Optimize -> IO b) + -> z3 b +liftOptimize0 f_s = + do ctx <- getContext + liftIO . f_s ctx =<< getOptimize + +liftOptimize1 :: MonadOptimize z3 => + (Base.Context -> Base.Optimize -> a -> IO b) + -> a -> z3 b +liftOptimize1 f_s a = + do ctx <- getContext + liftIO . (\s -> f_s ctx s a) =<< getOptimize + +liftOptimize2 :: MonadOptimize z3 => (Base.Context -> Base.Optimize -> a -> b -> IO c) + -> a -> b -> z3 c +liftOptimize2 f a b = do + ctx <- getContext + slv <- getOptimize + liftIO $ f ctx slv a b + ------------------------------------------------- -- A simple Z3 monad. newtype Z3 a = Z3 { _unZ3 :: ReaderT Z3Env IO a } - deriving (Functor, Applicative, Monad, MonadIO, MonadFix) + deriving (Functor, Applicative, Monad, MonadIO, MonadFix, MonadFail) -- | Z3 environment. data Z3Env @@ -526,6 +608,7 @@ envSolver :: Base.Solver , envContext :: Base.Context , envFixedpoint :: Base.Fixedpoint + , envOptimize :: Base.Optimize } instance MonadZ3 Z3 where @@ -535,6 +618,9 @@ instance MonadFixedpoint Z3 where getFixedpoint = Z3 $ asks envFixedpoint +instance MonadOptimize Z3 where + getOptimize = Z3 $ asks envOptimize + -- | Eval a Z3 script. evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a evalZ3With mbLogic opts (Z3 s) = do @@ -553,15 +639,13 @@ ctx <- mkContext cfg solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic fixedpoint <- Base.mkFixedpoint ctx - return $ Z3Env solver ctx fixedpoint + optimize <- Base.mkOptimize ctx + return $ Z3Env solver ctx fixedpoint optimize -- | Create a new Z3 environment. 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 +741,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: @@ -675,11 +763,11 @@ -- constructor and projections. mkTupleSort = liftFun2 Base.mkTupleSort --- | Create a contructor +-- | Create a constructor -- -- Reference: mkConstructor :: MonadZ3 z3 - => Symbol -- ^ Name of the sonstructor + => Symbol -- ^ Name of the constructor -> Symbol -- ^ Name of recognizer function -> [(Symbol, Maybe Sort, Int)] -- ^ Name, sort option, and sortRefs -> z3 Constructor @@ -833,10 +921,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 +997,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: @@ -1288,7 +1388,7 @@ mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST mkSelect = liftFun2 Base.mkSelect --- | Array update.   +-- | Array update. -- -- Reference: mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST @@ -1465,6 +1565,191 @@ mkBvNum = liftFun2 Base.mkBvNum --------------------------------------------------------------------- +-- Sequences and regular expressions + +-- | Create a sequence sort out of the sort for the elements. +mkSeqSort :: MonadZ3 z3 => Sort -> z3 Sort +mkSeqSort = liftFun1 Base.mkSeqSort + +-- | Check if s is a sequence sort. +isSeqSort :: MonadZ3 z3 => Sort -> z3 Bool +isSeqSort = liftFun1 Base.isSeqSort + +-- | Create a regular expression sort out of a sequence sort. +mkReSort :: MonadZ3 z3 => Sort -> z3 Sort +mkReSort = liftFun1 Base.mkReSort + +-- | Check if s is a regular expression sort. +isReSort :: MonadZ3 z3 => Sort -> z3 Bool +isReSort = liftFun1 Base.isReSort + +-- | Create a sort for 8 bit strings. This function creates a sort for ASCII +-- strings. Each character is 8 bits. +mkStringSort :: MonadZ3 z3 => z3 Sort +mkStringSort = liftScalar Base.mkStringSort + +-- | Check if s is a string sort. +isStringSort :: MonadZ3 z3 => Sort -> z3 Bool +isStringSort = liftFun1 Base.isStringSort + +-- | Create a string constant out of the string that is passed in. +mkString :: MonadZ3 z3 => String -> z3 AST +mkString = liftFun1 Base.mkString + +-- | Determine if s is a string constant. +isString :: MonadZ3 z3 => AST -> z3 Bool +isString = liftFun1 Base.isString + +-- | Retrieve the string constant stored in s. +getString :: MonadZ3 z3 => AST -> z3 String +getString = liftFun1 Base.getString + +-- | Create an empty sequence of the sequence sort seq. +mkSeqEmpty :: MonadZ3 z3 => Sort -> z3 AST +mkSeqEmpty = liftFun1 Base.mkSeqEmpty + +-- | Create a unit sequence of a. +mkSeqUnit :: MonadZ3 z3 => AST -> z3 AST +mkSeqUnit = liftFun1 Base.mkSeqUnit + +-- | Concatenate sequences. +mkSeqConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST +mkSeqConcat = liftFun2 Base.mkSeqConcat + +-- | Check if prefix is a prefix of s. +mkSeqPrefix :: MonadZ3 z3 + => AST -- ^ prefix + -> AST -- ^ s + -> z3 AST +mkSeqPrefix = liftFun2 Base.mkSeqPrefix + +-- | Check if suffix is a suffix of s. +mkSeqSuffix :: MonadZ3 z3 + => AST -- ^ suffix + -> AST -- ^ s + -> z3 AST +mkSeqSuffix = liftFun2 Base.mkSeqSuffix + +-- | Check if container contains containee. +mkSeqContains :: MonadZ3 z3 + => AST -- ^ container + -> AST -- ^ containee + -> z3 AST +mkSeqContains = liftFun2 Base.mkSeqContains + +-- | Extract subsequence starting at offset of length. +mkSeqExtract :: MonadZ3 z3 + => AST -- ^ s + -> AST -- ^ offset + -> AST -- ^ length + -> z3 AST +mkSeqExtract = liftFun3 Base.mkSeqExtract + +-- | Replace the first occurrence of src with dst in s. +mkSeqReplace :: MonadZ3 z3 + => AST -- ^ s + -> AST -- ^ src + -> AST -- ^ dst + -> z3 AST +mkSeqReplace = liftFun3 Base.mkSeqReplace + +-- | Retrieve from s the unit sequence positioned at position index. +mkSeqAt :: MonadZ3 z3 + => AST -- ^ s + -> AST -- ^ index + -> z3 AST +mkSeqAt = liftFun2 Base.mkSeqAt + +-- | Return the length of the sequence s. +mkSeqLength :: MonadZ3 z3 => AST -> z3 AST +mkSeqLength = liftFun1 Base.mkSeqLength + +-- | Return index of first occurrence of substr in s starting from offset +-- offset. If s does not contain substr, then the value is -1, if offset is the +-- length of s, then the value is -1 as well. The function is under-specified if +-- offset is negative or larger than the length of s. +mkSeqIndex :: MonadZ3 z3 + => AST -- ^ s + -> AST -- ^ substr + -> AST -- ^ offset + -> z3 AST +mkSeqIndex = liftFun3 Base.mkSeqIndex + +-- | Convert string to integer. +mkStrToInt :: MonadZ3 z3 => AST -> z3 AST +mkStrToInt = liftFun1 Base.mkStrToInt + +-- | Integer to string conversion. +mkIntToStr :: MonadZ3 z3 => AST -> z3 AST +mkIntToStr = liftFun1 Base.mkIntToStr + +-- | Create a regular expression that accepts the sequence. +mkSeqToRe :: MonadZ3 z3 => AST -> z3 AST +mkSeqToRe = liftFun1 Base.mkSeqToRe + +-- | Check if seq is in the language generated by the regular expression re. +mkSeqInRe :: MonadZ3 z3 + => AST -- ^ seq + -> AST -- ^ re + -> z3 AST +mkSeqInRe = liftFun2 Base.mkSeqInRe + +-- | Create the regular language re+. +mkRePlus :: MonadZ3 z3 => AST -> z3 AST +mkRePlus = liftFun1 Base.mkRePlus + +-- | Create the regular language re*. +mkReStar :: MonadZ3 z3 => AST -> z3 AST +mkReStar = liftFun1 Base.mkReStar + +-- | Create the regular language [re]. +mkReOption :: MonadZ3 z3 => AST -> z3 AST +mkReOption = liftFun1 Base.mkReOption + +-- | Create the union of the regular languages. +mkReUnion :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST +mkReUnion = liftFun2 Base.mkReUnion + +-- | Create the concatenation of the regular languages. +mkReConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST +mkReConcat = liftFun2 Base.mkReConcat + +-- | Create the range regular expression over two sequences of length 1. +mkReRange :: MonadZ3 z3 + => AST -- ^ lo + -> AST -- ^ hi + -> z3 AST +mkReRange = liftFun2 Base.mkReRange + +-- | Create a regular expression loop. The supplied regular expression r is +-- repeated between lo and hi times. The lo should be below hi with one +-- exception: when supplying the value hi as 0, the meaning is to repeat the +-- argument r at least lo number of times, and with an unbounded upper bound. +mkReLoop :: (Integral int, MonadZ3 z3) + => AST -- ^ r + -> int -- ^ lo + -> int -- ^ hi + -> z3 AST +mkReLoop = liftFun3 Base.mkReLoop + +-- | Create the intersection of the regular languages. +mkReIntersect :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST +mkReIntersect = liftFun2 Base.mkReIntersect + +-- | Create the complement of the regular language. +mkReComplement :: MonadZ3 z3 => AST -> z3 AST +mkReComplement = liftFun1 Base.mkReComplement + +-- | Create an empty regular expression of sort re. +mkReEmpty :: MonadZ3 z3 => Sort -> z3 AST +mkReEmpty = liftFun1 Base.mkReEmpty + +-- | Create an universal regular expression of sort re. +mkReFull :: MonadZ3 z3 => Sort -> z3 AST +mkReFull = liftFun1 Base.mkReFull + + +--------------------------------------------------------------------- -- Quantifiers mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern @@ -1686,6 +1971,9 @@ substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST substituteVars = liftFun2 Base.substituteVars +substitute :: MonadZ3 z3 => AST -> [(AST, AST)] -> z3 AST +substitute = liftFun2 Base.substitute + --------------------------------------------------------------------- -- Models @@ -1747,6 +2035,9 @@ isAsArray :: MonadZ3 z3 => AST -> z3 Bool isAsArray = liftFun1 Base.isAsArray +isEqAST :: MonadZ3 z3 => AST -> AST -> z3 Bool +isEqAST = liftFun2 Base.isEqAST + addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp addFuncInterp = liftFun3 Base.addFuncInterp @@ -1988,9 +2279,6 @@ -> z3 AST parseSMTLib2File = liftFun5 Base.parseSMTLib2File -getParserError :: MonadZ3 z3 => z3 String -getParserError = liftScalar Base.getParserError - --------------------------------------------------------------------- -- Miscellaneous @@ -2004,12 +2292,6 @@ class MonadZ3 m => MonadFixedpoint m where getFixedpoint :: m Base.Fixedpoint -fixedpointPush :: MonadFixedpoint z3 => z3 () -fixedpointPush = liftFixedpoint0 Base.fixedpointPush - -fixedpointPop :: MonadFixedpoint z3 => z3 () -fixedpointPop = liftFixedpoint0 Base.fixedpointPush - fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 () fixedpointAddRule = liftFixedpoint2 Base.fixedpointAddRule @@ -2029,30 +2311,77 @@ fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions --------------------------------------------------------------------- --- * Interpolation +-- Optimization -mkInterpolant :: MonadZ3 z3 => AST -> z3 AST -mkInterpolant = liftFun1 Base.mkInterpolant +class MonadZ3 m => MonadOptimize m where + getOptimize :: m Base.Optimize -getInterpolant :: MonadZ3 z3 => AST -> AST -> Params -> z3 [AST] -getInterpolant = liftFun3 Base.getInterpolant +optimizeAssert :: MonadOptimize z3 => AST -> z3 () +optimizeAssert = liftOptimize1 Base.optimizeAssert -computeInterpolant :: MonadZ3 z3 => AST -> Params - -> z3 (Maybe (Either Model [AST])) -computeInterpolant = liftFun2 Base.computeInterpolant +optimizeAssertAndTrack :: MonadOptimize z3 => AST -> AST -> z3 () +optimizeAssertAndTrack = liftOptimize2 Base.optimizeAssertAndTrack -readInterpolationProblem :: MonadZ3 z3 => FilePath -> z3 (Either String Base.InterpolationProblem) -readInterpolationProblem = liftFun1 Base.readInterpolationProblem +optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 () +optimizeAssertSoft = undefined -checkInterpolant :: MonadZ3 z3 => Base.InterpolationProblem -> [AST] -> z3 (Result, Maybe String) -checkInterpolant = liftFun2 Base.checkInterpolant +optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int +optimizeMaximize = liftOptimize1 Base.optimizeMaximize -interpolationProfile :: MonadZ3 z3 => z3 String -interpolationProfile = liftScalar Base.interpolationProfile +optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int +optimizeMinimize = liftOptimize1 Base.optimizeMinimize -writeInterpolationProblem :: MonadZ3 z3 => FilePath -> Base.InterpolationProblem -> z3 () -writeInterpolationProblem = liftFun2 Base.writeInterpolationProblem +optimizePush :: MonadOptimize z3 => z3 () +optimizePush = liftOptimize0 Base.optimizePush +optimizePop :: MonadOptimize z3 => z3 () +optimizePop = liftOptimize0 Base.optimizePop + +optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result +optimizeCheck = liftOptimize1 Base.optimizeCheck + +optimizeGetReasonUnknown :: MonadOptimize z3 => z3 String +optimizeGetReasonUnknown = liftOptimize0 Base.optimizeGetReasonUnknown + +optimizeGetModel :: MonadOptimize z3 => z3 Model +optimizeGetModel = liftOptimize0 Base.optimizeGetModel + +optimizeGetUnsatCore :: MonadOptimize z3 => z3 [AST] +optimizeGetUnsatCore = liftOptimize0 Base.optimizeGetUnsatCore + +optimizeSetParams :: MonadOptimize z3 => Params -> z3 () +optimizeSetParams = liftOptimize1 Base.optimizeSetParams + +optimizeGetLower :: MonadOptimize z3 => Int -> z3 AST +optimizeGetLower = liftOptimize1 Base.optimizeGetLower + +optimizeGetUpper :: MonadOptimize z3 => Int -> z3 AST +optimizeGetUpper = liftOptimize1 Base.optimizeGetLower + +optimizeGetUpperAsVector :: MonadOptimize z3 => Int -> z3 [AST] +optimizeGetUpperAsVector = liftOptimize1 Base.optimizeGetUpperAsVector + +optimizeGetLowerAsVector :: MonadOptimize z3 => Int -> z3 [AST] +optimizeGetLowerAsVector = liftOptimize1 Base.optimizeGetLowerAsVector + +optimizeToString :: MonadOptimize z3 => z3 String +optimizeToString = liftOptimize0 Base.optimizeToString + +optimizeFromString :: MonadOptimize z3 => String -> z3 () +optimizeFromString = liftOptimize1 Base.optimizeFromString + +optimizeFromFile :: MonadOptimize z3 => String -> z3 () +optimizeFromFile = liftOptimize1 Base.optimizeFromFile + +optimizeGetHelp :: MonadOptimize z3 => z3 String +optimizeGetHelp = liftOptimize0 Base.optimizeGetHelp + +optimizeGetAssertions :: MonadOptimize z3 => z3 [AST] +optimizeGetAssertions = liftOptimize0 Base.optimizeGetAssertions + +optimizeGetObjectives :: MonadOptimize z3 => z3 [AST] +optimizeGetObjectives = liftOptimize0 Base.optimizeGetObjectives + --------------------------------------------------------------------- -- * Solvers @@ -2122,6 +2451,14 @@ -- or if the result was 'Unsat'. solverGetModel :: MonadZ3 z3 => z3 Model solverGetModel = liftSolver0 Base.solverGetModel +-- +-- | Retrieve the proof for the last 'solverCheck' or 'solverCheckAssumptions'. +-- +-- The error handler is invoked if a proof is not available because +-- the commands above were not invoked for the given solver, +-- or if the result was different from 'Unsat' (so 'Sat' does not have a proof). +solverGetProof :: MonadZ3 z3 => z3 AST +solverGetProof = liftSolver0 Base.solverGetProof -- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions solverGetUnsatCore :: MonadZ3 z3 => z3 [AST] diff --git a/test/Z3/Base/Spec.hs b/test/Z3/Base/Spec.hs --- a/test/Z3/Base/Spec.hs +++ b/test/Z3/Base/Spec.hs @@ -39,11 +39,47 @@ Z3.getInt ctx ast; assert $ x == i + context "AST Equality and Substitution" $ do + specify "isEqAST" $ \ctx -> + monadicIO $ do + (r1, r2) <- run $ do + x1 <- Z3.mkFreshIntVar ctx "x1" + x2 <- Z3.mkFreshIntVar ctx "x2" + x3 <- Z3.mkFreshIntVar ctx "x3" + + s <- Z3.mkAdd ctx [x1, x2] + s' <- Z3.mkAdd ctx [x1, x2] + s23 <- Z3.mkAdd ctx [x2, x3] + + r1 <- Z3.isEqAST ctx s s' + r2 <- Z3.isEqAST ctx s s23 + + return (r1, r2) + assert r1 + assert (not r2) + + specify "substitute" $ \ctx -> + monadicIO $ do + r <- run $ do + x1 <- Z3.mkFreshIntVar ctx "x1" + x2 <- Z3.mkFreshIntVar ctx "x2" + x3 <- Z3.mkFreshIntVar ctx "x3" + x4 <- Z3.mkFreshIntVar ctx "x4" + + s12 <- Z3.mkAdd ctx [x1, x2] + s34 <- Z3.mkAdd ctx [x3, x4] + + s34' <- Z3.substitute ctx s12 [(x1, x3), (x2, x4)] + + Z3.isEqAST ctx s34 s34' + assert r + context "Bit-vectors" $ do specify "mkBvmul" $ \ctx -> - let bad = do + let bad = do { x <- Z3.mkFreshIntVar ctx "x"; Z3.mkBvmul ctx x x - in bad `shouldThrow` anyZ3Error - + } + in + bad `shouldThrow` anyZ3Error diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -1,5 +1,5 @@ Name: z3 -Version: 4.3.1 +Version: 408.2 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 4./x/ Theorem Prover (). @@ -30,10 +30,10 @@ Author: Iago Abal , David Castro Maintainer: Iago Abal -Copyright: 2012-2018, Iago Abal, David Castro +Copyright: 2012-2020, Iago Abal, David Castro Category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors Build-type: Simple -Cabal-version: >= 1.8 +Cabal-version: >= 1.10 Extra-source-files: README.md CHANGES.md HACKING.md @@ -59,14 +59,17 @@ -- 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 + if impl(ghc < 8) + Build-depends: semigroups >= 0.5 Build-tools: hsc2hs - Extensions: FlexibleInstances + + Default-language: Haskell2010 + Default-extensions: FlexibleInstances FlexibleContexts ForeignFunctionInterface MultiParamTypeClasses - Other-extensions: CPP DeriveDataTypeable EmptyDataDecls @@ -93,10 +96,12 @@ Build-depends: base >=4.5, z3, containers, - mtl >2.1 + transformers >= 0.2 else Buildable: False + Default-language: Haskell2010 + Hs-source-dirs: examples Main-Is: Examples.hs @@ -104,7 +109,6 @@ Example.Monad.Queens4All Example.Monad.DataTypes Example.Monad.FuncModel - Example.Monad.Interpolation Example.Monad.MutuallyRecursive Example.Monad.ParserInterface Example.Monad.Quantifiers @@ -118,7 +122,8 @@ Ghc-options: -Wall - Extensions: ScopedTypeVariables + Default-language: Haskell2010 + Default-extensions: ScopedTypeVariables Hs-source-dirs: test