Commits

Iago Abal committed 02c0832

Add Z3 API function benchmarkToSMTLibString
#changelog

Comments (0)

Files changed (3)

     , patternToString
     , sortToString
     , funcDeclToString
+    , benchmarkToSMTLibString
 
     -- * Error Handling
     , Z3Error(..)
 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
+
 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
 
   , patternToString
   , sortToString
   , funcDeclToString
+  , benchmarkToSMTLibString
   )
   where
 
                 -> 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)
 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