Iago Abal avatar Iago Abal committed 71b0274 Merge

Merge commit 0827f9053971

Comments (0)

Files changed (5)

     , App
     , Pattern
     , Model
+    , FuncInterp
+    , FuncEntry
     , Params
     , Solver
 
     , mkContext
     , delContext
     , withContext
+    , contextToString
+    , showContext
 
     -- * Symbols
+    , mkIntSymbol
     , mkStringSymbol
 
     -- * Sorts
     , evalT
     , evalFunc
     , evalArray
-    , showModel
-    , showContext
     , getFuncInterp
     , isAsArray
     , getAsArrayFuncDecl
     , funcEntryGetValue
     , funcEntryGetNumArgs
     , funcEntryGetArg
+    , modelToString
+    , showModel
 
     -- * Constraints
     , assertCnstr
     , patternToString
     , sortToString
     , funcDeclToString
+    , benchmarkToSMTLibString
 
     -- * Error Handling
     , Z3Error(..)
 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>
 --
 -- 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.
 --
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>
 getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
-getAsArrayFuncDecl ctx a =
-    FuncDecl <$> z3_get_as_array_func_decl (unContext ctx) (unAST a)
+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.
+-- | 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
 getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)]
 getMapFromInterp ctx interp =
     do n <- funcInterpGetNumEntries ctx interp
-       entries <- mapM (funcInterpGetEntry ctx interp) [0 .. n-1]
+       entries <- mapM (funcInterpGetEntry ctx interp) [0..n-1]
        mapM (getEntry ctx) entries
 
 getEntry :: Context -> FuncEntry -> IO ([AST], AST)
 getEntryArgs :: Context -> FuncEntry -> IO [AST]
 getEntryArgs ctx entry =
     do n <- funcEntryGetNumArgs ctx entry
-       mapM (funcEntryGetArg ctx entry) [0 .. n - 1]
+       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.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>
 getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
-getFuncInterp ctx m fDecl =
-    do ptr <- checkError ctx (z3_model_get_func_interp (unContext ctx) (unModel m) (unFuncDecl fDecl))
-       if ptr == nullPtr
-         then return Nothing
-         else return $ Just $ FuncInterp $ ptr
+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 funcInterp = fromIntegral <$> res
-    where
-      res = checkError ctx (z3_func_interp_get_num_entries
-                              (unContext ctx)
-                              (unFuncInterp funcInterp))
+funcInterpGetNumEntries ctx fi = checkError ctx $ fromIntegral <$>
+  z3_func_interp_get_num_entries (unContext ctx) (unFuncInterp fi)
 
--- | Return a "point" of the given function intepretation.
+-- | 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 funcInterp i = FuncEntry <$> res
-    where
-      res = checkError ctx (z3_func_interp_get_entry
-                               (unContext ctx)
-                               (unFuncInterp funcInterp)
-                               (fromIntegral i))
+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 funcInterp = AST <$> res
-    where
-      res = checkError ctx (z3_func_interp_get_else
-                              (unContext ctx)
-                              (unFuncInterp funcInterp))
+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.
+-- | 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 funcInterp = fromIntegral <$> res
-    where
-      res = checkError ctx (z3_func_interp_get_arity
-                              (unContext ctx)
-                              (unFuncInterp funcInterp))
+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 funcEntry = AST <$> res
-    where
-      res = checkError ctx (z3_func_entry_get_value
-                              (unContext ctx)
-                              (unFuncEntry funcEntry))
+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 funcEntry = fromIntegral <$> res
-    where
-      res = checkError ctx (z3_func_entry_get_num_args
-                              (unContext ctx)
-                              (unFuncEntry funcEntry))
+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 funcEntry i = AST <$> res
-    where
-      res = checkError ctx (z3_func_entry_get_arg
-                              (unContext ctx)
-                              (unFuncEntry funcEntry)
-                              (fromIntegral i))
+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
 --
 -- 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)
 --
         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.
 --
 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>
 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 =
 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
+
 ---------------------------------------------------------------------
 -- * 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
 
             -> 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 (_ 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>
     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. 
+-- | 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>
                                    -> Ptr Z3_func_interp
                                    -> IO CUInt
 
--- | Return a "point" of the given function intepretation. 
+-- | 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_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
 
 {-# 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
                               }
 
 -- | 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/Prelude.hs

 ---------------------------------------------------------------------
 -- 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
 -- | 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)
 -- | 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
 
 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
 
 {-# 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
 
 -- |
   , App
   , Pattern
   , Model
+  , FuncInterp
+  , FuncEntry
   , FuncModel(..)
 
   -- ** Satisfiability result
   , Result(..)
 
+  -- * Context
+  , contextToString
+  , showContext
+
   -- * Symbols
+  , mkIntSymbol
   , mkStringSymbol
 
   -- * Sorts
   , evalT
   , evalFunc
   , evalArray
+  , getFuncInterp
+  , isAsArray
+  , getAsArrayFuncDecl
+  , funcInterpGetNumEntries
+  , funcInterpGetEntry
+  , funcInterpGetElse
+  , funcInterpGetArity
+  , funcEntryGetValue
+  , funcEntryGetNumArgs
+  , funcEntryGetArg
+  , modelToString
   , showModel
-  , showContext
 
   -- * Constraints
   , assertCnstr
   , patternToString
   , sortToString
   , funcDeclToString
+  , benchmarkToSMTLibString
   )
   where
 
   , App
   , Pattern
   , Model
+  , FuncInterp
+  , FuncEntry
   , FuncModel(..)
   , Result(..)
   , Logic(..)
                 -> 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)
 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>
 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
  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
 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
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.