Commits

David Castro  committed ec84419

Generalized quantifiers.

forall :: QExpr t => t -> Expr Bool

Example types of class QExpr t:
f :: Expr Integer -> Expr Bool
f :: Expr Bool -> Expr Bool
...
f :: Expr Integer -> Expr Rational -> Expr Bool
f :: Expr Integer -> Expr Rational -> QBody

QBody is the type of a quantified expression body. It is an 'Expr Bool'
annotated with a list [Pattern]:

t :: Expr Bool

t `instanceWhen` [Pat p1, Pat p2, ...]

  • Participants
  • Parent commits 859033a

Comments (0)

Files changed (4)

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/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
+