z3 0.3.0 → 0.3.1

raw patch · 7 files changed

+1200/−238 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Z3.Base: FuncModel :: [([AST], AST)] -> AST -> FuncModel

+ Z3.Base: benchmarkToSMTLibString :: Context -> String -> String -> String -> String -> [AST] -> AST -> IO String

+ Z3.Base: contextToString :: Context -> IO String

+ Z3.Base: data FuncEntry

+ Z3.Base: data FuncInterp

+ Z3.Base: data FuncModel

+ Z3.Base: evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)

+ Z3.Base: evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)

+ Z3.Base: funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST

+ Z3.Base: funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int

+ Z3.Base: funcEntryGetValue :: Context -> FuncEntry -> IO AST

+ Z3.Base: funcInterpGetArity :: Context -> FuncInterp -> IO Int

+ Z3.Base: funcInterpGetElse :: Context -> FuncInterp -> IO AST

+ Z3.Base: funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry

+ Z3.Base: funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int

+ Z3.Base: getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl

+ Z3.Base: getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)

+ Z3.Base: instance Eq FuncEntry

+ Z3.Base: instance Eq FuncInterp

+ Z3.Base: interpElse :: FuncModel -> AST

+ Z3.Base: interpMap :: FuncModel -> [([AST], AST)]

+ Z3.Base: isAsArray :: Context -> AST -> IO Bool

+ Z3.Base: mkIntSymbol :: Integral int => Context -> int -> IO Symbol

+ Z3.Base: mkTupleSort :: Context -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])

+ Z3.Base: mkUninterpretedSort :: Context -> Symbol -> IO Sort

+ Z3.Base: modelToString :: Context -> Model -> IO String

+ Z3.Monad: FuncModel :: [([AST], AST)] -> AST -> FuncModel

+ Z3.Monad: benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String

+ Z3.Monad: contextToString :: MonadZ3 z3 => z3 String

+ Z3.Monad: data FuncEntry

+ Z3.Monad: data FuncInterp

+ Z3.Monad: data FuncModel

+ Z3.Monad: evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)

+ Z3.Monad: evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)

+ Z3.Monad: funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST

+ Z3.Monad: funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int

+ Z3.Monad: funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST

+ Z3.Monad: funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int

+ Z3.Monad: funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST

+ Z3.Monad: funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry

+ Z3.Monad: funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int

+ Z3.Monad: getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl

+ Z3.Monad: getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int

+ Z3.Monad: getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)

+ Z3.Monad: interpElse :: FuncModel -> AST

+ Z3.Monad: interpMap :: FuncModel -> [([AST], AST)]

+ Z3.Monad: isAsArray :: MonadZ3 z3 => AST -> z3 Bool

+ Z3.Monad: mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST

+ Z3.Monad: mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort

+ Z3.Monad: mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST

+ Z3.Monad: mkBvSort :: MonadZ3 z3 => Int -> z3 Sort

+ Z3.Monad: mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST

+ Z3.Monad: mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST

+ Z3.Monad: mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvneg :: MonadZ3 z3 => AST -> z3 AST

+ Z3.Monad: mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST

+ Z3.Monad: mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvnot :: MonadZ3 z3 => AST -> z3 AST

+ Z3.Monad: mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvredand :: MonadZ3 z3 => AST -> z3 AST

+ Z3.Monad: mkBvredor :: MonadZ3 z3 => AST -> z3 AST

+ Z3.Monad: mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST

+ Z3.Monad: mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST

+ Z3.Monad: mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST

+ Z3.Monad: mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol

+ Z3.Monad: mkMap :: MonadZ3 z3 => FuncDecl -> Int -> [AST] -> z3 AST

+ Z3.Monad: mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST

+ Z3.Monad: mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST

+ Z3.Monad: mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST

+ Z3.Monad: mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST

+ Z3.Monad: mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST

+ Z3.Monad: mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST

+ Z3.Monad: mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])

+ Z3.Monad: mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort

+ Z3.Monad: mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST

+ Z3.Monad: modelToString :: MonadZ3 z3 => Model -> z3 String

Files

Z3/Base.hs +447/−200
Z3/Base/C.hsc +133/−2
Z3/Lang/Monad.hs +6/−7
Z3/Lang/Nat.hs +8/−0
Z3/Lang/Prelude.hs +12/−13
Z3/Monad.hs +586/−9
z3.cabal +8/−7

Z3/Base.hs view

@@ -16,199 +16,220 @@ -- TODO Rename showModel and showContext to match Z3 C API names. module Z3.Base ( -    -- * Types-      Config-    , Context-    , Symbol-    , AST-    , Sort-    , FuncDecl-    , App-    , Pattern-    , Model-    , Params-    , Solver+  -- * Types+    Config+  , Context+  , Symbol+  , AST+  , Sort+  , FuncDecl+  , App+  , Pattern+  , Model+  , FuncInterp+  , FuncEntry+  , Params+  , Solver -    -- ** Satisfiability result-    , Result(..)+  -- ** Satisfiability result+  , Result(..) -    -- * Configuration-    , mkConfig-    , delConfig-    , withConfig-    , setParamValue+  -- * Configuration+  , mkConfig+  , delConfig+  , withConfig+  , setParamValue -    -- * Context-    , mkContext-    , delContext-    , withContext+  -- * Context+  , mkContext+  , delContext+  , withContext+  , contextToString+  , showContext -    -- * Symbols-    , mkStringSymbol+  -- * Symbols+  , mkIntSymbol+  , mkStringSymbol -    -- * Sorts-    , mkBoolSort-    , mkIntSort-    , mkRealSort-    , mkBvSort-    , mkArraySort+  -- * Sorts+  , mkUninterpretedSort+  , mkBoolSort+  , mkIntSort+  , mkRealSort+  , mkBvSort+  , mkArraySort+  , mkTupleSort -    -- * Constants and Applications-    , mkFuncDecl-    , mkApp-    , mkConst-    , mkTrue-    , mkFalse-    , mkEq-    , mkNot-    , mkIte-    , mkIff-    , mkImplies-    , mkXor-    , mkAnd-    , mkOr-    , mkDistinct-    , mkAdd-    , mkMul-    , mkSub-    , mkUnaryMinus-    , mkDiv-    , mkMod-    , mkRem-    , mkLt-    , mkLe-    , mkGt-    , mkGe-    , mkInt2Real-    , mkReal2Int-    , mkIsInt+  -- * Constants and Applications+  , mkFuncDecl+  , mkApp+  , mkConst+  , mkTrue+  , mkFalse+  , mkEq+  , mkNot+  , mkIte+  , mkIff+  , mkImplies+  , mkXor+  , mkAnd+  , mkOr+  , mkDistinct+  , mkAdd+  , mkMul+  , mkSub+  , mkUnaryMinus+  , mkDiv+  , mkMod+  , mkRem+  , mkLt+  , mkLe+  , mkGt+  , mkGe+  , mkInt2Real+  , mkReal2Int+  , mkIsInt -    -- * Bit-vectors-    , mkBvnot-    , mkBvredand-    , mkBvredor-    , mkBvand-    , mkBvor-    , mkBvxor-    , mkBvnand-    , mkBvnor-    , mkBvxnor-    , mkBvneg-    , mkBvadd-    , mkBvsub-    , mkBvmul-    , mkBvudiv-    , mkBvsdiv-    , mkBvurem-    , mkBvsrem-    , mkBvsmod-    , mkBvult-    , mkBvslt-    , mkBvule-    , mkBvsle-    , mkBvuge-    , mkBvsge-    , mkBvugt-    , mkBvsgt-    , mkConcat-    , mkExtract-    , mkSignExt-    , mkZeroExt-    , mkRepeat-    , mkBvshl-    , mkBvlshr-    , mkBvashr-    , mkRotateLeft-    , mkRotateRight-    , mkExtRotateLeft-    , mkExtRotateRight-    , mkInt2bv-    , mkBv2int-    , mkBvnegNoOverflow-    , mkBvaddNoOverflow-    , mkBvaddNoUnderflow-    , mkBvsubNoOverflow-    , mkBvsubNoUnderflow-    , mkBvmulNoOverflow-    , mkBvmulNoUnderflow-    , mkBvsdivNoOverflow+  -- * Bit-vectors+  , mkBvnot+  , mkBvredand+  , mkBvredor+  , mkBvand+  , mkBvor+  , mkBvxor+  , mkBvnand+  , mkBvnor+  , mkBvxnor+  , mkBvneg+  , mkBvadd+  , mkBvsub+  , mkBvmul+  , mkBvudiv+  , mkBvsdiv+  , mkBvurem+  , mkBvsrem+  , mkBvsmod+  , mkBvult+  , mkBvslt+  , mkBvule+  , mkBvsle+  , mkBvuge+  , mkBvsge+  , mkBvugt+  , mkBvsgt+  , mkConcat+  , mkExtract+  , mkSignExt+  , mkZeroExt+  , mkRepeat+  , mkBvshl+  , mkBvlshr+  , mkBvashr+  , mkRotateLeft+  , mkRotateRight+  , mkExtRotateLeft+  , mkExtRotateRight+  , mkInt2bv+  , mkBv2int+  , mkBvnegNoOverflow+  , mkBvaddNoOverflow+  , mkBvaddNoUnderflow+  , mkBvsubNoOverflow+  , mkBvsubNoUnderflow+  , mkBvmulNoOverflow+  , mkBvmulNoUnderflow+  , mkBvsdivNoOverflow -    -- * Arrays-    , mkSelect-    , mkStore-    , mkConstArray-    , mkMap-    , mkArrayDefault+  -- * Arrays+  , mkSelect+  , mkStore+  , mkConstArray+  , mkMap+  , mkArrayDefault -    -- * Numerals-    , mkNumeral-    , mkInt-    , mkReal+  -- * Numerals+  , mkNumeral+  , mkInt+  , mkReal -    -- * Quantifiers-    , mkPattern-    , mkBound-    , mkForall-    , mkExists+  -- * Quantifiers+  , mkPattern+  , mkBound+  , mkForall+  , mkExists -    -- * Accessors-    , getBvSortSize-    , getSort-    , getBool-    , getInt-    , getReal+  -- * Accessors+  , getBvSortSize+  , getSort+  , getBool+  , getInt+  , getReal -    -- * Models-    , eval-    , evalT-    , showModel-    , showContext+  -- * Models+  , FuncModel (..)+  , eval+  , evalT+  , evalFunc+  , evalArray+  , getFuncInterp+  , isAsArray+  , getAsArrayFuncDecl+  , funcInterpGetNumEntries+  , funcInterpGetEntry+  , funcInterpGetElse+  , funcInterpGetArity+  , funcEntryGetValue+  , funcEntryGetNumArgs+  , funcEntryGetArg+  , modelToString+  , showModel -    -- * Constraints-    , assertCnstr-    , check-    , getModel-    , delModel-    , push-    , pop+  -- * Constraints+  , assertCnstr+  , check+  , getModel+  , delModel+  , push+  , pop  -    -- * Parameters-    , mkParams-    , paramsSetBool-    , paramsSetUInt-    , paramsSetDouble-    , paramsSetSymbol-    , paramsToString+  -- * Parameters+  , mkParams+  , paramsSetBool+  , paramsSetUInt+  , paramsSetDouble+  , paramsSetSymbol+  , paramsToString -    -- * Solvers-    , Logic(..)-    , mkSolver-    , mkSimpleSolver-    , mkSolverForLogic-    , solverSetParams-    , solverPush-    , solverPop-    , solverReset-    , solverAssertCnstr-    , solverAssertAndTrack-    , solverCheck-    --, solverGetModel-    , solverCheckAndGetModel-    , solverGetReasonUnknown+  -- * Solvers+  , Logic(..)+  , mkSolver+  , mkSimpleSolver+  , mkSolverForLogic+  , solverSetParams+  , solverPush+  , solverPop+  , solverReset+  , solverAssertCnstr+  , solverAssertAndTrack+  , solverCheck+  --, solverGetModel+  , solverCheckAndGetModel+  , solverGetReasonUnknown -    -- * String Conversion-    , ASTPrintMode(..)-    , setASTPrintMode-    , astToString-    , patternToString-    , sortToString-    , funcDeclToString+  -- * String Conversion+  , ASTPrintMode(..)+  , setASTPrintMode+  , astToString+  , patternToString+  , sortToString+  , funcDeclToString+  , benchmarkToSMTLibString -    -- * Error Handling-    , Z3Error(..)-    , Z3ErrorCode(..)-    ) where+  -- * Error Handling+  , Z3Error(..)+  , Z3ErrorCode(..)+  ) where  import Z3.Base.C @@ -268,6 +289,14 @@ newtype Model = Model { unModel :: Ptr Z3_model }     deriving Eq +-- | A interpretation of a function.+newtype FuncInterp = FuncInterp { unFuncInterp :: Ptr Z3_func_interp }+    deriving Eq++--  | An entry in an interpreted function+newtype FuncEntry = FuncEntry { unFuncEntry :: Ptr Z3_func_entry }+    deriving Eq+ -- | A Z3 parameter set. Starting at Z3 4.0, parameter sets are used -- to configure many components such as: simplifiers, tactics, -- solvers, etc.@@ -402,9 +431,33 @@ withContext :: Config -> (Context -> IO a) -> IO a withContext cfg = bracket (mkContext cfg) delContext +-- | Convert the given logical context into a string.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216>+contextToString :: Context -> IO String+contextToString c =+  checkError c $ z3_context_to_string (unContext c) >>= peekCString++-- | Alias for 'contextToString'.+showContext :: Context -> IO String+showContext = contextToString+ --------------------------------------------------------------------- -- Symbols +-- | Create a Z3 symbol using an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3df806baf6124df3e63a58cf23e12411>+mkIntSymbol :: Integral int => Context -> int -> IO Symbol+mkIntSymbol ctx i+  | 0 <= i && i <= 2^(30::Int)-1+  = Symbol <$> z3_mk_int_symbol (unContext ctx) (fromIntegral i)+  | otherwise+  = error "Z3.Base.mkIntSymbol: invalid range"++{-# SPECIALIZE mkIntSymbol :: Context -> Int -> IO Symbol #-}+{-# SPECIALIZE mkIntSymbol :: Context -> Integer -> IO Symbol #-}+ -- | Create a Z3 symbol using a string. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>@@ -418,8 +471,14 @@ -- Sorts  -- TODO Sorts: Z3_is_eq_sort--- TODO Sorts: Z3_mk_uninterpreted_sort +-- | Create a free (uninterpreted) type using the given name (symbol).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>+mkUninterpretedSort :: Context -> Symbol -> IO Sort+mkUninterpretedSort c sy = checkError c $+  Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy)+ -- | Create the /Boolean/ type. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>@@ -453,6 +512,30 @@ mkArraySort :: Context -> Sort -> Sort -> IO Sort mkArraySort c dom rng = checkError c $ Sort <$> z3_mk_array_sort (unContext c) (unSort dom) (unSort rng) +-- | Create a tuple type+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>+mkTupleSort :: Context                         -- ^ Context+            -> Symbol                          -- ^ Name of the sort+            -> [(Symbol, Sort)]                -- ^ Name and sort of each field+            -> IO (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function+                                               -- declarations for the+                                               -- constructor and projections.+mkTupleSort c sym symSorts = checkError c $+  let (syms, sorts) = unzip symSorts+  in withArrayLen (map unSymbol syms) $ \ n symsPtr ->+     withArray (map unSort sorts) $ \ sortsPtr ->+     alloca $ \ outConstrPtr ->+     allocaArray n $ \ outProjsPtr -> do+       sort <- checkError c $ z3_mk_tuple_sort+                   (unContext c) (unSymbol sym)+                   (fromIntegral n) symsPtr sortsPtr+                   outConstrPtr outProjsPtr+       outConstr <- peek outConstrPtr+       outProjs  <- peekArray n outProjsPtr+       return (Sort sort, FuncDecl outConstr, map FuncDecl outProjs)++ -- TODO Sorts: from Z3_mk_array_sort on  ---------------------------------------------------------------------@@ -1200,7 +1283,8 @@ -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4> getBool :: Context -> AST -> IO (Maybe Bool)-getBool c a = checkError c $ castLBool <$> z3_get_bool_value (unContext c) (unAST a)+getBool c a = checkError c $+  castLBool <$> z3_get_bool_value (unContext c) (unAST a)  -- | Return numeral value, as a string of a numeric constant term. --@@ -1247,6 +1331,148 @@ evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST)) evalT c m = fmap T.sequence . T.mapM (eval c m) +-- | The interpretation of a function is a mapping part (arguments to values)+-- and an 'else' part.+data FuncModel = FuncModel+    { interpMap :: [([AST], AST)]+    , interpElse :: AST+    }++-- | Evaluate a function declaration to a list of argument/value pairs.+evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)+evalFunc ctx m fDecl =+    do interpMb <- getFuncInterp ctx m fDecl+       case interpMb of+         Nothing -> return Nothing+         Just interp ->+             do funcMap  <- getMapFromInterp ctx interp+                elsePart <- funcInterpGetElse ctx interp+                return (Just $ FuncModel funcMap elsePart)++-- | Evaluate an array as a function, if possible.+evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)+evalArray ctx model array =+    do -- The array must first be evaluated normally, to get it into+       -- 'as-array' form, which is required to acquire the FuncDecl.+       evaldArrayMb <- eval ctx model array+       case evaldArrayMb of+         Nothing -> return Nothing+         Just evaldArray ->+             do canConvert <- isAsArray ctx evaldArray+                if canConvert+                  then+                    do arrayDecl <- getAsArrayFuncDecl ctx evaldArray+                       evalFunc ctx model arrayDecl+                  else return Nothing+++-- | Return the function declaration f associated with a (_ as_array f) node.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>+getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl+getAsArrayFuncDecl ctx a = checkError ctx $+  FuncDecl <$> z3_get_as_array_func_decl (unContext ctx) (unAST a)++-- | The (_ as-array f) AST node is a construct for assigning interpretations+-- for arrays in Z3. It is the array such that forall indices i we have that+-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE+-- if the a is an as-array AST node.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>+isAsArray :: Context -> AST -> IO Bool+isAsArray ctx a = toBool <$> z3_is_as_array (unContext ctx) (unAST a)+++getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)]+getMapFromInterp ctx interp =+    do n <- funcInterpGetNumEntries ctx interp+       entries <- mapM (funcInterpGetEntry ctx interp) [0..n-1]+       mapM (getEntry ctx) entries++getEntry :: Context -> FuncEntry -> IO ([AST], AST)+getEntry ctx entry =+    do val <- funcEntryGetValue ctx entry+       args <- getEntryArgs ctx entry+       return (args, val)++getEntryArgs :: Context -> FuncEntry -> IO [AST]+getEntryArgs ctx entry =+    do n <- funcEntryGetNumArgs ctx entry+       mapM (funcEntryGetArg ctx entry) [0..n-1]++-- | Return the interpretation of the function f in the model m.+-- Return NULL, if the model does not assign an interpretation for f.+-- That should be interpreted as: the f does not matter.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>+getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)+getFuncInterp c m fd = do+  ptr <- checkError c $+           z3_model_get_func_interp (unContext c) (unModel m) (unFuncDecl fd)+  return $ FuncInterp <$> ptrToMaybe ptr++-- | Return the number of entries in the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>+funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int+funcInterpGetNumEntries ctx fi = checkError ctx $ fromIntegral <$>+  z3_func_interp_get_num_entries (unContext ctx) (unFuncInterp fi)++-- | Return a _point_ of the given function intepretation.+-- It represents the value of f in a particular point.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>+funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry+funcInterpGetEntry ctx fi i = checkError ctx $ FuncEntry <$>+  z3_func_interp_get_entry (unContext ctx) (unFuncInterp fi) (fromIntegral i)++-- | Return the 'else' value of the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>+funcInterpGetElse :: Context -> FuncInterp -> IO AST+funcInterpGetElse ctx fi = checkError ctx $+  AST <$> z3_func_interp_get_else (unContext ctx) (unFuncInterp fi)++-- | Return the arity (number of arguments) of the given function+-- interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>+funcInterpGetArity :: Context -> FuncInterp -> IO Int+funcInterpGetArity ctx fi = checkError ctx $+  fromIntegral <$> z3_func_interp_get_arity (unContext ctx) (unFuncInterp fi)++-- | Return the value of this point.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>+funcEntryGetValue :: Context -> FuncEntry -> IO AST+funcEntryGetValue ctx entry = checkError ctx $+  AST <$> z3_func_entry_get_value (unContext ctx) (unFuncEntry entry)++-- | Return the number of arguments in a Z3_func_entry object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>+funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int+funcEntryGetNumArgs ctx entry = checkError ctx $ fromIntegral <$>+  z3_func_entry_get_num_args (unContext ctx) (unFuncEntry entry)++-- | Return an argument of a Z3_func_entry object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>+funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST+funcEntryGetArg ctx entry i = checkError ctx $ AST <$>+  z3_func_entry_get_arg (unContext ctx) (unFuncEntry entry) (fromIntegral i)++-- | Convert the given model into a string.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>+modelToString :: Context -> Model -> IO String+modelToString c m = checkError c $+  z3_model_to_string (unContext c) (unModel m) >>= peekCString++-- | Alias for 'modelToString'.+showModel :: Context -> Model -> IO String+showModel = modelToString+ --------------------------------------------------------------------- -- Constraints @@ -1269,7 +1495,8 @@ -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a> assertCnstr :: Context -> AST -> IO ()-assertCnstr ctx ast = checkError ctx $ z3_assert_cnstr (unContext ctx) (unAST ast)+assertCnstr ctx ast = checkError ctx $+  z3_assert_cnstr (unContext ctx) (unAST ast)  -- | Get model (logical context is consistent) --@@ -1283,8 +1510,7 @@         peekModel p | p == nullPtr = return Nothing                     | otherwise    = mkModel <$> peek p         mkModel :: Ptr Z3_model -> Maybe Model-        mkModel p | p == nullPtr = Nothing-                  | otherwise    = Just $ Model p+        mkModel = fmap Model . ptrToMaybe  -- | Delete a model object. --@@ -1292,18 +1518,6 @@ delModel :: Context -> Model -> IO () delModel c m = checkError c $ z3_del_model (unContext c) (unModel m) --- | Convert the given model into a string.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>-showModel :: Context -> Model -> IO String-showModel c m = checkError c $ z3_model_to_string (unContext c) (unModel m) >>= peekCString---- | Convert the given logical context into a string.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216>-showContext :: Context -> IO String-showContext c = checkError c $ z3_context_to_string (unContext c) >>= peekCString- -- | Check whether the given logical context is consistent or not. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>@@ -1323,18 +1537,18 @@ mkParams c = checkError c $ Params <$> z3_mk_params (unContext c)  paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()-paramsSetBool c params sym b =-  checkError c $ z3_params_set_bool (unContext c) (unParams params) (unSymbol sym) (unBool b)+paramsSetBool c params sym b = checkError c $+  z3_params_set_bool (unContext c) (unParams params) (unSymbol sym) (unBool b)  paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()-paramsSetUInt c params sym v =-  checkError c $ z3_params_set_uint (unContext c) (unParams params) (unSymbol sym)-                                    (fromIntegral v)+paramsSetUInt c params sym v = checkError c $+  z3_params_set_uint (unContext c) (unParams params)+        (unSymbol sym) (fromIntegral v)  paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()-paramsSetDouble c params sym v =-  checkError c $ z3_params_set_double (unContext c) (unParams params) (unSymbol sym)-                                      (realToFrac v)+paramsSetDouble c params sym v = checkError c $+  z3_params_set_double (unContext c) (unParams params)+        (unSymbol sym) (realToFrac v)  paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO () paramsSetSymbol c params sym v =@@ -1596,3 +1810,36 @@ funcDeclToString :: Context -> FuncDecl -> IO String funcDeclToString ctx funcDecl =   checkError ctx $ z3_func_decl_to_string (unContext ctx) (unFuncDecl funcDecl) >>= peekCString++-- | Convert the given benchmark into SMT-LIB formatted string.+--+-- The output format can be configured via 'setASTPrintMode'.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4>+benchmarkToSMTLibString :: Context+                            -> String   -- ^ name+                            -> String   -- ^ logic+                            -> String   -- ^ status+                            -> String   -- ^ attributes+                            -> [AST]    -- ^ assumptions+                            -> AST      -- ^ formula+                            -> IO String+benchmarkToSMTLibString c name logic st attr assump f =+  withCString name $ \cname ->+  withCString logic $ \clogic ->+  withCString st $ \cst ->+  withCString attr $ \cattr ->+  withArray (map unAST assump) $ \cassump ->+    z3_benchmark_to_smtlib_string (unContext c) cname clogic cst cattr+                                  numAssump cassump (unAST f)+      >>= peekCString+  where numAssump = genericLength assump++---------------------------------------------------------------------+-- Utils++-- | Wraps a non-null pointer with 'Just', or else returns 'Nothing'.+ptrToMaybe :: Ptr a -> Maybe (Ptr a)+ptrToMaybe ptr | ptr == nullPtr = Nothing+               | otherwise      = Just ptr+

Z3/Base/C.hsc view

@@ -54,6 +54,12 @@ -- | A model for the constraints asserted into the logical context. data Z3_model +-- | The interpretation of a function returned from the model.+data Z3_func_interp++-- | An entry in a function interpretation.+data Z3_func_entry+ -- | A solver for Z3, that is, an engine for collecting and solving -- constraints using a specific algorithm or set of algorithms. data Z3_solver@@ -153,19 +159,29 @@ --------------------------------------------------------------------- -- * Symbols +-- | Create a Z3 symbol using an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3df806baf6124df3e63a58cf23e12411>+foreign import ccall unsafe "Z3_mk_int_symbol"+    z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol)+ -- | Create a Z3 symbol using a C string. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae> foreign import ccall unsafe "Z3_mk_string_symbol"     z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol) - --------------------------------------------------------------------- -- * Sorts  -- TODO Sorts: Z3_is_eq_sort--- TODO Sorts: Z3_mk_uninterpreted_sort +-- | Create a free (uninterpreted) type using the given name (symbol).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>+foreign import ccall unsafe "Z3_mk_uninterpreted_sort"+    z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort)+ -- | Create the Boolean type. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>@@ -198,6 +214,19 @@ foreign import ccall unsafe "Z3_mk_array_sort"     z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort) +-- | Create a tuple type+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>+foreign import ccall unsafe "Z3_mk_tuple_sort"+    z3_mk_tuple_sort :: Ptr Z3_context+                     -> Ptr Z3_symbol+                     -> CUInt+                     -> Ptr (Ptr Z3_symbol)+                     -> Ptr (Ptr Z3_sort)+                     -> Ptr (Ptr Z3_func_decl)+                     -> Ptr (Ptr Z3_func_decl)+                     -> IO (Ptr Z3_sort)+ -- TODO Sorts: from Z3_mk_array_sort on  @@ -867,6 +896,94 @@             -> Ptr (Ptr Z3_ast)             -> IO Z3_bool +-- | The (_ as-array f) AST node is a construct for assigning interpretations for+-- arrays in Z3. It is the array such that forall indices i we have that+-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE if+-- the a is an as-array AST node.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>+foreign import ccall unsafe "Z3_is_as_array"+    z3_is_as_array :: Ptr Z3_context+                   -> Ptr Z3_ast+                   -> IO Z3_bool++-- | Return the function declaration f associated with a (_ as_array f) node.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>+foreign import ccall unsafe "Z3_get_as_array_func_decl"+    z3_get_as_array_func_decl :: Ptr Z3_context+                              -> Ptr Z3_ast+                              -> IO (Ptr Z3_func_decl)++-- | Return the interpretation of the function f in the model m.+-- Return NULL, if the model does not assign an interpretation for f.+-- That should be interpreted as: the f does not matter.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>+foreign import ccall unsafe "Z3_model_get_func_interp"+    z3_model_get_func_interp :: Ptr Z3_context+                             -> Ptr Z3_model+                             -> Ptr Z3_func_decl+                             -> IO (Ptr Z3_func_interp)++-- | Return the number of entries in the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>+foreign import ccall unsafe "Z3_func_interp_get_num_entries"+    z3_func_interp_get_num_entries :: Ptr Z3_context+                                   -> Ptr Z3_func_interp+                                   -> IO CUInt++-- | Return a "point" of the given function intepretation.+-- It represents the value of f in a particular point.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>+foreign import ccall unsafe "Z3_func_interp_get_entry"+    z3_func_interp_get_entry :: Ptr Z3_context+                             -> Ptr Z3_func_interp+                             -> CUInt+                             -> IO (Ptr Z3_func_entry)++-- | Return the 'else' value of the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>+foreign import ccall unsafe "Z3_func_interp_get_else"+    z3_func_interp_get_else :: Ptr Z3_context+                            -> Ptr Z3_func_interp+                            -> IO (Ptr Z3_ast)+-- | Return the arity (number of arguments) of the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>+foreign import ccall unsafe "Z3_func_interp_get_arity"+    z3_func_interp_get_arity :: Ptr Z3_context+                             -> Ptr Z3_func_interp+                             -> IO CUInt++-- | Return the value of this point.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>+foreign import ccall unsafe "Z3_func_entry_get_value"+    z3_func_entry_get_value :: Ptr Z3_context+                            -> Ptr Z3_func_entry+                            -> IO (Ptr Z3_ast)++-- | Return the number of arguments in a Z3_func_entry object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>+foreign import ccall unsafe "Z3_func_entry_get_num_args"+    z3_func_entry_get_num_args :: Ptr Z3_context+                               -> Ptr Z3_func_entry+                               -> IO CUInt++-- | Return an argument of a Z3_func_entry object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>+foreign import ccall unsafe "Z3_func_entry_get_arg"+    z3_func_entry_get_arg :: Ptr Z3_context+                          -> Ptr Z3_func_entry+                          -> CUInt+                          -> IO (Ptr Z3_ast)+ --------------------------------------------------------------------- -- * Constraints @@ -1124,6 +1241,20 @@ -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga15243dcad77f5571e28e8aa1da465675> foreign import ccall unsafe "Z3_func_decl_to_string"     z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string++-- | Convert the given benchmark into SMT-LIB formatted string.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4>+foreign import ccall unsafe "Z3_benchmark_to_smtlib_string"+    z3_benchmark_to_smtlib_string :: Ptr Z3_context+                                      -> Z3_string        -- ^ name+                                      -> Z3_string        -- ^ logic+                                      -> Z3_string        -- ^ status+                                      -> Z3_string        -- ^ attributes+                                      -> CUInt            -- ^ assumptions#+                                      -> Ptr (Ptr Z3_ast) -- ^ assumptions+                                      -> Ptr Z3_ast       -- ^ formula+                                      -> IO Z3_string  --------------------------------------------------------------------- -- * Error Handling

Z3/Lang/Monad.hs view

@@ -4,6 +4,10 @@ {-# LANGUAGE NamedFieldPuns             #-} {-# LANGUAGE ScopedTypeVariables        #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}+  -- This is just to avoid warnings because we import fragile new Z3 API stuff+  -- from Z3.Base+ -- | -- Module    : Z3.Lang.Monad -- Copyright : (c) Iago Abal, 2012@@ -61,7 +65,6 @@ -- The Z3 Monad  -- | Z3 monad.--- newtype Z3 a = Z3 (StateT Z3State IO a)     deriving (Functor, Applicative, Monad, MonadIO, MonadState Z3State) @@ -70,7 +73,6 @@   getContext = Z3 $ gets context  -- | Internal state of Z3 monad.--- data Z3State     = Z3State { uniqVal :: !Uniq               , context :: Base.Context@@ -79,12 +81,10 @@               }  -- | Eval a Z3 script.--- evalZ3 :: Z3 a -> IO a evalZ3 = evalZ3With stdArgs  -- | Eval a Z3 script.--- evalZ3With :: Args -> Z3 a -> IO a evalZ3With args (Z3 s) =   Base.withConfig $ \cfg -> do@@ -98,13 +98,12 @@                               }  -- | Fresh symbol name.----fresh :: Z3 (Uniq, String)+fresh :: Z3 Uniq fresh = do     st <- get     let i = uniqVal st     put st { uniqVal = i + 1 }-    return (uniqVal st, 'v':show i)+    return i  ------------------------------------------------- -- Arguments

Z3/Lang/Nat.hs view

@@ -26,6 +26,14 @@ import Control.Applicative ( (<$>) ) import Data.Typeable +-- | This type allows to reason about natural numbers.+--+-- Naturals are just integers plus a @(>= 0)@ invariant, and we ensure that+-- this invariant is always preserved by transparently adding new assertions+-- to the context.+--+-- Note that arithmetic on naturals must result in natural numbers, otherwise+-- the problem becomes /unsatisfiable/. newtype Nat = Nat { unNat :: Integer }   deriving (Eq,Ord,Enum,Real,Typeable)

Z3/Lang/Prelude.hs view

@@ -121,11 +121,10 @@ --------------------------------------------------------------------- -- Commands -createVar :: forall a. IsTy a => Int -> String -> Z3 (Expr a)-createVar u str = do-    smb  <- mkStringSymbol str+createVar :: forall a. IsTy a => Uniq -> Symbol -> Z3 (Expr a)+createVar u sym = do     srt  <- mkSort  (TY :: TY a)-    cnst <- mkConst smb srt+    cnst <- mkConst sym srt     let e = Const u cnst     assert $ typeInv e     return e@@ -133,14 +132,14 @@ -- | Declare skolem variables. var :: IsTy a => Z3 (Expr a) var = do-    (u, str) <- fresh-    createVar u str+    u <- fresh+    createVar u =<< mkIntSymbol u  -- | Declare skolem variables with a user specified name. namedVar :: IsTy a => String -> Z3 (Expr a) namedVar name = do-    (u, str) <- fresh-    createVar u $ name ++ "/" ++ str+    u <- fresh+    createVar u =<< mkStringSymbol (name ++ '/' : show u)  -- | Declare uninterpreted function of arity 1. fun1 :: (IsTy a, IsTy b) => Z3 (Expr a -> Expr b)@@ -189,8 +188,8 @@ -- | Declare uninterpreted function funDecl :: forall a. IsFun a => Z3 (FunApp a) funDecl = do-  (_u, str) <- fresh-  smb <- mkStringSymbol str+  u <- fresh+  smb <- mkIntSymbol u   dom <- domain (TY :: TY a)   rng <- range  (TY :: TY a)   fd  <- mkFuncDecl smb dom rng@@ -525,9 +524,9 @@  withSortedSymbol :: IsTy a => TY a -> (Base.Symbol -> Base.Sort -> Z3 b) -> Z3 b withSortedSymbol t f = do-  (_,n) <- fresh-  sx    <- mkStringSymbol n-  srt   <- mkSort t+  u   <- fresh+  sx  <- mkIntSymbol u+  srt <- mkSort t   f sx srt  instance IsTy a => QExpr (Expr a -> Expr Bool) where

Z3/Monad.hs view

@@ -1,6 +1,10 @@  {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}+  -- This is just to avoid warnings because we import fragile new Z3 API stuff+  -- from Z3.Base+ -- TODO: Error handling  -- |@@ -29,17 +33,29 @@   , App   , Pattern   , Model+  , FuncInterp+  , FuncEntry+  , FuncModel(..)    -- ** Satisfiability result   , Result(..) +  -- * Context+  , contextToString+  , showContext+   -- * Symbols+  , mkIntSymbol   , mkStringSymbol    -- * Sorts+  , mkUninterpretedSort   , mkBoolSort   , mkIntSort   , mkRealSort+  , mkBvSort+  , mkArraySort+  , mkTupleSort    -- * Constants and Applications   , mkFuncDecl@@ -71,6 +87,63 @@   , mkReal2Int   , mkIsInt +  -- * Bit-vectors+  , mkBvnot+  , mkBvredand+  , mkBvredor+  , mkBvand+  , mkBvor+  , mkBvxor+  , mkBvnand+  , mkBvnor+  , mkBvxnor+  , mkBvneg+  , mkBvadd+  , mkBvsub+  , mkBvmul+  , mkBvudiv+  , mkBvsdiv+  , mkBvurem+  , mkBvsrem+  , mkBvsmod+  , mkBvult+  , mkBvslt+  , mkBvule+  , mkBvsle+  , mkBvuge+  , mkBvsge+  , mkBvugt+  , mkBvsgt+  , mkConcat+  , mkExtract+  , mkSignExt+  , mkZeroExt+  , mkRepeat+  , mkBvshl+  , mkBvlshr+  , mkBvashr+  , mkRotateLeft+  , mkRotateRight+  , mkExtRotateLeft+  , mkExtRotateRight+  , mkInt2bv+  , mkBv2int+  , mkBvnegNoOverflow+  , mkBvaddNoOverflow+  , mkBvaddNoUnderflow+  , mkBvsubNoOverflow+  , mkBvsubNoUnderflow+  , mkBvmulNoOverflow+  , mkBvmulNoUnderflow+  , mkBvsdivNoOverflow++  -- * Arrays+  , mkSelect+  , mkStore+  , mkConstArray+  , mkMap+  , mkArrayDefault+   -- * Numerals   , mkNumeral   , mkInt@@ -83,6 +156,7 @@   , mkExists    -- * Accessors+  , getBvSortSize   , getBool   , getInt   , getReal@@ -90,8 +164,20 @@   -- * Models   , eval   , evalT+  , evalFunc+  , evalArray+  , getFuncInterp+  , isAsArray+  , getAsArrayFuncDecl+  , funcInterpGetNumEntries+  , funcInterpGetEntry+  , funcInterpGetElse+  , funcInterpGetArity+  , funcEntryGetValue+  , funcEntryGetNumArgs+  , funcEntryGetArg+  , modelToString   , showModel-  , showContext    -- * Constraints   , assertCnstr@@ -109,6 +195,7 @@   , patternToString   , sortToString   , funcDeclToString+  , benchmarkToSMTLibString   )   where @@ -121,6 +208,9 @@   , App   , Pattern   , Model+  , FuncInterp+  , FuncEntry+  , FuncModel(..)   , Result(..)   , Logic(..)   , ASTPrintMode(..)@@ -161,6 +251,12 @@                 -> a -> b -> c -> d -> z3 e liftFun4 f a b c d = getContext >>= \ctx -> liftIO (f ctx a b c d) +liftFun6 :: MonadZ3 z3 =>+              (Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO b)+                -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> z3 b+liftFun6 f x1 x2 x3 x4 x5 x6 =+  getContext >>= \ctx -> liftIO (f ctx x1 x2 x3 x4 x5 x6)+ liftSolver0 :: MonadZ3 z3 =>        (Base.Context -> Base.Solver -> IO b)     -> (Base.Context -> IO b)@@ -207,8 +303,23 @@ evalZ3 = evalZ3With Nothing stdOpts  ---------------------------------------------------------------------+-- Contexts++-- | Convert Z3's logical context into a string.+contextToString :: MonadZ3 z3 => z3 String+contextToString = liftScalar Base.contextToString++-- | Alias for 'contextToString'.+showContext :: MonadZ3 z3 => z3 String+showContext = contextToString++--------------------------------------------------------------------- -- Symbols +-- | Create a Z3 symbol using an integer.+mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol+mkIntSymbol = liftFun1 Base.mkIntSymbol+ -- | Create a Z3 symbol using a string. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>@@ -218,6 +329,12 @@ --------------------------------------------------------------------- -- Sorts +-- | Create a free (uninterpreted) type using the given name (symbol).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>+mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort+mkUninterpretedSort = liftFun1 Base.mkUninterpretedSort+ -- | Create the /boolean/ type. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>@@ -236,6 +353,32 @@ mkRealSort :: MonadZ3 z3 => z3 Sort mkRealSort = liftScalar Base.mkRealSort +-- | Create a bit-vector type of the given size.+--+-- This type can also be seen as a machine integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>+mkBvSort :: MonadZ3 z3 => Int -> z3 Sort+mkBvSort = liftFun1 Base.mkBvSort++-- | Create an array type+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>+--+mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort+mkArraySort = liftFun2 Base.mkArraySort++-- | Create a tuple type+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>+mkTupleSort :: MonadZ3 z3+            => Symbol                          -- ^ Name of the sort+            -> [(Symbol, Sort)]                -- ^ Name and sort of each field+            -> z3 (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function+                                               -- declarations for the+                                               -- constructor and projections.+mkTupleSort = liftFun2 Base.mkTupleSort+ --------------------------------------------------------------------- -- Constants and Applications @@ -407,6 +550,346 @@ mkIsInt = liftFun1 Base.mkIsInt  ---------------------------------------------------------------------+-- Bit-vectors++-- | Bitwise negation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>+mkBvnot :: MonadZ3 z3 => AST -> z3 AST+mkBvnot = liftFun1 Base.mkBvnot++-- | Take conjunction of bits in vector, return vector of length 1.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>+mkBvredand :: MonadZ3 z3 => AST -> z3 AST+mkBvredand = liftFun1 Base.mkBvredand++-- | Take disjunction of bits in vector, return vector of length 1.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>+mkBvredor :: MonadZ3 z3 => AST -> z3 AST+mkBvredor = liftFun1 Base.mkBvredor++-- | Bitwise and.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>+mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvand  = liftFun2 Base.mkBvand++-- | Bitwise or.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>+mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvor = liftFun2 Base.mkBvor++-- | Bitwise exclusive-or.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>+mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvxor = liftFun2 Base.mkBvxor++-- | Bitwise nand.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>+mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvnand = liftFun2 Base.mkBvnand++-- | Bitwise nor.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>+mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvnor = liftFun2 Base.mkBvnor++-- | Bitwise xnor.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>+mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvxnor = liftFun2 Base.mkBvxnor++-- | Standard two's complement unary minus.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7+mkBvneg :: MonadZ3 z3 => AST -> z3 AST+mkBvneg = liftFun1 Base.mkBvneg++-- | Standard two's complement addition.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>+mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvadd = liftFun2 Base.mkBvadd++-- | Standard two's complement subtraction.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>+mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsub = liftFun2 Base.mkBvsub++-- | Standard two's complement multiplication.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>+mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvmul = liftFun2 Base.mkBvmul++-- | Unsigned division.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>+mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvudiv = liftFun2 Base.mkBvudiv++-- | Two's complement signed division.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>+mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsdiv = liftFun2 Base.mkBvsdiv++-- | Unsigned remainder.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>+mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvurem = liftFun2 Base.mkBvurem++-- | Two's complement signed remainder (sign follows dividend).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>+mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsrem = liftFun2 Base.mkBvsrem++-- | Two's complement signed remainder (sign follows divisor).+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>+mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsmod = liftFun2 Base.mkBvsmod++-- | Unsigned less than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>+mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvult = liftFun2 Base.mkBvult++-- | Two's complement signed less than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>+mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvslt = liftFun2 Base.mkBvslt++-- | Unsigned less than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>+mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvule = liftFun2 Base.mkBvule++-- | Two's complement signed less than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>+mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsle = liftFun2 Base.mkBvsle++-- | Unsigned greater than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>+mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvuge = liftFun2 Base.mkBvuge++-- | Two's complement signed greater than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>+mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsge = liftFun2 Base.mkBvsge++-- | Unsigned greater than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>+mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvugt = liftFun2 Base.mkBvugt++-- | Two's complement signed greater than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>+mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsgt = liftFun2 Base.mkBvsgt++-- | Concatenate the given bit-vectors.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>+mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST+mkConcat = liftFun2 Base.mkConcat++-- | Extract the bits high down to low from a bitvector of size m to yield a new+-- bitvector of size /n/, where /n = high - low + 1/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>+mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST+mkExtract = liftFun3 Base.mkExtract++-- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector+-- of size /m+i/, where /m/ is the size of the given bit-vector.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>+mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST+mkSignExt = liftFun2 Base.mkSignExt++-- | Extend the given bit-vector with zeros to the (unsigned) equivalent+-- bitvector of size /m+i/, where /m/ is the size of the given bit-vector.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>+mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST+mkZeroExt = liftFun2 Base.mkZeroExt++-- | Repeat the given bit-vector up length /i/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>+mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST+mkRepeat = liftFun2 Base.mkRepeat++-- | Shift left.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>+mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvshl = liftFun2 Base.mkBvshl++-- | Logical shift right.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>+mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvlshr = liftFun2 Base.mkBvlshr++-- | Arithmetic shift right.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>+mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvashr = liftFun2 Base.mkBvashr++-- | Rotate bits of /t1/ to the left /i/ times.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>+mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST+mkRotateLeft = liftFun2 Base.mkRotateLeft++-- | Rotate bits of /t1/ to the right /i/ times.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>+mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST+mkRotateRight = liftFun2 Base.mkRotateRight++-- | Rotate bits of /t1/ to the left /t2/ times.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>+mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST+mkExtRotateLeft = liftFun2 Base.mkExtRotateLeft++-- | Rotate bits of /t1/ to the right /t2/ times.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>+mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST+mkExtRotateRight = liftFun2 Base.mkExtRotateRight++-- | Create an /n/ bit bit-vector from the integer argument /t1/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>+mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST+mkInt2bv = liftFun2 Base.mkInt2bv++-- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false,+-- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative+-- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/.+-- If /is_signed/ is true, /t1/ is treated as a signed bit-vector.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>+mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST+mkBv2int = liftFun2 Base.mkBv2int++-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/+-- does not overflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>+mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST+mkBvaddNoOverflow = liftFun3 Base.mkBvaddNoOverflow++-- | Create a predicate that checks that the bit-wise signed addition of /t1/+-- and /t2/ does not underflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>+mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvaddNoUnderflow = liftFun2 Base.mkBvaddNoUnderflow++-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/+-- and /t2/ does not overflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>+mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsubNoOverflow = liftFun2 Base.mkBvsubNoOverflow++-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and+-- /t2/ does not underflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>+mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsubNoUnderflow = liftFun2 Base.mkBvsubNoUnderflow++-- | Create a predicate that checks that the bit-wise signed division of /t1/+-- and /t2/ does not overflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>+mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvsdivNoOverflow = liftFun2 Base.mkBvsdivNoOverflow++-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as+-- a signed bit-vector.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>+mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST+mkBvnegNoOverflow = liftFun1 Base.mkBvnegNoOverflow++-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and+-- /t2/ does not overflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>+mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST+mkBvmulNoOverflow = liftFun3 Base.mkBvmulNoOverflow++-- | Create a predicate that checks that the bit-wise signed multiplication of+-- /t1/ and /t2/ does not underflow.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>+mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST+mkBvmulNoUnderflow = liftFun2 Base.mkBvmulNoUnderflow++---------------------------------------------------------------------+-- Arrays++-- | Array read. The argument a is the array and i is the index of the array+-- that gets read.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67>+mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST+mkSelect = liftFun2 Base.mkSelect++-- | 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+mkStore = liftFun3 Base.mkStore++-- | Create the constant array.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d>+mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST+mkConstArray = liftFun2 Base.mkConstArray++-- | map f on the the argument arrays.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>+mkMap :: MonadZ3 z3 => FuncDecl -> Int -> [AST] -> z3 AST+mkMap = liftFun3 Base.mkMap++-- | Access the array default value. Produces the default range value, for+-- arrays that can be represented as finite maps with a default range value.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d>+mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST+mkArrayDefault = liftFun1 Base.mkArrayDefault++--------------------------------------------------------------------- -- Numerals  -- | Create a numeral of a given sort.@@ -447,6 +930,12 @@ --------------------------------------------------------------------- -- Accessors +-- | Return the size of the given bit-vector sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>+getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int+getBvSortSize = liftFun1 Base.getBvSortSize+ -- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>@@ -472,6 +961,90 @@ evalT :: (MonadZ3 z3,Traversable t) => Model -> t AST -> z3 (Maybe (t AST)) evalT = liftFun2 Base.evalT +-- | Get function as a list of argument/value pairs.+evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)+evalFunc = liftFun2 Base.evalFunc++-- | Get array as a list of argument/value pairs, if it is+-- represented as a function (ie, using as-array).+evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)+evalArray = liftFun2 Base.evalArray++-- | Return the interpretation of the function f in the model m.+-- Return NULL, if the model does not assign an interpretation for f.+-- That should be interpreted as: the f does not matter.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>+getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)+getFuncInterp = liftFun2 Base.getFuncInterp++-- | The (_ as-array f) AST node is a construct for assigning interpretations+-- for arrays in Z3. It is the array such that forall indices i we have that+-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE+-- if the a is an as-array AST node.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>+isAsArray :: MonadZ3 z3 => AST -> z3 Bool+isAsArray = liftFun1 Base.isAsArray++-- | Return the function declaration f associated with a (_ as_array f) node.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>+getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl+getAsArrayFuncDecl = liftFun1 Base.getAsArrayFuncDecl++-- | Return the number of entries in the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>+funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int+funcInterpGetNumEntries = liftFun1 Base.funcInterpGetNumEntries++-- | Return a "point" of the given function intepretation.+-- It represents the value of f in a particular point.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>+funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry+funcInterpGetEntry = liftFun2 Base.funcInterpGetEntry++-- | Return the 'else' value of the given function interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>+funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST+funcInterpGetElse = liftFun1 Base.funcInterpGetElse++-- | Return the arity (number of arguments) of the given function+-- interpretation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>+funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int+funcInterpGetArity = liftFun1 Base.funcInterpGetArity++-- | Return the value of this point.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>+funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST+funcEntryGetValue = liftFun1 Base.funcEntryGetValue++-- | Return the number of arguments in a Z3_func_entry object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>+funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int+funcEntryGetNumArgs = liftFun1 Base.funcEntryGetNumArgs++-- | Return an argument of a Z3_func_entry object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>+funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST+funcEntryGetArg = liftFun2 Base.funcEntryGetArg++-- | Convert the given model into a string.+modelToString :: MonadZ3 z3 => Model -> z3 String+modelToString = liftFun1 Base.modelToString++-- | Alias for 'modelToString'.+showModel :: MonadZ3 z3 => Model -> z3 String+showModel = modelToString+ --------------------------------------------------------------------- -- Constraints @@ -509,14 +1082,6 @@  void $ T.traverse delModel mb_m  return (r, mb_e) --- | Convert the given model into a string.-showModel :: MonadZ3 z3 => Model -> z3 String-showModel = liftFun1 Base.showModel---- | Convert Z3's logical context into a string.-showContext :: MonadZ3 z3 => z3 String-showContext = liftScalar Base.showContext- -- | Check whether the given logical context is consistent or not. check :: MonadZ3 z3 => z3 Result check = liftSolver0 Base.solverCheck Base.check@@ -544,3 +1109,15 @@ funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String funcDeclToString = liftFun1 Base.funcDeclToString +-- | Convert the given benchmark into SMT-LIB formatted string.+--+-- The output format can be configured via 'setASTPrintMode'.+benchmarkToSMTLibString :: MonadZ3 z3 =>+                               String   -- ^ name+                            -> String   -- ^ logic+                            -> String   -- ^ status+                            -> String   -- ^ attributes+                            -> [AST]    -- ^ assumptions1+                            -> AST      -- ^ formula+                            -> z3 String+benchmarkToSMTLibString = liftFun6 Base.benchmarkToSMTLibString

z3.cabal view

@@ -1,5 +1,5 @@ Name:                z3-Version:             0.3.0+Version:             0.3.1 Synopsis:            Bindings for the Z3 Theorem Prover Description:     Bindings for the Z3 Theorem Prover (<http://z3.codeplex.com>).@@ -18,10 +18,11 @@     dynamic libraries (\/usr\/lib) and header files (\/usr\/include), or else     use the --extra-lib-dirs and --extra-include-dirs Cabal flags.     .-    * Hackage fails to compile this package because of the z3 dependency.+    * Hackage fails to compile this package because of the (unsatisfied) /libz3/+    dependency.     .     * Haddock documentation can be found at-    <http://www.iagoabal.eu/z3-haskell/doc/0.3.0>+    <http://www.iagoabal.eu/z3-haskell/doc/0.3.1>. Homepage:            http://bitbucket.org/iago/z3-haskell License:             BSD3 License-file:        LICENSE@@ -63,8 +64,7 @@      ghc-options: -Wall ---  modify in MonadState causes <<loop>> in mtl-2.1, so we forbide this mtl---  version in this library.+    -- Ban to mtl-2.1: modify in MonadState causes <<loop>> in mtl-2.1     Build-depends:       base > 3 && < 5, containers, mtl < 2.1 || > 2.1      Build-tools:         hsc2hs@@ -73,8 +73,9 @@      includes:            z3.h -    -- In OS X libz3 is linked statically against libgomp-    if os(darwin)+    -- In OS X libz3 is linked statically against libgomp.+    -- In Windows Z3 is compiled using MS C++.+    if os(darwin) || os(windows)         extra-libraries:     z3     else         extra-libraries:     gomp z3 gomp