diff --git a/Z3/Base.hs b/Z3/Base.hs --- a/Z3/Base.hs +++ b/Z3/Base.hs @@ -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: +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: +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: @@ -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: +mkUninterpretedSort :: Context -> Symbol -> IO Sort +mkUninterpretedSort c sy = checkError c $ + Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy) + -- | Create the /Boolean/ type. -- -- Reference: @@ -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: +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: 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: +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: +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: +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: +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: +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: +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: +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: +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: +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: +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: +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: 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: -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: -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: @@ -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: +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 + diff --git a/Z3/Base/C.hsc b/Z3/Base/C.hsc --- a/Z3/Base/C.hsc +++ b/Z3/Base/C.hsc @@ -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: +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: 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: +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: @@ -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: +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: +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: +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: +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: +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: +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: +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: +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: +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: +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: +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: 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: +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 diff --git a/Z3/Lang/Monad.hs b/Z3/Lang/Monad.hs --- a/Z3/Lang/Monad.hs +++ b/Z3/Lang/Monad.hs @@ -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 diff --git a/Z3/Lang/Nat.hs b/Z3/Lang/Nat.hs --- a/Z3/Lang/Nat.hs +++ b/Z3/Lang/Nat.hs @@ -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) diff --git a/Z3/Lang/Prelude.hs b/Z3/Lang/Prelude.hs --- a/Z3/Lang/Prelude.hs +++ b/Z3/Lang/Prelude.hs @@ -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 diff --git a/Z3/Monad.hs b/Z3/Monad.hs --- a/Z3/Monad.hs +++ b/Z3/Monad.hs @@ -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: @@ -218,6 +329,12 @@ --------------------------------------------------------------------- -- Sorts +-- | Create a free (uninterpreted) type using the given name (symbol). +-- +-- Reference: +mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort +mkUninterpretedSort = liftFun1 Base.mkUninterpretedSort + -- | Create the /boolean/ type. -- -- Reference: @@ -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: +mkBvSort :: MonadZ3 z3 => Int -> z3 Sort +mkBvSort = liftFun1 Base.mkBvSort + +-- | Create an array type +-- +-- Reference: +-- +mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort +mkArraySort = liftFun2 Base.mkArraySort + +-- | Create a tuple type +-- +-- Reference: +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: +mkBvnot :: MonadZ3 z3 => AST -> z3 AST +mkBvnot = liftFun1 Base.mkBvnot + +-- | Take conjunction of bits in vector, return vector of length 1. +-- +-- Reference: +mkBvredand :: MonadZ3 z3 => AST -> z3 AST +mkBvredand = liftFun1 Base.mkBvredand + +-- | Take disjunction of bits in vector, return vector of length 1. +-- +-- Reference: +mkBvredor :: MonadZ3 z3 => AST -> z3 AST +mkBvredor = liftFun1 Base.mkBvredor + +-- | Bitwise and. +-- +-- Reference: +mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvand = liftFun2 Base.mkBvand + +-- | Bitwise or. +-- +-- Reference: +mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvor = liftFun2 Base.mkBvor + +-- | Bitwise exclusive-or. +-- +-- Reference: +mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvxor = liftFun2 Base.mkBvxor + +-- | Bitwise nand. +-- +-- Reference: +mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvnand = liftFun2 Base.mkBvnand + +-- | Bitwise nor. +-- +-- Reference: +mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvnor = liftFun2 Base.mkBvnor + +-- | Bitwise xnor. +-- +-- Reference: +mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvxnor = liftFun2 Base.mkBvxnor + +-- | Standard two's complement unary minus. +-- +-- Reference: AST -> z3 AST +mkBvneg = liftFun1 Base.mkBvneg + +-- | Standard two's complement addition. +-- +-- Reference: +mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvadd = liftFun2 Base.mkBvadd + +-- | Standard two's complement subtraction. +-- +-- Reference: +mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsub = liftFun2 Base.mkBvsub + +-- | Standard two's complement multiplication. +-- +-- Reference: +mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvmul = liftFun2 Base.mkBvmul + +-- | Unsigned division. +-- +-- Reference: +mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvudiv = liftFun2 Base.mkBvudiv + +-- | Two's complement signed division. +-- +-- Reference: +mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsdiv = liftFun2 Base.mkBvsdiv + +-- | Unsigned remainder. +-- +-- Reference: +mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvurem = liftFun2 Base.mkBvurem + +-- | Two's complement signed remainder (sign follows dividend). +-- +-- Reference: +mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsrem = liftFun2 Base.mkBvsrem + +-- | Two's complement signed remainder (sign follows divisor). +-- +-- Reference: +mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsmod = liftFun2 Base.mkBvsmod + +-- | Unsigned less than. +-- +-- Reference: +mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvult = liftFun2 Base.mkBvult + +-- | Two's complement signed less than. +-- +-- Reference: +mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvslt = liftFun2 Base.mkBvslt + +-- | Unsigned less than or equal to. +-- +-- Reference: +mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvule = liftFun2 Base.mkBvule + +-- | Two's complement signed less than or equal to. +-- +-- Reference: +mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsle = liftFun2 Base.mkBvsle + +-- | Unsigned greater than or equal to. +-- +-- Reference: +mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvuge = liftFun2 Base.mkBvuge + +-- | Two's complement signed greater than or equal to. +-- +-- Reference: +mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsge = liftFun2 Base.mkBvsge + +-- | Unsigned greater than. +-- +-- Reference: +mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvugt = liftFun2 Base.mkBvugt + +-- | Two's complement signed greater than. +-- +-- Reference: +mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvsgt = liftFun2 Base.mkBvsgt + +-- | Concatenate the given bit-vectors. +-- +-- Reference: +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: +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: +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: +mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST +mkZeroExt = liftFun2 Base.mkZeroExt + +-- | Repeat the given bit-vector up length /i/. +-- +-- Reference: +mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST +mkRepeat = liftFun2 Base.mkRepeat + +-- | Shift left. +-- +-- Reference: +mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvshl = liftFun2 Base.mkBvshl + +-- | Logical shift right. +-- +-- Reference: +mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvlshr = liftFun2 Base.mkBvlshr + +-- | Arithmetic shift right. +-- +-- Reference: +mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST +mkBvashr = liftFun2 Base.mkBvashr + +-- | Rotate bits of /t1/ to the left /i/ times. +-- +-- Reference: +mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST +mkRotateLeft = liftFun2 Base.mkRotateLeft + +-- | Rotate bits of /t1/ to the right /i/ times. +-- +-- Reference: +mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST +mkRotateRight = liftFun2 Base.mkRotateRight + +-- | Rotate bits of /t1/ to the left /t2/ times. +-- +-- Reference: +mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST +mkExtRotateLeft = liftFun2 Base.mkExtRotateLeft + +-- | Rotate bits of /t1/ to the right /t2/ times. +-- +-- Reference: +mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST +mkExtRotateRight = liftFun2 Base.mkExtRotateRight + +-- | Create an /n/ bit bit-vector from the integer argument /t1/. +-- +-- Reference: +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: +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: +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: +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: +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: +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: +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: +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: +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: +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: +mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST +mkSelect = liftFun2 Base.mkSelect + +-- | Array update.   +-- +-- Reference: +mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST +mkStore = liftFun3 Base.mkStore + +-- | Create the constant array. +-- +-- Reference: +mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST +mkConstArray = liftFun2 Base.mkConstArray + +-- | map f on the the argument arrays. +-- +-- Reference: +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: +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: +getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int +getBvSortSize = liftFun1 Base.getBvSortSize + -- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/. -- -- Reference: @@ -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: +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: +isAsArray :: MonadZ3 z3 => AST -> z3 Bool +isAsArray = liftFun1 Base.isAsArray + +-- | Return the function declaration f associated with a (_ as_array f) node. +-- +-- Reference: +getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl +getAsArrayFuncDecl = liftFun1 Base.getAsArrayFuncDecl + +-- | Return the number of entries in the given function interpretation. +-- +-- Reference: +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: +funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry +funcInterpGetEntry = liftFun2 Base.funcInterpGetEntry + +-- | Return the 'else' value of the given function interpretation. +-- +-- Reference: +funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST +funcInterpGetElse = liftFun1 Base.funcInterpGetElse + +-- | Return the arity (number of arguments) of the given function +-- interpretation. +-- +-- Reference: +funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int +funcInterpGetArity = liftFun1 Base.funcInterpGetArity + +-- | Return the value of this point. +-- +-- Reference: +funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST +funcEntryGetValue = liftFun1 Base.funcEntryGetValue + +-- | Return the number of arguments in a Z3_func_entry object. +-- +-- Reference: +funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int +funcEntryGetNumArgs = liftFun1 Base.funcEntryGetNumArgs + +-- | Return an argument of a Z3_func_entry object. +-- +-- Reference: +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 diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -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 - + . Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE @@ -63,8 +64,7 @@ ghc-options: -Wall --- modify in MonadState causes <> in mtl-2.1, so we forbide this mtl --- version in this library. + -- Ban to mtl-2.1: modify in MonadState causes <> 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