finite domain sorts

Author: strake

src/Z3/Base.hs

@@ -105,6 +105,7 @@ module Z3.Base (
   , mkIntSort
   , mkRealSort
   , mkBvSort
+  , mkFiniteDomainSort
   , mkArraySort
   , mkTupleSort
   , mkConstructor
@@ -743,7 +744,9 @@ mkBvSort c i
   | i >= 0    = liftFun1 z3_mk_bv_sort c i
   | otherwise = error "Z3.Base.mkBvSort: negative size"
 
--- TODO: Z3_mk_finite_domain_sort
+-- | Create a finite-domain type.
+mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort
+mkFiniteDomainSort = liftFun2 z3_mk_finite_domain_sort
 
 -- | Create an array type
 --

src/Z3/Base/C.hsc

@@ -243,6 +243,10 @@ foreign import ccall unsafe "Z3_mk_int_sort"
 foreign import ccall unsafe "Z3_mk_real_sort"
     z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
 
+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga62166c0e3f9a8be4ba492eee5a52ce1b>
+foreign import ccall unsafe "Z3_mk_finite_domain_sort"
+    z3_mk_finite_domain_sort :: Ptr Z3_context -> Ptr Z3_symbol -> CULLong -> IO (Ptr Z3_sort)
+
 -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>
 foreign import ccall unsafe "Z3_mk_bv_sort"
     z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort)

src/Z3/Monad.hs

@@ -64,6 +64,7 @@ module Z3.Monad
   , mkIntSort
   , mkRealSort
   , mkBvSort
+  , mkFiniteDomainSort
   , mkArraySort
   , mkTupleSort
   , mkConstructor
@@ -657,6 +658,10 @@ mkRealSort = liftScalar Base.mkRealSort
 mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
 mkBvSort = liftFun1 Base.mkBvSort
 
+-- | Create a finite-domain type.
+mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort
+mkFiniteDomainSort = liftFun2 Base.mkFiniteDomainSort
+
 -- | Create an array type
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>