Commits

David Castro committed 3ed95f8

Changed types of mkForall and mkExists in Z3.Base

  • Participants
  • Parent commits e720c2c

Comments (0)

Files changed (3)

   | i >= 0    = AST <$> z3_mk_bound (unContext c) (fromIntegral i) (unSort s)
   | otherwise = error "Z3.Base.mkBound: negative de-Bruijn index"
 
-mkForall :: Context -> [Pattern] -> Symbol -> Sort -> AST -> IO AST
+mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
 mkForall c pats x s p
-  = withArray pats    $ \patsPtr ->
-    with (unSymbol x) $ \xptr ->
-    with (unSort s)   $ \sptr ->
-      AST <$> z3_mk_forall cptr 0 n (castPtr patsPtr) 1 sptr xptr (unAST p)
+  = withArray (map unPattern pats) $ \patsPtr ->
+    withArray (map unSymbol  x   ) $ \xptr ->
+    withArray (map unSort    s   ) $ \sptr ->
+      AST <$> z3_mk_forall cptr 0 n patsPtr 1 sptr xptr (unAST p)
   where n    = fromIntegral $ length pats
         cptr = unContext c
 
-mkExists :: Context -> [Pattern] -> Symbol -> Sort -> AST -> IO AST
+mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
 mkExists c pats x s p
-  = withArray pats    $ \patsPtr ->
-    with (unSymbol x) $ \xptr ->
-    with (unSort s)   $ \sptr ->
-      AST <$> z3_mk_exists cptr 0 n (castPtr patsPtr) 1 sptr xptr (unAST p)
+  = withArray (map unPattern pats) $ \patsPtr ->
+    withArray (map unSymbol  x   ) $ \xptr ->
+    withArray (map unSort    s   ) $ \sptr ->
+      AST <$> z3_mk_exists cptr 0 n patsPtr 1 sptr xptr (unAST p)
   where n    = fromIntegral $ length pats
         cptr = unContext c
 

File Z3/Lang/Monad.hs

 mkBound :: Int -> Base.Sort -> Z3 Base.AST
 mkBound = liftZ3Op3 Base.mkBound
 
-mkForall :: [Base.Pattern] -> Base.Symbol -> Base.Sort -> Base.AST -> Z3 Base.AST
+mkForall :: [Base.Pattern]
+            -> [Base.Symbol] -> [Base.Sort]
+            -> Base.AST -> Z3 Base.AST
 mkForall = liftZ3Op5 Base.mkForall
 
-mkExists :: [Base.Pattern] -> Base.Symbol -> Base.Sort -> Base.AST -> Z3 Base.AST
+mkExists :: [Base.Pattern]
+            -> [Base.Symbol] -> [Base.Sort]
+            -> Base.AST -> Z3 Base.AST
 mkExists = liftZ3Op5 Base.mkExists
 
 mkEq :: CmpOpE -> [Base.AST] -> Z3 Base.AST

File Z3/Lang/Prelude.hs

          (body,mb_pat) <- newQLayout $ \x -> liftM2 (,)
                               (compileBool $ mkBody q x)
                               (T.mapM mkPat (mb_mk_pat <*> pure x))
-         mkQExpr q (maybeToList mb_pat) sx srt body
+         mkQExpr q (maybeToList mb_pat) [sx] [srt] body
   where mkBody ForAll x = let b = f x in and_ (typeInv x:typecheck b) ==> b
         mkBody Exists x = let b = f x in and_ (b:typeInv x:typecheck b)
         mkPat (Pat e) = do ast <- compile e; mkPattern [ast]