Commits

Scott West committed 97b74d4

Adding solverGetNumScopes binding
#changelog

Edited-by: Iago Abal <mail@iagoabal.eu>

Comments (0)

Files changed (3)

   , solverPush
   , solverPop
   , solverReset
+  , solverGetNumScopes
   , solverAssertCnstr
   , solverAssertAndTrack
   , solverCheck
 pop ctx cnt = checkError ctx $ z3_pop (unContext ctx) $ fromIntegral cnt
 
 -- TODO Constraints: Z3_get_num_scopes
+
 -- TODO Constraints: Z3_persist_ast
 
 -- | Assert a constraing into the logical context.
 solverReset :: Context -> Solver -> IO ()
 solverReset c solver = checkError c $ z3_solver_reset (unContext c) (unSolver solver)
 
+-- | Number of backtracking points.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd4b4a6465601835341b477b75725b28>
+solverGetNumScopes :: Context -> Solver -> IO Int
+solverGetNumScopes ctx solver = fmap fromIntegral $
+  checkError ctx $ z3_solver_get_num_scopes (unContext ctx) (unSolver solver)
+
 solverAssertCnstr :: Context -> Solver -> AST -> IO ()
 solverAssertCnstr c solver ast =
   checkError c $ z3_solver_assert (unContext c) (unSolver solver) (unAST ast)
 foreign import ccall unsafe "Z3_solver_pop"
     z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO ()
 
+-- | Number of backtracking points.
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd4b4a6465601835341b477b75725b28>
+foreign import ccall unsafe "Z3_solver_get_num_scopes"
+    z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt
+
 -- | Remove all assertions from a solver.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4a4a215b9130d7980e3c393fe857335f>
   , withModel
   , push
   , pop
+  , getNumScopes
 
   -- * String Conversion
   , ASTPrintMode(..)
 pop :: MonadZ3 z3 => Int -> z3 ()
 pop = liftSolver1 Base.solverPop Base.pop
 
+-- | Get number of backtracking points.
+getNumScopes :: MonadZ3 z3 => z3 Int
+getNumScopes = liftSolver0 Base.solverGetNumScopes
+                           (error "getNumScopes requires solver")
+
 -- | Assert a constraing into the logical context.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>