z3 0.1.1 → 0.2.0
raw patch · 16 files changed
+1796/−900 lines, 16 files
Files
- Z3/Base.hs +297/−171
- Z3/Base/C.hsc +54/−17
- Z3/Exprs.hs +0/−211
- Z3/Exprs/Internal.hs +0/−109
- Z3/Lang.hs +19/−0
- Z3/Lang/Exprs.hs +237/−0
- Z3/Lang/Lg2.hs +40/−0
- Z3/Lang/Monad.hs +314/−0
- Z3/Lang/Monad.hs-boot +10/−0
- Z3/Lang/Nat.hs +113/−0
- Z3/Lang/Pow2.hs +42/−0
- Z3/Lang/Prelude.hs +630/−0
- Z3/Lang/TY.hs +23/−0
- Z3/Monad.hs +0/−284
- Z3/Types.hs +0/−99
- z3.cabal +17/−9
Z3/Base.hs view
@@ -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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef> ---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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c> ---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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b> -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga69564aaa9f2a76556b54f5bbff8e7175>+-- | 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga25e5269d6845bb8ae03b551f09f5d46d>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a> -- 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 : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a> ---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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03> ---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
Z3/Base/C.hsc view
@@ -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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>@@ -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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7e975b7d7ac96de1db73d8f71166c663>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga69564aaa9f2a76556b54f5bbff8e7175>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga25e5269d6845bb8ae03b551f09f5d46d>----foreign import ccall unsafe "Z3_get_denominator"- z3_get_denominator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- TODO Modifiers
− Z3/Exprs.hs
@@ -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 <iago.abal@gmail.com>,--- David Castro <david.castro.dcp@gmail.com>--- 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
− Z3/Exprs/Internal.hs
@@ -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 <iago.abal@gmail.com>,--- David Castro <david.castro.dcp@gmail.com>--- 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)
+ Z3/Lang.hs view
@@ -0,0 +1,19 @@++-- |+-- Module : Z3.Lang+-- Copyright : (c) Iago Abal, 2012+-- (c) David Castro, 2012+-- License : BSD3+-- Maintainer: Iago Abal <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+-- Stability : experimental+--++module Z3.Lang (+ module Z3.Lang.Prelude+ , module Z3.Lang.Nat+ ) where+++import Z3.Lang.Prelude+import Z3.Lang.Nat
+ Z3/Lang/Exprs.hs view
@@ -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 <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+-- 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)
+ Z3/Lang/Lg2.hs view
@@ -0,0 +1,40 @@++{-# LANGUAGE ScopedTypeVariables #-}++-- |+-- Module : Z3.Lang.Lg2+-- Copyright : (c) Iago Abal, 2012+-- (c) David Castro, 2012+-- License : BSD3+-- Maintainer: Iago Abal <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>++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
+ Z3/Lang/Monad.hs view
@@ -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 <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+-- 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
+ Z3/Lang/Monad.hs-boot view
@@ -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)
+ Z3/Lang/Nat.hs view
@@ -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 <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>++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!"+
+ Z3/Lang/Pow2.hs view
@@ -0,0 +1,42 @@++{-# LANGUAGE ScopedTypeVariables #-}++-- |+-- Module : Z3.Lang.Pow+-- Copyright : (c) Iago Abal, 2012+-- (c) David Castro, 2012+-- License : BSD3+-- Maintainer: Iago Abal <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>++-- 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+
+ Z3/Lang/Prelude.hs view
@@ -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 <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+-- 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!"
+ Z3/Lang/TY.hs view
@@ -0,0 +1,23 @@++{-# LANGUAGE DeriveDataTypeable #-}++-- |+-- Module : Z3.Lang.TY+-- Copyright : (c) Iago Abal, 2012+-- (c) David Castro, 2012+-- License : BSD3+-- Maintainer: Iago Abal <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>++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)
− Z3/Monad.hs
@@ -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 <iago.abal@gmail.com>,--- David Castro <david.castro.dcp@gmail.com>--- 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."
− Z3/Types.hs
@@ -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 <iago.abal@gmail.com>,--- David Castro <david.castro.dcp@gmail.com>---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
z3.cabal view
@@ -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: <http://www.iagoabal.eu/z3-haskell/doc>+ . More information about Z3: .- * <http://research.microsoft.com/en-us/um/redmond/projects/z3/>+ * <http://z3.codeplex.com> 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