Commits

Scott West committed 223b077

Add tuple sort support and example
#changelog

Comments (0)

Files changed (5)

     , mkRealSort
     , mkBvSort
     , mkArraySort
+    , mkTupleSort
 
     -- * Constants and Applications
     , mkFuncDecl
 mkArraySort :: Context -> Sort -> Sort -> IO Sort
 mkArraySort c dom rng = checkError c $ Sort <$> z3_mk_array_sort (unContext c) (unSort dom) (unSort rng)
 
+-- | Create a tuple type
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>
+mkTupleSort :: Context                         -- ^ Context
+            -> Symbol                          -- ^ Name of the sort
+            -> [(Symbol, Sort)]                -- ^ Name and sort of each field
+            -> IO (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function
+                                               -- declarations for the
+                                               -- constructor and projections.
+mkTupleSort c sym symSorts = checkError c $
+  let (syms, sorts) = unzip symSorts
+  in withArrayLen (map unSymbol syms) $ \ n symsPtr ->
+     withArray (map unSort sorts) $ \ sortsPtr ->
+     alloca $ \ outConstrPtr ->
+     allocaArray n $ \ outProjsPtr -> do
+       sort <- checkError c $ z3_mk_tuple_sort
+                   (unContext c) (unSymbol sym)
+                   (fromIntegral n) symsPtr sortsPtr
+                   outConstrPtr outProjsPtr
+       outConstr <- peek outConstrPtr
+       outProjs  <- peekArray n outProjsPtr
+       return (Sort sort, FuncDecl outConstr, map FuncDecl outProjs)
+
+
 -- TODO Sorts: from Z3_mk_array_sort on
 
 ---------------------------------------------------------------------
 foreign import ccall unsafe "Z3_mk_array_sort"
     z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort)
 
+-- | Create a tuple type
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>
+foreign import ccall unsafe "Z3_mk_tuple_sort"
+    z3_mk_tuple_sort :: Ptr Z3_context
+                     -> Ptr Z3_symbol
+                     -> CUInt
+                     -> Ptr (Ptr Z3_symbol)
+                     -> Ptr (Ptr Z3_sort)
+                     -> Ptr (Ptr Z3_func_decl)
+                     -> Ptr (Ptr Z3_func_decl)
+                     -> IO (Ptr Z3_sort)
+
 -- TODO Sorts: from Z3_mk_array_sort on
 
 
   , mkRealSort
   , mkBvSort
   , mkArraySort
+  , mkTupleSort
 
   -- * Constants and Applications
   , mkFuncDecl
 mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
 mkArraySort = liftFun2 Base.mkArraySort
 
+-- | Create a tuple type
+--
+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>
+mkTupleSort :: MonadZ3 z3
+            => Symbol                          -- ^ Name of the sort
+            -> [(Symbol, Sort)]                -- ^ Name and sort of each field
+            -> z3 (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function
+                                               -- declarations for the
+                                               -- constructor and projections.
+mkTupleSort = liftFun2 Base.mkTupleSort
 
 ---------------------------------------------------------------------
 -- Constants and Applications

examples/examples.cabal

                        z3 ==0.3.1,
                        containers,
                        mtl >2.1
+
+executable mz3-tuple
+  hs-source-dirs:      monad
+  main-is:             Tuple.hs
+  -- other-modules:
+  build-depends:       base ==4.5.*,
+                       z3 ==0.3.1,
+                       containers,
+                       mtl >2.1

examples/monad/Tuple.hs

+module Main where
+
+import Z3.Monad
+
+tupleScript :: Z3 String
+tupleScript =
+    do intSort <- mkIntSort
+       argSym  <- mkStringSymbol "arg"
+       arg1Sym <- mkStringSymbol "arg1"
+       arg2Sym <- mkStringSymbol "arg2"
+       (argSort, constr, [proj1, proj2]) <-
+           mkTupleSort argSym [(arg1Sym, intSort), (arg2Sym, intSort)]
+
+       tSym <- mkStringSymbol "t"
+       t <- mkConst tSym argSort
+
+       p2 <- mkApp proj2 [t]
+       mkInt (5 :: Int) >>= mkGt p2 >>= assertCnstr
+
+       (_res, modelMb) <- getModel
+       case modelMb of
+         Just model -> showModel model
+         Nothing -> return "Couldn't construct model"
+
+
+main :: IO ()
+main = evalZ3 tupleScript >>= putStrLn