Commits

Iago Abal committed dffebe8

Low-level support of uninterpreted sorts

Comments (0)

Files changed (3)

     , mkStringSymbol
 
     -- * Sorts
+    , mkUninterpretedSort
     , mkBoolSort
     , mkIntSort
     , mkRealSort
 -- Sorts
 
 -- TODO Sorts: Z3_is_eq_sort
--- TODO Sorts: Z3_mk_uninterpreted_sort
+
+-- | Create a free (uninterpreted) type using the given name (symbol).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>
+mkUninterpretedSort :: Context -> Symbol -> IO Sort
+mkUninterpretedSort c sy = checkError c $
+  Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy)
 
 -- | Create the /Boolean/ type.
 --
 -- * Sorts
 
 -- TODO Sorts: Z3_is_eq_sort
--- TODO Sorts: Z3_mk_uninterpreted_sort
+
+-- | Create a free (uninterpreted) type using the given name (symbol).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>
+foreign import ccall unsafe "Z3_mk_uninterpreted_sort"
+    z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort)
 
 -- | Create the Boolean type.
 --
   , mkStringSymbol
 
   -- * Sorts
+  , mkUninterpretedSort
   , mkBoolSort
   , mkIntSort
   , mkRealSort
 ---------------------------------------------------------------------
 -- Sorts
 
+-- | Create a free (uninterpreted) type using the given name (symbol).
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>
+mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
+mkUninterpretedSort = liftFun1 Base.mkUninterpretedSort
+
 -- | Create the /boolean/ type.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>