Commits

Iago Abal committed 1ea059c

Add mkIntSymbol API call

  • Participants
  • Parent commits e517e59

Comments (0)

Files changed (3)

     , withContext
 
     -- * Symbols
+    , mkIntSymbol
     , mkStringSymbol
 
     -- * Sorts
 ---------------------------------------------------------------------
 -- 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>
 ---------------------------------------------------------------------
 -- * 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>
   , Result(..)
 
   -- * Symbols
+  , mkIntSymbol
   , mkStringSymbol
 
   -- * Sorts
 ---------------------------------------------------------------------
 -- 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>