Commits

David Castro  committed 2e4c35d Merge

Automated merge with ssh://bitbucket.org/iago/z3-haskell

  • Participants
  • Parent commits 26c9dfe, ec84419

Comments (0)

Files changed (6)

     , Model
 
     -- ** Satisfiability result
-    , Result
+    , Result(..)
 
     -- * Configuration
     , mkConfig
   withArray (map unAST es) $ \aptr ->
     Pattern <$> z3_mk_pattern (unContext c) n aptr
   where n = genericLength es
-
 mkBound :: Context -> Int -> Sort -> IO AST
 mkBound c i s
   | i >= 0    = AST <$> z3_mk_bound (unContext c) (fromIntegral i) (unSort s)
   = 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)
+      AST <$> z3_mk_forall cptr 0 n patsPtr len sptr xptr (unAST p)
   where n    = genericLength pats
         cptr = unContext c
+        len
+          | l == 0        = error "Z3.Base.mkForall:\
+              \ forall with 0 bound variables"
+          | l /= length x = error "Z3.Base.mkForall:\
+              \ different number of symbols and sorts"
+          | otherwise     = fromIntegral l
+          where l = length s
 
 mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
 mkExists c pats x s 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)
+      AST <$> z3_mk_exists cptr 0 n patsPtr len sptr xptr (unAST p)
   where n    = fromIntegral $ length pats
         cptr = unContext c
+        len
+          | l == 0        = error "Z3.Base.mkForall:\
+              \ forall with 0 bound variables"
+          | l /= length x = error "Z3.Base.mkForall:\
+              \ different number of symbols and sorts"
+          | otherwise     = fromIntegral l
+          where l = length s
 
 ---------------------------------------------------------------------
 -- Accessors
       (toResult lb,) <$> peekModel mptr
   where peekModel :: Ptr (Ptr Z3_model) -> IO (Maybe Model)
         peekModel p | p == nullPtr = return Nothing
-                    | otherwise    = Just . Model <$> peek p
+                    | otherwise    = mkModel <$> peek p
+        mkModel :: Ptr Z3_model -> Maybe Model
+        mkModel p | p == nullPtr = Nothing
+                  | otherwise    = Just $ Model p 
 
 -- | Delete a model object.
 --

File Z3/Lang/Exprs.hs

     , Expr (..)
     , Pattern (..)
     , Quantifier(..)
+    , QExpr(..)
     , FunApp (..)
     , BoolBinOp (..)
     , BoolMultiOp (..)
   --  | Variadic boolean expressions
   BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool
   --  | Quantified formula
-  Quant :: IsTy a => Quantifier
-                     -> (Expr a -> Expr Bool)      --  ^ body
-                     -> Maybe (Expr a -> Pattern)  --  ^ pattern
-                     -> Expr Bool
+  Quant :: QExpr t => Quantifier -> t -> Expr Bool
   --  | Arithmetic negation
   Neg :: IsNum a => Expr a -> Expr a
   --  | Arithmetic expressions for commutative rings
   --  | Application
   App :: IsTy a  => FunApp a -> Expr a
 
+class QExpr t where
+  compileQuant :: Quantifier -> [Base.Symbol] -> [Base.Sort] -> t -> Z3 Base.AST
+
 -- | Quantifier pattern.
 --
 data Pattern where

File Z3/Lang/Lg2.hs

 declareLg2 = do
   lg2::Expr a -> Expr a <- fun1
   -- invariants
-  assert $ forallP (\x -> x >* 0 ==> lg2 x >=* 0)
-                   (\x -> Pat $ lg2 x)
-  assert $ forallP (\x -> x >* 0 ==> lg2 x <* x)
-                   (\x -> Pat $ lg2 x)
+  assert $ forall $ \x -> (x >* 0 ==> lg2 x >=* 0) `instanceWhen` [Pat $ lg2 x]
+  assert $ forall $ \x -> (x >* 0 ==> lg2 x <* x)  `instanceWhen` [Pat $ lg2 x]
   assert $ forall $ \x -> 
               x >* 0 ==> (lg2 (x+1) ==* lg2 x ||*  lg2 (x+1) ==* 1 + lg2 x)
   -- base cases

File Z3/Lang/Monad.hs

     , mkBound
     , mkForall
     , mkExists
+    , mkQuant
     , mkEq
     , mkCmp
     , mkFuncDecl
             -> Base.AST -> Z3 Base.AST
 mkExists = liftZ3Op5 Base.mkExists
 
+mkQuant :: Quantifier
+           -> [Base.Pattern]
+           -> [Base.Symbol] -> [Base.Sort]
+           -> Base.AST -> Z3 Base.AST
+mkQuant ForAll = mkForall
+mkQuant Exists = mkExists
+
 mkEq :: CmpOpE -> [Base.AST] -> Z3 Base.AST
 mkEq Distinct = liftZ3Op2 Base.mkDistinct
 mkEq Neq      = mkNot <=< mkEq Eq

File Z3/Lang/Pow2.hs

 declarePow2 = do
   pow2::Expr a -> Expr a <- fun1
   -- invariants
-  assert $ forallP (\x -> x <* 0 ==> pow2 x ==* 0)
-                   (\x -> Pat $ pow2 x)
-  assert $ forallP (\x -> x >=* 0 ==> pow2 x >* 0)
-                   (\x -> Pat $ pow2 x)
-  assert $ forallP (\x -> x >=* 0 ==> pow2 x >* x)
-                   (\x -> Pat $ pow2 x)
+  assert $ forall $ \x -> (x <* 0 ==> pow2 x ==* 0)
+                          `instanceWhen` [Pat $ pow2 x]
+  assert $ forall $ \x -> (x >=* 0 ==> pow2 x >* 0)
+                          `instanceWhen` [Pat $ pow2 x]
+  assert $ forall $ \x -> (x >=* 0 ==> pow2 x >* x)
+                          `instanceWhen` [Pat $ pow2 x]
   -- base cases
   assert $ pow2 0 ==* 1
   assert $ pow2 1 ==* 2
   -- recursive definition
-  assert $ forallP (\x -> x >* 1 ==> pow2 x ==* 2 * pow2 (x-1))
-                   (\x -> Pat $ pow2 x)
+  assert $ forall $ \x -> (x >* 1 ==> pow2 x ==* 2 * pow2 (x-1))
+                          `instanceWhen` [Pat $ pow2 x]
   -- and that's it!
   return pow2
 

File Z3/Lang/Prelude.hs

     , xor
     , implies, (==>)
     , iff, (<=>)
-    , forall, forallP
-    , exists, existsP
+    , forall
+    , exists
+    , instanceWhen
     , (//), (%*), (%%)
     , divides
     , (==*), (/=*)
 import Z3.Lang.Monad
 import Z3.Lang.TY
 
-import Control.Applicative ( (<$>), (<*>), pure )
-import Control.Monad ( liftM2 )
-import Data.Maybe ( maybeToList )
-import qualified Data.Traversable as T
+import Control.Applicative ( (<$>) )
 #if __GLASGOW_HASKELL__ < 704
 import Data.Typeable ( Typeable1(..), typeOf )
 import Unsafe.Coerce ( unsafeCoerce )
 fun2 = do
     (fd :: FunApp (a -> b -> c)) <- funDecl
     let f e1 e2 = App $ PApp (PApp fd e1) e2
-    assert $ forall $ \a -> forall $ \b -> typeInv (f a b)
+    assert $ forall $ \a b -> typeInv (f a b)
     return f
 
 
 fun3 = do
     (fd :: FunApp (a -> b -> c -> d)) <- funDecl
     let f e1 e2 e3 = App $ PApp (PApp (PApp fd e1) e2) e3
-    assert $ forall $ \a ->
-             forall $ \b ->
-             forall $ \c ->
-               typeInv (f a b c)
+    assert $ forall $ \a b c -> typeInv (f a b c)
     return f
 
 -- | Declare uninterpreted function of arity 4.
 fun4 = do
     (fd :: FunApp (a -> b -> c -> d -> e)) <- funDecl
     let f e1 e2 e3 e4 = App $ PApp (PApp (PApp (PApp fd e1) e2) e3) e4
-    assert $ forall $ \a ->
-             forall $ \b ->
-             forall $ \c ->
-             forall $ \d ->
-               typeInv (f a b c d)
+    assert $ forall $ \a b c d -> typeInv (f a b c d)
     return f
 
 -- | Declare uninterpreted function of arity 5.
 fun5 = do
     (fd :: FunApp (a -> b -> c -> d -> e -> f)) <- funDecl
     let f e1 e2 e3 e4 e5 = App $ PApp (PApp (PApp (PApp (PApp fd e1) e2) e3) e4) e5
-    assert $ forall $ \a ->
-             forall $ \b ->
-             forall $ \c ->
-             forall $ \d ->
-             forall $ \e ->
-               typeInv (f a b c d e)
+    assert $ forall $ \a b c d e -> typeInv (f a b c d e)
     return f
 
 -- | Declare uninterpreted function
 p ||* (BoolMulti Or qs) = or_ (p:qs)
 p ||* q = or_ [p,q]
 
--- | Forall formula.
+-- | Quantified formulas.
 --
-forall :: forall a. IsTy a => (Expr a -> Expr Bool) -> Expr Bool
-forall f = Quant ForAll f Nothing
 
-forallP :: IsTy a => (Expr a -> Expr Bool)    -- ^ body
-                      -> (Expr a -> Pattern)  -- ^ pattern
-                      -> Expr Bool
-forallP f = Quant ForAll f . Just
+forall  :: QExpr t => t -> Expr Bool
+forall f = Quant ForAll f
 
--- | Exists formula.
-exists :: forall a. IsTy a => (Expr a -> Expr Bool) -> Expr Bool
-exists f = Quant Exists f Nothing
+exists  :: QExpr t => t -> Expr Bool
+exists f = Quant Exists f
 
-existsP :: IsTy a => (Expr a -> Expr Bool)    -- ^ body
-                      -> (Expr a -> Pattern)  -- ^ pattern
-                      -> Expr Bool
-existsP f = Quant Exists f . Just
+instanceWhen :: Expr Bool -> [Pattern] -> QBody
+instanceWhen = QBody
 
 -- | Integer division.
 --
   tcBool e1
   tcBool e2
 tcBool (BoolMulti _op es) = mapM_ tcBool es
-tcBool (Quant _q _f _p) = ok
+tcBool (Quant _q _f) = ok
 tcBool (CmpE _op es) = do
   mapM_ tc es
 tcBool (CmpI _op e1 e2) = do
 compileBool (BoolMulti op es)
     = do es' <- mapM compileBool es
          mkBoolMulti op es'
-compileBool (Quant q (f :: Expr a -> Expr Bool)
-                     (mb_mk_pat :: Maybe (Expr a -> Pattern)))
-    = do (_,n) <- fresh
-         sx  <- mkStringSymbol n
-         srt <- mkSort (TY :: TY a)
-         (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
-  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]
-        mkQExpr ForAll = mkForall
-        mkQExpr Exists = mkExists
+compileBool (Quant q f)
+    = compileQuant q [] [] f
 compileBool (CmpE op es)
     = do es' <- mapM compile es
          mkEq op es'
 compileBool _
     = error "Z3.Lang.Prelude.compileBool: Panic! Impossible constructor in pattern matching!"
 
+withSortedSymbol :: IsTy a => TY a -> (Base.Symbol -> Base.Sort -> Z3 b) -> Z3 b
+withSortedSymbol t f = do
+  (_,n) <- fresh
+  sx    <- mkStringSymbol n
+  srt   <- mkSort t
+  f sx srt
+
+instance IsTy a => QExpr (Expr a -> Expr Bool) where
+  compileQuant q smbs srts f = do
+    withSortedSymbol (TY :: TY a) $ \sx srt ->
+      newQLayout $ \x -> do
+        body    <- compileBool $ mkBody q x
+        mkQuant q [] (sx:smbs) (srt:srts) 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)
+
+data QBody = QBody (Expr Bool) [Pattern]
+
+instance IsTy a => QExpr (Expr a -> QBody) where
+  compileQuant q smbs srts f = do
+    withSortedSymbol (TY :: TY a) $ \sx srt ->
+      newQLayout $ \x -> do
+        let QBody body pats = mapFst (mkBody q x) (f x)
+        astbody <- compileBool body
+        pat_lst <- mkPat pats
+        mkQuant q pat_lst (sx:smbs) (srt:srts) astbody
+    where mkBody ForAll x b = and_ (typeInv x:typecheck b) ==> b
+          mkBody Exists x b = and_ (b:typeInv x:typecheck b)
+          mkPat []  = return []
+          mkPat lst = mapM compile lst >>= \args -> (:[]) <$> mkPattern args
+          mapFst mf (QBody a b) = QBody (mf a) b
+
+instance (IsTy a, QExpr (b -> c)) => QExpr (Expr a -> b -> c) where
+  compileQuant q smbs srts f =
+    withSortedSymbol (TY :: TY a) $ \sx srt ->
+      newQLayout $ \x ->
+        compileQuant q (sx:smbs) (srt:srts) (f x)
+
 ----------------------------------------------------------------------
 -- Integers
 
   where doApp2AST :: FunApp t -> [Base.AST] -> Z3 Base.AST
         doApp2AST (FuncDecl fd) acc = mkApp fd acc
         doApp2AST (PApp e1 e2)  acc = compile e2 >>= doApp2AST e1 . (: acc)
+
+----------------------------------------------------------------------
+-- Patterns
+
+instance Compilable Pattern where
+  compile (Pat e) = compile e
+