packages feed

z3 4.3.1 → 408.2

raw patch · 14 files changed

Files

CHANGES.md view
@@ -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
README.md view
@@ -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:++    <z3-version>.<bindings-version>[.<patch-level>]++The `<z3-version>` indicates which version of Z3 is supported, it is computed as+_x*100+y_ for Z3 _x.y_. For example, versions _408.y.z_ of these bindings are+meant to support versions _4.8.*_ of Z3.+This version policy is in line with Haskell's PVP.  ## Installation
examples/Example/Monad/DataTypes.hs view
@@ -3,7 +3,7 @@ module Example.Monad.DataTypes where  import Z3.Monad-import Control.Monad.Trans (liftIO)+import Control.Monad.IO.Class (liftIO)  run :: IO () run = evalZ3 datatypeScript
− examples/Example/Monad/Interpolation.hs 
@@ -1,35 +0,0 @@--- | Compute interpolant for an unsatisfiable conjunction of formulas-module Example.Monad.Interpolation-  ( run )-  where--import Control.Monad-import Control.Monad.Trans ( liftIO )--import Z3.Monad--run :: IO ()-run = do-    env <- newItpEnv Nothing stdOpts-    evalZ3WithEnv z3 env--z3 = do-    a <- mkFreshBoolVar "a"-    b <- mkFreshBoolVar "b"--    na <- mkNot a-    nb <- mkNot b--    f1 <- mkIff a b-    f2 <- mkIff a nb--    g1 <- mkInterpolant f1-    g2 <- mkInterpolant f2-    g3 <- mkInterpolant =<< mkTrue--    params <- mkParams-    res <- flip computeInterpolant params =<< mkAnd [g1, g2, g3]--    case res of-        Just (Right itps) -> mapM_ (liftIO . putStrLn <=< astToString) itps-        otherwise         -> error "could not compute interpolants"
examples/Example/Monad/MutuallyRecursive.hs view
@@ -3,7 +3,7 @@ module Example.Monad.MutuallyRecursive where  import Z3.Monad-import Control.Monad.Trans (liftIO)+import Control.Monad.IO.Class (liftIO)  run :: IO () run = evalZ3 datatypeScript
examples/Example/Monad/QuantifierElimination.hs view
@@ -3,7 +3,7 @@   where  import Control.Monad-import Control.Monad.Trans ( liftIO )+import Control.Monad.IO.Class (liftIO)  import Z3.Monad
examples/Example/Monad/Quantifiers.hs view
@@ -3,7 +3,7 @@   where  import Control.Monad-import Control.Monad.Trans ( liftIO )+import Control.Monad.IO.Class (liftIO)  import Z3.Monad
examples/Example/Monad/ToSMTLib.hs view
@@ -5,7 +5,6 @@  import Control.Applicative import Control.Monad ( join )-import Control.Monad.Trans import Data.Maybe import qualified Data.Traversable as T
examples/Examples.hs view
@@ -10,7 +10,6 @@ import qualified Example.Monad.QuantifierElimination import qualified Example.Monad.ToSMTLib import qualified Example.Monad.Tuple-import qualified Example.Monad.Interpolation import qualified Example.Monad.ParserInterface  import System.Environment@@ -27,9 +26,6 @@     )   , ("funcModel"     , Example.Monad.FuncModel.run-    )-  , ("interpolation"-    , Example.Monad.Interpolation.run     )   , ("mutuallyRecursive"     , Example.Monad.MutuallyRecursive.run
src/Z3/Base.hs view
@@ -105,6 +105,7 @@   , mkIntSort   , mkRealSort   , mkBvSort+  , mkFiniteDomainSort   , mkArraySort   , mkTupleSort   , mkConstructor@@ -142,6 +143,7 @@   , mkAnd   , mkOr   , mkDistinct+  , mkDistinct1   -- ** Helpers   , mkBool @@ -149,6 +151,7 @@   , mkAdd   , mkMul   , mkSub+  , mkSub1   , mkUnaryMinus   , mkDiv   , mkMod@@ -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 <model>)@--- /unsat/   -> @Just (Right <interp>)@--- /unknown/ -> @Nothing@-computeInterpolant :: Context -> AST -> Params-                   -> IO (Maybe (Either Model [AST]))-computeInterpolant c p ps =-  alloca $ \interp ->-  alloca $ \model ->-  h2c p $ \pat -> do-  h2c ps $ \params -> do-    res <- toHsCheckError c $ \ctx ->-      z3_compute_interpolant ctx pat params interp model-    case res of-         Sat   -> Just . Left <$> peekToHs c model-         Unsat -> Just . Right <$> peekToHs c interp-         Undef -> return Nothing+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
src/Z3/Base/C.hsc view
@@ -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: <http://z3prover.github.io/api/html/group__capi.html#ga62166c0e3f9a8be4ba492eee5a52ce1b>+foreign import ccall unsafe "Z3_mk_finite_domain_sort"+    z3_mk_finite_domain_sort :: Ptr Z3_context -> Ptr Z3_symbol -> CULLong -> IO (Ptr Z3_sort)+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688> foreign import ccall unsafe "Z3_mk_bv_sort"     z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort)@@ -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: <http://z3prover.github.io/api/html/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85>@@ -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: <https://z3prover.github.io/api/html/group__capi.html#ga0f8ba9b735388e010044b8a1d39c6af0>+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: <https://z3prover.github.io/api/html/group__capi.html#gabc6d17e7862f2db40c778409152e931f>+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: <http://z3prover.github.io/api/html/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda> 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: <http://z3prover.github.io/api/html/group__capi.html#ga0d5e342cd83ed43185bcfdc583513959>-foreign import ccall unsafe "Z3_mk_interpolant"-    z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1fd3d3fe7bc4426c4787c3cc8cf92864>-foreign import ccall unsafe "Z3_mk_interpolation_context"-    z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context)---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad4417737993c62d39a6624118427f506>-foreign import ccall unsafe "Z3_get_interpolant"-    z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast-                       -> Ptr Z3_params -> IO (Ptr Z3_ast_vector)---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf62f6b456349886273e15d3cfe8656fe>-foreign import ccall unsafe "Z3_compute_interpolant"-    z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params-                           -> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model)-                           -> IO Z3_lbool---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2bf6a92d53d65fc32163792bedd5d31f>-foreign import ccall unsafe "Z3_read_interpolation_problem"-    z3_read_interpolation_problem :: Ptr Z3_context -> Ptr CUInt -> Ptr (Ptr Z3_ast)-                                  -> Ptr (Ptr CUInt) -> Ptr CChar -> Ptr Z3_string-                                  -- TODO: report "inexact" result type-                                  -> Ptr CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_bool---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gadf50d7093abe5a892593baef552bbf89>-foreign import ccall unsafe "Z3_check_interpolant"-    z3_check_interpolant :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt-                         -> Ptr (Ptr Z3_ast) -> Ptr Z3_string -> CUInt-                         -- TODO: report "inexact" result type-                         -> Ptr (Ptr Z3_ast) -> IO Z3_lbool---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad45c5746cd1eefe4f2fc6df956c9cd8e>-foreign import ccall unsafe "Z3_interpolation_profile"-    z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2a8ee59130e23e10568a1f70e387c608>-foreign import ccall unsafe "Z3_write_interpolation_problem"-    z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast)-                                   -> Ptr CUInt -> Ptr CChar -> CUInt-                                   -> Ptr (Ptr Z3_ast) -> IO ()----------------------------------------------------------------------- -- * Tactics  -- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaa4b9d53ba194d2d3a8bb2f55bec7e78e>@@ -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: <http://z3prover.github.io/api/html/group__capi.html#gaba0fc4849eb0d1538d52aaa08f86a7c0>+foreign import ccall unsafe "Z3_solver_get_proof"+    z3_solver_get_proof :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast)+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabb4f8ed6a09873f5aeefe9cc01010864> 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 <http://z3prover.github.io/api/html/group__capi.html#ga96b11da43464071c4ec35418d1cc3483>-foreign import ccall unsafe "Z3_get_parser_error"-  z3_get_parser_error :: Ptr Z3_context -> IO Z3_string- --------------------------------------------------------------------- -- * Error Handling @@ -1497,11 +1576,7 @@  -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6> foreign import ccall unsafe "Z3_get_error_msg"-    z3_get_error_msg :: Z3_error_code -> IO Z3_string---- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92>-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)
src/Z3/Monad.hs view
@@ -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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>@@ -675,11 +763,11 @@                                                -- constructor and projections. mkTupleSort = liftFun2 Base.mkTupleSort --- | Create a contructor+-- | Create a constructor -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0> 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7> mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST mkDistinct = liftFun1 Base.mkDistinct +-- | Same as 'mkDistinct' but type-safe.+mkDistinct1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST+mkDistinct1 = liftFun1 Base.mkDistinct1+ -- | Create an AST node representing /not(a)/. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>@@ -903,10 +997,16 @@  -- | Create an AST node representing args[0] - ... - args[num_args - 1]. --+-- Requires a non-empty list.+-- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9> mkSub :: MonadZ3 z3 => [AST] -> z3 AST mkSub = liftFun1 Base.mkSub +-- | Same as 'mkSub' but type-safe.+mkSub1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST+mkSub1 = liftFun1 Base.mkSub1+ -- | Create an AST node representing -arg. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>@@ -1288,7 +1388,7 @@ mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST mkSelect = liftFun2 Base.mkSelect --- | Array update.   +-- | Array update. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593> 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]
test/Z3/Base/Spec.hs view
@@ -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
z3.cabal view
@@ -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 (<https://github.com/Z3Prover/z3>).@@ -30,10 +30,10 @@ Author:              Iago Abal <mail@iagoabal.eu>,                      David Castro <david.castro.dcp@gmail.com> Maintainer:          Iago Abal <mail@iagoabal.eu>-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 <<loop>> 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