diff --git a/Z3/Base.hs b/Z3/Base.hs --- a/Z3/Base.hs +++ b/Z3/Base.hs @@ -1,8 +1,14 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} -- | -- Module : Z3.Base @@ -23,18 +29,19 @@ , Symbol , AST , Sort + , FuncDecl , App , Pattern , Model , castAST - + -- ** Satisfiability result , Result(..) -- ** Z3 types , Z3Type(..) - , Z3Scalar(..) + , Z3Fun() , Z3Num -- * Configuration @@ -56,6 +63,8 @@ , mkRealSort -- * Constants and Applications + , mkFuncDecl + , mkApp1, mkApp2, mkApp3, mkApp4, mkApp5 , mkConst , mkTrue , mkFalse @@ -87,6 +96,11 @@ , mkInt , mkReal + -- * Quantifiers + , mkPattern + , mkBound + , mkForall + -- * Accessors , getBool , getInt @@ -103,29 +117,27 @@ ) where import Z3.Base.C -import Z3.Types.TY +import Z3.Lang.TY import Control.Applicative ( (<$>) ) -import Control.Monad ( liftM2 ) -import Data.Typeable ( Typeable ) import Data.Int import Data.Ratio ( Ratio, numerator, denominator, (%) ) -import Data.Word import Data.Typeable ( Typeable, typeOf ) -import Foreign hiding ( newForeignPtr, toBool ) +import Data.Word +import Foreign hiding ( newForeignPtr, addForeignPtrFinalizer, toBool ) import Foreign.C ( CInt, CUInt, CLLong, CULLong , peekCString , withCString ) -import Foreign.Concurrent ( newForeignPtr ) +import Foreign.Concurrent ( newForeignPtr, addForeignPtrFinalizer ) --------------------------------------------------------------------- -- Types -- -- | A Z3 /configuration object/. --- -- +-- -- /Notes:/ -- -- * The resource is automatically managed by the Haskell garbage @@ -135,9 +147,18 @@ newtype Config = Config { unConfig :: ForeignPtr Z3_config } deriving Eq +-- | withConfig. +-- +-- Just an auxiliary function to avoid the "withForeignPtr . unConfig" +-- boilerplate +-- +withConfig :: Config -> (Ptr Z3_config -> IO a) -> IO a +withConfig = withForeignPtr . unConfig + + -- | A Z3 /logical context/. --- -- +-- -- /Notes:/ -- -- * The resource is automatically managed by the Haskell garbage @@ -147,25 +168,33 @@ newtype Context = Context { unContext :: ForeignPtr Z3_context } deriving Eq +-- | withContext. +-- +-- Just an auxiliary function to avoid the "withForeignPtr . unContext" +-- boilerplate +-- +withContext :: Context -> (Ptr Z3_context -> IO a) -> IO a +withContext = withForeignPtr . unContext + -- | A Z3 /Lisp-link symbol/. --- +-- newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol } deriving (Eq, Ord, Show, Storable) -- | A Z3 /AST node/. --- +-- -- TODO: Does the extra type safety provided by the phantom type worth -- complicating the higher-level layers such as 'Z3.Monad' ? -- newtype AST a = AST { unAST :: Ptr Z3_ast } - deriving (Eq, Ord, Show, Storable) + deriving (Eq, Ord, Show, Storable, Typeable) -- | Cast an 'AST a' to 'AST b' when 'a' and 'b' are the same type. -- -- This is useful when unpacking an existentially quantified AST. -- castAST :: forall a b. (Z3Type a, Z3Type b) => AST a -> Maybe (AST b) -castAST (AST a) +castAST (AST a) | typeOf (TY::TY a) == typeOf (TY::TY b) = Just (AST a) | otherwise = Nothing @@ -174,12 +203,17 @@ newtype Sort a = Sort { unSort :: Ptr Z3_sort } deriving (Eq, Ord, Show, Storable) +-- | Kind of AST used to represent function symbols. +-- +newtype FuncDecl a = FuncDecl { unFuncDecl :: Ptr Z3_func_decl } + deriving (Eq, Ord, Show, Storable, Typeable) + -- | A kind of Z3 AST used to represent constant and function declarations. -- newtype App a = App { _unApp :: Ptr Z3_app } deriving (Eq, Ord, Show, Storable) --- | A kind of AST used to represent pattern and multi-patterns used to +-- | A kind of AST used to represent pattern and multi-patterns used to -- guide quantifier instantiation. -- newtype Pattern = Pattern { _unPattern :: Ptr Z3_pattern } @@ -187,26 +221,33 @@ -- | A model for the constraints asserted into the logical context. -- -data Model - = Model { - modelContext :: Context - , unModel :: ForeignPtr Z3_model - } +newtype Model = Model { unModel :: Ptr Z3_model } deriving Eq -- | Result of a satisfiability check. -- -data Result - = Sat +data Result a + = Sat a | Unsat | Undef - deriving (Eq, Ord, Enum, Bounded, Read, Show) + deriving (Eq, Ord, Read, Show) +instance Functor Result where + fmap f (Sat x) = Sat $ f x + fmap _ Unsat = Unsat + fmap _ Undef = Undef + +instance Monad Result where + return = Sat + Sat x >>= f = f x + Unsat >>= _ = Unsat + Undef >>= _ = Undef + -- | Convert 'Z3_lbool' from Z3.Base.C to 'Result' -- -toResult :: Z3_lbool -> Result +toResult :: Z3_lbool -> Result () toResult lb - | lb == z3_l_true = Sat + | lb == z3_l_true = Sat () | lb == z3_l_false = Unsat | lb == z3_l_undef = Undef | otherwise = error "Z3.Base.toResult: illegal `Z3_lbool' value" @@ -227,40 +268,49 @@ -- | A Z3 type -- -class Typeable a => Z3Type a where +class (Eq a, Show a, Typeable a) => Z3Type a where mkSort :: Context -> IO (Sort a) + mkValue :: Context -> a -> IO (AST a) + getValue :: Context -> AST a -> IO a instance Z3Type Bool where mkSort = mkBoolSort + mkValue ctx True = mkTrue ctx + mkValue ctx False = mkFalse ctx + getValue ctx a = maybe False id <$> getBool ctx a instance Z3Type Integer where mkSort = mkIntSort + mkValue = mkInt + getValue = getInt instance Z3Type Rational where mkSort = mkRealSort + mkValue = mkReal + getValue = getReal --- | A Z3 scalar type +-- | A Function type -- -class (Eq a, Show a, Z3Type a) => Z3Scalar a where - mkValue :: Context -> a -> IO (AST a) - getValue :: Context -> AST a -> IO (Maybe a) +class Z3Fun a where + -- Private functions: domain, range + domain :: Context -> TY a -> IO (CUInt, [Ptr Z3_sort]) + range :: Context -> TY a -> IO (Ptr Z3_sort) -instance Z3Scalar Bool where - mkValue ctx True = mkTrue ctx - mkValue ctx False = mkFalse ctx - getValue = getBool +instance (Z3Type a, Z3Type b) => Z3Fun (a -> b) where + domain ctx _ = (1,) . (: []) . unSort <$> (mkSort ctx :: IO (Sort a)) + range ctx _ = unSort <$> (mkSort ctx :: IO (Sort b)) -instance Z3Scalar Integer where - mkValue ctx = mkInt ctx - getValue ctx ast = Just <$> getInt ctx ast +instance (Z3Type a, Z3Fun (b -> c)) => Z3Fun (a -> b -> c) where + domain ctx _ = do + (srt1 :: Sort a) <- mkSort ctx + (n,lst) <- domain ctx (TY :: TY (b -> c)) + return (n + 1, unSort srt1 : lst) + range ctx _ = range ctx (TY :: TY (b -> c)) -instance Z3Scalar Rational where - mkValue ctx = mkReal ctx - getValue ctx ast = Just <$> getReal ctx ast -- | A Z3 numeric type -- -class (Z3Scalar a, Num a) => Z3Num a where +class (Z3Type a, Num a) => Z3Num a where instance Z3Num Integer where instance Z3Num Rational where @@ -285,9 +335,9 @@ -- setParamValue :: Config -> String -> String -> IO () setParamValue cfg s1 s2 = - withForeignPtr (unConfig cfg) $ \cfgPtr -> - withCString s1 $ \cs1 -> - withCString s2 $ \cs2 -> + withConfig cfg $ \cfgPtr -> + withCString s1 $ \cs1 -> + withCString s2 $ \cs2 -> z3_set_param_value cfgPtr cs1 cs2 -- | Set the /MODEL/ configuration parameter. @@ -311,7 +361,7 @@ -- default: 'True', enable/disable type checker. -- set_WELL_SORTED_CHECK :: Config -> Bool -> IO () -set_WELL_SORTED_CHECK cfg True = setParamValue cfg "MWELL_SORTED_CHECK" "true" +set_WELL_SORTED_CHECK cfg True = setParamValue cfg "WELL_SORTED_CHECK" "true" set_WELL_SORTED_CHECK cfg False = setParamValue cfg "WELL_SORTED_CHECK" "false" --------------------------------------------------------------------- @@ -322,7 +372,7 @@ -- Reference: -- mkContext :: Config -> IO Context -mkContext cfg = withForeignPtr (unConfig cfg) $ \cfgPtr -> do +mkContext cfg = withConfig cfg $ \cfgPtr -> do ptr <- z3_mk_context cfgPtr fptr <- newForeignPtr ptr (z3_del_context ptr) return $! Context fptr @@ -336,9 +386,9 @@ -- mkStringSymbol :: Context -> String -> IO Symbol mkStringSymbol ctx s = - withForeignPtr (unContext ctx) $ \ctxPtr -> - withCString s $ \cs -> - Symbol <$> z3_mk_string_symbol ctxPtr cs + withContext ctx $ \ctxPtr -> + withCString s $ \cs -> + Symbol <$> z3_mk_string_symbol ctxPtr cs --------------------------------------------------------------------- -- Sorts @@ -351,7 +401,7 @@ -- Reference: -- mkBoolSort :: Context -> IO (Sort Bool) -mkBoolSort c = withForeignPtr (unContext c) $ \cptr -> +mkBoolSort c = withContext c $ \cptr -> Sort <$> z3_mk_bool_sort cptr -- | Create an integer type. @@ -359,7 +409,7 @@ -- Reference: -- mkIntSort :: Context -> IO (Sort Integer) -mkIntSort c = withForeignPtr (unContext c) $ \cptr -> +mkIntSort c = withContext c $ \cptr -> Sort <$> z3_mk_int_sort cptr -- | Create a real type. @@ -367,7 +417,7 @@ -- Reference: -- mkRealSort :: Context -> IO (Sort Rational) -mkRealSort c = withForeignPtr (unContext c) $ \cptr -> +mkRealSort c = withContext c $ \cptr -> Sort <$> z3_mk_real_sort cptr -- TODO Sorts: from Z3_mk_real_sort on @@ -375,15 +425,72 @@ --------------------------------------------------------------------- -- Constants and Applications --- TODO Constants and Applications: Z3_mk_func_decl --- TODO Constants and Applications: Z3_mk_app +-- | A Z3 function +mkFuncDecl :: forall t. Z3Fun t => Context -> Symbol -> IO (FuncDecl t) +mkFuncDecl ctx (Symbol smb) = withContext ctx $ \ctxPtr -> do + (len, dom) <- domain ctx (TY :: TY t) + rng <- range ctx (TY :: TY t) + withArray dom $ \c_dom -> + FuncDecl <$> z3_mk_func_decl ctxPtr smb len c_dom rng +-- | Create a constant or function application. +-- +-- Reference: +-- +mkApp1 :: (Z3Type a, Z3Type b) + => Context + -> FuncDecl (a -> b) + -> AST a + -> IO (AST b) +mkApp1 ctx fd a + = AST <$> mkApp ctx fd [unAST a] + +mkApp2 :: (Z3Type a, Z3Type b, Z3Type c) + => Context + -> FuncDecl (a -> b -> c) + -> AST a -> AST b + -> IO (AST c) +mkApp2 ctx fd a b + = AST <$> mkApp ctx fd [unAST a,unAST b] + +mkApp3 :: (Z3Type a, Z3Type b, Z3Type c , Z3Type d) + => Context + -> FuncDecl (a -> b -> c -> d) + -> AST a -> AST b -> AST c + -> IO (AST d) +mkApp3 ctx fd a b c + = AST <$> mkApp ctx fd [unAST a,unAST b,unAST c] + +mkApp4 :: (Z3Type a, Z3Type b, Z3Type c , Z3Type d, Z3Type e) + => Context + -> FuncDecl (a -> b -> c -> d -> e) + -> AST a -> AST b -> AST c -> AST d + -> IO (AST e) +mkApp4 ctx fd a b c d + = AST <$> mkApp ctx fd [unAST a,unAST b,unAST c,unAST d] + +mkApp5 :: (Z3Type a, Z3Type b, Z3Type c , Z3Type d, Z3Type e, Z3Type f) + => Context + -> FuncDecl (a -> b -> c -> d -> e -> f) + -> AST a -> AST b -> AST c -> AST d -> AST e + -> IO (AST f) +mkApp5 ctx fd a b c d e + = AST <$> mkApp ctx fd [unAST a,unAST b ,unAST c,unAST d ,unAST e] + + +mkApp :: Context -> FuncDecl t -> [Ptr Z3_ast] -> IO (Ptr Z3_ast) +mkApp ctx fd args = + withContext ctx $ \ctxPtr -> + withArray args $ \pargs -> + z3_mk_app ctxPtr (unFuncDecl fd) (fromIntegral $ length args) pargs + + -- | Declare and create a constant. -- -- Reference: -- -mkConst :: Context -> Symbol -> Sort a -> IO (AST a) -mkConst c x s = withForeignPtr (unContext c) $ \cptr -> +mkConst :: Z3Type a => Context -> Symbol -> Sort a -> IO (AST a) +mkConst c x s = withContext c $ \cptr -> AST <$> z3_mk_const cptr (unSymbol x) (unSort s) -- TODO Constants and Applications: Z3_mk_fresh_func_decl @@ -394,7 +501,7 @@ -- Reference: -- mkTrue :: Context -> IO (AST Bool) -mkTrue c = withForeignPtr (unContext c) $ \cptr -> +mkTrue c = withContext c $ \cptr -> AST <$> z3_mk_true cptr -- | Create an AST node representing /false/. @@ -402,15 +509,15 @@ -- Reference: -- mkFalse :: Context -> IO (AST Bool) -mkFalse c = withForeignPtr (unContext c) $ \cptr -> +mkFalse c = withContext c $ \cptr -> AST <$> z3_mk_false cptr -- | Create an AST node representing l = r. -- -- Reference: -- -mkEq :: Z3Scalar a => Context -> AST a -> AST a -> IO (AST Bool) -mkEq c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkEq :: Z3Type a => Context -> AST a -> AST a -> IO (AST Bool) +mkEq c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_eq cptr (unAST e1) (unAST e2) -- | Create an AST node representing not(a). @@ -418,7 +525,7 @@ -- Reference: -- mkNot :: Context -> AST Bool -> IO (AST Bool) -mkNot c e = withForeignPtr (unContext c) $ \cptr -> +mkNot c e = withContext c $ \cptr -> AST <$> z3_mk_not cptr (unAST e) -- | Create an AST node representing an if-then-else: ite(t1, t2, t3). @@ -426,31 +533,31 @@ -- Reference: -- mkIte :: Context -> AST Bool -> AST a -> AST a -> IO (AST a) -mkIte c g e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkIte c g e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_ite cptr (unAST g) (unAST e1) (unAST e2) --- | Create an AST node representing t1 iff t2. +-- | Create an AST node representing t1 iff t2. -- -- Reference: -- mkIff :: Context -> AST Bool -> AST Bool -> IO (AST Bool) -mkIff c p q = withForeignPtr (unContext c) $ \cptr -> +mkIff c p q = withContext c $ \cptr -> AST <$> z3_mk_iff cptr (unAST p) (unAST q) --- | Create an AST node representing t1 implies t2. +-- | Create an AST node representing t1 implies t2. -- -- Reference: -- mkImplies :: Context -> AST Bool -> AST Bool -> IO (AST Bool) -mkImplies c p q = withForeignPtr (unContext c) $ \cptr -> +mkImplies c p q = withContext c $ \cptr -> AST <$> z3_mk_implies cptr (unAST p) (unAST q) --- | Create an AST node representing t1 xor t2. +-- | Create an AST node representing t1 xor t2. -- -- Reference: -- mkXor :: Context -> AST Bool -> AST Bool -> IO (AST Bool) -mkXor c p q = withForeignPtr (unContext c) $ \cptr -> +mkXor c p q = withContext c $ \cptr -> AST <$> z3_mk_xor cptr (unAST p) (unAST q) -- | Create an AST node representing args[0] and ... and args[num_args-1]. @@ -459,46 +566,46 @@ -- mkAnd :: Context -> [AST Bool] -> IO (AST Bool) mkAnd _ [] = error "Z3.Base.mkAnd: empty list of expressions" -mkAnd c es - = withArray es $ \aptr -> - withForeignPtr (unContext c) $ \cptr -> - AST <$> z3_mk_and cptr n (castPtr aptr) +mkAnd c es = + withArray es $ \aptr -> + withContext c $ \cptr -> + AST <$> z3_mk_and cptr n (castPtr aptr) where n = fromIntegral $ length es --- | Create an AST node representing args[0] or ... or args[num_args-1]. +-- | Create an AST node representing args[0] or ... or args[num_args-1]. -- -- Reference: -- mkOr :: Context -> [AST Bool] -> IO (AST Bool) mkOr _ [] = error "Z3.Base.mkOr: empty list of expressions" -mkOr c es - = withArray es $ \aptr -> - withForeignPtr (unContext c) $ \cptr -> - AST <$> z3_mk_or cptr n (castPtr aptr) +mkOr c es = + withArray es $ \aptr -> + withContext c $ \cptr -> + AST <$> z3_mk_or cptr n (castPtr aptr) where n = fromIntegral $ length es --- | Create an AST node representing args[0] + ... + args[num_args-1]. +-- | Create an AST node representing args[0] + ... + args[num_args-1]. -- -- Reference: -- mkAdd :: Z3Num a => Context -> [AST a] -> IO (AST a) mkAdd _ [] = error "Z3.Base.mkAdd: empty list of expressions" -mkAdd c es - = withArray es $ \aptr -> - withForeignPtr (unContext c) $ \cptr -> - AST <$> z3_mk_add cptr n (castPtr aptr) +mkAdd c es = + withArray es $ \aptr -> + withContext c $ \cptr -> + AST <$> z3_mk_add cptr n (castPtr aptr) where n = fromIntegral $ length es --- | Create an AST node representing args[0] * ... * args[num_args-1]. +-- | Create an AST node representing args[0] * ... * args[num_args-1]. -- -- Reference: -- mkMul :: Z3Num a => Context -> [AST a] -> IO (AST a) mkMul _ [] = error "Z3.Base.mkMul: empty list of expressions" -mkMul c es - = withArray es $ \aptr -> - withForeignPtr (unContext c) $ \cptr -> - AST <$> z3_mk_mul cptr n (castPtr aptr) +mkMul c es = + withArray es $ \aptr -> + withContext c $ \cptr -> + AST <$> z3_mk_mul cptr n (castPtr aptr) where n = fromIntegral $ length es -- | Create an AST node representing args[0] - ... - args[num_args - 1]. @@ -507,10 +614,10 @@ -- mkSub ::Z3Num a => Context -> [AST a] -> IO (AST a) mkSub _ [] = error "Z3.Base.mkSub: empty list of expressions" -mkSub c es - = withArray es $ \aptr -> - withForeignPtr (unContext c) $ \cptr -> - AST <$> z3_mk_sub cptr n (castPtr aptr) +mkSub c es = + withArray es $ \aptr -> + withContext c $ \cptr -> + AST <$> z3_mk_sub cptr n (castPtr aptr) where n = fromIntegral $ length es -- | Create an AST node representing -arg. @@ -518,7 +625,7 @@ -- Reference: -- mkUnaryMinus :: Z3Num a => Context -> AST a -> IO (AST a) -mkUnaryMinus c e = withForeignPtr (unContext c) $ \cptr -> +mkUnaryMinus c e = withContext c $ \cptr -> AST <$> z3_mk_unary_minus cptr (unAST e) -- | Create an AST node representing arg1 div arg2. @@ -526,7 +633,7 @@ -- Reference: -- mkDiv :: Z3Num a => Context -> AST a -> AST a -> IO (AST a) -mkDiv c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkDiv c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_div cptr (unAST e1) (unAST e2) -- | Create an AST node representing arg1 mod arg2. @@ -534,7 +641,7 @@ -- Reference: -- mkMod :: Context -> AST Integer -> AST Integer -> IO (AST Integer) -mkMod c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkMod c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_mod cptr (unAST e1) (unAST e2) -- | Create an AST node representing arg1 rem arg2. @@ -542,7 +649,7 @@ -- Reference: -- mkRem :: Context -> AST Integer -> AST Integer -> IO (AST Integer) -mkRem c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkRem c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_rem cptr (unAST e1) (unAST e2) -- | Create less than. @@ -550,7 +657,7 @@ -- Reference: -- mkLt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkLt c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkLt c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_lt cptr (unAST e1) (unAST e2) -- | Create less than or equal to. @@ -558,7 +665,7 @@ -- Reference: -- mkLe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkLe c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkLe c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_le cptr (unAST e1) (unAST e2) -- | Create greater than. @@ -566,7 +673,7 @@ -- Reference: -- mkGt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkGt c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkGt c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_gt cptr (unAST e1) (unAST e2) -- | Create greater than or equal to. @@ -574,7 +681,7 @@ -- Reference: -- mkGe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkGe c e1 e2 = withForeignPtr (unContext c) $ \cptr -> +mkGe c e1 e2 = withContext c $ \cptr -> AST <$> z3_mk_ge cptr (unAST e1) (unAST e2) -- | Coerce an integer to a real. @@ -582,7 +689,7 @@ -- Reference: -- mkInt2Real :: Context -> AST Integer -> IO (AST Rational) -mkInt2Real c e = withForeignPtr (unContext c) $ \cptr -> +mkInt2Real c e = withContext c $ \cptr -> AST <$> z3_mk_int2real cptr (unAST e) -- | Coerce a real to an integer. @@ -590,7 +697,7 @@ -- Reference: -- mkReal2Int :: Context -> AST Rational -> IO (AST Integer) -mkReal2Int c e = withForeignPtr (unContext c) $ \cptr -> +mkReal2Int c e = withContext c $ \cptr -> AST <$> z3_mk_real2int cptr (unAST e) -- | Check if a real number is an integer. @@ -598,7 +705,7 @@ -- Reference: -- mkIsInt :: Context -> AST Rational -> IO (AST Bool) -mkIsInt c e = withForeignPtr (unContext c) $ \cptr -> +mkIsInt c e = withContext c $ \cptr -> AST <$> z3_mk_is_int cptr (unAST e) -- TODO Bit-vector, Arrays, Sets @@ -613,8 +720,8 @@ -- mkNumeral :: Z3Num a => Context -> String -> Sort a -> IO (AST a) mkNumeral c str s = - withForeignPtr (unContext c) $ \cptr -> - withCString str $ \cstr-> + withContext c $ \cptr -> + withCString str $ \cstr-> AST <$> z3_mk_numeral cptr cstr (unSort s) ------------------------------------------------- @@ -623,35 +730,35 @@ -- | Create a numeral of sort /int/. mkInt :: Integral a => Context -> a -> IO (AST Integer) mkInt c n = mkIntSort c >>= mkNumeral c n_str - where n_str = show $ toInteger n + where n_str = show $ toInteger n {-# INLINE mkIntZ3 #-} mkIntZ3 :: Z3Num a => Context -> Int32 -> Sort a -> IO (AST a) mkIntZ3 c n s = - withForeignPtr (unContext c) $ \ctxPtr -> - AST <$> z3_mk_int ctxPtr cn (unSort s) - where cn = fromIntegral n :: CInt + withContext c $ \ctxPtr -> + AST <$> z3_mk_int ctxPtr cn (unSort s) + where cn = fromIntegral n :: CInt {-# INLINE mkUnsignedIntZ3 #-} mkUnsignedIntZ3 :: Z3Num a => Context -> Word32 -> Sort a -> IO (AST a) mkUnsignedIntZ3 c n s = - withForeignPtr (unContext c) $ \ctxPtr -> - AST <$> z3_mk_unsigned_int ctxPtr cn (unSort s) - where cn = fromIntegral n :: CUInt + withContext c $ \ctxPtr -> + AST <$> z3_mk_unsigned_int ctxPtr cn (unSort s) + where cn = fromIntegral n :: CUInt {-# INLINE mkInt64Z3 #-} mkInt64Z3 :: Z3Num a => Context -> Int64 -> Sort a -> IO (AST a) mkInt64Z3 c n s = - withForeignPtr (unContext c) $ \ctxPtr -> - AST <$> z3_mk_int64 ctxPtr cn (unSort s) - where cn = fromIntegral n :: CLLong + withContext c $ \ctxPtr -> + AST <$> z3_mk_int64 ctxPtr cn (unSort s) + where cn = fromIntegral n :: CLLong {-# INLINE mkUnsignedInt64Z3 #-} mkUnsignedInt64Z3 :: Z3Num a => Context -> Word64 -> Sort a -> IO (AST a) mkUnsignedInt64Z3 c n s = - withForeignPtr (unContext c) $ \ctxPtr -> - AST <$> z3_mk_unsigned_int64 ctxPtr cn (unSort s) - where cn = fromIntegral n :: CULLong + withContext c $ \ctxPtr -> + AST <$> z3_mk_unsigned_int64 ctxPtr cn (unSort s) + where cn = fromIntegral n :: CULLong {-# RULES "mkInt/mkInt_IntZ3" mkInt = mkInt_IntZ3 #-} mkInt_IntZ3 :: Context -> Int32 -> IO (AST Integer) @@ -675,18 +782,18 @@ -- | Create a numeral of sort /real/. mkReal :: Real r => Context -> r -> IO (AST Rational) mkReal c n = mkRealSort c >>= mkNumeral c n_str - where r = toRational n - r_n = toInteger $ numerator r - r_d = toInteger $ denominator r - n_str = show r_n ++ " / " ++ show r_d + where r = toRational n + r_n = toInteger $ numerator r + r_d = toInteger $ denominator r + n_str = show r_n ++ " / " ++ show r_d {-# RULES "mkReal/mkRealZ3" mkReal = mkRealZ3 #-} mkRealZ3 :: Context -> Ratio Int32 -> IO (AST Rational) mkRealZ3 c r = - withForeignPtr (unContext c) $ \ctxPtr -> - AST <$> z3_mk_real ctxPtr n d - where n = (fromIntegral $ numerator r) :: CInt - d = (fromIntegral $ denominator r) :: CInt + withContext c $ \ctxPtr -> + AST <$> z3_mk_real ctxPtr n d + where n = (fromIntegral $ numerator r) :: CInt + d = (fromIntegral $ denominator r) :: CInt {-# RULES "mkReal/mkReal_IntZ3" mkReal = mkReal_IntZ3 #-} mkReal_IntZ3 :: Context -> Int32 -> IO (AST Rational) @@ -704,8 +811,32 @@ mkReal_UnsignedInt64Z3 :: Context -> Word64 -> IO (AST Rational) mkReal_UnsignedInt64Z3 c n = mkRealSort c >>= mkUnsignedInt64Z3 c n --- TODO Quantifiers +--------------------------------------------------------------------- +-- Quantifiers +mkPattern :: Context -> [AST a] -> IO Pattern +mkPattern _ [] = error "Z3.Base.mkPattern: empty list of expressions" +mkPattern c es = + withArray es $ \aptr -> + withContext c $ \cptr -> + Pattern <$> z3_mk_pattern cptr n (castPtr aptr) + where n = fromIntegral $ length es + +mkBound :: Context -> Int -> Sort a -> IO (AST a) +mkBound c i s + | i >= 0 = withContext c $ \cptr -> + AST <$> z3_mk_bound cptr (fromIntegral i) (unSort s) + | otherwise = error "Z3.Base.mkBound: negative de-Bruijn index" + +mkForall :: Context -> [Pattern] -> Symbol -> Sort a -> AST Bool -> IO (AST Bool) +mkForall c pats x s p + = withArray pats $ \patsPtr -> + with (unSymbol x) $ \xptr -> + with (unSort s) $ \sptr -> + withContext c $ \cptr -> + AST <$> z3_mk_forall cptr 0 n (castPtr patsPtr) 1 sptr xptr (unAST p) + where n = fromIntegral $ length pats + --------------------------------------------------------------------- -- Accessors @@ -723,43 +854,36 @@ -- Reference: -- getBool :: Context -> AST Bool -> IO (Maybe Bool) -getBool c a = withForeignPtr (unContext c) $ \ctxPtr -> +getBool c a = withContext c $ \ctxPtr -> castLBool <$> z3_get_bool_value ctxPtr (unAST a) --- | Return numeral value, as a string of a numeric constant term. +-- | Return numeral value, as a string of a numeric constant term. -- -- Reference: -- getNumeralString :: Z3Num a => Context -> AST a -> IO String -getNumeralString c a = withForeignPtr (unContext c) $ \ctxPtr -> +getNumeralString c a = withContext c $ \ctxPtr -> peekCString =<< z3_get_numeral_string ctxPtr (unAST a) -- | Return 'Z3Int' value -- -getInt :: Num a => Context -> AST Integer -> IO a -getInt c a = fromInteger . read <$> getNumeralString c a +getInt :: Context -> AST Integer -> IO Integer +getInt c a = read <$> getNumeralString c a --- | Return the numerator (as a numeral AST) of a numeral AST of sort /real/. --- --- Reference: +-- | Return 'Z3Real' value -- -getNumerator :: Context -> AST Rational -> IO Integer -getNumerator c a = withForeignPtr (unContext c) $ \ctxPtr -> - z3_get_numerator ctxPtr (unAST a) >>= getInt c . AST +getReal :: Context -> AST Rational -> IO Rational +getReal c a = parse <$> getNumeralString c a + where parse :: String -> Rational + parse s + | [(i, sj)] <- reads s = i % parseDen (dropWhile (== ' ') sj) + | otherwise = error "Z3.Base.getReal: no parse" --- | Return the denominator (as a numeral AST) of a numeral AST of sort /real/. --- --- Reference: --- -getDenominator :: Context -> AST Rational -> IO Integer -getDenominator c a = withForeignPtr (unContext c) $ \ctxPtr -> - z3_get_denominator ctxPtr (unAST a) >>= getInt c . AST + parseDen :: String -> Integer + parseDen "" = 1 + parseDen ('/':sj) = read sj + parseDen _ = error "Z3.Base.getReal: no parse" --- | Return 'Z3Real' value --- -getReal :: Fractional a => Context -> AST Rational -> IO a -getReal c a = fromRational <$> - liftM2 (%) (getNumerator c a) (getDenominator c a) -- TODO Modifiers @@ -767,16 +891,17 @@ -- Models mkModel :: Context -> Ptr Z3_model -> IO Model -mkModel ctx ptr = withForeignPtr (unContext ctx) $ \ctxPtr -> - Model ctx <$> newForeignPtr ptr (z3_del_model ctxPtr ptr) +mkModel ctx ptr = withForeignPtr fptr $ \ctxPtr -> do + addForeignPtrFinalizer fptr $ z3_del_model ctxPtr ptr + return $ Model ptr + where fptr = unContext ctx -- | Evaluate an AST node in the given model. -eval :: Model -> AST a -> IO (Maybe (AST a)) -eval m a - = withForeignPtr (unContext $ modelContext m) $ \ctxPtr -> - withForeignPtr (unModel m) $ \mdlPtr -> - alloca $ \aptr2 -> - z3_eval ctxPtr mdlPtr (unAST a) aptr2 >>= peekAST aptr2 . toBool +eval :: Context -> Model -> AST a -> IO (Maybe (AST a)) +eval ctx m a = + withContext ctx $ \ctxPtr -> + alloca $ \aptr2 -> + z3_eval ctxPtr (unModel m) (unAST a) aptr2 >>= peekAST aptr2 . toBool where peekAST :: Ptr (Ptr Z3_ast) -> Bool -> IO (Maybe (AST a)) peekAST _p False = return Nothing peekAST p True = Just . AST <$> peek p @@ -794,32 +919,33 @@ -- Reference: -- assertCnstr :: Context -> AST Bool -> IO () -assertCnstr ctx ast = - withForeignPtr (unContext ctx) $ \ctxPtr -> - z3_assert_cnstr ctxPtr (unAST ast) +assertCnstr ctx ast = withContext ctx $ \ctxPtr -> + z3_assert_cnstr ctxPtr (unAST ast) -- | Get model (logical context is consistent) -- -- Reference : -- -getModel :: Context -> IO (Result, Maybe Model) -getModel c = withForeignPtr (unContext c) $ \ctxPtr -> +getModel :: Context -> IO (Result Model) +getModel c = withContext c $ \ctxPtr -> alloca $ \mptr -> z3_check_and_get_model ctxPtr mptr >>= peekModel mptr . toResult where peekModel :: Ptr (Ptr Z3_model) - -> Result - -> IO (Result, Maybe Model) - peekModel p r | p == nullPtr = return (r, Nothing) - | otherwise = do z3m <- peek p - m <- mkModel c z3m - return (r, Just m) + -> Result () + -> IO (Result Model) + peekModel _ Unsat = return Unsat + peekModel _ Undef = return Undef + peekModel p (Sat ()) | p == nullPtr = error "Z3.Base.getModel: Panic! nullPtr!" + | otherwise = do z3m <- peek p + m <- mkModel c z3m + return $ Sat m --- | Check whether the given logical context is consistent or not. +-- | Check whether the given logical context is consistent or not. -- -- Reference: -- -check :: Context -> IO Result -check ctx = toResult <$> withForeignPtr (unContext ctx) z3_check +check :: Context -> IO (Result ()) +check ctx = toResult <$> withContext ctx z3_check -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities diff --git a/Z3/Base/C.hsc b/Z3/Base/C.hsc --- a/Z3/Base/C.hsc +++ b/Z3/Base/C.hsc @@ -42,6 +42,9 @@ -- | A kind of AST used to represent types. data Z3_sort +-- | A kind of AST used to represent function symbols. +data Z3_func_decl + -- | A kind of AST used to represent constant and function declarations. data Z3_app @@ -159,9 +162,29 @@ --------------------------------------------------------------------- -- * Constants and Applications --- TODO Constants and Applications: Z3_mk_func_decl --- TODO Constants and Applications: Z3_mk_app +-- | Declare a constant or function. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_func_decl" + z3_mk_func_decl :: Ptr Z3_context + -> Ptr Z3_symbol + -> CUInt + -> Ptr (Ptr Z3_sort) + -> Ptr Z3_sort + -> IO (Ptr Z3_func_decl) +-- | Create a constant or function application. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_app" + z3_mk_app :: Ptr Z3_context + -> Ptr Z3_func_decl + -> CUInt + -> Ptr (Ptr Z3_ast) + -> IO (Ptr Z3_ast) + -- | Declare and create a constant. -- -- Reference: @@ -395,8 +418,36 @@ foreign import ccall unsafe "Z3_mk_unsigned_int64" z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- TODO Quantifiers +--------------------------------------------------------------------- +-- * Quantifiers +-- | Create a pattern for quantifier instantiation. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_pattern" + z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) + +-- | Create a bound variable. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bound" + z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) + +-- | Create a forall formula. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_forall" + z3_mk_forall :: 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 From 'Z3_mk_exists' on. + --------------------------------------------------------------------- -- * Accessors @@ -414,20 +465,6 @@ -- foreign import ccall unsafe "Z3_get_numeral_string" z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string - --- | Return the numerator (as a numeral AST) of a numeral AST of sort Int. --- --- Reference: --- -foreign import ccall unsafe "Z3_get_numerator" - z3_get_numerator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) - --- | Return the denominator (as a numeral AST) of a numeral AST of sort Real. --- --- Reference: --- -foreign import ccall unsafe "Z3_get_denominator" - z3_get_denominator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- TODO Modifiers diff --git a/Z3/Exprs.hs b/Z3/Exprs.hs deleted file mode 100644 --- a/Z3/Exprs.hs +++ /dev/null @@ -1,211 +0,0 @@ -{-# OPTIONS_GHC -fno-warn-orphans #-} -{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} - -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE StandaloneDeriving #-} - --- | --- Module : Z3.Exprs --- Copyright : (c) Iago Abal, 2012 --- (c) David Castro, 2012 --- License : BSD3 --- Maintainer: Iago Abal , --- David Castro --- Stability : experimental - --- TODO: Pretty-printing of expressions - -module Z3.Exprs ( - - module Z3.Types - - -- * Abstract syntax - , Expr - - -- * Constructing expressions - , true - , false - , not_ - , and_, (&&*) - , or_, (||*) - , xor - , implies, (==>) - , iff, (<=>) - , (//), (%*), (%%) - , (==*), (/=*) - , (<=*), (<*) - , (>=*), (>*) - , ite - - ) where - - -import Z3.Exprs.Internal -import Z3.Types - -import Data.Typeable ( Typeable1(..), typeOf ) -import Unsafe.Coerce ( unsafeCoerce ) - - -deriving instance Show (Expr a) -deriving instance Typeable1 Expr - -instance Eq (Expr a) where - (Lit l1) == (Lit l2) = l1 == l2 - (Const a) == (Const b) = a == b - (Not e1) == (Not e2) = e1 == e2 - (BoolBin op1 p1 q1) == (BoolBin op2 p2 q2) - = op1 == op2 && p1 == p2 && q1 == q2 - (BoolMulti op1 ps) == (BoolMulti op2 qs) - | length ps == length qs = op1 == op2 && and (zipWith (==) ps qs) - (Neg e1) == (Neg e2) = e1 == e2 - (CRingArith op1 as) == (CRingArith op2 bs) - | length as == length bs = op1 == op2 && and (zipWith (==) as bs) - (IntArith op1 a1 b1) == (IntArith op2 a2 b2) - = op1 == op2 && a1 == a2 && b1 == b2 - (RealArith op1 a1 b1) == (RealArith op2 a2 b2) - = op1 == op2 && a1 == a2 && b1 == b2 - (CmpE op1 a1 b1) == (CmpE op2 a2 b2) - | op1 == op2 && typeOf a1 == typeOf a2 - = a1 == unsafeCoerce a2 && b1 == unsafeCoerce b2 - (CmpI op1 a1 b1) == (CmpI op2 a2 b2) - | op1 == op2 && typeOf a1 == typeOf a2 - = a1 == unsafeCoerce a2 && b1 == unsafeCoerce b2 - (Ite g1 a1 b1) == (Ite g2 a2 b2) = g1 == g2 && a1 == a2 && b1 == b2 - _e1 == _e2 = False - - --- * Constructing expressions - -instance IsNum a => Num (Expr a) where - (CRingArith Add as) + (CRingArith Add bs) = CRingArith Add (as ++ bs) - (CRingArith Add as) + b = CRingArith Add (b:as) - a + (CRingArith Add bs) = CRingArith Add (a:bs) - a + b = CRingArith Add [a,b] - (CRingArith Mul as) * (CRingArith Mul bs) = CRingArith Mul (as ++ bs) - (CRingArith Mul as) * b = CRingArith Mul (b:as) - a * (CRingArith Mul bs) = CRingArith Mul (a:bs) - a * b = CRingArith Mul [a,b] - (CRingArith Sub as) - b = CRingArith Sub (as ++ [b]) - a - b = CRingArith Sub [a,b] - negate = Neg - abs e = ite (e >=* 0) e (-e) - signum e = ite (e >* 0) 1 (ite (e ==* 0) 0 (-1)) - fromInteger = literal . fromInteger - -instance IsReal a => Fractional (Expr a) where - (/) = RealArith Div - fromRational = literal . fromRational - -infixl 7 //, %*, %% -infix 4 ==*, /=*, <*, <=*, >=*, >* -infixr 3 &&*, ||*, `xor` -infixr 2 `implies`, `iff`, ==>, <=> - --- | /literal/ constructor. --- -literal :: IsScalar a => a -> Expr a -literal = Lit - --- | Boolean literals. --- -true, false :: Expr Bool -true = Lit True -false = Lit False - --- | Boolean negation --- -not_ :: Expr Bool -> Expr Bool -not_ = Not - --- | Boolean binary /xor/. --- -xor :: Expr Bool -> Expr Bool -> Expr Bool -xor = BoolBin Xor --- | Boolean implication --- -implies :: Expr Bool -> Expr Bool -> Expr Bool -implies = BoolBin Implies --- | An alias for 'implies'. --- -(==>) :: Expr Bool -> Expr Bool -> Expr Bool -(==>) = implies --- | Boolean /if and only if/. --- -iff :: Expr Bool -> Expr Bool -> Expr Bool -iff = BoolBin Iff --- | An alias for 'iff'. --- -(<=>) :: Expr Bool -> Expr Bool -> Expr Bool -(<=>) = iff - --- | Boolean variadic /and/. --- -and_ :: [Expr Bool] -> Expr Bool -and_ = BoolMulti And --- | Boolean variadic /or/. --- -or_ :: [Expr Bool] -> Expr Bool -or_ = BoolMulti Or - --- | Boolean binary /and/. --- -(&&*) :: Expr Bool -> Expr Bool -> Expr Bool -(BoolMulti And ps) &&* (BoolMulti And qs) = and_ (ps ++ qs) -(BoolMulti And ps) &&* q = and_ (q:ps) -p &&* (BoolMulti And qs) = and_ (p:qs) -p &&* q = and_ [p,q] --- | Boolean binary /or/. --- -(||*) :: Expr Bool -> Expr Bool -> Expr Bool -(BoolMulti Or ps) ||* (BoolMulti Or qs) = or_ (ps ++ qs) -(BoolMulti Or ps) ||* q = or_ (q:ps) -p ||* (BoolMulti Or qs) = or_ (p:qs) -p ||* q = or_ [p,q] - --- | Integer division. --- -(//) :: IsInt a => Expr a -> Expr a -> Expr a -(//) = IntArith Quot --- | Integer modulo. --- -(%*) :: IsInt a => Expr a -> Expr a -> Expr a -(%*) = IntArith Mod --- | Integer remainder. --- -(%%) :: IsInt a => Expr a -> Expr a -> Expr a -(%%) = IntArith Rem - - --- | Equals. --- -(==*) :: IsScalar a => Expr a -> Expr a -> Expr Bool -(==*) = CmpE Eq --- | Not equals. --- -(/=*) :: IsScalar a => Expr a -> Expr a -> Expr Bool -(/=*) = CmpE Neq - - --- | Less or equals than. --- -(<=*) :: IsNum a => Expr a -> Expr a -> Expr Bool -(<=*) = CmpI Le --- | Less than. --- -(<*) :: IsNum a => Expr a -> Expr a -> Expr Bool -(<*) = CmpI Lt --- | Greater or equals than. --- -(>=*) :: IsNum a => Expr a -> Expr a -> Expr Bool -(>=*) = CmpI Ge --- | Greater than. --- -(>*) :: IsNum a => Expr a -> Expr a -> Expr Bool -(>*) = CmpI Gt - --- | /if-then-else/. --- -ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a -ite = Ite diff --git a/Z3/Exprs/Internal.hs b/Z3/Exprs/Internal.hs deleted file mode 100644 --- a/Z3/Exprs/Internal.hs +++ /dev/null @@ -1,109 +0,0 @@ - -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE StandaloneDeriving #-} - --- | --- Module : Z3.Exprs.Internal --- Copyright : (c) Iago Abal, 2012 --- (c) David Castro, 2012 --- License : BSD3 --- Maintainer: Iago Abal , --- David Castro --- Stability : experimental - -module Z3.Exprs.Internal where - - -import Z3.Types - -import Data.Typeable ( Typeable ) - - --- | Unique identifiers --- -type Uniq = Int - -{-# WARNING Lit - , Const - , Not - , BoolBin - , BoolMulti - , Neg - , CRingArith - , IntArith - , RealArith - , CmpE - , CmpI - , Ite - "You are using a constructor of type Expr, \ - \which you should NOT be using! \ - \In fact, you should not be importing this \ - \module at all! Import Z3.Exprs instead!" #-} - --- | Abstract syntax. --- -data Expr :: * -> * where - -- | Literals - Lit :: IsScalar a => a -> Expr a - -- | Constants - Const :: !Uniq -> Expr a - -- | Logical negation - Not :: Expr Bool -> Expr Bool - -- | Binary boolean expressions - BoolBin :: BoolBinOp -> Expr Bool -> Expr Bool -> Expr Bool - -- | Variadic boolean expressions - BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool - -- | Arithmetic negation - Neg :: IsNum a => Expr a -> Expr a - -- | Arithmetic expressions for commutative rings - CRingArith :: IsNum a => CRingOp -> [Expr a] -> Expr a - -- | Integer arithmetic - IntArith :: IsInt a => IntOp -> Expr a -> Expr a -> Expr a - -- | Real arithmetic - RealArith :: IsReal a => RealOp -> Expr a -> Expr a -> Expr a - -- | Comparison expressions - CmpE :: IsScalar a => CmpOpE -> Expr a -> Expr a -> Expr Bool - CmpI :: IsNum a => CmpOpI -> Expr a -> Expr a -> Expr Bool - -- | if-then-else expressions - Ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a - -{-# WARNING BoolBinOp - , BoolMultiOp - , CRingOp - , IntOp - , RealOp - , CmpOpE - , CmpOpI - "You should NOT be using this type or data constructor! \ - \In fact, you should not be importing this \ - \module at all! Import Z3.Exprs instead!" #-} - --- | Boolean binary operations. -data BoolBinOp = Xor | Implies | Iff - deriving (Eq,Show) - --- | Boolean variadic operations. -data BoolMultiOp = And | Or - deriving (Eq,Show) - --- | Commutative ring operations. -data CRingOp = Add | Mul | Sub - deriving (Eq,Show) - --- | Operations for sort /int/. -data IntOp = Quot | Mod | Rem - deriving (Eq,Show) - --- | Operations for sort /real/. -data RealOp = Div - deriving (Eq,Show) - --- | Equality testing. -data CmpOpE = Eq | Neq - deriving (Eq, Show, Typeable) - --- | Inequality comparisons. -data CmpOpI = Le | Lt | Ge | Gt - deriving (Eq, Show, Typeable) diff --git a/Z3/Lang.hs b/Z3/Lang.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang.hs @@ -0,0 +1,19 @@ + +-- | +-- Module : Z3.Lang +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental +-- + +module Z3.Lang ( + module Z3.Lang.Prelude + , module Z3.Lang.Nat + ) where + + +import Z3.Lang.Prelude +import Z3.Lang.Nat diff --git a/Z3/Lang/Exprs.hs b/Z3/Lang/Exprs.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/Exprs.hs @@ -0,0 +1,237 @@ +{-# OPTIONS_GHC -funbox-strict-fields #-} + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} + +-- | +-- Module : Z3.Lang.Exprs +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental +-- + +module Z3.Lang.Exprs ( + -- * Types + TypeZ3 + , Compilable(..) + , IsTy(..) + , IsFun + + -- ** Numeric types + , IsNum + , IsInt + , IsReal + + -- * Abstract syntax + , Uniq + , Layout + , Expr (..) + , Pattern (..) + , FunApp (..) + , BoolBinOp (..) + , BoolMultiOp (..) + , CRingOp (..) + , IntOp (..) + , RealOp (..) + , CmpOpE (..) + , CmpOpI (..) + + -- * Type checking + , typecheck + , TCM + , TCC + , ok + , withHypo + , newTCC + , evalTCM + ) where + +import {-# SOURCE #-} Z3.Lang.Monad ( Z3 ) +import qualified Z3.Base as Base + +import Control.Monad.RWS +import Data.Typeable ( Typeable ) + +---------------------------------------------------------------------- +-- Types + +-- | Maps a type to the underlying Z3 type. +-- +type family TypeZ3 a + +type instance TypeZ3 (Expr a) = TypeZ3 a +type instance TypeZ3 (FunApp a) = TypeZ3 a + +-- | Compilable /things/. +-- +class Base.Z3Type (TypeZ3 t) => Compilable t where + compile :: t -> Z3 (Base.AST (TypeZ3 t)) + +-- | Types for expressions. +-- +class (Eq a, Show a, Typeable a, Compilable (Expr a)) => IsTy a where + -- | Type invariant. + -- Introduced when creating a variable. + -- + typeInv :: Expr a -> Expr Bool + + -- | Typecheck an expression. + -- + tc :: Expr a -> TCM () + + -- | Convert from underlying Z3 type to type. + -- + fromZ3Type :: TypeZ3 a -> a + + -- | Convert from a type to its underlying Z3 type. + -- + toZ3Type :: a -> TypeZ3 a + +-- | Function types. +-- +class Base.Z3Fun (TypeZ3 a) => IsFun a where + +------------------------------------------------------------ +-- Numeric types +-- +-- Future Work: We would like to instance 'IsInt' with 'Int32' to provide +-- support for reasoning about 32-bit integer arithmetic with overflow. +-- It would be also interesting (but perhaps more tricky) to support +-- floating point arithmetic by creating an instance of 'IsReal' for +-- 'Double'. +-- + +-- | Numeric types. +-- +class (IsTy a, Num a, Base.Z3Num (TypeZ3 a)) => IsNum a where + +-- | Typeclass for Haskell Z3 numbers of /int/ sort in Z3. +-- +class (IsNum a, Integral a, TypeZ3 a ~ Integer) => IsInt a where + +-- | Typeclass for Haskell Z3 numbers of /real/ sort in Z3. +-- +class (IsNum a, Fractional a, Real a, TypeZ3 a ~ Rational) => IsReal a where + +------------------------------------------------------------ +-- Abstract syntax + +-- | Unique identifiers. +-- +type Uniq = Int + +-- | Quantifier layout level. +-- +type Layout = Int + +-- | Abstract syntax. +-- +data Expr :: * -> * where + -- | Literals + Lit :: IsTy a => a -> Expr a + -- | Constants + Const :: !Uniq -> Base.AST (TypeZ3 a) -> Expr a + -- | Tag, for converting from HOAS to de-Bruijn + Tag :: !Layout -> Expr a + -- | Logical negation + Not :: Expr Bool -> Expr Bool + -- | Binary boolean expressions + 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 + -- | Arithmetic negation + Neg :: IsNum a => Expr a -> Expr a + -- | Arithmetic expressions for commutative rings + CRingArith :: IsNum a => CRingOp -> [Expr a] -> Expr a + -- | Integer arithmetic + IntArith :: IsInt a => IntOp -> Expr a -> Expr a -> Expr a + -- | Real arithmetic + RealArith :: IsReal a => RealOp -> Expr a -> Expr a -> Expr a + -- | Equality testing. + CmpE :: IsTy a => CmpOpE -> Expr a -> Expr a -> Expr Bool + -- | Ordering comparisons. + CmpI :: IsNum a => CmpOpI -> Expr a -> Expr a -> Expr Bool + -- | if-then-else expressions + Ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a + -- | Application + App :: IsTy a => FunApp a -> Expr a + +-- | Quantifier pattern. +-- +data Pattern where + Pat :: IsTy a => Expr a -> Pattern + +-- | Z3 function +-- +data FunApp :: * -> * where + -- | Function declaration + FuncDecl :: IsFun a => Base.FuncDecl (TypeZ3 a) -> FunApp a + -- | Partial application + PApp :: IsTy a => FunApp (a -> b) -> Expr a -> FunApp b + +-- | Boolean binary operations. +data BoolBinOp = Xor | Implies | Iff + deriving (Eq,Show) + +-- | Boolean variadic operations. +data BoolMultiOp = And | Or + deriving (Eq,Show) + +-- | Commutative ring operations. +data CRingOp = Add | Mul | Sub + deriving (Eq,Show) + +-- | Operations for sort /int/. +data IntOp = Quot | Mod | Rem + deriving (Eq,Show) + +-- | Operations for sort /real/. +data RealOp = Div + deriving (Eq,Show) + +-- | Equality testing. +data CmpOpE = Eq | Neq + deriving (Eq, Show, Typeable) + +-- | Ordering comparisons. +data CmpOpI = Le | Lt | Ge | Gt + deriving (Eq, Show, Typeable) + +---------------------------------------------------------------------- +-- Typecheck monad + +newtype TCM a = TCM { unTCM :: RWS Context [TCC] () a } + deriving Monad + +type TCC = Expr Bool + +type Context = [Expr Bool] + +ok :: TCM () +ok = return () + +withHypo :: Expr Bool -> TCM a -> TCM a +withHypo h = TCM . local (h:) . unTCM + +newTCC :: [Expr Bool] -> TCM () +newTCC tccs = TCM $ do + hs <- ask + tell $ map (mkTCC hs) tccs + where mkTCC [] = id + mkTCC hs = BoolBin Implies (BoolMulti And hs) + +evalTCM :: TCM a -> (a,[TCC]) +evalTCM m = evalRWS (unTCM m) [] () + +typecheck :: IsTy a => Expr a -> [Expr Bool] +typecheck e = snd $ evalTCM (tc e) diff --git a/Z3/Lang/Lg2.hs b/Z3/Lang/Lg2.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/Lg2.hs @@ -0,0 +1,40 @@ + +{-# LANGUAGE ScopedTypeVariables #-} + +-- | +-- Module : Z3.Lang.Lg2 +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro + +module Z3.Lang.Lg2 + ( declareLg2 ) + where + +import Z3.Lang.Prelude + +-- | Ceiling logarithm base two. +-- Axiomatization of the /lg2/ function. +-- Most likely Z3 is going to diverge if you use /lg2/ to specify a satisfiable +-- problem since it cannot construct a recursive definition for /lg2/, but it +-- should work fine for unsatisfiable instances. +declareLg2 :: IsInt a => Z3 (Expr a -> Expr a) +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) + -- base cases + assert $ lg2 1 ==* 0 + assert $ lg2 2 ==* 1 + -- recursive definition + assert $ forallP (\x -> x >* 2 &&* (2 `divides` x) ==> lg2 x ==* 1 + lg2 (x//2)) + (\x -> Pat $ lg2 x) + assert $ forallP (\x -> x >* 2 &&* not_ (2 `divides` x) ==> lg2 x ==* lg2 (x+1)) + (\x -> Pat $ lg2 x) + -- and that's it! + return lg2 diff --git a/Z3/Lang/Monad.hs b/Z3/Lang/Monad.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/Monad.hs @@ -0,0 +1,314 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | +-- Module : Z3.Lang.Monad +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental + +module Z3.Lang.Monad ( + -- * Z3 Monad + Z3 + , Z3State(..) + , evalZ3 + , Args(..) + , stdArgs + , evalZ3With + , fresh + , deBruijnIx + , newQLayout + + -- ** Lifted Z3.Base functions + , liftZ3 + , assertCnstr + , check + , eval + , getBool + , getInt + , getReal + , getModel + , getValue + , mkSort + , mkStringSymbol + , mkLiteral + , mkNot + , mkBoolBin + , mkBoolMulti + , mkPattern + , mkBound + , mkForall + , mkEq + , mkCmp + , mkFuncDecl + , mkApp1 + , mkApp2 + , mkApp3 + , mkApp4 + , mkApp5 + , mkConst + , mkUnaryMinus + , mkCRingArith + , mkIntArith + , mkRealArith + , mkIte + + -- * Satisfiability result + , Base.Result(..) + + ) where + +import Z3.Lang.Exprs + +import qualified Z3.Base as Base + +import Control.Applicative ( Applicative ) +import Control.Monad.State + +--------------------------------------------------------------------- +-- The Z3 Monad + +-- | Z3 monad. +-- +newtype Z3 a = Z3 (StateT Z3State IO a) + deriving (Functor, Applicative, Monad) + +instance MonadState Z3State Z3 where + get = Z3 $ StateT $ \s -> return (s,s) + put st = Z3 $ StateT $ \_ -> return ((), st) + +-- | Internal state of Z3 monad. +-- +data Z3State + = Z3State { uniqVal :: !Uniq + , context :: Base.Context + , qLayout :: !Layout + } + +-- | Eval a Z3 script. +-- +evalZ3 :: Z3 a -> IO a +evalZ3 = evalZ3With stdArgs + +-- | Eval a Z3 script. +-- +evalZ3With :: Args -> Z3 a -> IO a +evalZ3With args (Z3 s) = do + cfg <- Base.mkConfig + Base.set_MODEL cfg True + Base.set_MODEL_PARTIAL cfg False + Base.setParamValue cfg "WARNING" "false" + iniConfig cfg args + ctx <- Base.mkContext cfg + evalStateT s Z3State { uniqVal = 0 + , context = ctx + , qLayout = 0 + } + +-- | Fresh symbol name. +-- +fresh :: Z3 (Uniq, String) +fresh = do + st <- get + let i = uniqVal st + put st { uniqVal = i + 1 } + return (uniqVal st, 'v':show i) + +------------------------------------------------- +-- Arguments + +data Args + = Args { + softTimeout :: Maybe Int + -- ^ soft timeout (in milliseconds) + } + +stdArgs :: Args +stdArgs + = Args { + softTimeout = Nothing + } + +iniConfig :: Base.Config -> Args -> IO () +iniConfig cfg args = do + Base.setParamValue cfg "SOFT_TIMEOUT" soft_timeout_val + where soft_timeout_val = show $ maybe 0 id $ softTimeout args + +------------------------------------------------- +-- HOAX-deBruijn conversion + +getQLayout :: Z3 Layout +getQLayout = gets qLayout + +deBruijnIx :: Layout -> Z3 Int +deBruijnIx k = do lyt <- getQLayout; return $ lyt-k-1 + +newQLayout :: (Expr a -> Z3 b) -> Z3 b +newQLayout f = do + lyt <- getQLayout + incQLayout + x <- f (Tag lyt) + decQLayout + return x + where incQLayout = modify (\st@Z3State{qLayout} -> st{ qLayout = qLayout+1 }) + decQLayout = modify (\st@Z3State{qLayout} -> st{ qLayout = qLayout-1 }) + +--------------------------------------------------------------------- +-- Lifted Base functions + +liftZ3 :: IO a -> Z3 a +liftZ3 = Z3 . lift + +liftZ3Op :: (Base.Context -> IO b) -> Z3 b +liftZ3Op f = liftZ3 . f =<< gets context + +liftZ3Op2 :: (Base.Context -> a -> IO b) -> a -> Z3 b +liftZ3Op2 f a = gets context >>= \ctx -> liftZ3 (f ctx a) + +liftZ3Op3 :: (Base.Context -> a -> b -> IO c) -> a -> b -> Z3 c +liftZ3Op3 f a b = gets context >>= \ctx -> liftZ3 (f ctx a b) + +liftZ3Op4 :: (Base.Context -> a -> b -> c -> IO d) -> a -> b -> c -> Z3 d +liftZ3Op4 f a b c = gets context >>= \ctx -> liftZ3 (f ctx a b c) + +liftZ3Op5 :: (Base.Context -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d -> Z3 e +liftZ3Op5 f a b c d = gets context >>= \ctx -> liftZ3 (f ctx a b c d) + +assertCnstr :: Base.AST Bool -> Z3 () +assertCnstr = liftZ3Op2 Base.assertCnstr + +-- | Check satisfiability. +check :: Z3 (Base.Result ()) +check = liftZ3Op Base.check + +eval :: Base.Model -> Base.AST a -> Z3 (Maybe (Base.AST a)) +eval = liftZ3Op3 Base.eval + +getBool :: Base.AST Bool -> Z3 (Maybe Bool) +getBool = liftZ3Op2 Base.getBool + +getInt :: Base.AST Integer -> Z3 Integer +getInt = liftZ3Op2 Base.getInt + +getReal :: Base.AST Rational -> Z3 Rational +getReal = liftZ3Op2 Base.getReal + +getModel :: Z3 (Base.Result Base.Model) +getModel = liftZ3Op Base.getModel + +getValue :: Base.Z3Type a => Base.AST a -> Z3 a +getValue = liftZ3Op2 Base.getValue + +mkSort :: Base.Z3Type a => Z3 (Base.Sort a) +mkSort = liftZ3Op Base.mkSort + +mkStringSymbol :: String -> Z3 Base.Symbol +mkStringSymbol = liftZ3Op2 Base.mkStringSymbol + +mkLiteral :: forall a. Base.Z3Type a => a -> Z3 (Base.AST a) +mkLiteral = liftZ3Op2 Base.mkValue + +mkNot :: Base.AST Bool -> Z3 (Base.AST Bool) +mkNot = liftZ3Op2 Base.mkNot + +mkBoolBin :: BoolBinOp -> Base.AST Bool -> Base.AST Bool -> Z3 (Base.AST Bool) +mkBoolBin Xor = liftZ3Op3 Base.mkXor +mkBoolBin Implies = liftZ3Op3 Base.mkImplies +mkBoolBin Iff = liftZ3Op3 Base.mkIff + +mkBoolMulti :: BoolMultiOp -> [Base.AST Bool] -> Z3 (Base.AST Bool) +mkBoolMulti And = liftZ3Op2 Base.mkAnd +mkBoolMulti Or = liftZ3Op2 Base.mkOr + +mkPattern :: Base.Z3Type a => [Base.AST a] -> Z3 Base.Pattern +mkPattern = liftZ3Op2 Base.mkPattern + +mkBound :: Base.Z3Type a => Int -> Base.Sort a -> Z3 (Base.AST a) +mkBound = liftZ3Op3 Base.mkBound + +mkForall :: Base.Z3Type a => [Base.Pattern] -> Base.Symbol -> Base.Sort a -> Base.AST Bool -> Z3 (Base.AST Bool) +mkForall = liftZ3Op5 Base.mkForall + +mkEq :: Base.Z3Type a => CmpOpE + -> Base.AST a -> Base.AST a + -> Z3 (Base.AST Bool) +mkEq Eq = liftZ3Op3 Base.mkEq +mkEq Neq = liftZ3Op3 mkNeq + where mkNeq ctx b1 = Base.mkNot ctx <=< Base.mkEq ctx b1 + +mkCmp :: Base.Z3Num a => CmpOpI + -> Base.AST a -> Base.AST a + -> Z3 (Base.AST Bool) +mkCmp Le = liftZ3Op3 Base.mkLe +mkCmp Lt = liftZ3Op3 Base.mkLt +mkCmp Ge = liftZ3Op3 Base.mkGe +mkCmp Gt = liftZ3Op3 Base.mkGt + +mkFuncDecl :: Base.Z3Fun a => Base.Symbol + -> Z3 (Base.FuncDecl a) +mkFuncDecl = liftZ3Op2 Base.mkFuncDecl + +mkApp1 :: (Base.Z3Type a, Base.Z3Type b) + => Base.FuncDecl (a -> b) + -> Base.AST a + -> Z3 (Base.AST b) +mkApp1 = liftZ3Op3 Base.mkApp1 + +mkApp2 :: (Base.Z3Type a, Base.Z3Type b, Base.Z3Type c) + => Base.FuncDecl (a -> b -> c) + -> Base.AST a -> Base.AST b + -> Z3 (Base.AST c) +mkApp2 = liftZ3Op4 Base.mkApp2 + +mkApp3 :: (Base.Z3Type a, Base.Z3Type b, Base.Z3Type c , Base.Z3Type d) + => Base.FuncDecl (a -> b -> c -> d) + -> Base.AST a -> Base.AST b -> Base.AST c + -> Z3 (Base.AST d) +mkApp3 fd a b c + = gets context >>= \ctx -> liftZ3 $ Base.mkApp3 ctx fd a b c + +mkApp4 :: (Base.Z3Type a, Base.Z3Type b, Base.Z3Type c , Base.Z3Type d, Base.Z3Type e) + => Base.FuncDecl (a -> b -> c -> d -> e) + -> Base.AST a -> Base.AST b -> Base.AST c -> Base.AST d + -> Z3 (Base.AST e) +mkApp4 fd a b c d + = gets context >>= \ctx -> liftZ3 $ Base.mkApp4 ctx fd a b c d + +mkApp5 :: (Base.Z3Type a, Base.Z3Type b, Base.Z3Type c , Base.Z3Type d, Base.Z3Type e, Base.Z3Type f) + => Base.FuncDecl (a -> b -> c -> d -> e -> f) + -> Base.AST a -> Base.AST b -> Base.AST c -> Base.AST d -> Base.AST e + -> Z3 (Base.AST f) +mkApp5 fd a b c d e + = gets context >>= \ctx -> liftZ3 $ Base.mkApp5 ctx fd a b c d e + +mkConst :: Base.Z3Type a => Base.Symbol -> Base.Sort a -> Z3 (Base.AST a) +mkConst = liftZ3Op3 Base.mkConst + +mkUnaryMinus :: Base.Z3Num a => Base.AST a -> Z3 (Base.AST a) +mkUnaryMinus = liftZ3Op2 Base.mkUnaryMinus + +mkCRingArith :: Base.Z3Num a => CRingOp -> [Base.AST a] -> Z3 (Base.AST a) +mkCRingArith Add = liftZ3Op2 Base.mkAdd +mkCRingArith Mul = liftZ3Op2 Base.mkMul +mkCRingArith Sub = liftZ3Op2 Base.mkSub + +mkIntArith :: IntOp + -> Base.AST Integer -> Base.AST Integer + -> Z3 (Base.AST Integer) +mkIntArith Quot = liftZ3Op3 Base.mkDiv +mkIntArith Mod = liftZ3Op3 Base.mkMod +mkIntArith Rem = liftZ3Op3 Base.mkRem + +mkRealArith :: RealOp + -> Base.AST Rational -> Base.AST Rational + -> Z3 (Base.AST Rational) +mkRealArith Div = liftZ3Op3 Base.mkDiv + +mkIte :: Base.AST Bool -> Base.AST a -> Base.AST a -> Z3 (Base.AST a) +mkIte = liftZ3Op4 Base.mkIte diff --git a/Z3/Lang/Monad.hs-boot b/Z3/Lang/Monad.hs-boot new file mode 100644 --- /dev/null +++ b/Z3/Lang/Monad.hs-boot @@ -0,0 +1,10 @@ + +module Z3.Lang.Monad + ( Z3 ) + where + +import Control.Monad.State ( StateT ) + +data Z3State + +newtype Z3 a = Z3 (StateT Z3State IO a) diff --git a/Z3/Lang/Nat.hs b/Z3/Lang/Nat.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/Nat.hs @@ -0,0 +1,113 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} + +-- | +-- Module : Z3.Lang.Nat +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro + +module Z3.Lang.Nat + ( Nat ) + where + +import Z3.Base ( AST ) +import Z3.Lang.Exprs +import Z3.Lang.Monad +import Z3.Lang.Prelude + +import Data.Typeable + +newtype Nat = Nat { unNat :: Integer } + deriving (Eq,Ord,Enum,Real,Typeable) + +instance Show Nat where + show = show . unNat + +instance Num Nat where + Nat n + Nat m = Nat $ n + m + Nat n - Nat m + | n >= m = Nat $ n-m + | otherwise = error "Cannot subtract" + Nat n * Nat m = Nat $ n * m + abs = id + signum = Nat . signum . unNat + negate 0 = 0 + negate _ = error "Cannot negate a natural number" + fromInteger n | n >= 0 = Nat n + | otherwise = error "Not a natural number" + +instance Integral Nat where + quotRem (Nat n) (Nat m) = (Nat q,Nat r) + where (q,r) = quotRem n m + toInteger = unNat + +type instance TypeZ3 Nat = Integer + +instance Compilable (Expr Nat) where + compile = compileNat + +instance IsTy Nat where + typeInv e = e >=* 0 + tc = tcNat + fromZ3Type = Nat + toZ3Type = unNat + +instance IsNum Nat where +instance IsInt Nat where + +tcNat :: Expr Nat -> TCM () +tcNat (Lit _) = ok +tcNat (Const _ _) = ok +tcNat (Tag _) = ok +tcNat (Neg e) = do + newTCC [e ==* 0] + tcNat e +tcNat (CRingArith Sub es) = do + newTCC $ zipWith (>=*) (scanl1 (-) es) (tail es) + mapM_ tcNat es +tcNat (CRingArith _op es) = mapM_ tcNat es +tcNat (IntArith _op e1 e2) = do + newTCC [e2 /=* 0] + tcNat e1 + tcNat e2 +tcNat (Ite eb e1 e2) = do + tc eb + withHypo eb $ tcNat e1 + withHypo (Not eb) $ tcNat e2 +tcNat (App _) = ok +tcNat _ = error "Z3.Lang.Nat.tcNat: Panic!\ + \ Impossible constructor in pattern matching!" + +compileNat :: Expr Nat -> Z3 (AST Integer) +compileNat (Lit a) + = mkLiteral (toZ3Type a) +compileNat (Const _ u) + = return u +compileNat (Tag lyt) + = do ix <- deBruijnIx lyt + srt <- mkSort + mkBound ix srt +compileNat (Neg e) + = mkUnaryMinus =<< compileNat e +compileNat (CRingArith op es) + = mkCRingArith op =<< mapM compileNat es +compileNat (IntArith op e1 e2) + = do e1' <- compileNat e1 + e2' <- compileNat e2 + mkIntArith op e1' e2' +compileNat (Ite eb e1 e2) + = do eb' <- compile eb + e1' <- compileNat e1 + e2' <- compileNat e2 + mkIte eb' e1' e2' +compileNat (App e) + = compile e +compileNat _ + = error "Z3.Lang.Nat.compileNat: Panic!\ + \ Impossible constructor in pattern matching!" + diff --git a/Z3/Lang/Pow2.hs b/Z3/Lang/Pow2.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/Pow2.hs @@ -0,0 +1,42 @@ + +{-# LANGUAGE ScopedTypeVariables #-} + +-- | +-- Module : Z3.Lang.Pow +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro + +-- TODO generalize for x^y +module Z3.Lang.Pow2 + ( declarePow2 ) + where + +import Z3.Lang.Prelude + +-- | Raise to the power of 2. +-- Axiomatization of the /2^n/ function. +-- Most likely Z3 is going to diverge if you use /2^n/ to specify a satisfiable +-- problem, since it cannot construct a recursive definition for /2^n/, but it +-- should work fine for unsatisfiable instances. +declarePow2 :: IsInt a => Z3 (Expr a -> Expr a) +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) + -- 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) + -- and that's it! + return pow2 + diff --git a/Z3/Lang/Prelude.hs b/Z3/Lang/Prelude.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/Prelude.hs @@ -0,0 +1,630 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- Module : Z3.Lang.Prelude +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental +-- + +-- TODO: Pretty-printing of expressions + +module Z3.Lang.Prelude ( + + -- * Z3 script + Z3 + , Base.Result(..) + , evalZ3 + , Args(..) + , stdArgs + , evalZ3With + + -- ** Commands + , var + , fun1, fun2, fun3, fun4, fun5 + , assert + , let_ + , check + , checkModel + + -- * Expressions + , Expr + , Pattern(..) + , IsTy + , IsNum + , IsInt + , IsReal + , literal + , true + , false + , not_ + , and_, (&&*) + , or_, (||*) + , xor + , implies, (==>) + , iff, (<=>) + , forall, forallP + , (//), (%*), (%%) + , divides + , (==*), (/=*) + , (<=*), (<*) + , (>=*), (>*) + , min_, max_ + , ite + + ) where + +import Z3.Base ( AST ) +import qualified Z3.Base as Base +import Z3.Lang.Exprs +import Z3.Lang.Monad + +import Control.Applicative ( (<$>), (<*>), pure ) +import Control.Monad ( liftM, liftM2, liftM3, liftM4, liftM5, join ) +import Data.Maybe ( maybeToList ) +import qualified Data.Traversable as T +#if __GLASGOW_HASKELL__ < 704 +import Data.Typeable ( Typeable1(..), typeOf ) +import Unsafe.Coerce ( unsafeCoerce ) +#else +import Data.Typeable ( Typeable1(..) ) +#endif + +--------------------------------------------------------------------- +-- Utils + +-- | Compile while introducing TCCs into the script. +-- +compileWithTCC :: IsTy a => Expr a -> Z3 (Base.AST (TypeZ3 a)) +compileWithTCC e = do + assertCnstr =<< compile (and_ $ typecheck e) + compile e + +--------------------------------------------------------------------- +-- Commands + +-- | Declare skolem variables. +-- +var :: forall a. IsTy a => Z3 (Expr a) +var = do + (u, str) <- fresh + smb <- mkStringSymbol str + (srt :: Base.Sort (TypeZ3 a)) <- mkSort + cnst <- mkConst smb srt + let e = Const u cnst + assert $ typeInv e + return e + +-- | Declare uninterpreted function of arity 1. +-- +fun1 :: (IsTy a, IsTy b) => Z3 (Expr a -> Expr b) +fun1 = do + (fd :: FunApp (a -> b)) <- funDecl + let f e = App $ PApp fd e + assert $ forall $ \a -> typeInv (f a) + return f + +-- | Declare uninterpreted function of arity 2. +-- +fun2 :: (IsTy a, IsTy b, IsTy c) => Z3 (Expr a -> Expr b -> Expr c) +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) + return f + + +-- | Declare uninterpreted function of arity 3. +-- +fun3 :: (IsTy a, IsTy b, IsTy c, IsTy d) + => Z3 (Expr a -> Expr b -> Expr c -> Expr d) +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) + return f + +-- | Declare uninterpreted function of arity 4. +-- +fun4 :: (IsTy a, IsTy b, IsTy c, IsTy d, IsTy e) + => Z3 (Expr a -> Expr b -> Expr c -> Expr d -> Expr e) +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) + return f + +-- | Declare uninterpreted function of arity 5. +-- +fun5 :: (IsTy a, IsTy b, IsTy c, IsTy d, IsTy e, IsTy f) + => Z3 (Expr a -> Expr b -> Expr c -> Expr d -> Expr e -> Expr f) +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) + return f + +-- | Declare uninterpreted function +-- +funDecl :: forall a. IsFun a => Z3 (FunApp a) +funDecl = do + (_u, str) <- fresh + smb <- mkStringSymbol str + (fd :: Base.FuncDecl (TypeZ3 a)) <- mkFuncDecl smb + return (FuncDecl fd) + +-- | Make assertion in current context. +-- +assert :: Expr Bool -> Z3 () +assert (Lit True) = return () +assert e = compileWithTCC e >>= assertCnstr + +-- | Introduce an auxiliary declaration to name a given expression. +-- +-- If you really want sharing use this instead of Haskell's /let/. +-- +let_ :: IsTy a => Expr a -> Z3 (Expr a) +let_ e@(Lit _) = return e +let_ e@(Const _ _) = return e +let_ e = do + aux <- var + assert (aux ==* e) + return aux + +-- | Check satisfiability and evaluate the given expression if a model exists. +-- +checkModel :: forall a. IsTy a => Expr a -> Z3 (Result a) +checkModel e = do + a <- compileWithTCC e + m <- getModel + fixResult a m + where fixResult :: Base.AST (TypeZ3 a) -> Result Base.Model -> Z3 (Result a) + fixResult _ (Base.Undef) = return Base.Undef + fixResult _ (Base.Unsat) = return Base.Unsat + fixResult a (Base.Sat m) = peek =<< eval m a + + peek :: Maybe (Base.AST (TypeZ3 a)) -> Z3 (Base.Result a) + peek (Just a) = Base.Sat . fromZ3Type <$> getValue a + peek Nothing = error "Z3.Lang.Monad.eval: quantified expression or partial model!" + +---------------------------------------------------------------------- +-- Expressions + +deriving instance Typeable1 Expr + +-- In GHC 7.4 Eq and Show are no longer superclasses of Num +#if __GLASGOW_HASKELL__ < 704 +deriving instance Show (FunApp a) +deriving instance Show (Expr a) + +instance Eq (Expr a) where + _e1 == _e2 = error "Z3.Lang.Expr: equality not supported" +#endif + +instance IsNum a => Num (Expr a) where + (CRingArith Add as) + (CRingArith Add bs) = CRingArith Add (as ++ bs) + (CRingArith Add as) + b = CRingArith Add (b:as) + a + (CRingArith Add bs) = CRingArith Add (a:bs) + a + b = CRingArith Add [a,b] + (CRingArith Mul as) * (CRingArith Mul bs) = CRingArith Mul (as ++ bs) + (CRingArith Mul as) * b = CRingArith Mul (b:as) + a * (CRingArith Mul bs) = CRingArith Mul (a:bs) + a * b = CRingArith Mul [a,b] + (CRingArith Sub as) - b = CRingArith Sub (as ++ [b]) + a - b = CRingArith Sub [a,b] + negate = Neg + abs e = ite (e >=* 0) e (-e) + signum e = ite (e >* 0) 1 (ite (e ==* 0) 0 (-1)) + fromInteger = literal . fromInteger + +instance IsReal a => Fractional (Expr a) where + (/) = RealArith Div + fromRational = literal . fromRational + +infixl 7 //, %*, %% +infix 4 ==*, /=*, <*, <=*, >=*, >* +infixr 3 &&*, ||*, `xor` +infixr 2 `implies`, `iff`, ==>, <=> + +-- | /literal/ constructor. +-- +literal :: IsTy a => a -> Expr a +literal = Lit + +-- | Boolean literals. +-- +true, false :: Expr Bool +true = Lit True +false = Lit False + +-- | Boolean negation +-- +not_ :: Expr Bool -> Expr Bool +not_ = Not + +-- | Boolean binary /xor/. +-- +xor :: Expr Bool -> Expr Bool -> Expr Bool +xor = BoolBin Xor +-- | Boolean implication +-- +implies :: Expr Bool -> Expr Bool -> Expr Bool +p `implies` (BoolBin Implies q r) + = (p &&* q) `implies` r +p `implies` q = BoolBin Implies p q +-- | An alias for 'implies'. +-- +(==>) :: Expr Bool -> Expr Bool -> Expr Bool +(==>) = implies +-- | Boolean /if and only if/. +-- +iff :: Expr Bool -> Expr Bool -> Expr Bool +iff = BoolBin Iff +-- | An alias for 'iff'. +-- +(<=>) :: Expr Bool -> Expr Bool -> Expr Bool +(<=>) = iff + +-- | Boolean variadic /and/. +-- +and_ :: [Expr Bool] -> Expr Bool +and_ [] = true +and_ bs = BoolMulti And bs +-- | Boolean variadic /or/. +-- +or_ :: [Expr Bool] -> Expr Bool +or_ [] = false +or_ bs = BoolMulti Or bs + +-- | Boolean binary /and/. +-- +(&&*) :: Expr Bool -> Expr Bool -> Expr Bool +(BoolMulti And ps) &&* (BoolMulti And qs) = and_ (ps ++ qs) +(BoolMulti And ps) &&* q = and_ (q:ps) +p &&* (BoolMulti And qs) = and_ (p:qs) +p &&* q = and_ [p,q] +-- | Boolean binary /or/. +-- +(||*) :: Expr Bool -> Expr Bool -> Expr Bool +(BoolMulti Or ps) ||* (BoolMulti Or qs) = or_ (ps ++ qs) +(BoolMulti Or ps) ||* q = or_ (q:ps) +p ||* (BoolMulti Or qs) = or_ (p:qs) +p ||* q = or_ [p,q] + +-- | Forall formula. +-- +forall :: forall a. IsTy a => (Expr a -> Expr Bool) -> Expr Bool +forall f = ForAll f Nothing + +forallP :: IsTy a => (Expr a -> Expr Bool) -- ^ body + -> (Expr a -> Pattern) -- ^ pattern + -> Expr Bool +forallP f = ForAll f . Just + +-- | Integer division. +-- +(//) :: IsInt a => Expr a -> Expr a -> Expr a +(//) = IntArith Quot +-- | Integer modulo. +-- +(%*) :: IsInt a => Expr a -> Expr a -> Expr a +(%*) = IntArith Mod +-- | Integer remainder. +-- +(%%) :: IsInt a => Expr a -> Expr a -> Expr a +(%%) = IntArith Rem + +-- | @k `divides` n == n %* k ==* 0@ +-- +divides :: IsInt a => Expr a -> Expr a -> Expr Bool +k `divides` n = n %* k ==* 0 +{-# INLINE divides #-} + +-- | Equals. +-- +(==*) :: IsTy a => Expr a -> Expr a -> Expr Bool +(==*) = CmpE Eq +-- | Not equals. +-- +(/=*) :: IsTy a => Expr a -> Expr a -> Expr Bool +(/=*) = CmpE Neq + +-- | Less or equals than. +-- +(<=*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(<=*) = CmpI Le + +-- | Less than. +-- +(<*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(<*) = CmpI Lt + +-- | Greater or equals than. +-- +(>=*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(>=*) = CmpI Ge + +-- | Greater than. +-- +(>*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(>*) = CmpI Gt + +-- | Minimum. +-- +min_ :: IsNum a => Expr a -> Expr a -> Expr a +min_ x y = ite (x <=* y) x y + +-- | Maximum. +-- +max_ :: IsNum a => Expr a -> Expr a -> Expr a +max_ x y = ite (x >=* y) x y + +-- | /if-then-else/. +-- +ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a +ite = Ite + +---------------------------------------------------------------------- +-- Booleans + +type instance TypeZ3 Bool = Bool + +instance Compilable (Expr Bool) where + compile = compileBool + +instance IsTy Bool where + typeInv = const true + tc = tcBool + fromZ3Type = id + toZ3Type = id + +tcBool :: Expr Bool -> TCM () +tcBool (Lit _) = ok +tcBool (Const _ _) = ok +tcBool (Tag _) = ok +tcBool (Not b) = tcBool b +tcBool (BoolBin Implies e1 e2) = do + tcBool e1 + withHypo e1 $ tcBool e2 +tcBool (BoolBin _op e1 e2) = do + tcBool e1 + tcBool e2 +tcBool (BoolMulti _op es) = mapM_ tcBool es +tcBool (ForAll _f _p) = ok +tcBool (CmpE _op e1 e2) = do + tc e1 + tc e2 +tcBool (CmpI _op e1 e2) = do + tc e1 + tc e2 +tcBool (Ite eb e1 e2) = do + tcBool eb + withHypo eb $ tcBool e1 + withHypo (Not eb) $ tcBool e2 +tcBool (App _app) = ok +tcBool _ + = error "Z3.Lang.Prelude.tcBool: Panic! Impossible constructor in pattern matching!" + +compileBool :: Expr Bool -> Z3 (AST Bool) +compileBool (Lit a) + = mkLiteral a +compileBool (Const _ u) + = return u +compileBool (Tag lyt) + = do ix <- deBruijnIx lyt + srt <- mkSort + mkBound ix srt +compileBool (Not b) + = do b' <- compileBool b + mkNot b' +compileBool (BoolBin op e1 e2) + = do e1' <- compileBool e1 + e2' <- compileBool e2 + mkBoolBin op e1' e2' +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))) + = do (_,n) <- fresh + sx <- mkStringSymbol n + srt :: Base.Sort (TypeZ3 a) <- mkSort + (body,mb_pat) <- newQLayout $ \x -> liftM2 (,) + (compileBool $ mkBody 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 + mkPat (Pat e) = do ast <- compile e; mkPattern [ast] +compileBool (CmpE op e1 e2) + = do e1' <- compile e1 + e2' <- compile e2 + mkEq op e1' e2' +compileBool (CmpI op e1 e2) + = do e1' <- compile e1 + e2' <- compile e2 + mkCmp op e1' e2' +compileBool (Ite b e1 e2) + = do b' <- compileBool b + e1' <- compileBool e1 + e2' <- compileBool e2 + mkIte b' e1' e2' +compileBool (App e) + = compile e +compileBool _ + = error "Z3.Lang.Prelude.compileBool: Panic! Impossible constructor in pattern matching!" + +---------------------------------------------------------------------- +-- Integers + +type instance TypeZ3 Integer = Integer + +instance Compilable (Expr Integer) where + compile = compileInteger + +instance IsTy Integer where + typeInv = const true + tc = tcInteger + fromZ3Type = id + toZ3Type = id + +instance IsNum Integer where +instance IsInt Integer where + +tcInteger :: Expr Integer -> TCM () +tcInteger (Lit _) = ok +tcInteger (Const _ _) = ok +tcInteger (Tag _) = ok +tcInteger (Neg e) = tcInteger e +tcInteger (CRingArith _op es) = mapM_ tcInteger es +tcInteger (IntArith _op e1 e2) = do + newTCC [e2 /=* 0] + tcInteger e1 + tcInteger e2 +tcInteger (Ite eb e1 e2) = do + tc eb + withHypo eb $ tcInteger e1 + withHypo (Not eb) $ tcInteger e2 +tcInteger (App _) = ok +tcInteger _ + = error "Z3.Lang.Prelude.tcInteger: Panic! Impossible constructor in pattern matching!" + +compileInteger :: Expr Integer -> Z3 (AST Integer) +compileInteger (Lit a) + = mkLiteral a +compileInteger (Const _ u) + = return u +compileInteger (Tag lyt) + = do ix <- deBruijnIx lyt + srt <- mkSort + mkBound ix srt +compileInteger (Neg e) + = mkUnaryMinus =<< compileInteger e +compileInteger (CRingArith op es) + = mkCRingArith op =<< mapM compileInteger es +compileInteger (IntArith op e1 e2) + = do e1' <- compileInteger e1 + e2' <- compileInteger e2 + mkIntArith op e1' e2' +compileInteger (Ite eb e1 e2) + = do eb' <- compile eb + e1' <- compileInteger e1 + e2' <- compileInteger e2 + mkIte eb' e1' e2' +compileInteger (App e) + = compile e +compileInteger _ + = error "Z3.Lang.Prelude.compileInteger: Panic! Impossible constructor in pattern matching!" + +---------------------------------------------------------------------- +-- Rationals + +type instance TypeZ3 Rational = Rational + +instance Compilable (Expr Rational) where + compile = compileRational + +instance IsTy Rational where + typeInv = const true + tc = tcRational + fromZ3Type = id + toZ3Type = id + +instance IsNum Rational where +instance IsReal Rational where + +tcRational :: Expr Rational -> TCM () +tcRational (Lit _) = ok +tcRational (Const _ _) = ok +tcRational (Tag _) = ok +tcRational (Neg e) = tcRational e +tcRational (CRingArith _op es) = mapM_ tcRational es +tcRational (RealArith Div e1 e2) = do + newTCC [e2 /=* 0] + tcRational e1 + tcRational e2 +tcRational (Ite eb e1 e2) = do + tc eb + withHypo eb $ tcRational e1 + withHypo (Not eb) $ tcRational e2 +tcRational (App _) = ok +tcRational _ + = error "Z3.Lang.Prelude.tcRational: Panic! Impossible constructor in pattern matching!" + +compileRational :: Expr Rational -> Z3 (AST Rational) +compileRational (Lit a) + = mkLiteral a +compileRational (Const _ u) + = return u +compileRational (Tag lyt) + = do ix <- deBruijnIx lyt + srt <- mkSort + mkBound ix srt +compileRational (Neg e) + = mkUnaryMinus =<< compileRational e +compileRational (CRingArith op es) + = mkCRingArith op =<< mapM compileRational es +compileRational (RealArith op@Div e1 e2) + = do e1' <- compileRational e1 + e2' <- compileRational e2 + mkRealArith op e1' e2' +compileRational (Ite eb e1 e2) + = do eb' <- compile eb + e1' <- compileRational e1 + e2' <- compileRational e2 + mkIte eb' e1' e2' +compileRational (App e) + = compile e +compileRational _ + = error "Z3.Lang.Prelude.compileRational: Panic! Impossible constructor in pattern matching!" + +---------------------------------------------------------------------- +-- Functions + +type instance TypeZ3 (a -> b) = TypeZ3 a -> TypeZ3 b + +instance (IsTy a, IsTy b) => IsFun (a -> b) where +instance (IsTy a, IsFun (b -> c)) => IsFun (a -> b -> c) where + +instance IsTy a => Compilable (FunApp a) where + compile = app2AST + +app2AST :: IsTy a => FunApp a -> Z3 (Base.AST (TypeZ3 a)) +app2AST (PApp(FuncDecl fd)e1) = join $ + liftM (mkApp1 fd) (compile e1) +app2AST (PApp(PApp(FuncDecl fd)e1)e2) = join $ + liftM2 (mkApp2 fd) (compile e1) (compile e2) +app2AST (PApp(PApp(PApp(FuncDecl fd)e1)e2)e3) = join $ + liftM3 (mkApp3 fd) (compile e1) (compile e2) (compile e3) +app2AST (PApp(PApp(PApp(PApp(FuncDecl fd)e1)e2)e3)e4) = join $ + liftM4 (mkApp4 fd) (compile e1) (compile e2) (compile e3) (compile e4) +app2AST (PApp(PApp(PApp(PApp(PApp(FuncDecl fd)e1)e2)e3)e4)e5) = join $ + liftM5 (mkApp5 fd) (compile e1) (compile e2) (compile e3) (compile e4) (compile e5) +app2AST _ = error "Z3.Lang.Prelude.app2AST: Panic! Impossible function application!" diff --git a/Z3/Lang/TY.hs b/Z3/Lang/TY.hs new file mode 100644 --- /dev/null +++ b/Z3/Lang/TY.hs @@ -0,0 +1,23 @@ + +{-# LANGUAGE DeriveDataTypeable #-} + +-- | +-- Module : Z3.Lang.TY +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro + +module Z3.Lang.TY where + + +import Data.Data ( Data, Typeable ) + + +-- | An alternative to 'undefined' to fake type parameters. +-- +-- Example: @TY :: TY Integer@ instead of @undefined :: Integer@ +-- +data TY a = TY + deriving (Data,Typeable) diff --git a/Z3/Monad.hs b/Z3/Monad.hs deleted file mode 100644 --- a/Z3/Monad.hs +++ /dev/null @@ -1,284 +0,0 @@ -{-# OPTIONS_GHC -funbox-strict-fields #-} -{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} - -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE ScopedTypeVariables #-} - --- | --- Module : Z3.Monad --- Copyright : (c) Iago Abal, 2012 --- (c) David Castro, 2012 --- License : BSD3 --- Maintainer: Iago Abal , --- David Castro --- Stability : experimental - - -module Z3.Monad ( - -- * Z3 Monad - Z3 - , evalZ3 - - -- * Satisfiability result - , Base.Result(..) - - -- * Z3 actions - , var - , assert - , let_ - , check - - , module Z3.Exprs - - ) where - -import qualified Z3.Base as Base -import Z3.Exprs -import Z3.Exprs.Internal - -import Control.Monad -import Control.Monad.State.Strict -import Data.Maybe ( fromMaybe ) -import qualified Data.IntMap as Map - ---------------------------------------------------------------------- --- The Z3 Monad - --- | Z3 monad. --- -newtype Z3 a = Z3 (StateT Z3State IO a) - deriving (Functor, Monad) - -instance MonadState Z3State Z3 where - get = Z3 $ StateT $ \s -> return (s,s) - put st = Z3 $ StateT $ \_ -> return ((), st) - --- | Existential type. Used to store constants keeping sort info. --- -data AnyAST = forall a. Base.Z3Type a => AnyAST (Base.AST a) - --- | Internal state of Z3 monad. --- -data Z3State - = Z3State { uniqVal :: !Uniq - , context :: Base.Context - , consts :: Map.IntMap AnyAST - } - --- | Eval a Z3 script. --- -evalZ3 :: Z3 a -> IO a -evalZ3 (Z3 s) = do - cfg <- Base.mkConfig - Base.set_MODEL cfg True - Base.set_MODEL_PARTIAL cfg False - ctx <- Base.mkContext cfg - evalStateT s Z3State { uniqVal = 0 - , context = ctx - , consts = Map.empty - } - --- | Fresh symbol name. --- -fresh :: Z3 (Uniq, String) -fresh = do - st <- get - let i = uniqVal st - put st { uniqVal = i + 1 } - return (uniqVal st, 'v':show i) - --- | Add a constant of type @Base.AST a@ to the state. --- -addConst :: Base.Z3Type a => Uniq -> Base.AST a -> Z3 () -addConst u ast = do - st <- get - put st { consts = Map.insert u (AnyAST ast) (consts st) } - --- | Get a 'Base.AST' stored in the Z3State. --- -{- TODO: I believe that getConst return type should be Z3 (Base.AST a) - instead. If Map.lookup returns nothing then we "panic" because - an undefined constant, if Base.castAST returns nothing then we - panic because of type mismatch. We have the duty to guarantee - that none of these errors would ever happen. - - Iago --} -getConst :: forall a. Base.Z3Type a => Uniq -> Z3 (Maybe (Base.AST a)) -getConst u = liftM mlookup (gets consts) - where mlookup :: Map.IntMap AnyAST -> Maybe (Base.AST a) - mlookup m = Map.lookup u m >>= \(AnyAST e) -> Base.castAST e - ---------------------------------------------------------------------- --- Constructing expressions - --- | Declare skolem variables. --- -var :: forall a. IsTy a => Z3 (Expr a) -var = do - ctx <- gets context - (u, str) <- fresh - smb <- mkStringSymbol_ ctx str - (srt :: Base.Sort (TypeZ3 a)) <- Z3 . lift $ Base.mkSort ctx - addConst u =<< mkConst_ ctx smb srt - return $ Const u - --- | Make assertion in current context. --- -assert :: Expr Bool -> Z3 () -assert = join . liftM2 assertCnstr_ (gets context) . compile - --- | Introduce an auxiliary declaration to name a given expression. --- --- If you really want sharing use this instead of Haskell's /let/. --- -let_ :: IsScalar a => Expr a -> Z3 (Expr a) -let_ e = do - aux <- var - assert (aux ==* e) - return aux - --- | Check current context. --- -check :: Z3 Base.Result -check = check_ =<< gets context - --- | Create a 'Base.AST' from a 'Expr'. --- -compile :: IsTy a => Expr a -> Z3 (Base.AST (TypeZ3 a)) -compile (Lit a) - = flip mkLiteral_ (toZ3Type a) =<< gets context -compile (Const u) - = liftM (fromMaybe $ error uNDEFINED_CONST) $ getConst u -compile (Not b) - = do ctx <- gets context - b' <- compile b - mkNot_ ctx b' -compile (BoolBin op e1 e2) - = do ctx <- gets context - e1' <- compile e1 - e2' <- compile e2 - mkBoolBin_ ctx op e1' e2' -compile (BoolMulti op es) - = do ctx <- gets context - es' <- mapM compile es - mkBoolMulti_ ctx op es' -compile (Neg e) - = do ctx <- gets context - e' <- compile e - mkUnaryMinus_ ctx e' -compile (CRingArith op es) - = do ctx <- gets context - es' <- mapM compile es - mkCRingArith_ ctx op es' -compile (IntArith op e1 e2) - = do ctx <- gets context - e1' <- compile e1 - e2' <- compile e2 - mkIntArith_ ctx op e1' e2' -compile (RealArith op e1 e2) - = do ctx <- gets context - e1' <- compile e1 - e2' <- compile e2 - mkRealArith_ ctx op e1' e2' -compile (CmpE op e1 e2) - = do ctx <- gets context - e1' <- compile e1 - e2' <- compile e2 - mkEq_ ctx op e1' e2' -compile (CmpI op e1 e2) - = do ctx <- gets context - e1' <- compile e1 - e2' <- compile e2 - mkCmp_ ctx op e1' e2' -compile (Ite b e1 e2) - = do ctx <- gets context - b' <- compile b - e1' <- compile e1 - e2' <- compile e2 - mkIte_ ctx b' e1' e2' - ---------------------------------------------------------------------- --- Internal lifted Base functions - -assertCnstr_ :: Base.Context -> Base.AST Bool -> Z3 () -assertCnstr_ ctx = Z3 . lift . Base.assertCnstr ctx - -check_ :: Base.Context -> Z3 Base.Result -check_ = Z3 . lift . Base.check - -mkStringSymbol_ :: Base.Context -> String -> Z3 Base.Symbol -mkStringSymbol_ ctx = Z3 . lift . Base.mkStringSymbol ctx - -mkLiteral_ :: forall a. Base.Z3Scalar a => Base.Context -> a -> Z3 (Base.AST a) -mkLiteral_ ctx = Z3 . lift . Base.mkValue ctx - -mkNot_ :: Base.Context -> Base.AST Bool -> Z3 (Base.AST Bool) -mkNot_ ctx = Z3 . lift . Base.mkNot ctx - -mkBoolBin_ :: Base.Context -> BoolBinOp -> - Base.AST Bool -> Base.AST Bool -> Z3 (Base.AST Bool) -mkBoolBin_ ctx Xor b1 = Z3 . lift . Base.mkXor ctx b1 -mkBoolBin_ ctx Implies b1 = Z3 . lift . Base.mkImplies ctx b1 -mkBoolBin_ ctx Iff b1 = Z3 . lift . Base.mkIff ctx b1 - -mkBoolMulti_ :: Base.Context -> BoolMultiOp -> - [Base.AST Bool] -> Z3 (Base.AST Bool) -mkBoolMulti_ ctx And = Z3 . lift . Base.mkAnd ctx -mkBoolMulti_ ctx Or = Z3 . lift . Base.mkAnd ctx - -mkEq_ :: Base.Z3Scalar a => Base.Context -> CmpOpE -> - Base.AST a -> Base.AST a -> Z3 (Base.AST Bool) -mkEq_ ctx Eq e1 = Z3 . lift . Base.mkEq ctx e1 -mkEq_ ctx Neq e1 = Z3 . lift . (Base.mkNot ctx <=< Base.mkEq ctx e1) - -mkCmp_ :: Base.Z3Num a => Base.Context -> CmpOpI -> - Base.AST a -> Base.AST a -> Z3 (Base.AST Bool) -mkCmp_ ctx Le e1 = Z3 . lift . Base.mkLe ctx e1 -mkCmp_ ctx Lt e1 = Z3 . lift . Base.mkLt ctx e1 -mkCmp_ ctx Ge e1 = Z3 . lift . Base.mkGe ctx e1 -mkCmp_ ctx Gt e1 = Z3 . lift . Base.mkGt ctx e1 - -mkConst_ :: Base.Z3Type a => Base.Context - -> Base.Symbol -> Base.Sort a -> Z3 (Base.AST a) -mkConst_ ctx smb = Z3 . lift . Base.mkConst ctx smb - -mkUnaryMinus_ :: Base.Z3Num a => Base.Context -> Base.AST a -> Z3 (Base.AST a) -mkUnaryMinus_ ctx = Z3 . lift . Base.mkUnaryMinus ctx - -mkCRingArith_ :: Base.Z3Num a => Base.Context - -> CRingOp -> [Base.AST a] -> Z3 (Base.AST a) -mkCRingArith_ ctx Add = Z3 . lift . Base.mkAdd ctx -mkCRingArith_ ctx Mul = Z3 . lift . Base.mkMul ctx -mkCRingArith_ ctx Sub = Z3 . lift . Base.mkSub ctx - -mkIntArith_ :: Base.Context - -> IntOp - -> Base.AST Integer -> Base.AST Integer - -> Z3 (Base.AST Integer) -mkIntArith_ ctx Quot e1 = Z3 . lift . Base.mkDiv ctx e1 -mkIntArith_ ctx Mod e1 = Z3 . lift . Base.mkMod ctx e1 -mkIntArith_ ctx Rem e1 = Z3 . lift . Base.mkRem ctx e1 - -mkRealArith_ :: Base.Context - -> RealOp - -> Base.AST Rational -> Base.AST Rational - -> Z3 (Base.AST Rational) -mkRealArith_ ctx Div e1 = Z3 . lift . Base.mkDiv ctx e1 - -mkIte_ :: Base.Context - -> Base.AST Bool - -> Base.AST a -> Base.AST a - -> Z3 (Base.AST a) -mkIte_ ctx b e1 = Z3 . lift . Base.mkIte ctx b e1 - ---------------------------------------------------------------------- --- Error messages - -uNDEFINED_CONST :: String -uNDEFINED_CONST = "Panic! Undefined constant or unexpected\ - \constant sort." diff --git a/Z3/Types.hs b/Z3/Types.hs deleted file mode 100644 --- a/Z3/Types.hs +++ /dev/null @@ -1,99 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeSynonymInstances #-} - - --- | --- Module : Z3.Types --- Copyright : (c) Iago Abal, 2012 --- (c) David Castro, 2012 --- License : BSD3 --- Maintainer: Iago Abal , --- David Castro - - -module Z3.Types ( - - -- * Types - TypeZ3 - , IsTy - , IsScalar(..) - - -- ** Numeric types - , IsNum - , IsInt - , IsReal - - ) where - -import Z3.Base ( Z3Type, Z3Scalar, Z3Num ) - -import Data.Typeable ( Typeable ) - ----------------------------------------------------------------------- --- Types - --- | Maps a type to the underlying Z3 type. --- -type family TypeZ3 a - -type instance TypeZ3 Bool = Bool -type instance TypeZ3 Integer = Integer -type instance TypeZ3 Rational = Rational - --- | Types for expressions. --- -class (Typeable a, Z3Type (TypeZ3 a)) => IsTy a where - -instance IsTy Bool where -instance IsTy Integer where -instance IsTy Rational where - --- | Scalar types. --- -class (Eq a, Show a, IsTy a, Z3Scalar(TypeZ3 a)) => IsScalar a where - fromZ3Type :: TypeZ3 a -> a - toZ3Type :: a -> TypeZ3 a - -instance IsScalar Bool where - fromZ3Type = id - toZ3Type = id - -instance IsScalar Integer where - fromZ3Type = id - toZ3Type = id - -instance IsScalar Rational where - fromZ3Type = id - toZ3Type = id - ------------------------------------------------------------- --- Numeric types --- --- Future Work: We would like to instance 'IsInt' with 'Int32' to provide --- support for reasoning about 32-bit integer arithmetic with overflow. --- It would be also interesting (but perhaps more tricky) to support --- floating point arithmetic by creating an instance of 'IsReal' for --- 'Double'. --- - --- | Numeric types. --- -class (IsScalar a, Num a, Z3Num (TypeZ3 a)) => IsNum a where -instance IsNum Integer where -instance IsNum Rational where - --- | Typeclass for Haskell Z3 numbers of /int/ sort in Z3. --- -class (IsNum a, Integral a, TypeZ3 a ~ Integer) => IsInt a where -instance IsInt Integer where - --- | Typeclass for Haskell Z3 numbers of /real/ sort in Z3. --- -class (IsNum a, Fractional a, Real a, TypeZ3 a ~ Rational) => IsReal a where -instance IsReal Rational where diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -1,5 +1,5 @@ Name: z3 -Version: 0.1.1 +Version: 0.2.0 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 Theorem Prover. @@ -7,11 +7,17 @@ This package is still a work in progress. Low and medium-level bindings to the Z3 API are provided ("Z3.Base.C" and "Z3.Base") in the spirit of yices-painless. These APIs are still incomplete but usable. - The high-level API ("Z3.Monad") is still very experimental. + The high-level API ("Z3.Lang") is still very experimental and likely to change. . + Installation (Unix-like): Just be sure to use the standard locations for + dynamic libraries (\/usr\/lib) and header files (\/usr\/include), or else use + the appropriate Cabal flags. + . + Haddock documentation: + . More information about Z3: . - * + * Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE @@ -34,15 +40,17 @@ Z3.Base Z3.Base.C - Z3.Exprs - - Z3.Monad - - Z3.Types + Z3.Lang + Z3.Lang.Prelude + Z3.Lang.Nat + Z3.Lang.Lg2 + Z3.Lang.Pow2 Other-modules: - Z3.Exprs.Internal + Z3.Lang.Exprs + Z3.Lang.Monad + Z3.Lang.TY ghc-options: -Wall