Commits

David Castro committed 0182a8c

Existential quantifier.

  • Participants
  • Parent commits adbae0d

Comments (0)

Files changed (5)

     , mkPattern
     , mkBound
     , mkForall
+    , mkExists
 
     -- * Accessors
     , getBool
   where n    = fromIntegral $ length pats
         cptr = unContext c
 
+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)
+  where n    = fromIntegral $ length pats
+        cptr = unContext c
+
 ---------------------------------------------------------------------
 -- Accessors
 
                   -> Ptr Z3_ast
                   -> IO (Ptr Z3_ast)
 
--- TODO From 'Z3_mk_exists' on.
+-- | Create an exists formula.
+--
+-- Referece: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407
+foreign import ccall unsafe "Z3_mk_exists"
+  z3_mk_exists :: Ptr Z3_context -> CUInt
+                  -> CUInt -> Ptr (Ptr Z3_pattern)
+                  -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_symbol)
+                  -> Ptr Z3_ast
+                  -> IO (Ptr Z3_ast)
+
+-- TODO: Z3_mk_quantifier, Z3_mk_quantifier_ex, Z3_mk_forall_const,
+-- Z3_mk_exists_const, Z3_mk_quantifier_const, Z3_mk_quantifier_const_ex 
 
 ---------------------------------------------------------------------
 -- * Accessors
     , Layout
     , Expr (..)
     , Pattern (..)
+    , Quantifier(..)
     , FunApp (..)
     , BoolBinOp (..)
     , BoolMultiOp (..)
   BoolBin :: BoolBinOp -> Expr Bool -> Expr Bool -> Expr Bool
   --  | Variadic boolean expressions
   BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool
-  --  | Forall formula
-  ForAll :: IsTy a => (Expr a -> Expr Bool)       --  ^ body
-                    -> Maybe (Expr a -> Pattern)  --  ^ pattern
-                    -> Expr Bool
+  --  | Quantified formula
+  Quant :: IsTy a => Quantifier
+                     -> (Expr a -> Expr Bool)      --  ^ body
+                     -> Maybe (Expr a -> Pattern)  --  ^ pattern
+                     -> Expr Bool
   --  | Arithmetic negation
   Neg :: IsNum a => Expr a -> Expr a
   --  | Arithmetic expressions for commutative rings
 data Pattern where
   Pat :: IsTy a => Expr a -> Pattern
 
+-- | Quantifiers
+data Quantifier = ForAll | Exists
+  deriving (Eq, Show)
+
 -- | Z3 function
 --
 data FunApp :: * -> * where
     , mkPattern
     , mkBound
     , mkForall
+    , mkExists
     , mkEq
     , mkCmp
     , mkFuncDecl
 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 = liftZ3Op5 Base.mkExists
+
 mkEq :: CmpOpE -> [Base.AST] -> Z3 Base.AST
 mkEq Distinct = liftZ3Op2 Base.mkDistinct
 mkEq Neq      = mkNot <=< mkEq Eq

Z3/Lang/Prelude.hs

     , implies, (==>)
     , iff, (<=>)
     , forall, forallP
+    , exists, existsP
     , (//), (%*), (%%)
     , divides
     , (==*), (/=*)
 -- | Forall formula.
 --
 forall :: forall a. IsTy a => (Expr a -> Expr Bool) -> Expr Bool
-forall f = ForAll f Nothing
+forall f = Quant ForAll f Nothing
 
 forallP :: IsTy a => (Expr a -> Expr Bool)    -- ^ body
                       -> (Expr a -> Pattern)  -- ^ pattern
                       -> Expr Bool
-forallP f = ForAll f . Just
+forallP f = Quant ForAll f . Just
+
+-- | Exists formula.
+exists :: forall a. IsTy a => (Expr a -> Expr Bool) -> Expr Bool
+exists f = Quant Exists f Nothing
+
+existsP :: IsTy a => (Expr a -> Expr Bool)    -- ^ body
+                      -> (Expr a -> Pattern)  -- ^ pattern
+                      -> Expr Bool
+existsP f = Quant Exists f . Just
 
 -- | Integer division.
 --
   tcBool e1
   tcBool e2
 tcBool (BoolMulti _op es) = mapM_ tcBool es
-tcBool (ForAll _f _p) = ok
+tcBool (Quant _q _f _p) = 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 (ForAll (f :: Expr a -> Expr Bool)
-                    (mb_mk_pat :: Maybe (Expr a -> Pattern)))
+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 x)
+                              (compileBool $ mkBody q x)
                               (T.mapM mkPat (mb_mk_pat <*> pure x))
-         mkForall (maybeToList mb_pat) sx srt body
-  where mkBody x = let b = f x in and_ (typeInv x:typecheck b) ==> b
+         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 (CmpE op es)
     = do es' <- mapM compile es
          mkEq op es'