Commits

Iago Abal committed fd34a95

Fix coding style and 'ptrToMaybe' refactoring

Comments (0)

Files changed (2)

     , mkContext
     , delContext
     , withContext
+    , contextToString
+    , showContext
 
     -- * Symbols
     , mkIntSymbol
     , evalT
     , evalFunc
     , evalArray
-    , showModel
-    , showContext
     , getFuncInterp
     , isAsArray
     , getAsArrayFuncDecl
     , funcEntryGetValue
     , funcEntryGetNumArgs
     , funcEntryGetArg
+    , modelToString
+    , showModel
 
     -- * Constraints
     , assertCnstr
 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
 
 --
 -- 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 =
       >>= 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
+
   -- ** Satisfiability result
   , Result(..)
 
+  -- * Context
+  , contextToString
+  , showContext
+
   -- * Symbols
   , mkIntSymbol
   , mkStringSymbol
   , evalT
   , evalFunc
   , evalArray
-  , showModel
-  , showContext
   , getFuncInterp
   , isAsArray
   , getAsArrayFuncDecl
   , funcEntryGetValue
   , funcEntryGetNumArgs
   , funcEntryGetArg
+  , modelToString
+  , showModel
 
   -- * Constraints
   , assertCnstr
 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.
 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
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.