Commits

Nathan Howell committed 6bc8685

Support context push/pop

Comments (2)

  1. Iago Abal

    We'll accept this, but push/pop are likely to be replaced by some other function for the next release. So in practice we are accepting push/pop just for Z3.Base.

Files changed (4)

     , assertCnstr
     , check
     , getModel
+    , push
+    , pop
 
     ) where
 
 -- Constraints
 
 -- TODO Constraints: Z3_push
+push :: Context -> IO ()
+push ctx =
+  withContext ctx $ \ctxPtr ->
+    z3_push ctxPtr
+
+pop :: Context -> Int -> IO ()
+pop ctx cnt =
+  withContext ctx $ \ctxPtr ->
+    z3_pop ctxPtr (fromIntegral cnt)
+
 -- TODO Constraints: Z3_pop
 -- TODO Constraints: Z3_get_num_scopes
 -- TODO Constraints: Z3_persist_ast
 ---------------------------------------------------------------------
 -- * Constraints
 
--- TODO Constraints: Z3_push
+foreign import ccall unsafe "Z3_push"
+    z3_push :: Ptr Z3_context -> IO ()
+
 -- TODO Constraints: Z3_pop
+foreign import ccall unsafe "Z3_pop"
+    z3_pop :: Ptr Z3_context -> CUInt -> IO ()
+
 -- TODO Constraints: Z3_get_num_scopes
 -- TODO Constraints: Z3_persist_ast
 
     , mkIntArith
     , mkRealArith
     , mkIte
+    , pop
+    , push
 
     -- * Satisfiability result
     , Base.Result(..)
 getBool :: Base.AST Bool -> Z3 (Maybe Bool)
 getBool = liftZ3Op2 Base.getBool
 
+push :: Z3 ()
+push = liftZ3Op Base.push
+
+pop :: Int -> Z3 ()
+pop = liftZ3Op2 Base.pop
+
 getInt :: Base.AST Integer -> Z3 Integer
 getInt = liftZ3Op2 Base.getInt
 

Z3/Lang/Prelude.hs

     , let_
     , check
     , checkModel
+    , push, pop
 
     -- * Expressions
     , Expr