diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c)2012, Iago Abal, David Castro +Copyright (c)2012-2013, Iago Abal, David Castro All rights reserved. diff --git a/Z3/Base.hs b/Z3/Base.hs --- a/Z3/Base.hs +++ b/Z3/Base.hs @@ -1,953 +1,1598 @@ -{-# 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 --- Copyright : (c) Iago Abal, 2012 --- (c) David Castro, 2012 --- License : BSD3 --- Maintainer: Iago Abal , --- David Castro --- --- Medium-level bindings, highly inspired by yices-painless. --- - -module Z3.Base ( - - -- * Types - Config - , Context - , Symbol - , AST - , Sort - , FuncDecl - , App - , Pattern - , Model - - , castAST - - -- ** Satisfiability result - , Result(..) - - -- ** Z3 types - , Z3Type(..) - , Z3Fun() - , Z3Num - - -- * Configuration - , mkConfig - , setParamValue - , set_MODEL - , set_MODEL_PARTIAL - , set_WELL_SORTED_CHECK - - -- * Context - , mkContext - - -- * Symbols - , mkStringSymbol - - -- * Sorts - , mkBoolSort - , mkIntSort - , mkRealSort - - -- * Constants and Applications - , mkFuncDecl - , mkApp1, mkApp2, mkApp3, mkApp4, mkApp5 - , mkConst - , mkTrue - , mkFalse - , mkEq - , mkNot - , mkIte - , mkIff - , mkImplies - , mkXor - , mkAnd - , mkOr - , mkAdd - , mkMul - , mkSub - , mkUnaryMinus - , mkDiv - , mkMod - , mkRem - , mkLt - , mkLe - , mkGt - , mkGe - , mkInt2Real - , mkReal2Int - , mkIsInt - - -- * Numerals - , mkNumeral - , mkInt - , mkReal - - -- * Quantifiers - , mkPattern - , mkBound - , mkForall - - -- * Accessors - , getBool - , getInt - , getReal - - -- * Models - , eval - - -- * Constraints - , assertCnstr - , check - , getModel - - ) where - -import Z3.Base.C -import Z3.Lang.TY - -import Control.Applicative ( (<$>) ) -import Data.Int -import Data.Ratio ( Ratio, numerator, denominator, (%) ) -import Data.Typeable ( Typeable, typeOf ) -import Data.Word -import Foreign hiding ( newForeignPtr, addForeignPtrFinalizer, toBool ) -import Foreign.C - ( CInt, CUInt, CLLong, CULLong - , peekCString - , withCString ) -import Foreign.Concurrent ( newForeignPtr, addForeignPtrFinalizer ) - ---------------------------------------------------------------------- --- Types --- - --- | A Z3 /configuration object/. --- --- --- /Notes:/ --- --- * The resource is automatically managed by the Haskell garbage --- collector, and the structure is automatically deleted once it is out --- of scope (no need to call 'z3_del_config'). --- -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 --- collector, and the structure is automatically deleted once it is out --- of scope (no need to call 'z3_del_context'). --- -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, 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) - | typeOf (TY::TY a) == typeOf (TY::TY b) = Just (AST a) - | otherwise = Nothing - --- | Kind of Z3 AST representing /types/. --- -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 --- guide quantifier instantiation. --- -newtype Pattern = Pattern { _unPattern :: Ptr Z3_pattern } - deriving (Eq, Ord, Show, Storable) - --- | A model for the constraints asserted into the logical context. --- -newtype Model = Model { unModel :: Ptr Z3_model } - deriving Eq - --- | Result of a satisfiability check. --- -data Result a - = Sat a - | Unsat - | Undef - 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 lb - | lb == z3_l_true = Sat () - | lb == z3_l_false = Unsat - | lb == z3_l_undef = Undef - | otherwise = error "Z3.Base.toResult: illegal `Z3_lbool' value" - --- | Convert 'Z3_bool' to 'Bool'. --- --- 'Foreign.toBool' should be OK but this is convenient. --- -toBool :: Z3_bool -> Bool -toBool b - | b == z3_true = True - | b == z3_false = False - | otherwise = error "Z3.Base.toBool: illegal `Z3_bool' value" - ------------------------------------------------------------ --- Z3 types --- - --- | A Z3 type --- -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 Function type --- -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 (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 (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)) - - --- | A Z3 numeric type --- -class (Z3Type a, Num a) => Z3Num a where -instance Z3Num Integer where -instance Z3Num Rational where - ---------------------------------------------------------------------- --- Configuration - --- | Create a configuration. --- --- Reference: --- -mkConfig :: IO Config -mkConfig = do - ptr <- z3_mk_config - fptr <- newForeignPtr ptr (z3_del_config ptr) - return $! Config fptr - --- | Set a configuration parameter. --- --- Reference: --- --- See: --- -setParamValue :: Config -> String -> String -> IO () -setParamValue cfg s1 s2 = - withConfig cfg $ \cfgPtr -> - withCString s1 $ \cs1 -> - withCString s2 $ \cs2 -> - z3_set_param_value cfgPtr cs1 cs2 - --- | Set the /MODEL/ configuration parameter. --- --- default: 'True', enable/disable model construction. --- -set_MODEL :: Config -> Bool -> IO () -set_MODEL cfg True = setParamValue cfg "MODEL" "true" -set_MODEL cfg False = setParamValue cfg "MODEL" "false" - --- | Set the /MODEL_PARTIAL/ configuration parameter. --- --- default: 'False', enable/disable partial function interpretations. --- -set_MODEL_PARTIAL :: Config -> Bool -> IO () -set_MODEL_PARTIAL cfg True = setParamValue cfg "MODEL_PARTIAL" "true" -set_MODEL_PARTIAL cfg False = setParamValue cfg "MODEL_PARTIAL" "false" - --- | Set the /WELL_SORTED_CHECK/ configuration parameter. --- --- default: 'True', enable/disable type checker. --- -set_WELL_SORTED_CHECK :: Config -> Bool -> IO () -set_WELL_SORTED_CHECK cfg True = setParamValue cfg "WELL_SORTED_CHECK" "true" -set_WELL_SORTED_CHECK cfg False = setParamValue cfg "WELL_SORTED_CHECK" "false" - ---------------------------------------------------------------------- --- Context - --- | Create a context using the given configuration. --- --- Reference: --- -mkContext :: Config -> IO Context -mkContext cfg = withConfig cfg $ \cfgPtr -> do - ptr <- z3_mk_context cfgPtr - fptr <- newForeignPtr ptr (z3_del_context ptr) - return $! Context fptr - ---------------------------------------------------------------------- --- Symbols - --- | Create a Z3 symbol using a string. --- --- Reference: --- -mkStringSymbol :: Context -> String -> IO Symbol -mkStringSymbol ctx s = - withContext ctx $ \ctxPtr -> - withCString s $ \cs -> - Symbol <$> z3_mk_string_symbol ctxPtr cs - ---------------------------------------------------------------------- --- Sorts - --- TODO Sorts: Z3_is_eq_sort --- TODO Sorts: Z3_mk_uninterpreted_sort - --- | Create the Boolean type. --- --- Reference: --- -mkBoolSort :: Context -> IO (Sort Bool) -mkBoolSort c = withContext c $ \cptr -> - Sort <$> z3_mk_bool_sort cptr - --- | Create an integer type. --- --- Reference: --- -mkIntSort :: Context -> IO (Sort Integer) -mkIntSort c = withContext c $ \cptr -> - Sort <$> z3_mk_int_sort cptr - --- | Create a real type. --- --- Reference: --- -mkRealSort :: Context -> IO (Sort Rational) -mkRealSort c = withContext c $ \cptr -> - Sort <$> z3_mk_real_sort cptr - --- TODO Sorts: from Z3_mk_real_sort on - ---------------------------------------------------------------------- --- Constants and Applications - --- | 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 :: 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 --- TODO Constants and Applications: Z3_mk_fresh_const - --- | Create an AST node representing /true/. --- --- Reference: --- -mkTrue :: Context -> IO (AST Bool) -mkTrue c = withContext c $ \cptr -> - AST <$> z3_mk_true cptr - --- | Create an AST node representing /false/. --- --- Reference: --- -mkFalse :: Context -> IO (AST Bool) -mkFalse c = withContext c $ \cptr -> - AST <$> z3_mk_false cptr - --- | Create an AST node representing l = r. --- --- Reference: --- -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). --- --- Reference: --- -mkNot :: Context -> AST Bool -> IO (AST Bool) -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). --- --- Reference: --- -mkIte :: Context -> AST Bool -> AST a -> AST a -> IO (AST a) -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. --- --- Reference: --- -mkIff :: Context -> AST Bool -> AST Bool -> IO (AST Bool) -mkIff c p q = withContext c $ \cptr -> - AST <$> z3_mk_iff cptr (unAST p) (unAST q) - --- | Create an AST node representing t1 implies t2. --- --- Reference: --- -mkImplies :: Context -> AST Bool -> AST Bool -> IO (AST Bool) -mkImplies c p q = withContext c $ \cptr -> - AST <$> z3_mk_implies cptr (unAST p) (unAST q) - --- | Create an AST node representing t1 xor t2. --- --- Reference: --- -mkXor :: Context -> AST Bool -> AST Bool -> IO (AST Bool) -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]. --- --- Reference: --- -mkAnd :: Context -> [AST Bool] -> IO (AST Bool) -mkAnd _ [] = error "Z3.Base.mkAnd: empty list of expressions" -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]. --- --- Reference: --- -mkOr :: Context -> [AST Bool] -> IO (AST Bool) -mkOr _ [] = error "Z3.Base.mkOr: empty list of expressions" -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]. --- --- 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 -> - 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]. --- --- 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 -> - 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]. --- --- Reference: --- -mkSub ::Z3Num a => Context -> [AST a] -> IO (AST a) -mkSub _ [] = error "Z3.Base.mkSub: empty list of expressions" -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. --- --- Reference: --- -mkUnaryMinus :: Z3Num a => Context -> AST a -> IO (AST a) -mkUnaryMinus c e = withContext c $ \cptr -> - AST <$> z3_mk_unary_minus cptr (unAST e) - --- | Create an AST node representing arg1 div arg2. --- --- Reference: --- -mkDiv :: Z3Num a => Context -> AST a -> AST a -> IO (AST a) -mkDiv c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_div cptr (unAST e1) (unAST e2) - --- | Create an AST node representing arg1 mod arg2. --- --- Reference: --- -mkMod :: Context -> AST Integer -> AST Integer -> IO (AST Integer) -mkMod c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_mod cptr (unAST e1) (unAST e2) - --- | Create an AST node representing arg1 rem arg2. --- --- Reference: --- -mkRem :: Context -> AST Integer -> AST Integer -> IO (AST Integer) -mkRem c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_rem cptr (unAST e1) (unAST e2) - --- | Create less than. --- --- Reference: --- -mkLt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkLt c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_lt cptr (unAST e1) (unAST e2) - --- | Create less than or equal to. --- --- Reference: --- -mkLe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkLe c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_le cptr (unAST e1) (unAST e2) - --- | Create greater than. --- --- Reference: --- -mkGt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkGt c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_gt cptr (unAST e1) (unAST e2) - --- | Create greater than or equal to. --- --- Reference: --- -mkGe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool) -mkGe c e1 e2 = withContext c $ \cptr -> - AST <$> z3_mk_ge cptr (unAST e1) (unAST e2) - --- | Coerce an integer to a real. --- --- Reference: --- -mkInt2Real :: Context -> AST Integer -> IO (AST Rational) -mkInt2Real c e = withContext c $ \cptr -> - AST <$> z3_mk_int2real cptr (unAST e) - --- | Coerce a real to an integer. --- --- Reference: --- -mkReal2Int :: Context -> AST Rational -> IO (AST Integer) -mkReal2Int c e = withContext c $ \cptr -> - AST <$> z3_mk_real2int cptr (unAST e) - --- | Check if a real number is an integer. --- --- Reference: --- -mkIsInt :: Context -> AST Rational -> IO (AST Bool) -mkIsInt c e = withContext c $ \cptr -> - AST <$> z3_mk_is_int cptr (unAST e) - --- TODO Bit-vector, Arrays, Sets - - ---------------------------------------------------------------------- --- Numerals - --- | Create a numeral of a given sort. --- --- Reference: --- -mkNumeral :: Z3Num a => Context -> String -> Sort a -> IO (AST a) -mkNumeral c str s = - withContext c $ \cptr -> - withCString str $ \cstr-> - AST <$> z3_mk_numeral cptr cstr (unSort s) - -------------------------------------------------- --- Numerals / Integers - --- | 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 - -{-# INLINE mkIntZ3 #-} -mkIntZ3 :: Z3Num a => Context -> Int32 -> Sort a -> IO (AST a) -mkIntZ3 c n s = - 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 = - 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 = - 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 = - 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) -mkInt_IntZ3 c n = mkIntSort c >>= mkIntZ3 c n - -{-# RULES "mkInt/mkInt_UnsignedIntZ3" mkInt = mkInt_UnsignedIntZ3 #-} -mkInt_UnsignedIntZ3 :: Context -> Word32 -> IO (AST Integer) -mkInt_UnsignedIntZ3 c n = mkIntSort c >>= mkUnsignedIntZ3 c n - -{-# RULES "mkInt/mkInt_Int64Z3" mkInt = mkInt_Int64Z3 #-} -mkInt_Int64Z3 :: Context -> Int64 -> IO (AST Integer) -mkInt_Int64Z3 c n = mkIntSort c >>= mkInt64Z3 c n - -{-# RULES "mkInt/mkInt_UnsignedInt64Z3" mkInt = mkInt_UnsignedInt64Z3 #-} -mkInt_UnsignedInt64Z3 :: Context -> Word64 -> IO (AST Integer) -mkInt_UnsignedInt64Z3 c n = mkIntSort c >>= mkUnsignedInt64Z3 c n - -------------------------------------------------- --- Numerals / Reals - --- | 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 - -{-# RULES "mkReal/mkRealZ3" mkReal = mkRealZ3 #-} -mkRealZ3 :: Context -> Ratio Int32 -> IO (AST Rational) -mkRealZ3 c r = - 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) -mkReal_IntZ3 c n = mkRealSort c >>= mkIntZ3 c n - -{-# RULES "mkReal/mkReal_UnsignedIntZ3" mkReal = mkReal_UnsignedIntZ3 #-} -mkReal_UnsignedIntZ3 :: Context -> Word32 -> IO (AST Rational) -mkReal_UnsignedIntZ3 c n = mkRealSort c >>= mkUnsignedIntZ3 c n - -{-# RULES "mkReal/mkReal_Int64Z3" mkReal = mkReal_Int64Z3 #-} -mkReal_Int64Z3 :: Context -> Int64 -> IO (AST Rational) -mkReal_Int64Z3 c n = mkRealSort c >>= mkInt64Z3 c n - -{-# RULES "mkReal/mkReal_UnsignedInt64Z3" mkReal = mkReal_UnsignedInt64Z3 #-} -mkReal_UnsignedInt64Z3 :: Context -> Word64 -> IO (AST Rational) -mkReal_UnsignedInt64Z3 c n = mkRealSort c >>= mkUnsignedInt64Z3 c n - ---------------------------------------------------------------------- --- 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 - --- | Cast a 'Z3_lbool' from Z3.Base.C to @Bool@. -castLBool :: Z3_lbool -> Maybe Bool -castLBool lb - | lb == z3_l_true = Just True - | lb == z3_l_false = Just False - | lb == z3_l_undef = Nothing - | otherwise = error "Z3.Base.castLBool: illegal `Z3_lbool' value" - --- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF --- otherwise. --- --- Reference: --- -getBool :: Context -> AST Bool -> IO (Maybe Bool) -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. --- --- Reference: --- -getNumeralString :: Z3Num a => Context -> AST a -> IO String -getNumeralString c a = withContext c $ \ctxPtr -> - peekCString =<< z3_get_numeral_string ctxPtr (unAST a) - --- | Return 'Z3Int' value --- -getInt :: Context -> AST Integer -> IO Integer -getInt c a = read <$> getNumeralString c a - --- | Return 'Z3Real' value --- -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" - - parseDen :: String -> Integer - parseDen "" = 1 - parseDen ('/':sj) = read sj - parseDen _ = error "Z3.Base.getReal: no parse" - - --- TODO Modifiers - ---------------------------------------------------------------------- --- Models - -mkModel :: Context -> Ptr Z3_model -> IO Model -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 :: 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 - ---------------------------------------------------------------------- --- Constraints - --- TODO Constraints: Z3_push --- TODO Constraints: Z3_pop --- TODO Constraints: Z3_get_num_scopes --- TODO Constraints: Z3_persist_ast - --- | Assert a constraing into the logical context. --- --- Reference: --- -assertCnstr :: Context -> AST Bool -> IO () -assertCnstr ctx ast = withContext ctx $ \ctxPtr -> - z3_assert_cnstr ctxPtr (unAST ast) - --- | Get model (logical context is consistent) --- --- Reference : --- -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 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. --- --- Reference: --- -check :: Context -> IO (Result ()) -check ctx = toResult <$> withContext ctx z3_check - --- TODO Constraints: Z3_check_assumptions --- TODO Constraints: Z3_get_implied_equalities - --- TODO From section 'Constraints' on. +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE TupleSections #-} + +-- | +-- Module : Z3.Base +-- Copyright : (c) Iago Abal, 2012-2013 +-- (c) David Castro, 2012-2013 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- +-- Low-level bindings to Z3 API. + +-- TODO Rename showModel and showContext to match Z3 C API names. +module Z3.Base ( + + -- * Types + Config + , Context + , Symbol + , AST + , Sort + , FuncDecl + , App + , Pattern + , Model + , Params + , Solver + + -- ** Satisfiability result + , Result(..) + + -- * Configuration + , mkConfig + , delConfig + , withConfig + , setParamValue + + -- * Context + , mkContext + , delContext + , withContext + + -- * Symbols + , mkStringSymbol + + -- * Sorts + , mkBoolSort + , mkIntSort + , mkRealSort + , mkBvSort + , mkArraySort + + -- * Constants and Applications + , mkFuncDecl + , mkApp + , mkConst + , mkTrue + , mkFalse + , mkEq + , mkNot + , mkIte + , mkIff + , mkImplies + , mkXor + , mkAnd + , mkOr + , mkDistinct + , mkAdd + , mkMul + , mkSub + , mkUnaryMinus + , mkDiv + , mkMod + , mkRem + , mkLt + , mkLe + , mkGt + , mkGe + , mkInt2Real + , mkReal2Int + , mkIsInt + + -- * Bit-vectors + , mkBvnot + , mkBvredand + , mkBvredor + , mkBvand + , mkBvor + , mkBvxor + , mkBvnand + , mkBvnor + , mkBvxnor + , mkBvneg + , mkBvadd + , mkBvsub + , mkBvmul + , mkBvudiv + , mkBvsdiv + , mkBvurem + , mkBvsrem + , mkBvsmod + , mkBvult + , mkBvslt + , mkBvule + , mkBvsle + , mkBvuge + , mkBvsge + , mkBvugt + , mkBvsgt + , mkConcat + , mkExtract + , mkSignExt + , mkZeroExt + , mkRepeat + , mkBvshl + , mkBvlshr + , mkBvashr + , mkRotateLeft + , mkRotateRight + , mkExtRotateLeft + , mkExtRotateRight + , mkInt2bv + , mkBv2int + , mkBvnegNoOverflow + , mkBvaddNoOverflow + , mkBvaddNoUnderflow + , mkBvsubNoOverflow + , mkBvsubNoUnderflow + , mkBvmulNoOverflow + , mkBvmulNoUnderflow + , mkBvsdivNoOverflow + + -- * Arrays + , mkSelect + , mkStore + , mkConstArray + , mkMap + , mkArrayDefault + + -- * Numerals + , mkNumeral + , mkInt + , mkReal + + -- * Quantifiers + , mkPattern + , mkBound + , mkForall + , mkExists + + -- * Accessors + , getBvSortSize + , getSort + , getBool + , getInt + , getReal + + -- * Models + , eval + , evalT + , showModel + , showContext + + -- * Constraints + , assertCnstr + , check + , getModel + , delModel + , push + , pop + + + -- * Parameters + , mkParams + , paramsSetBool + , paramsSetUInt + , paramsSetDouble + , paramsSetSymbol + , paramsToString + + -- * Solvers + , Logic(..) + , mkSolver + , mkSimpleSolver + , mkSolverForLogic + , solverSetParams + , solverPush + , solverPop + , solverReset + , solverAssertCnstr + , solverAssertAndTrack + , solverCheck + --, solverGetModel + , solverCheckAndGetModel + , solverGetReasonUnknown + + -- * String Conversion + , ASTPrintMode(..) + , setASTPrintMode + , astToString + , patternToString + , sortToString + , funcDeclToString + + -- * Error Handling + , Z3Error(..) + , Z3ErrorCode(..) + ) where + +import Z3.Base.C + +import Control.Applicative ( (<$>), (<*) ) +import Control.Exception ( Exception, bracket, throw ) +import Control.Monad ( when ) +import Data.List ( genericLength ) +import Data.Int +import Data.Ratio ( Ratio, numerator, denominator, (%) ) +import Data.Traversable ( Traversable ) +import qualified Data.Traversable as T +import Data.Typeable ( Typeable ) +import Data.Word +import Foreign hiding ( toBool ) +import Foreign.C + ( CInt, CUInt, CLLong, CULLong + , peekCString + , withCString ) + +--------------------------------------------------------------------- +-- Types + +-- | A Z3 /configuration object/. +newtype Config = Config { unConfig :: Ptr Z3_config } + deriving Eq + +-- | A Z3 /logical context/. +newtype Context = Context { unContext :: Ptr Z3_context } + deriving Eq + +-- | A Z3 /Lisp-link symbol/. +newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol } + deriving (Eq, Ord, Show, Storable) + +-- | A Z3 /AST node/. +newtype AST = AST { unAST :: Ptr Z3_ast } + deriving (Eq, Ord, Show, Storable, Typeable) + +-- | Kind of Z3 AST representing /types/. +newtype Sort = Sort { unSort :: Ptr Z3_sort } + deriving (Eq, Ord, Show, Storable) + +-- | Kind of AST used to represent function symbols. +newtype FuncDecl = 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 = App { _unApp :: Ptr Z3_app } + deriving (Eq, Ord, Show, Storable) + +-- | A kind of AST used to represent pattern and multi-patterns used to +-- guide quantifier instantiation. +newtype Pattern = Pattern { unPattern :: Ptr Z3_pattern } + deriving (Eq, Ord, Show, Storable) + +-- | A model for the constraints asserted into the logical context. +newtype Model = Model { unModel :: Ptr Z3_model } + deriving Eq + +-- | A Z3 parameter set. Starting at Z3 4.0, parameter sets are used +-- to configure many components such as: simplifiers, tactics, +-- solvers, etc. +newtype Params = Params { unParams :: Ptr Z3_params } + deriving Eq + +-- | A Z3 solver engine +newtype Solver = Solver { unSolver :: Ptr Z3_solver } + deriving Eq + +-- | Result of a satisfiability check. +data Result + = Sat + | Unsat + | Undef + deriving (Eq, Ord, Read, Show) + +-- | Convert 'Z3_lbool' from Z3.Base.C to 'Result' +toResult :: Z3_lbool -> Result +toResult lb + | lb == z3_l_true = Sat + | lb == z3_l_false = Unsat + | lb == z3_l_undef = Undef + | otherwise = error "Z3.Base.toResult: illegal `Z3_lbool' value" + +-- | Convert 'Z3_bool' to 'Bool'. +-- +-- 'Foreign.toBool' should be OK but this is more convenient. +toBool :: Z3_bool -> Bool +toBool b + | b == z3_true = True + | b == z3_false = False + | otherwise = error "Z3.Base.toBool: illegal `Z3_bool' value" + +-- | Convert 'Bool' to 'Z3_bool'. +unBool :: Bool -> Z3_bool +unBool True = z3_true +unBool False = z3_false + +-- | Z3 exceptions. +data Z3Error = Z3Error + { errCode :: Z3ErrorCode + , errMsg :: String + } + deriving Typeable + +instance Show Z3Error where + show (Z3Error _ s) = s + +data Z3ErrorCode = SortError | IOB | InvalidArg | ParserError | NoParser + | InvalidPattern | MemoutFail | FileAccessError | InternalFatal + | InvalidUsage | DecRefError | Z3Exception + deriving (Show, Typeable) + +toZ3Error :: Z3_error_code -> Z3ErrorCode +toZ3Error e + | e == z3_sort_error = SortError + | e == z3_iob = IOB + | e == z3_invalid_arg = InvalidArg + | e == z3_parser_error = ParserError + | e == z3_no_parser = NoParser + | e == z3_invalid_pattern = InvalidPattern + | e == z3_memout_fail = MemoutFail + | e == z3_file_access_error = FileAccessError + | e == z3_internal_fatal = InternalFatal + | e == z3_invalid_usage = InvalidUsage + | e == z3_dec_ref_error = DecRefError + | e == z3_exception = Z3Exception + | otherwise = error "Z3.Base.toZ3Error: illegal `Z3_error_code' value" + +instance Exception Z3Error + +-- | Throws a z3 error +z3Error :: Z3ErrorCode -> String -> IO () +z3Error cd = throw . Z3Error cd + +-- | Throw an exception if a Z3 error happened +checkError :: Context -> IO a -> IO a +checkError c m = m <* (z3_get_error_code (unContext c) >>= throwZ3Exn) + where throwZ3Exn i = when (i /= z3_ok) $ getErrStr i >>= z3Error (toZ3Error i) + getErrStr i = peekCString =<< z3_get_error_msg_ex (unContext c) i + +--------------------------------------------------------------------- +-- Configuration + +-- | Create a configuration. +-- +-- Reference: +mkConfig :: IO Config +mkConfig = Config <$> z3_mk_config + +-- | Delete a configuration. +-- +-- Reference: +delConfig :: Config -> IO () +delConfig = z3_del_config . unConfig + +-- | Run a computation using a temporally created configuration. +withConfig :: (Config -> IO a) -> IO a +withConfig = bracket mkConfig delConfig + +-- | Set a configuration parameter. +-- +-- Reference: +-- +-- See: +setParamValue :: Config -> String -> String -> IO () +setParamValue cfg s1 s2 = + withCString s1 $ \cs1 -> + withCString s2 $ \cs2 -> + z3_set_param_value (unConfig cfg) cs1 cs2 + +--------------------------------------------------------------------- +-- Context + +-- | Create a context using the given configuration. +-- +-- Reference: +mkContext :: Config -> IO Context +mkContext cfg = do + ctxPtr <- z3_mk_context (unConfig cfg) + z3_set_error_handler ctxPtr nullFunPtr + return $ Context ctxPtr + +-- | Delete the given logical context. +-- +-- Reference: +delContext :: Context -> IO () +delContext = z3_del_context . unContext + +-- | Run a computation using a temporally created context. +withContext :: Config -> (Context -> IO a) -> IO a +withContext cfg = bracket (mkContext cfg) delContext + +--------------------------------------------------------------------- +-- Symbols + +-- | Create a Z3 symbol using a string. +-- +-- Reference: +mkStringSymbol :: Context -> String -> IO Symbol +mkStringSymbol ctx s = + withCString s $ \cs -> + checkError ctx $ + Symbol <$> z3_mk_string_symbol (unContext ctx) cs + +--------------------------------------------------------------------- +-- Sorts + +-- TODO Sorts: Z3_is_eq_sort +-- TODO Sorts: Z3_mk_uninterpreted_sort + +-- | Create the /Boolean/ type. +-- +-- Reference: +mkBoolSort :: Context -> IO Sort +mkBoolSort c = checkError c $ Sort <$> z3_mk_bool_sort (unContext c) + +-- | Create an /integer/ type. +-- +-- Reference: +mkIntSort :: Context -> IO Sort +mkIntSort c = checkError c $ Sort <$> z3_mk_int_sort (unContext c) + +-- | Create a /real/ type. +-- +-- Reference: +mkRealSort :: Context -> IO Sort +mkRealSort c = checkError c $ Sort <$> z3_mk_real_sort (unContext c) + +-- | Create a bit-vector type of the given size. +-- +-- This type can also be seen as a machine integer. +-- +-- Reference: +mkBvSort :: Context -> Int -> IO Sort +mkBvSort c n = checkError c $ Sort <$> z3_mk_bv_sort (unContext c) (fromIntegral n) + +-- | Create an array type +-- +-- Reference: +-- +mkArraySort :: Context -> Sort -> Sort -> IO Sort +mkArraySort c dom rng = checkError c $ Sort <$> z3_mk_array_sort (unContext c) (unSort dom) (unSort rng) + +-- TODO Sorts: from Z3_mk_array_sort on + +--------------------------------------------------------------------- +-- Constants and Applications + +-- | A Z3 function +mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl +mkFuncDecl ctx smb dom rng = + withArray (map unSort dom) $ \c_dom -> + checkError ctx $ + FuncDecl <$> z3_mk_func_decl (unContext ctx) + (unSymbol smb) + (genericLength dom) + c_dom + (unSort rng) + +-- | Create a constant or function application. +-- +-- Reference: +mkApp :: Context -> FuncDecl -> [AST] -> IO AST +mkApp ctx fd args = + withArray (map unAST args) $ \pargs -> + checkError ctx $ + AST <$> z3_mk_app ctxPtr fdPtr numArgs pargs + where ctxPtr = unContext ctx + fdPtr = unFuncDecl fd + numArgs = genericLength args + +-- | Declare and create a constant. +-- +-- Reference: +mkConst :: Context -> Symbol -> Sort -> IO AST +mkConst c x s = checkError c $ AST <$> z3_mk_const (unContext c) (unSymbol x) (unSort s) + +-- TODO Constants and Applications: Z3_mk_fresh_func_decl +-- TODO Constants and Applications: Z3_mk_fresh_const + +-- | Create an AST node representing /true/. +-- +-- Reference: +mkTrue :: Context -> IO AST +mkTrue c = checkError c $ AST <$> z3_mk_true (unContext c) + +-- | Create an AST node representing /false/. +-- +-- Reference: +mkFalse :: Context -> IO AST +mkFalse c = checkError c $ AST <$> z3_mk_false (unContext c) + +-- | Create an AST node representing /l = r/. +-- +-- Reference: +mkEq :: Context -> AST -> AST -> IO AST +mkEq c e1 e2 = checkError c $ AST <$> z3_mk_eq (unContext c) (unAST e1) (unAST e2) + +-- | The distinct construct is used for declaring the arguments pairwise +-- distinct. +-- +-- Reference: +mkDistinct :: Context -> [AST] -> IO AST +mkDistinct _ [] = error "Z3.Base.mkDistinct: empty list of expressions" +mkDistinct c es = + withArray (map unAST es) $ \aptr -> + checkError c $ + AST <$> z3_mk_distinct (unContext c) n aptr + where n = genericLength es + +-- | Create an AST node representing /not(a)/. +-- +-- Reference: +mkNot :: Context -> AST -> IO AST +mkNot c e = checkError c $ AST <$> z3_mk_not (unContext c) (unAST e) + +-- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/. +-- +-- Reference: +mkIte :: Context -> AST -> AST -> AST -> IO AST +mkIte c g e1 e2 = + checkError c $ AST <$> z3_mk_ite (unContext c) (unAST g) (unAST e1) (unAST e2) + +-- | Create an AST node representing /t1 iff t2/. +-- +-- Reference: +mkIff :: Context -> AST -> AST -> IO AST +mkIff c p q = checkError c $ AST <$> z3_mk_iff (unContext c) (unAST p) (unAST q) + +-- | Create an AST node representing /t1 implies t2/. +-- +-- Reference: +mkImplies :: Context -> AST -> AST -> IO AST +mkImplies c p q = checkError c $ AST <$> z3_mk_implies (unContext c) (unAST p) (unAST q) + +-- | Create an AST node representing /t1 xor t2/. +-- +-- Reference: +mkXor :: Context -> AST -> AST -> IO AST +mkXor c p q = checkError c $ AST <$> z3_mk_xor (unContext c) (unAST p) (unAST q) + +-- | Create an AST node representing args[0] and ... and args[num_args-1]. +-- +-- Reference: +mkAnd :: Context -> [AST] -> IO AST +mkAnd _ [] = error "Z3.Base.mkAnd: empty list of expressions" +mkAnd c es = + withArray (map unAST es) $ \aptr -> + checkError c $ + AST <$> z3_mk_and (unContext c) n aptr + where n = genericLength es + +-- | Create an AST node representing args[0] or ... or args[num_args-1]. +-- +-- Reference: +mkOr :: Context -> [AST] -> IO AST +mkOr _ [] = error "Z3.Base.mkOr: empty list of expressions" +mkOr c es = + withArray (map unAST es) $ \aptr -> + checkError c $ + AST <$> z3_mk_or (unContext c) n aptr + where n = genericLength es + +-- | Create an AST node representing args[0] + ... + args[num_args-1]. +-- +-- Reference: +mkAdd :: Context -> [AST] -> IO AST +mkAdd _ [] = error "Z3.Base.mkAdd: empty list of expressions" +mkAdd c es = + withArray (map unAST es) $ \aptr -> + checkError c $ + AST <$> z3_mk_add (unContext c) n aptr + where n = genericLength es + +-- | Create an AST node representing args[0] * ... * args[num_args-1]. +-- +-- Reference: +mkMul :: Context -> [AST] -> IO AST +mkMul _ [] = error "Z3.Base.mkMul: empty list of expressions" +mkMul c es = + withArray (map unAST es) $ \aptr -> + checkError c $ + AST <$> z3_mk_mul (unContext c) n aptr + where n = genericLength es + +-- | Create an AST node representing args[0] - ... - args[num_args - 1]. +-- +-- Reference: +mkSub :: Context -> [AST] -> IO AST +mkSub _ [] = error "Z3.Base.mkSub: empty list of expressions" +mkSub c es = + withArray (map unAST es) $ \aptr -> + checkError c $ + AST <$> z3_mk_sub (unContext c) n aptr + where n = genericLength es + +-- | Create an AST node representing -arg. +-- +-- Reference: +mkUnaryMinus :: Context -> AST -> IO AST +mkUnaryMinus c e = checkError c $ AST <$> z3_mk_unary_minus (unContext c) (unAST e) + +-- | Create an AST node representing arg1 div arg2. +-- +-- Reference: +mkDiv :: Context -> AST -> AST -> IO AST +mkDiv c e1 e2 = checkError c $ AST <$> z3_mk_div (unContext c) (unAST e1) (unAST e2) + +-- | Create an AST node representing arg1 mod arg2. +-- +-- Reference: +mkMod :: Context -> AST -> AST -> IO AST +mkMod c e1 e2 = checkError c $ AST <$> z3_mk_mod (unContext c) (unAST e1) (unAST e2) + +-- | Create an AST node representing arg1 rem arg2. +-- +-- Reference: +mkRem :: Context -> AST -> AST -> IO AST +mkRem c e1 e2 = checkError c $ AST <$> z3_mk_rem (unContext c) (unAST e1) (unAST e2) + +-- | Create less than. +-- +-- Reference: +mkLt :: Context -> AST -> AST -> IO AST +mkLt c e1 e2 = checkError c $ AST <$> z3_mk_lt (unContext c) (unAST e1) (unAST e2) + +-- | Create less than or equal to. +-- +-- Reference: +mkLe :: Context -> AST -> AST -> IO AST +mkLe c e1 e2 = checkError c $ AST <$> z3_mk_le (unContext c) (unAST e1) (unAST e2) + +-- | Create greater than. +-- +-- Reference: +mkGt :: Context -> AST -> AST -> IO AST +mkGt c e1 e2 = checkError c $ AST <$> z3_mk_gt (unContext c) (unAST e1) (unAST e2) + +-- | Create greater than or equal to. +-- +-- Reference: +mkGe :: Context -> AST -> AST -> IO AST +mkGe c e1 e2 = checkError c $ AST <$> z3_mk_ge (unContext c) (unAST e1) (unAST e2) + +-- | Coerce an integer to a real. +-- +-- Reference: +mkInt2Real :: Context -> AST -> IO AST +mkInt2Real c e = checkError c $ AST <$> z3_mk_int2real (unContext c) (unAST e) + +-- | Coerce a real to an integer. +-- +-- Reference: +mkReal2Int :: Context -> AST -> IO AST +mkReal2Int c e = checkError c $ AST <$> z3_mk_real2int (unContext c) (unAST e) + +-- | Check if a real number is an integer. +-- +-- Reference: +mkIsInt :: Context -> AST -> IO AST +mkIsInt c e = checkError c $ AST <$> z3_mk_is_int (unContext c) (unAST e) + +--------------------------------------------------------------------- +-- Bit-vectors + +-- | Bitwise negation. +-- +-- Reference: +mkBvnot :: Context -> AST -> IO AST +mkBvnot c e = checkError c $ AST <$> z3_mk_bvnot (unContext c) (unAST e) + +-- | Take conjunction of bits in vector, return vector of length 1. +-- +-- Reference: +mkBvredand :: Context -> AST -> IO AST +mkBvredand c e = checkError c $ AST <$> z3_mk_bvredand (unContext c) (unAST e) + +-- | Take disjunction of bits in vector, return vector of length 1. +-- +-- Reference: +mkBvredor :: Context -> AST -> IO AST +mkBvredor c e = checkError c $ AST <$> z3_mk_bvredor (unContext c) (unAST e) + +-- | Bitwise and. +-- +-- Reference: +mkBvand :: Context -> AST -> AST -> IO AST +mkBvand c e1 e2 = checkError c $ AST <$> z3_mk_bvand (unContext c) (unAST e1) (unAST e2) + +-- | Bitwise or. +-- +-- Reference: +mkBvor :: Context -> AST -> AST -> IO AST +mkBvor c e1 e2 = checkError c $ AST <$> z3_mk_bvor (unContext c) (unAST e1) (unAST e2) + +-- | Bitwise exclusive-or. +-- +-- Reference: +mkBvxor :: Context -> AST -> AST -> IO AST +mkBvxor c e1 e2 = checkError c $ AST <$> z3_mk_bvxor (unContext c) (unAST e1) (unAST e2) + +-- | Bitwise nand. +-- +-- Reference: +mkBvnand :: Context -> AST -> AST -> IO AST +mkBvnand c e1 e2 = checkError c $ AST <$> z3_mk_bvnand (unContext c) (unAST e1) (unAST e2) + +-- | Bitwise nor. +-- +-- Reference: +mkBvnor :: Context -> AST -> AST -> IO AST +mkBvnor c e1 e2 = checkError c $ AST <$> z3_mk_bvnor (unContext c) (unAST e1) (unAST e2) + +-- | Bitwise xnor. +-- +-- Reference: +mkBvxnor :: Context -> AST -> AST -> IO AST +mkBvxnor c e1 e2 = checkError c $ AST <$> z3_mk_bvxnor (unContext c) (unAST e1) (unAST e2) + +-- | Standard two's complement unary minus. +-- +-- Reference: AST -> IO AST +mkBvneg c e = checkError c $ AST <$> z3_mk_bvneg (unContext c) (unAST e) + +-- | Standard two's complement addition. +-- +-- Reference: +mkBvadd :: Context -> AST -> AST -> IO AST +mkBvadd c e1 e2 = checkError c $ AST <$> z3_mk_bvadd (unContext c) (unAST e1) (unAST e2) + +-- | Standard two's complement subtraction. +-- +-- Reference: +mkBvsub :: Context -> AST -> AST -> IO AST +mkBvsub c e1 e2 = checkError c $ AST <$> z3_mk_bvsub (unContext c) (unAST e1) (unAST e2) + +-- | Standard two's complement multiplication. +-- +-- Reference: +mkBvmul :: Context -> AST -> AST -> IO AST +mkBvmul c e1 e2 = checkError c $ AST <$> z3_mk_bvmul (unContext c) (unAST e1) (unAST e2) + +-- | Unsigned division. +-- +-- Reference: +mkBvudiv :: Context -> AST -> AST -> IO AST +mkBvudiv c e1 e2 = checkError c $ AST <$> z3_mk_bvudiv (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed division. +-- +-- Reference: +mkBvsdiv :: Context -> AST -> AST -> IO AST +mkBvsdiv c e1 e2 = checkError c $ AST <$> z3_mk_bvsdiv (unContext c) (unAST e1) (unAST e2) + +-- | Unsigned remainder. +-- +-- Reference: +mkBvurem :: Context -> AST -> AST -> IO AST +mkBvurem c e1 e2 = checkError c $ AST <$> z3_mk_bvurem (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed remainder (sign follows dividend). +-- +-- Reference: +mkBvsrem :: Context -> AST -> AST -> IO AST +mkBvsrem c e1 e2 = checkError c $ AST <$> z3_mk_bvsrem (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed remainder (sign follows divisor). +-- +-- Reference: +mkBvsmod :: Context -> AST -> AST -> IO AST +mkBvsmod c e1 e2 = checkError c $ AST <$> z3_mk_bvsmod (unContext c) (unAST e1) (unAST e2) + +-- | Unsigned less than. +-- +-- Reference: +mkBvult :: Context -> AST -> AST -> IO AST +mkBvult c e1 e2 = checkError c $ AST <$> z3_mk_bvult (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed less than. +-- +-- Reference: +mkBvslt :: Context -> AST -> AST -> IO AST +mkBvslt c e1 e2 = checkError c $ AST <$> z3_mk_bvslt (unContext c) (unAST e1) (unAST e2) + +-- | Unsigned less than or equal to. +-- +-- Reference: +mkBvule :: Context -> AST -> AST -> IO AST +mkBvule c e1 e2 = checkError c $ AST <$> z3_mk_bvule (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed less than or equal to. +-- +-- Reference: +mkBvsle :: Context -> AST -> AST -> IO AST +mkBvsle c e1 e2 = checkError c $ AST <$> z3_mk_bvsle (unContext c) (unAST e1) (unAST e2) + +-- | Unsigned greater than or equal to. +-- +-- Reference: +mkBvuge :: Context -> AST -> AST -> IO AST +mkBvuge c e1 e2 = checkError c $ AST <$> z3_mk_bvuge (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed greater than or equal to. +-- +-- Reference: +mkBvsge :: Context -> AST -> AST -> IO AST +mkBvsge c e1 e2 = checkError c $ AST <$> z3_mk_bvsge (unContext c) (unAST e1) (unAST e2) + +-- | Unsigned greater than. +-- +-- Reference: +mkBvugt :: Context -> AST -> AST -> IO AST +mkBvugt c e1 e2 = checkError c $ AST <$> z3_mk_bvugt (unContext c) (unAST e1) (unAST e2) + +-- | Two's complement signed greater than. +-- +-- Reference: +mkBvsgt :: Context -> AST -> AST -> IO AST +mkBvsgt c e1 e2 = checkError c $ AST <$> z3_mk_bvsgt (unContext c) (unAST e1) (unAST e2) + +-- | Concatenate the given bit-vectors. +-- +-- Reference: +mkConcat :: Context -> AST -> AST -> IO AST +mkConcat c e1 e2 = checkError c $ AST <$> z3_mk_concat (unContext c) (unAST e1) (unAST e2) + +-- | Extract the bits high down to low from a bitvector of size m to yield a new +-- bitvector of size /n/, where /n = high - low + 1/. +-- +-- Reference: +mkExtract :: Context -> Int -> Int -> AST -> IO AST +mkExtract c j i e + = checkError c $ AST <$> z3_mk_extract (unContext c) (fromIntegral j) (fromIntegral i) (unAST e) + +-- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector +-- of size /m+i/, where /m/ is the size of the given bit-vector. +-- +-- Reference: +mkSignExt :: Context -> Int -> AST -> IO AST +mkSignExt c i e + = checkError c $ AST <$> z3_mk_sign_ext (unContext c) (fromIntegral i) (unAST e) + +-- | Extend the given bit-vector with zeros to the (unsigned) equivalent +-- bitvector of size /m+i/, where /m/ is the size of the given bit-vector. +-- +-- Reference: +mkZeroExt :: Context -> Int -> AST -> IO AST +mkZeroExt c i e + = checkError c $ AST <$> z3_mk_zero_ext (unContext c) (fromIntegral i) (unAST e) + +-- | Repeat the given bit-vector up length /i/. +-- +-- Reference: +mkRepeat :: Context -> Int -> AST -> IO AST +mkRepeat c i e + = checkError c $ AST <$> z3_mk_repeat (unContext c) (fromIntegral i) (unAST e) + +-- | Shift left. +-- +-- Reference: +mkBvshl :: Context -> AST -> AST -> IO AST +mkBvshl c e1 e2 = checkError c $ AST <$> z3_mk_bvshl (unContext c) (unAST e1) (unAST e2) + +-- | Logical shift right. +-- +-- Reference: +mkBvlshr :: Context -> AST -> AST -> IO AST +mkBvlshr c e1 e2 = checkError c $ AST <$> z3_mk_bvlshr (unContext c) (unAST e1) (unAST e2) + +-- | Arithmetic shift right. +-- +-- Reference: +mkBvashr :: Context -> AST -> AST -> IO AST +mkBvashr c e1 e2 = checkError c $ AST <$> z3_mk_bvashr (unContext c) (unAST e1) (unAST e2) + +-- | Rotate bits of /t1/ to the left /i/ times. +-- +-- Reference: +mkRotateLeft :: Context -> Int -> AST -> IO AST +mkRotateLeft c i e + = checkError c $ AST <$> z3_mk_rotate_left (unContext c) (fromIntegral i) (unAST e) + +-- | Rotate bits of /t1/ to the right /i/ times. +-- +-- Reference: +mkRotateRight :: Context -> Int -> AST -> IO AST +mkRotateRight c i e + = checkError c $ AST <$> z3_mk_rotate_right (unContext c) (fromIntegral i) (unAST e) + +-- | Rotate bits of /t1/ to the left /t2/ times. +-- +-- Reference: +mkExtRotateLeft :: Context -> AST -> AST -> IO AST +mkExtRotateLeft c e1 e2 + = checkError c $ AST <$> z3_mk_ext_rotate_left (unContext c) (unAST e1) (unAST e2) + +-- | Rotate bits of /t1/ to the right /t2/ times. +-- +-- Reference: +mkExtRotateRight :: Context -> AST -> AST -> IO AST +mkExtRotateRight c e1 e2 + = checkError c $ AST <$> z3_mk_ext_rotate_right (unContext c) (unAST e1) (unAST e2) + +-- | Create an /n/ bit bit-vector from the integer argument /t1/. +-- +-- Reference: +mkInt2bv :: Context -> Int -> AST -> IO AST +mkInt2bv c i e + = checkError c $ AST <$> z3_mk_int2bv (unContext c) (fromIntegral i) (unAST e) + +-- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false, +-- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative +-- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/. +-- If /is_signed/ is true, /t1/ is treated as a signed bit-vector. +-- +-- Reference: +mkBv2int :: Context -> AST -> Bool -> IO AST +mkBv2int c e is_signed + = checkError c $ AST <$> z3_mk_bv2int (unContext c) (unAST e) (unBool is_signed) + +-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/ +-- does not overflow. +-- +-- Reference: +mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST +mkBvaddNoOverflow c e1 e2 is_signed = + checkError c $ AST <$> z3_mk_bvadd_no_overflow (unContext c) (unAST e1) (unAST e2) + (unBool is_signed) + +-- | Create a predicate that checks that the bit-wise signed addition of /t1/ +-- and /t2/ does not underflow. +-- +-- Reference: +mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST +mkBvaddNoUnderflow c e1 e2 = + checkError c $ AST <$> z3_mk_bvadd_no_underflow (unContext c) (unAST e1) (unAST e2) + +-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/ +-- and /t2/ does not overflow. +-- +-- Reference: +mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST +mkBvsubNoOverflow c e1 e2 = + checkError c $ AST <$> z3_mk_bvsub_no_overflow (unContext c) (unAST e1) (unAST e2) + +-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and +-- /t2/ does not underflow. +-- +-- Reference: +mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST +mkBvsubNoUnderflow c e1 e2 = + checkError c $ AST <$> z3_mk_bvsub_no_underflow (unContext c) (unAST e1) (unAST e2) + +-- | Create a predicate that checks that the bit-wise signed division of /t1/ +-- and /t2/ does not overflow. +-- +-- Reference: +mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST +mkBvsdivNoOverflow c e1 e2 = + checkError c $ AST <$> z3_mk_bvsdiv_no_overflow (unContext c) (unAST e1) (unAST e2) + +-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as +-- a signed bit-vector. +-- +-- Reference: +mkBvnegNoOverflow :: Context -> AST -> IO AST +mkBvnegNoOverflow c e = + checkError c $ AST <$> z3_mk_bvneg_no_overflow (unContext c) (unAST e) + +-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and +-- /t2/ does not overflow. +-- +-- Reference: +mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST +mkBvmulNoOverflow c e1 e2 is_signed = + checkError c $ AST <$> z3_mk_bvmul_no_overflow (unContext c) (unAST e1) (unAST e2) + (unBool is_signed) + +-- | Create a predicate that checks that the bit-wise signed multiplication of +-- /t1/ and /t2/ does not underflow. +-- +-- Reference: +mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST +mkBvmulNoUnderflow c e1 e2 = + checkError c $ AST <$> z3_mk_bvmul_no_underflow (unContext c) (unAST e1) (unAST e2) + +--------------------------------------------------------------------- +-- Arrays + +-- | Array read. The argument a is the array and i is the index of the array +-- that gets read. +-- +-- Reference: +mkSelect :: Context -> AST -> AST -> IO AST +mkSelect c a1 a2 = checkError c $ AST <$> z3_mk_select (unContext c) (unAST a1) (unAST a2) + +-- | Array update.   +-- +-- Reference: +mkStore :: Context -> AST -> AST -> AST -> IO AST +mkStore c a1 a2 a3 = checkError c $ AST <$> z3_mk_store (unContext c) (unAST a1) (unAST a2) (unAST a3) + +-- | Create the constant array. +-- +-- Reference: +mkConstArray :: Context -> Sort -> AST -> IO AST +mkConstArray c s a = checkError c $ AST <$> z3_mk_const_array (unContext c) (unSort s) (unAST a) + +-- | map f on the the argument arrays. +-- +-- Reference: +mkMap :: Context -> FuncDecl -> Int -> [AST] -> IO AST +mkMap c f n args = withArray (map unAST args) $ \args' -> + checkError c $ AST <$> z3_mk_map (unContext c) (unFuncDecl f) (fromIntegral n) args' + +-- | Access the array default value. Produces the default range value, for +-- arrays that can be represented as finite maps with a default range value. +-- +-- Reference: +mkArrayDefault :: Context -> AST -> IO AST +mkArrayDefault c a = checkError c $ AST <$> z3_mk_array_default (unContext c) (unAST a) + +-- TODO Sets + +--------------------------------------------------------------------- +-- Numerals + +-- | Create a numeral of a given sort. +-- +-- Reference: +mkNumeral :: Context -> String -> Sort -> IO AST +mkNumeral c str s = + withCString str $ \cstr-> + checkError c $ AST <$> z3_mk_numeral (unContext c) cstr (unSort s) + +------------------------------------------------- +-- Numerals / Integers + +-- | Create a numeral of sort /int/. +mkInt :: Integral a => Context -> a -> IO AST +mkInt c n = mkIntSort c >>= mkNumeral c n_str + where n_str = show $ toInteger n + +{-# INLINE mkIntZ3 #-} +mkIntZ3 :: Context -> Int32 -> Sort -> IO AST +mkIntZ3 c n s = checkError c $ AST <$> z3_mk_int (unContext c) cn (unSort s) + where cn = fromIntegral n :: CInt + +{-# INLINE mkUnsignedIntZ3 #-} +mkUnsignedIntZ3 :: Context -> Word32 -> Sort -> IO AST +mkUnsignedIntZ3 c n s = checkError c $ AST <$> z3_mk_unsigned_int (unContext c) cn (unSort s) + where cn = fromIntegral n :: CUInt + +{-# INLINE mkInt64Z3 #-} +mkInt64Z3 :: Context -> Int64 -> Sort -> IO AST +mkInt64Z3 c n s = checkError c $ AST <$> z3_mk_int64 (unContext c) cn (unSort s) + where cn = fromIntegral n :: CLLong + +{-# INLINE mkUnsignedInt64Z3 #-} +mkUnsignedInt64Z3 :: Context -> Word64 -> Sort -> IO AST +mkUnsignedInt64Z3 c n s = + checkError c $ AST <$> z3_mk_unsigned_int64 (unContext c) cn (unSort s) + where cn = fromIntegral n :: CULLong + +{-# RULES "mkInt/mkInt_IntZ3" mkInt = mkInt_IntZ3 #-} +mkInt_IntZ3 :: Context -> Int32 -> IO AST +mkInt_IntZ3 c n = mkIntSort c >>= mkIntZ3 c n + +{-# RULES "mkInt/mkInt_UnsignedIntZ3" mkInt = mkInt_UnsignedIntZ3 #-} +mkInt_UnsignedIntZ3 :: Context -> Word32 -> IO AST +mkInt_UnsignedIntZ3 c n = mkIntSort c >>= mkUnsignedIntZ3 c n + +{-# RULES "mkInt/mkInt_Int64Z3" mkInt = mkInt_Int64Z3 #-} +mkInt_Int64Z3 :: Context -> Int64 -> IO AST +mkInt_Int64Z3 c n = mkIntSort c >>= mkInt64Z3 c n + +{-# RULES "mkInt/mkInt_UnsignedInt64Z3" mkInt = mkInt_UnsignedInt64Z3 #-} +mkInt_UnsignedInt64Z3 :: Context -> Word64 -> IO AST +mkInt_UnsignedInt64Z3 c n = mkIntSort c >>= mkUnsignedInt64Z3 c n + +------------------------------------------------- +-- Numerals / Reals + +-- | Create a numeral of sort /real/. +mkReal :: Real r => Context -> r -> IO AST +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 + +{-# RULES "mkReal/mkRealZ3" mkReal = mkRealZ3 #-} +mkRealZ3 :: Context -> Ratio Int32 -> IO AST +mkRealZ3 c r = checkError c $ AST <$> z3_mk_real (unContext c) 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 +mkReal_IntZ3 c n = mkRealSort c >>= mkIntZ3 c n + +{-# RULES "mkReal/mkReal_UnsignedIntZ3" mkReal = mkReal_UnsignedIntZ3 #-} +mkReal_UnsignedIntZ3 :: Context -> Word32 -> IO AST +mkReal_UnsignedIntZ3 c n = mkRealSort c >>= mkUnsignedIntZ3 c n + +{-# RULES "mkReal/mkReal_Int64Z3" mkReal = mkReal_Int64Z3 #-} +mkReal_Int64Z3 :: Context -> Int64 -> IO AST +mkReal_Int64Z3 c n = mkRealSort c >>= mkInt64Z3 c n + +{-# RULES "mkReal/mkReal_UnsignedInt64Z3" mkReal = mkReal_UnsignedInt64Z3 #-} +mkReal_UnsignedInt64Z3 :: Context -> Word64 -> IO AST +mkReal_UnsignedInt64Z3 c n = mkRealSort c >>= mkUnsignedInt64Z3 c n + +--------------------------------------------------------------------- +-- Quantifiers + +mkPattern :: Context -> [AST] -> IO Pattern +mkPattern _ [] = error "Z3.Base.mkPattern: empty list of expressions" +mkPattern c es = + withArray (map unAST es) $ \aptr -> + checkError c $ Pattern <$> z3_mk_pattern (unContext c) n aptr + where n = genericLength es + +mkBound :: Context -> Int -> Sort -> IO AST +mkBound c i s + | i >= 0 = checkError c $ AST <$> z3_mk_bound (unContext c) (fromIntegral i) (unSort s) + | otherwise = error "Z3.Base.mkBound: negative de-Bruijn index" + +mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST +mkForall c pats x s p + = withArray (map unPattern pats) $ \patsPtr -> + withArray (map unSymbol x ) $ \xptr -> + withArray (map unSort s ) $ \sptr -> + checkError c $ AST <$> z3_mk_forall cptr 0 n patsPtr len sptr xptr (unAST p) + where n = genericLength pats + cptr = unContext c + len + | l == 0 = error "Z3.Base.mkForall:\ + \ forall with 0 bound variables" + | l /= length x = error "Z3.Base.mkForall:\ + \ different number of symbols and sorts" + | otherwise = fromIntegral l + where l = length s + +mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST +mkExists c pats x s p + = withArray (map unPattern pats) $ \patsPtr -> + withArray (map unSymbol x ) $ \xptr -> + withArray (map unSort s ) $ \sptr -> + checkError c $ AST <$> z3_mk_exists cptr 0 n patsPtr len sptr xptr (unAST p) + where n = fromIntegral $ length pats + cptr = unContext c + len + | l == 0 = error "Z3.Base.mkForall:\ + \ forall with 0 bound variables" + | l /= length x = error "Z3.Base.mkForall:\ + \ different number of symbols and sorts" + | otherwise = fromIntegral l + where l = length s + +--------------------------------------------------------------------- +-- Accessors + +-- | Return the size of the given bit-vector sort. +-- +-- Reference: +getBvSortSize :: Context -> Sort -> IO Int +getBvSortSize c s = + checkError c $ fromIntegral <$> z3_get_bv_sort_size (unContext c) (unSort s) + +-- | Return the sort of an AST node. +-- +-- Reference: +getSort :: Context -> AST -> IO Sort +getSort c e = checkError c $ Sort <$> z3_get_sort (unContext c) (unAST e) + +-- | Cast a 'Z3_lbool' from Z3.Base.C to @Bool@. +castLBool :: Z3_lbool -> Maybe Bool +castLBool lb + | lb == z3_l_true = Just True + | lb == z3_l_false = Just False + | lb == z3_l_undef = Nothing + | otherwise = error "Z3.Base.castLBool: illegal `Z3_lbool' value" + +-- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF +-- otherwise. +-- +-- Reference: +getBool :: Context -> AST -> IO (Maybe Bool) +getBool c a = checkError c $ castLBool <$> z3_get_bool_value (unContext c) (unAST a) + +-- | Return numeral value, as a string of a numeric constant term. +-- +-- Reference: +getNumeralString :: Context -> AST -> IO String +getNumeralString c a = checkError c $ peekCString =<< z3_get_numeral_string ctxPtr (unAST a) + where ctxPtr = unContext c + +-- | Return 'Z3Int' value +getInt :: Context -> AST -> IO Integer +getInt c a = read <$> getNumeralString c a + +-- | Return 'Z3Real' value +getReal :: Context -> AST -> 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" + + parseDen :: String -> Integer + parseDen "" = 1 + parseDen ('/':sj) = read sj + parseDen _ = error "Z3.Base.getReal: no parse" + + +-- TODO Modifiers + +--------------------------------------------------------------------- +-- Models + +-- | Evaluate an AST node in the given model. +eval :: Context -> Model -> AST -> IO (Maybe AST) +eval ctx m a = + alloca $ \aptr2 -> + checkError ctx $ z3_eval ctxPtr (unModel m) (unAST a) aptr2 >>= peekAST aptr2 . toBool + where peekAST :: Ptr (Ptr Z3_ast) -> Bool -> IO (Maybe AST) + peekAST _p False = return Nothing + peekAST p True = Just . AST <$> peek p + + ctxPtr = unContext ctx + +-- | Evaluate a collection of AST nodes in the given model. +evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST)) +evalT c m = fmap T.sequence . T.mapM (eval c m) + +--------------------------------------------------------------------- +-- Constraints + +-- | Create a backtracking point. +-- +-- Reference: +push :: Context -> IO () +push c = checkError c $ z3_push $ unContext c + +-- | Backtrack /n/ backtracking points. +-- +-- Reference: +pop :: Context -> Int -> IO () +pop ctx cnt = checkError ctx $ z3_pop (unContext ctx) $ fromIntegral cnt + +-- TODO Constraints: Z3_get_num_scopes +-- TODO Constraints: Z3_persist_ast + +-- | Assert a constraing into the logical context. +-- +-- Reference: +assertCnstr :: Context -> AST -> IO () +assertCnstr ctx ast = checkError ctx $ z3_assert_cnstr (unContext ctx) (unAST ast) + +-- | Get model (logical context is consistent) +-- +-- Reference : +getModel :: Context -> IO (Result, Maybe Model) +getModel c = + alloca $ \mptr -> + checkError c (z3_check_and_get_model (unContext c) mptr) >>= \lb -> + (toResult lb,) <$> peekModel mptr + where peekModel :: Ptr (Ptr Z3_model) -> IO (Maybe Model) + peekModel p | p == nullPtr = return Nothing + | otherwise = mkModel <$> peek p + mkModel :: Ptr Z3_model -> Maybe Model + mkModel p | p == nullPtr = Nothing + | otherwise = Just $ Model p + +-- | Delete a model object. +-- +-- Reference: +delModel :: Context -> Model -> IO () +delModel c m = checkError c $ z3_del_model (unContext c) (unModel m) + +-- | Convert the given model into a string. +-- +-- Reference: +showModel :: Context -> Model -> IO String +showModel c m = checkError c $ z3_model_to_string (unContext c) (unModel m) >>= peekCString + +-- | Convert the given logical context into a string. +-- +-- Reference: +showContext :: Context -> IO String +showContext c = checkError c $ z3_context_to_string (unContext c) >>= peekCString + +-- | Check whether the given logical context is consistent or not. +-- +-- Reference: +check :: Context -> IO Result +check ctx = checkError ctx $ toResult <$> z3_check (unContext ctx) + +-- TODO Constraints: Z3_check_assumptions +-- TODO Constraints: Z3_get_implied_equalities + +-- TODO From section 'Constraints' on. + + +--------------------------------------------------------------------- +-- * Parameters + +mkParams :: Context -> IO Params +mkParams c = checkError c $ Params <$> z3_mk_params (unContext c) + +paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO () +paramsSetBool c params sym b = + checkError c $ z3_params_set_bool (unContext c) (unParams params) (unSymbol sym) (unBool b) + +paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO () +paramsSetUInt c params sym v = + checkError c $ z3_params_set_uint (unContext c) (unParams params) (unSymbol sym) + (fromIntegral v) + +paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO () +paramsSetDouble c params sym v = + checkError c $ z3_params_set_double (unContext c) (unParams params) (unSymbol sym) + (realToFrac v) + +paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO () +paramsSetSymbol c params sym v = + checkError c $ z3_params_set_symbol (unContext c) (unParams params) (unSymbol sym) + (unSymbol v) + +paramsToString :: Context -> Params -> IO String +paramsToString c (Params params) = + checkError c (z3_params_to_string (unContext c) params) >>= peekCString + + +--------------------------------------------------------------------- +-- Solvers + +{-# WARNING Logic + , mkSolver + , mkSimpleSolver + , mkSolverForLogic + , solverSetParams + , solverPush + , solverPop + , solverReset + , solverAssertCnstr + , solverAssertAndTrack + , solverCheck + , solverCheckAndGetModel + , solverGetReasonUnknown + "New Z3 API support is still incomplete and fragile: \ + \you may experience segmentation faults!" + #-} + +-- | Solvers available in Z3. +-- +-- These are described at +-- +-- /WARNING/: Support for solvers is fragile, you may experience segmentation +-- faults! +data Logic + = AUFLIA + -- ^ Closed formulas over the theory of linear integer arithmetic + -- and arrays extended with free sort and function symbols but + -- restricted to arrays with integer indices and values. + + | AUFLIRA + -- ^ Closed linear formulas with free sort and function symbols over + -- one- and two-dimentional arrays of integer index and real + -- value. + + | AUFNIRA + -- ^ Closed formulas with free function and predicate symbols over a + -- theory of arrays of arrays of integer index and real value. + + | LRA + -- ^ Closed linear formulas in linear real arithmetic. + + | QF_ABV + -- ^ Closed quantifier-free formulas over the theory of bitvectors + -- and bitvector arrays. + + | QF_AUFBV + -- ^ Closed quantifier-free formulas over the theory of bitvectors + -- and bitvector arrays extended with free sort and function + -- symbols. + + | QF_AUFLIA + -- ^ Closed quantifier-free linear formulas over the theory of + -- integer arrays extended with free sort and function symbols. + + | QF_AX + -- ^ Closed quantifier-free formulas over the theory of arrays with + -- extensionality. + + | QF_BV + -- ^ Closed quantifier-free formulas over the theory of fixed-size + -- bitvectors. + + | QF_IDL + -- ^ Difference Logic over the integers. In essence, Boolean + -- combinations of inequations of the form x - y < b where x and y + -- are integer variables and b is an integer constant. + + | QF_LIA + -- ^ Unquantified linear integer arithmetic. In essence, Boolean + -- combinations of inequations between linear polynomials over + -- integer variables. + + | QF_LRA + -- ^ Unquantified linear real arithmetic. In essence, Boolean + -- combinations of inequations between linear polynomials over + -- real variables. + + | QF_NIA + -- ^ Quantifier-free integer arithmetic. + + | QF_NRA + -- ^ Quantifier-free real arithmetic. + + | QF_RDL + -- ^ Difference Logic over the reals. In essence, Boolean + -- combinations of inequations of the form x - y < b where x and y + -- are real variables and b is a rational constant. + + | QF_UF + -- ^ Unquantified formulas built over a signature of uninterpreted + -- (i.e., free) sort and function symbols. + + | QF_UFBV + -- ^ Unquantified formulas over bitvectors with uninterpreted sort + -- function and symbols. + + | QF_UFIDL + -- ^ Difference Logic over the integers (in essence) but with + -- uninterpreted sort and function symbols. + + | QF_UFLIA + -- ^ Unquantified linear integer arithmetic with uninterpreted sort + -- and function symbols. + + | QF_UFLRA + -- ^ Unquantified linear real arithmetic with uninterpreted sort and + -- function symbols. + + | QF_UFNRA + -- ^ Unquantified non-linear real arithmetic with uninterpreted sort + -- and function symbols. + + | UFLRA + -- ^ Linear real arithmetic with uninterpreted sort and function + -- symbols. + + | UFNIA + -- ^ Non-linear integer arithmetic with uninterpreted sort and + -- function symbols. + +instance Show Logic where + show AUFLIA = "AUFLIA" + show AUFLIRA = "AUFLIRA" + show AUFNIRA = "AUFNIRA" + show LRA = "LRA" + show QF_ABV = "QF_ABV" + show QF_AUFBV = "QF_AUFBV" + show QF_AUFLIA = "QF_AUFLIA" + show QF_AX = "QF_AX" + show QF_BV = "QF_BV" + show QF_IDL = "QF_IDL" + show QF_LIA = "QF_LIA" + show QF_LRA = "QF_LRA" + show QF_NIA = "QF_NIA" + show QF_NRA = "QF_NRA" + show QF_RDL = "QF_RDL" + show QF_UF = "QF_UF" + show QF_UFBV = "QF_UFBV" + show QF_UFIDL = "QF_UFIDL" + show QF_UFLIA = "QF_UFLIA" + show QF_UFLRA = "QF_UFLRA" + show QF_UFNRA = "QF_UFNRA" + show UFLRA = "UFLRA" + show UFNIA = "UFNIA" + +mkSolver :: Context -> IO Solver +mkSolver c = checkError c $ Solver <$> z3_mk_solver (unContext c) + +mkSimpleSolver :: Context -> IO Solver +mkSimpleSolver c = checkError c $ Solver <$> z3_mk_simple_solver (unContext c) + +mkSolverForLogic :: Context -> Logic -> IO Solver +mkSolverForLogic c logic = + do sym <- mkStringSymbol c (show logic) + checkError c $ Solver <$> z3_mk_solver_for_logic (unContext c) (unSymbol sym) + +solverSetParams :: Context -> Solver -> Params -> IO () +solverSetParams c solver params = + checkError c $ z3_solver_set_params (unContext c) (unSolver solver) (unParams params) + +solverPush :: Context -> Solver -> IO () +solverPush c solver = checkError c $ z3_solver_push (unContext c) (unSolver solver) + +solverPop :: Context -> Solver -> Int -> IO () +solverPop c solver i = + checkError c $ z3_solver_pop (unContext c) (unSolver solver) (fromIntegral i) + +solverReset :: Context -> Solver -> IO () +solverReset c solver = checkError c $ z3_solver_reset (unContext c) (unSolver solver) + +solverAssertCnstr :: Context -> Solver -> AST -> IO () +solverAssertCnstr c solver ast = + checkError c $ z3_solver_assert (unContext c) (unSolver solver) (unAST ast) + +solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO () +solverAssertAndTrack c solver constraint var = + checkError c $ z3_solver_assert_and_track (unContext c) (unSolver solver) + (unAST constraint) (unAST var) + +solverCheck :: Context -> Solver -> IO Result +solverCheck c solver = + checkError c $ toResult <$> z3_solver_check (unContext c) (unSolver solver) + +solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model) +solverCheckAndGetModel c (Solver s) = + do res <- checkError c $ toResult <$> z3_solver_check cptr s + mmodel <- case res of + Sat -> checkError c $ (Just . Model) <$> z3_solver_get_model cptr s + _ -> return Nothing + return (res, mmodel) + where cptr = unContext c + +solverGetReasonUnknown :: Context -> Solver -> IO String +solverGetReasonUnknown c solver = + checkError c $ z3_solver_get_reason_unknown (unContext c) (unSolver solver) >>= peekCString + +--------------------------------------------------------------------- +-- String Conversion + +-- | Pretty-printing mode for converting ASTs to strings. The mode +-- can be one of the following: +-- +-- * Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format. +-- +-- * Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format. +-- +-- * Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x +-- compliant format. +-- +-- * Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x +-- compliant format. +data ASTPrintMode + = Z3_PRINT_SMTLIB_FULL + | Z3_PRINT_LOW_LEVEL + | Z3_PRINT_SMTLIB_COMPLIANT + | Z3_PRINT_SMTLIB2_COMPLIANT + +-- | Set the pretty-printing mode for converting ASTs to strings. +setASTPrintMode :: Context -> ASTPrintMode -> IO () +setASTPrintMode ctx Z3_PRINT_SMTLIB_FULL = + checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_smtlib_full +setASTPrintMode ctx Z3_PRINT_LOW_LEVEL = + checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_low_level +setASTPrintMode ctx Z3_PRINT_SMTLIB_COMPLIANT = + checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_smtlib_compliant +setASTPrintMode ctx Z3_PRINT_SMTLIB2_COMPLIANT = + checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_smtlib2_compliant + +-- | Convert an AST to a string. +astToString :: Context -> AST -> IO String +astToString ctx ast = + checkError ctx $ z3_ast_to_string (unContext ctx) (unAST ast) >>= peekCString + +-- | Convert a pattern to a string. +patternToString :: Context -> Pattern -> IO String +patternToString ctx pattern = + checkError ctx $ z3_pattern_to_string (unContext ctx) (unPattern pattern) >>= peekCString + +-- | Convert a sort to a string. +sortToString :: Context -> Sort -> IO String +sortToString ctx sort = + checkError ctx $ z3_sort_to_string (unContext ctx) (unSort sort) >>= peekCString + +-- | Convert a FuncDecl to a string. +funcDeclToString :: Context -> FuncDecl -> IO String +funcDeclToString ctx funcDecl = + checkError ctx $ z3_func_decl_to_string (unContext ctx) (unFuncDecl funcDecl) >>= peekCString diff --git a/Z3/Base/C.hsc b/Z3/Base/C.hsc --- a/Z3/Base/C.hsc +++ b/Z3/Base/C.hsc @@ -3,14 +3,13 @@ -- | -- Module : Z3.Base.C --- Copyright : (c) Iago Abal, 2012 --- (c) David Castro, 2012 +-- Copyright : (c) Iago Abal, 2012-2013 +-- (c) David Castro, 2012-2013 -- License : BSD3 -- Maintainer: Iago Abal , -- David Castro -- -- Low-level bindings, highly inspired by yices-painless. --- module Z3.Base.C where @@ -48,13 +47,20 @@ -- | A kind of AST used to represent constant and function declarations. data Z3_app --- | 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. -data Z3_pattern +data Z3_pattern -- | A model for the constraints asserted into the logical context. data Z3_model +-- | A solver for Z3, that is, an engine for collecting and solving +-- constraints using a specific algorithm or set of algorithms. +data Z3_solver + +-- | A parameter set for Z3. +data Z3_params + -- | Lifted Boolean type: false, undefined, true. type Z3_lbool = CInt @@ -67,6 +73,9 @@ -- | Boolean type. It is just an alias for int. type Z3_bool = CInt +-- | Z3 custom error handler +type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO () + -- | Z3_bool values z3_true, z3_false :: Z3_lbool z3_true = #const Z3_TRUE @@ -75,27 +84,53 @@ -- | Z3 String type type Z3_string = CString +-- | Z3 pretty-printing modes +type Z3_ast_print_mode = CInt +z3_print_smtlib_full :: Z3_ast_print_mode +z3_print_smtlib_full = #const Z3_PRINT_SMTLIB_FULL +z3_print_low_level :: Z3_ast_print_mode +z3_print_low_level = #const Z3_PRINT_LOW_LEVEL +z3_print_smtlib_compliant :: Z3_ast_print_mode +z3_print_smtlib_compliant = #const Z3_PRINT_SMTLIB_COMPLIANT +z3_print_smtlib2_compliant :: Z3_ast_print_mode +z3_print_smtlib2_compliant = #const Z3_PRINT_SMTLIB2_COMPLIANT + +-- | Z3 error codes +type Z3_error_code = CInt +#{enum Z3_error_code, + , z3_ok = Z3_OK + , z3_sort_error = Z3_SORT_ERROR + , z3_iob = Z3_IOB + , z3_invalid_arg = Z3_INVALID_ARG + , z3_parser_error = Z3_PARSER_ERROR + , z3_no_parser = Z3_NO_PARSER + , z3_invalid_pattern = Z3_INVALID_PATTERN + , z3_memout_fail = Z3_MEMOUT_FAIL + , z3_file_access_error = Z3_FILE_ACCESS_ERROR + , z3_internal_fatal = Z3_INTERNAL_FATAL + , z3_invalid_usage = Z3_INVALID_USAGE + , z3_dec_ref_error = Z3_DEC_REF_ERROR + , z3_exception = Z3_EXCEPTION + } + --------------------------------------------------------------------- -- * Create configuration -- | Create a configuration. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_config" z3_mk_config :: IO (Ptr Z3_config) -- | Delete the given configuration object. -- -- Reference: --- foreign import ccall unsafe "Z3_del_config" z3_del_config :: Ptr Z3_config -> IO () -- | Set a configuration parameter. -- -- Reference: --- foreign import ccall unsafe "Z3_set_param_value" z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO () @@ -106,25 +141,21 @@ -- | Create a context using the given configuration. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_context" z3_mk_context :: Ptr Z3_config -> IO (Ptr Z3_context) -- | Delete the given logical context. -- -- Reference: --- foreign import ccall unsafe "Z3_del_context" z3_del_context :: Ptr Z3_context -> IO () - --------------------------------------------------------------------- -- * Symbols -- | Create a Z3 symbol using a C string. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_string_symbol" z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol) @@ -138,34 +169,44 @@ -- | Create the Boolean type. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_bool_sort" z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Create an integer type. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_int_sort" z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Create a real type. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_real_sort" z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- TODO Sorts: from Z3_mk_real_sort on +-- | Create a bit-vector type of the given size. +-- +-- This type can also be seen as a machine integer. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bv_sort" + z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort) +-- | Create an array type +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_array_sort" + z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort) +-- TODO Sorts: from Z3_mk_array_sort on + + --------------------------------------------------------------------- -- * Constants and Applications -- | Declare a constant or function. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_func_decl" z3_mk_func_decl :: Ptr Z3_context -> Ptr Z3_symbol @@ -177,7 +218,6 @@ -- | Create a constant or function application. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_app" z3_mk_app :: Ptr Z3_context -> Ptr Z3_func_decl @@ -188,7 +228,6 @@ -- | Declare and create a constant. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_const" z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast) @@ -201,220 +240,548 @@ -- | Create an AST node representing /true/. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_true" z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) -- | Create an AST node representing /false/. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_false" z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast) -- | Create an AST node representing l = r. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_eq" z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- TODO: Z3_mk_distinct +foreign import ccall unsafe "Z3_mk_distinct" + z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Create an AST node representing not(a). -- -- Reference: --- foreign import ccall unsafe "Z3_mk_not" z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create an AST node representing an if-then-else: ite(t1, t2, t3). -- -- Reference: --- foreign import ccall unsafe "Z3_mk_ite" z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing t1 iff t2. +-- | Create an AST node representing t1 iff t2. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_iff" z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing t1 implies t2. +-- | Create an AST node representing t1 implies t2. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_implies" z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing t1 xor t2. +-- | Create an AST node representing t1 xor t2. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_xor" z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create an AST node representing args[0] and ... and args[num_args-1]. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_and" z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | 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: --- foreign import ccall unsafe "Z3_mk_or" z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Arithmetic: Integers and Reals --- | Create an AST node representing args[0] + ... + args[num_args-1]. +-- | Create an AST node representing args[0] + ... + args[num_args-1]. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_add" z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Create an AST node representing args[0] * ... * args[num_args-1]. +-- | Create an AST node representing args[0] * ... * args[num_args-1]. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_mul" z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Create an AST node representing args[0] - ... - args[num_args - 1]. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_sub" z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) -- | Create an AST node representing -arg. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_unary_minus" z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create an AST node representing arg1 div arg2. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_div" z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create an AST node representing arg1 mod arg2. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_mod" z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create an AST node representing arg1 rem arg2. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_rem" z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create less than. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_lt" z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create less than or equal to. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_le" z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create greater than. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_gt" z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Create greater than or equal to. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_ge" z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Coerce an integer to a real. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_int2real" z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Coerce a real to an integer. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_real2int" z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -- | Check if a real number is an integer. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_is_int" z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- TODO Bit-vectors, Arrays, Sets +--------------------------------------------------------------------- +-- * Bit-vectors +-- | Bitwise negation. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvnot" + z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Take conjunction of bits in vector, return vector of length 1. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvredand" + z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Take disjunction of bits in vector, return vector of length 1. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvredor" + z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Bitwise and. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvand" + z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Bitwise or. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvor" + z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Bitwise exclusive-or. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvxor" + z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Bitwise nand. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvnand" + z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Bitwise nor. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvnor" + z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Bitwise xnor. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvxnor" + z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Standard two's complement unary minus. +-- +-- Reference: Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Standard two's complement addition. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvadd" + z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Standard two's complement subtraction. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsub" + z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Standard two's complement multiplication. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvmul" + z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Unsigned division. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvudiv" + z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed division. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsdiv" + z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Unsigned remainder. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvurem" + z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed remainder (sign follows dividend). +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsrem" + z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed remainder (sign follows divisor). +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsmod" + z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Unsigned less than. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvult" + z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed less than. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvslt" + z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Unsigned less than or equal to. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvule" + z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed less than or equal to. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsle" + z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Unsigned greater than or equal to. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvuge" + z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed greater than or equal to. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvsge" + z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Unsigned greater than. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvugt" + z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Two's complement signed greater than. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvsgt" + z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Concatenate the given bit-vectors. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_concat" + z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Extract the bits high down to low from a bitvector of size m to yield a new +-- bitvector of size /n/, where /n = high - low + 1/. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_extract" + z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector +-- of size /m+i/, where /m/ is the size of the given bit-vector. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_sign_ext" + z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Extend the given bit-vector with zeros to the (unsigned) equivalent +-- bitvector of size /m+i/, where /m/ is the size of the given bit-vector. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_zero_ext" + z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Repeat the given bit-vector up length /i/. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_repeat" + z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Shift left. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvshl" + z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Logical shift right. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvlshr" + z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Arithmetic shift right. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_bvashr" + z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Rotate bits of /t1/ to the left /i/ times. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_rotate_left" + z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Rotate bits of /t1/ to the right /i/ times. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_rotate_right" + z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Rotate bits of /t1/ to the left /t2/ times. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_ext_rotate_left" + z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Rotate bits of /t1/ to the right /t2/ times. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_ext_rotate_right" + z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create an /n/ bit bit-vector from the integer argument /t1/. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_mk_int2bv" + z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false, +-- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative +-- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/. +-- If /is_signed/ is true, /t1/ is treated as a signed bit-vector. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bv2int" + z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/ +-- does not overflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvadd_no_overflow" + z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise signed addition of /t1/ +-- and /t2/ does not underflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvadd_no_underflow" + z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/ +-- and /t2/ does not overflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsub_no_overflow" + z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and +-- /t2/ does not underflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsub_no_underflow" + z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise signed division of /t1/ +-- and /t2/ does not overflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvsdiv_no_overflow" + z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as +-- a signed bit-vector. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvneg_no_overflow" + z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and +-- /t2/ does not overflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvmul_no_overflow" + z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) + +-- | Create a predicate that checks that the bit-wise signed multiplication of +-- /t1/ and /t2/ does not underflow. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_bvmul_no_underflow" + z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-------------------------------------------------------------------------------- +-- * Arrays +-- | Array read. The argument a is the array and i is the index of the array +-- that gets read. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_select" + z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Array update.   +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_store" + z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Create the constant array. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_const_array" + z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | map f on the the argument arrays. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_map" + z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) + +-- | Access the array default value. Produces the default range value, for +-- arrays that can be represented as finite maps with a default range value. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_array_default" + z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- TODO Sets + --------------------------------------------------------------------- -- * Numerals -- | Create a numeral of a given sort. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_numeral" z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Create a real from a fraction. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_real" z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast) -- | Create a numeral of a given sort. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_int" z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Create a numeral of a given sort. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_unsigned_int" z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Create a numeral of a given sort. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_int64" z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Create a numeral of a given sort. -- -- Reference: --- foreign import ccall unsafe "Z3_mk_unsigned_int64" z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) @@ -424,21 +791,18 @@ -- | 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) @@ -446,23 +810,44 @@ -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- TODO From 'Z3_mk_exists' on. +-- | Create an exists formula. +-- +-- Referece: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407 +foreign import ccall unsafe "Z3_mk_exists" + z3_mk_exists :: Ptr Z3_context -> CUInt + -> CUInt -> Ptr (Ptr Z3_pattern) + -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_symbol) + -> Ptr Z3_ast + -> IO (Ptr Z3_ast) +-- TODO: Z3_mk_quantifier, Z3_mk_quantifier_ex, Z3_mk_forall_const, +-- Z3_mk_exists_const, Z3_mk_quantifier_const, Z3_mk_quantifier_const_ex + --------------------------------------------------------------------- -- * Accessors +-- | Return the size of the given bit-vector sort. +-- +-- Reference: +foreign import ccall unsafe "Z3_get_bv_sort_size" + z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt + +-- | Return the sort of an AST node. +-- +-- Reference: +foreign import ccall unsafe "Z3_get_sort" + z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) + -- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF -- otherwise. -- -- Reference: --- foreign import ccall unsafe "Z3_get_bool_value" z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool -- | Return numeral value, as a string of a numeric constant term. -- -- Reference: --- foreign import ccall unsafe "Z3_get_numeral_string" z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string @@ -475,7 +860,6 @@ -- and store the result in v. -- -- Reference: --- foreign import ccall unsafe "Z3_eval" z3_eval :: Ptr Z3_context -> Ptr Z3_model @@ -486,29 +870,31 @@ --------------------------------------------------------------------- -- * Constraints --- TODO Constraints: Z3_push +foreign import ccall unsafe "Z3_push" + z3_push :: Ptr Z3_context -> IO () + -- TODO Constraints: Z3_pop +foreign import ccall unsafe "Z3_pop" + z3_pop :: Ptr Z3_context -> CUInt -> IO () + -- TODO Constraints: Z3_get_num_scopes -- TODO Constraints: Z3_persist_ast -- | Assert a constraing into the logical context. -- -- Reference: --- foreign import ccall unsafe "Z3_assert_cnstr" z3_assert_cnstr :: Ptr Z3_context -> Ptr Z3_ast -> IO () -- | Check whether the given logical context is consistent or not. -- -- Reference : --- foreign import ccall unsafe "Z3_check_and_get_model" z3_check_and_get_model :: Ptr Z3_context -> Ptr (Ptr Z3_model) -> IO Z3_lbool --- | Check whether the given logical context is consistent or not. +-- | Check whether the given logical context is consistent or not. -- -- Reference: --- foreign import ccall unsafe "Z3_check" z3_check :: Ptr Z3_context -> IO Z3_lbool @@ -518,9 +904,256 @@ -- | Delete a model object. -- -- Reference: --- foreign import ccall unsafe "Z3_del_model" z3_del_model :: Ptr Z3_context -> Ptr Z3_model -> IO () +foreign import ccall unsafe "Z3_model_to_string" + z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO CString +foreign import ccall unsafe "Z3_context_to_string" + z3_context_to_string :: Ptr Z3_context -> IO CString + + -- TODO From section 'Constraints' on. + + +--------------------------------------------------------------------- +-- * Parameters + +-- | Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter +-- sets are used to configure many components such as: simplifiers, +-- tactics, solvers, etc. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_params" + z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params) + +-- | Increment the reference counter of the given parameter set. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_inc_ref" + z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () + +-- | Decrement the reference counter of the given parameter set. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_dec_ref" + z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () + +-- | Add a Boolean parameter k with value v to the parameter set p. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_set_bool" + z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> + Z3_bool -> IO () + +-- | Add an unsigned parameter k with value v to the parameter set p. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_set_uint" + z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> + CUInt -> IO () + +-- | Add a double parameter k with value v to the parameter set p. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_set_double" + z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> + CDouble -> IO () + +-- | Add a symbol parameter k with value v to the parameter set p. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_set_symbol" + z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> + Ptr Z3_symbol -> IO () + +-- | Convert a parameter set into a string. This function is mainly +-- used for printing the contents of a parameter set. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_to_string" + z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string + +{- +-- | Validate the parameter set p against the parameter description +-- set d. +-- +-- Reference: +foreign import ccall unsafe "Z3_params_validate" + z3_params_validate :: Ptr Z3_context -> Ptr Z3_params -> Z3_param_descrs -> IO () +-} + +--------------------------------------------------------------------- +-- * Solvers + +-- | Create an SMT solver that uses a set of builtin tactics. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_solver" + z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) + +-- | Create a simple solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_simple_solver" + z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) + +-- | Create a solver for a particular logic, as given by the SMTLIB +-- standard here: +-- +-- +-- +-- Reference: +foreign import ccall unsafe "Z3_mk_solver_for_logic" + z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver) + +-- | Set the parameters for a solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_set_params" + z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> + IO () + +-- | Increment the reference counter of the given solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_inc_ref" + z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () + +-- | Decrement the reference counter of the given solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_dec_ref" + z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () + +-- | Create a backtracking point in a solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_push" + z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO () + +-- | Backtrack to the nth-most recent backtracking point. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_pop" + z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO () + +-- | Remove all assertions from a solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_reset" + z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO () + +-- | Add a constraint to a solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_assert" + z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO () + +-- | Add a constraint to a solver and track it using a Boolean +-- constant, given as the last argument. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_assert_and_track" + z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver -> + Ptr Z3_ast -> Ptr Z3_ast -> IO () + +-- | Check whether the assertions in a given solver are consistent. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_check" + z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool + +-- | Retrieve the model for the last call to Z3_solver_check or +-- Z3_solver_check_assumptions on the given solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_get_model" + z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) + +-- | Return a brief justification for an "unknown" result (i.e., +-- Z3_L_UNDEF) for the last call to Z3_solver_check or +-- Z3_solver_check_assumptions on the given solver. +-- +-- Reference: +foreign import ccall unsafe "Z3_solver_get_reason_unknown" + z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> + IO Z3_string + +--------------------------------------------------------------------- +-- * String Conversion + +-- | Set the pretty-printing mode for converting ASTs to strings. The +-- mode can be one of the following: +-- +-- * z3_print_smtlib_full: Print AST nodes in SMTLIB verbose format. +-- +-- * z3_print_low_level: Print AST nodes using a low-level format. +-- +-- * z3_print_smtlib_compliant: Print AST nodes in SMTLIB 1.x +-- compliant format. +-- +-- * z3_print_smtlib2_compliant: Print AST nodes in SMTLIB 2.x +-- compliant format. +-- +-- Reference: +foreign import ccall unsafe "Z3_set_ast_print_mode" + z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO () + +-- | Convert an AST into a string using the current print mode. +-- +-- Reference: +foreign import ccall unsafe "Z3_ast_to_string" + z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string + +-- | Convert a pattern into a string using the current print mode. +-- +-- Reference: +foreign import ccall unsafe "Z3_pattern_to_string" + z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string + +-- | Convert a sort into a string using the current print mode. +-- +-- Reference: +foreign import ccall unsafe "Z3_sort_to_string" + z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string + +-- | Convert a func_decl into a string using the current print mode. +-- +-- Reference: +foreign import ccall unsafe "Z3_func_decl_to_string" + z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string + +--------------------------------------------------------------------- +-- * Error Handling + +-- | Return the error code for the last API call. +-- +-- Reference : +foreign import ccall unsafe "Z3_get_error_code" + z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code + +-- | Register a Z3 error handler. +-- +-- Reference : +foreign import ccall unsafe "Z3_set_error_handler" + z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO () + +-- | Set an error. +-- +-- Reference : +foreign import ccall unsafe "Z3_set_error" + z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO () + +-- | Return a string describing the given error code. +-- +-- Reference : +foreign import ccall unsafe "Z3_get_error_msg" + z3_get_error_msg :: Z3_error_code -> IO Z3_string + +-- | Return a string describing the given error code. +-- +-- Reference : +foreign import ccall unsafe "Z3_get_error_msg_ex" + z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string diff --git a/Z3/Lang.hs b/Z3/Lang.hs --- a/Z3/Lang.hs +++ b/Z3/Lang.hs @@ -7,7 +7,6 @@ -- Maintainer: Iago Abal , -- David Castro -- Stability : experimental --- module Z3.Lang ( module Z3.Lang.Prelude diff --git a/Z3/Lang/Exprs.hs b/Z3/Lang/Exprs.hs --- a/Z3/Lang/Exprs.hs +++ b/Z3/Lang/Exprs.hs @@ -3,6 +3,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeFamilies #-} @@ -14,25 +15,26 @@ -- Maintainer: Iago Abal , -- David Castro -- Stability : experimental --- module Z3.Lang.Exprs ( -- * Types - TypeZ3 - , Compilable(..) + Compilable(..) , IsTy(..) - , IsFun - + , IsFun(..) + , Castable(..) + -- ** Numeric types , IsNum , IsInt , IsReal - + -- * Abstract syntax , Uniq , Layout , Expr (..) , Pattern (..) + , Quantifier(..) + , QExpr(..) , FunApp (..) , BoolBinOp (..) , BoolMultiOp (..) @@ -53,49 +55,42 @@ ) where import {-# SOURCE #-} Z3.Lang.Monad ( Z3 ) +import Z3.Lang.TY 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 +-- Types -- | Compilable /things/. --- -class Base.Z3Type (TypeZ3 t) => Compilable t where - compile :: t -> Z3 (Base.AST (TypeZ3 t)) +class Compilable t where + compile :: t -> Z3 Base.AST -- | 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 + -- | Create a sort of the underlying Z3 type. + mkSort :: TY a -> Z3 Base.Sort + + -- | Create a value of the . + mkLiteral :: a -> Z3 Base.AST + + -- | Value extractor + getValue :: Base.AST -> Z3 a + + -- | Function types. --- -class Base.Z3Fun (TypeZ3 a) => IsFun a where +class IsFun a where + domain :: TY a -> Z3 [Base.Sort] + range :: TY a -> Z3 Base.Sort ------------------------------------------------------------ -- Numeric types @@ -105,38 +100,31 @@ -- 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 +class (IsTy a, Num 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 +class (IsNum a, Integral a) => 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 +class (IsNum a, Fractional a, Real a) => IsReal a where ------------------------------------------------------------ -- Abstract syntax -- | Unique identifiers. --- type Uniq = Int -- | Quantifier layout level. --- type Layout = Int --- | Abstract syntax. --- +-- | Expressions. data Expr :: * -> * where -- | Literals Lit :: IsTy a => a -> Expr a -- | Constants - Const :: !Uniq -> Base.AST (TypeZ3 a) -> Expr a + Const :: !Uniq -> Base.AST -> Expr a -- | Tag, for converting from HOAS to de-Bruijn Tag :: !Layout -> Expr a -- | Logical negation @@ -145,10 +133,8 @@ BoolBin :: BoolBinOp -> Expr Bool -> Expr Bool -> Expr Bool -- | Variadic boolean expressions BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool - -- | Forall formula - ForAll :: IsTy a => (Expr a -> Expr Bool) -- ^ body - -> Maybe (Expr a -> Pattern) -- ^ pattern - -> Expr Bool + -- | Quantified formula + Quant :: QExpr t => Quantifier -> t -> Expr Bool -- | Arithmetic negation Neg :: IsNum a => Expr a -> Expr a -- | Arithmetic expressions for commutative rings @@ -158,24 +144,37 @@ -- | Real arithmetic RealArith :: IsReal a => RealOp -> Expr a -> Expr a -> Expr a -- | Equality testing. - CmpE :: IsTy a => CmpOpE -> Expr a -> Expr a -> Expr Bool + CmpE :: IsTy a => CmpOpE -> [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 + -- | Casting between compatible types + Cast :: (IsTy a, IsTy b, Castable a b) => Expr a -> Expr b +-- | Quantifiable expressions. +class QExpr t where + compileQuant :: Quantifier -> [Base.Symbol] -> [Base.Sort] -> t -> Z3 Base.AST + +-- | Convertible types. +class (IsTy a, IsTy b) => Castable a b where + compileCast :: TY (a,b) -> Base.AST -> Z3 Base.AST + + -- | Quantifier pattern. --- data Pattern where Pat :: IsTy a => Expr a -> Pattern +-- | Quantifiers +data Quantifier = ForAll | Exists + deriving (Eq, Show) + -- | Z3 function --- data FunApp :: * -> * where -- | Function declaration - FuncDecl :: IsFun a => Base.FuncDecl (TypeZ3 a) -> FunApp a + FuncDecl :: IsFun a => Base.FuncDecl -> FunApp a -- | Partial application PApp :: IsTy a => FunApp (a -> b) -> Expr a -> FunApp b @@ -200,7 +199,7 @@ deriving (Eq,Show) -- | Equality testing. -data CmpOpE = Eq | Neq +data CmpOpE = Eq | Distinct deriving (Eq, Show, Typeable) -- | Ordering comparisons. diff --git a/Z3/Lang/Lg2.hs b/Z3/Lang/Lg2.hs --- a/Z3/Lang/Lg2.hs +++ b/Z3/Lang/Lg2.hs @@ -24,17 +24,16 @@ declareLg2 = do lg2::Expr a -> Expr a <- fun1 -- invariants - assert $ forallP (\x -> x >* 0 ==> lg2 x >=* 0) - (\x -> Pat $ lg2 x) - assert $ forallP (\x -> x >* 0 ==> lg2 x <* x) - (\x -> Pat $ lg2 x) + assert $ forall $ \x -> (x >* 0 ==> lg2 x >=* 0) `instanceWhen` [Pat $ lg2 x] + assert $ forall $ \x -> (x >* 0 ==> lg2 x <* x) `instanceWhen` [Pat $ lg2 x] + assert $ forall $ \x -> + x >* 0 ==> (lg2 (x+1) ==* lg2 x ||* lg2 (x+1) ==* 1 + lg2 x) -- base cases 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) + assert $ forall (\x -> lg2 (2*x) ==* 1 + lg2 x) + assert $ forall (\x -> lg2 (2*x+1) ==* lg2 (x+1)) -- and that's it! return lg2 + diff --git a/Z3/Lang/Monad.hs b/Z3/Lang/Monad.hs --- a/Z3/Lang/Monad.hs +++ b/Z3/Lang/Monad.hs @@ -13,6 +13,7 @@ -- David Castro -- Stability : experimental +-- TODO Discuss integration of pretty-printing functions from Z3.Monad module Z3.Lang.Monad ( -- * Z3 Monad Z3 @@ -20,56 +21,41 @@ , evalZ3 , Args(..) , stdArgs + , Logic(..) + , module Z3.Opts , 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 + , mkQuant , mkEq , mkCmp - , mkFuncDecl - , mkApp1 - , mkApp2 - , mkApp3 - , mkApp4 - , mkApp5 - , mkConst - , mkUnaryMinus , mkCRingArith , mkIntArith , mkRealArith - , mkIte -- * Satisfiability result - , Base.Result(..) + , Base.Result ) where import Z3.Lang.Exprs import qualified Z3.Base as Base +import qualified Z3.Monad as MonadZ3 +import Z3.Monad ( MonadZ3(..), Logic(..) ) +import Z3.Opts import Control.Applicative ( Applicative ) import Control.Monad.State +import qualified Data.Traversable as T --------------------------------------------------------------------- -- The Z3 Monad @@ -77,17 +63,18 @@ -- | Z3 monad. -- newtype Z3 a = Z3 (StateT Z3State IO a) - deriving (Functor, Applicative, Monad) + deriving (Functor, Applicative, Monad, MonadIO, MonadState Z3State) -instance MonadState Z3State Z3 where - get = Z3 $ StateT $ \s -> return (s,s) - put st = Z3 $ StateT $ \_ -> return ((), st) +instance MonadZ3 Z3 where + getSolver = Z3 $ gets solver + getContext = Z3 $ gets context -- | Internal state of Z3 monad. -- data Z3State = Z3State { uniqVal :: !Uniq , context :: Base.Context + , solver :: Maybe Base.Solver , qLayout :: !Layout } @@ -99,17 +86,16 @@ -- | 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 - } +evalZ3With args (Z3 s) = + Base.withConfig $ \cfg -> do + setArgs cfg args + Base.withContext cfg $ \ctx -> + do mbSolver <- T.mapM (Base.mkSolverForLogic ctx) $ logic args + evalStateT s Z3State { uniqVal = 0 + , context = ctx + , solver = mbSolver + , qLayout = 0 + } -- | Fresh symbol name. -- @@ -123,21 +109,34 @@ ------------------------------------------------- -- Arguments +{-# WARNING logic + "New Z3 API support is still incomplete and fragile: \ + \you may experience segmentation faults!" + #-} + data Args = Args { - softTimeout :: Maybe Int + logic :: Maybe Logic + -- ^ the logic to use; see + , softTimeout :: Maybe Int -- ^ soft timeout (in milliseconds) + , options :: Opts + -- ^ Z3 options } stdArgs :: Args stdArgs = Args { - softTimeout = Nothing + logic = Nothing + , softTimeout = Nothing + , options = stdOpts +? opt "MODEL" True + +? opt "MODEL_COMPLETION" True } -iniConfig :: Base.Config -> Args -> IO () -iniConfig cfg args = do +setArgs :: Base.Config -> Args -> IO () +setArgs cfg args = do Base.setParamValue cfg "SOFT_TIMEOUT" soft_timeout_val + setOpts cfg $ options args where soft_timeout_val = show $ maybe 0 id $ softTimeout args ------------------------------------------------- @@ -162,153 +161,50 @@ --------------------------------------------------------------------- -- 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 +mkBoolBin :: BoolBinOp -> Base.AST -> Base.AST -> Z3 Base.AST +mkBoolBin Xor = MonadZ3.mkXor +mkBoolBin Implies = MonadZ3.mkImplies +mkBoolBin Iff = MonadZ3.mkIff -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 +mkBoolMulti :: BoolMultiOp -> [Base.AST] -> Z3 Base.AST +mkBoolMulti And = MonadZ3.mkAnd +mkBoolMulti Or = MonadZ3.mkOr -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 +mkQuant :: Quantifier + -> [Base.Pattern] + -> [Base.Symbol] -> [Base.Sort] + -> Base.AST -> Z3 Base.AST +mkQuant ForAll = MonadZ3.mkForall +mkQuant Exists = MonadZ3.mkExists -mkConst :: Base.Z3Type a => Base.Symbol -> Base.Sort a -> Z3 (Base.AST a) -mkConst = liftZ3Op3 Base.mkConst +mkEq :: CmpOpE -> [Base.AST] -> Z3 Base.AST +mkEq Distinct = MonadZ3.mkDistinct +mkEq Eq = doMkEq + where doMkEq [e1,e2] + = MonadZ3.mkEq e1 e2 + doMkEq es + | length es < 2 = error "Z3.Lang.Monad.mkEq:\ + \ Invalid number of parameters." + | otherwise = join $ liftM (mkBoolMulti And) doEqs + where doEqs = mapM (uncurry $ MonadZ3.mkEq) pairs + pairs = init $ zip es $ tail $ cycle es -mkUnaryMinus :: Base.Z3Num a => Base.AST a -> Z3 (Base.AST a) -mkUnaryMinus = liftZ3Op2 Base.mkUnaryMinus +mkCmp :: CmpOpI -> Base.AST -> Base.AST -> Z3 Base.AST +mkCmp Le = MonadZ3.mkLe +mkCmp Lt = MonadZ3.mkLt +mkCmp Ge = MonadZ3.mkGe +mkCmp Gt = MonadZ3.mkGt -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 +mkCRingArith :: CRingOp -> [Base.AST] -> Z3 Base.AST +mkCRingArith Add = MonadZ3.mkAdd +mkCRingArith Mul = MonadZ3.mkMul +mkCRingArith Sub = MonadZ3.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 +mkIntArith :: IntOp -> Base.AST -> Base.AST -> Z3 Base.AST +mkIntArith Quot = MonadZ3.mkDiv +mkIntArith Mod = MonadZ3.mkMod +mkIntArith Rem = MonadZ3.mkRem -mkRealArith :: RealOp - -> Base.AST Rational -> Base.AST Rational - -> Z3 (Base.AST Rational) -mkRealArith Div = liftZ3Op3 Base.mkDiv +mkRealArith :: RealOp -> Base.AST -> Base.AST -> Z3 Base.AST +mkRealArith Div = MonadZ3.mkDiv -mkIte :: Base.AST Bool -> Base.AST a -> Base.AST a -> Z3 (Base.AST a) -mkIte = liftZ3Op4 Base.mkIte diff --git a/Z3/Lang/Nat.hs b/Z3/Lang/Nat.hs --- a/Z3/Lang/Nat.hs +++ b/Z3/Lang/Nat.hs @@ -1,6 +1,8 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} -- | @@ -15,11 +17,13 @@ ( Nat ) where -import Z3.Base ( AST ) +import Z3.Monad hiding ( Z3, mkEq, Pattern, evalZ3, evalZ3With ) import Z3.Lang.Exprs import Z3.Lang.Monad import Z3.Lang.Prelude +import Z3.Lang.TY +import Control.Applicative ( (<$>) ) import Data.Typeable newtype Nat = Nat { unNat :: Integer } @@ -46,17 +50,18 @@ 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 + mkSort _ = mkIntSort + mkLiteral = mkInt . unNat + getValue v = Nat <$> getInt v + + instance IsNum Nat where instance IsInt Nat where @@ -80,17 +85,18 @@ withHypo eb $ tcNat e1 withHypo (Not eb) $ tcNat e2 tcNat (App _) = ok +tcNat (Cast e) = tc e tcNat _ = error "Z3.Lang.Nat.tcNat: Panic!\ \ Impossible constructor in pattern matching!" -compileNat :: Expr Nat -> Z3 (AST Integer) +compileNat :: Expr Nat -> Z3 AST compileNat (Lit a) - = mkLiteral (toZ3Type a) + = mkLiteral (unNat a) compileNat (Const _ u) = return u compileNat (Tag lyt) = do ix <- deBruijnIx lyt - srt <- mkSort + srt <- mkSort (TY :: TY Nat) mkBound ix srt compileNat (Neg e) = mkUnaryMinus =<< compileNat e @@ -107,7 +113,12 @@ mkIte eb' e1' e2' compileNat (App e) = compile e +compileNat (Cast (e :: Expr a)) + = compile e >>= compileCast (TY :: TY (a, Nat)) compileNat _ = error "Z3.Lang.Nat.compileNat: Panic!\ \ Impossible constructor in pattern matching!" + +instance Castable Nat Integer where + compileCast _ = return diff --git a/Z3/Lang/Pow2.hs b/Z3/Lang/Pow2.hs --- a/Z3/Lang/Pow2.hs +++ b/Z3/Lang/Pow2.hs @@ -25,18 +25,18 @@ declarePow2 = do pow2::Expr a -> Expr a <- fun1 -- invariants - assert $ forallP (\x -> x <* 0 ==> pow2 x ==* 0) - (\x -> Pat $ pow2 x) - assert $ forallP (\x -> x >=* 0 ==> pow2 x >* 0) - (\x -> Pat $ pow2 x) - assert $ forallP (\x -> x >=* 0 ==> pow2 x >* x) - (\x -> Pat $ pow2 x) + assert $ forall $ \x -> (x <* 0 ==> pow2 x ==* 0) + `instanceWhen` [Pat $ pow2 x] + assert $ forall $ \x -> (x >=* 0 ==> pow2 x >* 0) + `instanceWhen` [Pat $ pow2 x] + assert $ forall $ \x -> (x >=* 0 ==> pow2 x >* x) + `instanceWhen` [Pat $ pow2 x] -- base cases assert $ pow2 0 ==* 1 assert $ pow2 1 ==* 2 -- recursive definition - assert $ forallP (\x -> x >* 1 ==> pow2 x ==* 2 * pow2 (x-1)) - (\x -> Pat $ pow2 x) + assert $ forall $ \x -> (x >* 1 ==> pow2 x ==* 2 * pow2 (x-1)) + `instanceWhen` [Pat $ pow2 x] -- and that's it! return pow2 diff --git a/Z3/Lang/Prelude.hs b/Z3/Lang/Prelude.hs --- a/Z3/Lang/Prelude.hs +++ b/Z3/Lang/Prelude.hs @@ -1,27 +1,28 @@ {-# 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 #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# 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 +-- Copyright : (c) Iago Abal, 2012-2013 +-- (c) David Castro, 2012-2013 -- License : BSD3 -- Maintainer: Iago Abal , -- David Castro -- Stability : experimental --- -- TODO: Pretty-printing of expressions @@ -29,19 +30,31 @@ -- * Z3 script Z3 - , Base.Result(..) + , Base.Result , evalZ3 , Args(..) , stdArgs + , Logic(..) , evalZ3With -- ** Commands , var + , namedVar , fun1, fun2, fun3, fun4, fun5 , assert , let_ , check + , showContext + , exprToString + , push, pop + + -- ** Models + , Model , checkModel + , checkModelWith + , checkModelWithResult + , showModel + , eval, evalT -- * Expressions , Expr @@ -50,16 +63,20 @@ , IsNum , IsInt , IsReal + , Castable , literal , true , false , not_ , and_, (&&*) , or_, (||*) + , distinct , xor , implies, (==>) , iff, (<=>) - , forall, forallP + , forall + , exists + , instanceWhen , (//), (%*), (%%) , divides , (==*), (/=*) @@ -67,17 +84,22 @@ , (>=*), (>*) , min_, max_ , ite + , cast ) where -import Z3.Base ( AST ) +-- import Z3.Base ( AST ) import qualified Z3.Base as Base +import Z3.Monad hiding ( Z3, mkEq, Pattern, Model, evalZ3, evalZ3With, eval, evalT, showModel ) +import qualified Z3.Monad as MonadZ3 import Z3.Lang.Exprs import Z3.Lang.Monad +import Z3.Lang.TY -import Control.Applicative ( (<$>), (<*>), pure ) -import Control.Monad ( liftM, liftM2, liftM3, liftM4, liftM5, join ) -import Data.Maybe ( maybeToList ) +import Control.Applicative ( Applicative, (<$>) ) +import Control.Monad.Reader ( ReaderT, ask, runReaderT ) +import Control.Monad.Trans ( lift ) +import Data.Traversable ( Traversable ) import qualified Data.Traversable as T #if __GLASGOW_HASKELL__ < 704 import Data.Typeable ( Typeable1(..), typeOf ) @@ -91,7 +113,7 @@ -- | Compile while introducing TCCs into the script. -- -compileWithTCC :: IsTy a => Expr a -> Z3 (Base.AST (TypeZ3 a)) +compileWithTCC :: IsTy a => Expr a -> Z3 Base.AST compileWithTCC e = do assertCnstr =<< compile (and_ $ typecheck e) compile e @@ -99,20 +121,28 @@ --------------------------------------------------------------------- -- 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 +createVar :: forall a. IsTy a => Int -> String -> Z3 (Expr a) +createVar u str = do + smb <- mkStringSymbol str + srt <- mkSort (TY :: TY a) cnst <- mkConst smb srt let e = Const u cnst assert $ typeInv e return e +-- | Declare skolem variables. +var :: IsTy a => Z3 (Expr a) +var = do + (u, str) <- fresh + createVar u str + +-- | Declare skolem variables with a user specified name. +namedVar :: IsTy a => String -> Z3 (Expr a) +namedVar name = do + (u, str) <- fresh + createVar u $ name ++ "/" ++ str + -- | Declare uninterpreted function of arity 1. --- fun1 :: (IsTy a, IsTy b) => Z3 (Expr a -> Expr b) fun1 = do (fd :: FunApp (a -> b)) <- funDecl @@ -121,68 +151,52 @@ 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) + assert $ forall $ \a 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) + assert $ forall $ \a b 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) + assert $ forall $ \a b c 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) + assert $ forall $ \a b c d 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 + dom <- domain (TY :: TY a) + rng <- range (TY :: TY a) + fd <- mkFuncDecl smb dom rng return (FuncDecl fd) -- | Make assertion in current context. --- assert :: Expr Bool -> Z3 () assert (Lit True) = return () assert e = compileWithTCC e >>= assertCnstr @@ -190,7 +204,6 @@ -- | 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 @@ -199,22 +212,53 @@ 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 +-- | Convert an Expr to a string. +exprToString :: Compilable (Expr a) => Expr a -> Z3 String +exprToString e = + compile e >>= astToString - 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!" +---------------------------------------------------------------------- +-- Models +-- | A computation derived from a model. +newtype Model a = Model { unModel :: ReaderT Base.Model Z3 a } + deriving (Applicative,Functor,Monad) + +-- | Check satisfiability and evaluate a model if some exists. +checkModel :: Model a -> Z3 (Maybe a) +checkModel = checkModelWith (const id) +{-# INLINE checkModel #-} + +-- | Check satisfiability and evaluate a model if some exists. +checkModelWith :: (Result -> Maybe a -> b) -> Model a -> Z3 b +checkModelWith f m = uncurry f <$> checkModelWithResult m +{-# INLINE checkModelWith #-} + +-- | Check satisfiability and evaluate a model if some exists, also +-- returning a 'Result' to the reason for any failure. +checkModelWithResult :: Model a -> Z3 (Result, Maybe a) +checkModelWithResult m = MonadZ3.withModel $ runReaderT (unModel m) + +-- | Show Z3's internal model. +showModel :: Model String +showModel = Model $ ask >>= lift . MonadZ3.showModel + +-- | Evaluate an expression within a model. +eval :: forall a. IsTy a => Expr a -> Model a +eval e = Model $ do + a <- lift $ compileWithTCC e + lift . fixResult a =<< ask + where fixResult :: Base.AST -> Base.Model -> Z3 a + fixResult a m = peek =<< MonadZ3.eval m a + + peek :: Maybe Base.AST -> Z3 a + peek (Just a) = getValue a + peek Nothing = error "Z3.Lang.Prelude.eval: quantified expression or partial model!" + +-- | Evaluate a collection of expressions within a model. +evalT :: (IsTy a,Traversable t) => t (Expr a) -> Model (t a) +evalT = T.traverse eval + ---------------------------------------------------------------------- -- Expressions @@ -240,7 +284,8 @@ a * b = CRingArith Mul [a,b] (CRingArith Sub as) - b = CRingArith Sub (as ++ [b]) a - b = CRingArith Sub [a,b] - negate = Neg + negate (CRingArith Sub [a,b]) = CRingArith Sub [b,a] + negate t = Neg t abs e = ite (e >=* 0) e (-e) signum e = ite (e >* 0) 1 (ite (e ==* 0) 0 (-1)) fromInteger = literal . fromInteger @@ -255,157 +300,162 @@ 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 variadic /distinct/. +distinct :: IsTy a => [Expr a] -> Expr Bool +distinct [] = true +distinct bs = CmpE Distinct 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. +-- | Universally quantified formula. +forall :: QExpr t => t -> Expr Bool +forall f = Quant ForAll f + +-- | Existentially quantified formula. +exists :: QExpr t => t -> Expr Bool +exists f = Quant Exists f + +-- | Pattern-based instantiation. +instanceWhen :: Expr Bool -> [Pattern] -> QBody +instanceWhen = QBody + +-- | Casting between compatible types -- -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 +cast :: (IsTy a, IsTy b, Castable a b) => Expr a -> Expr b +cast = Cast +instance Castable Integer Rational where + compileCast _ = mkInt2Real + +instance Castable Rational Integer where + compileCast _ = mkReal2Int + + -- | 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 +e1 ==* e2 = CmpE Eq [e1,e2] + -- | Not equals. --- (/=*) :: IsTy a => Expr a -> Expr a -> Expr Bool -(/=*) = CmpE Neq +e1 /=* e2 = CmpE Distinct [e1,e2] -- | 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 + mkSort _ = mkBoolSort + getValue v = maybe False id <$> getBool v + mkLiteral True = mkTrue + mkLiteral False = mkFalse + tcBool :: Expr Bool -> TCM () tcBool (Lit _) = ok tcBool (Const _ _) = ok @@ -418,10 +468,9 @@ 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 (Quant _q _f) = ok +tcBool (CmpE _op es) = do + mapM_ tc es tcBool (CmpI _op e1 e2) = do tc e1 tc e2 @@ -430,17 +479,18 @@ withHypo eb $ tcBool e1 withHypo (Not eb) $ tcBool e2 tcBool (App _app) = ok +tcBool (Cast e) = tc e tcBool _ = error "Z3.Lang.Prelude.tcBool: Panic! Impossible constructor in pattern matching!" -compileBool :: Expr Bool -> Z3 (AST Bool) +compileBool :: Expr Bool -> Z3 AST compileBool (Lit a) = mkLiteral a compileBool (Const _ u) = return u compileBool (Tag lyt) = do ix <- deBruijnIx lyt - srt <- mkSort + srt <- mkSort (TY :: TY Bool) mkBound ix srt compileBool (Not b) = do b' <- compileBool b @@ -452,21 +502,11 @@ 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 (Quant q f) + = compileQuant q [] [] f +compileBool (CmpE op es) + = do es' <- mapM compile es + mkEq op es' compileBool (CmpI op e1 e2) = do e1' <- compile e1 e2' <- compile e2 @@ -478,23 +518,63 @@ mkIte b' e1' e2' compileBool (App e) = compile e +compileBool (Cast (e :: Expr a)) + = compile e >>= compileCast (TY :: TY (a, Bool)) compileBool _ = error "Z3.Lang.Prelude.compileBool: Panic! Impossible constructor in pattern matching!" +withSortedSymbol :: IsTy a => TY a -> (Base.Symbol -> Base.Sort -> Z3 b) -> Z3 b +withSortedSymbol t f = do + (_,n) <- fresh + sx <- mkStringSymbol n + srt <- mkSort t + f sx srt + +instance IsTy a => QExpr (Expr a -> Expr Bool) where + compileQuant q smbs srts f = do + withSortedSymbol (TY :: TY a) $ \sx srt -> + newQLayout $ \x -> do + body <- compileBool $ mkBody q x + mkQuant q [] (sx:smbs) (srt:srts) body + where mkBody ForAll x = let b = f x in and_ (typeInv x:typecheck b) ==> b + mkBody Exists x = let b = f x in and_ (b:typeInv x:typecheck b) + +data QBody = QBody (Expr Bool) [Pattern] + +instance IsTy a => QExpr (Expr a -> QBody) where + compileQuant q smbs srts f = do + withSortedSymbol (TY :: TY a) $ \sx srt -> + newQLayout $ \x -> do + let QBody body pats = mapFst (mkBody q x) (f x) + astbody <- compileBool body + pat_lst <- mkPat pats + mkQuant q pat_lst (sx:smbs) (srt:srts) astbody + where mkBody ForAll x b = and_ (typeInv x:typecheck b) ==> b + mkBody Exists x b = and_ (b:typeInv x:typecheck b) + mkPat [] = return [] + mkPat lst = mapM compile lst >>= \args -> (:[]) <$> mkPattern args + mapFst mf (QBody a b) = QBody (mf a) b + +instance (IsTy a, QExpr t) => QExpr (Expr a -> t) where + compileQuant q smbs srts f = + withSortedSymbol (TY :: TY a) $ \sx srt -> + newQLayout $ \x -> + compileQuant q (sx:smbs) (srt:srts) (f x) + ---------------------------------------------------------------------- -- 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 + mkSort _ = mkIntSort + getValue = getInt + mkLiteral = mkInt + instance IsNum Integer where instance IsInt Integer where @@ -513,17 +593,18 @@ withHypo eb $ tcInteger e1 withHypo (Not eb) $ tcInteger e2 tcInteger (App _) = ok +tcInteger (Cast e) = tc e tcInteger _ = error "Z3.Lang.Prelude.tcInteger: Panic! Impossible constructor in pattern matching!" -compileInteger :: Expr Integer -> Z3 (AST Integer) +compileInteger :: Expr Integer -> Z3 AST compileInteger (Lit a) = mkLiteral a compileInteger (Const _ u) = return u compileInteger (Tag lyt) = do ix <- deBruijnIx lyt - srt <- mkSort + srt <- mkSort (TY :: TY Integer) mkBound ix srt compileInteger (Neg e) = mkUnaryMinus =<< compileInteger e @@ -540,23 +621,25 @@ mkIte eb' e1' e2' compileInteger (App e) = compile e +compileInteger (Cast (e :: Expr a)) + = compile e >>= compileCast (TY :: TY (a, Integer)) 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 + mkSort _ = mkRealSort + getValue = getReal + mkLiteral = mkReal + instance IsNum Rational where instance IsReal Rational where @@ -575,17 +658,18 @@ withHypo eb $ tcRational e1 withHypo (Not eb) $ tcRational e2 tcRational (App _) = ok +tcRational (Cast e) = tc e tcRational _ = error "Z3.Lang.Prelude.tcRational: Panic! Impossible constructor in pattern matching!" -compileRational :: Expr Rational -> Z3 (AST Rational) +compileRational :: Expr Rational -> Z3 AST compileRational (Lit a) = mkLiteral a compileRational (Const _ u) = return u compileRational (Tag lyt) = do ix <- deBruijnIx lyt - srt <- mkSort + srt <- mkSort (TY :: TY Rational) mkBound ix srt compileRational (Neg e) = mkUnaryMinus =<< compileRational e @@ -602,29 +686,36 @@ mkIte eb' e1' e2' compileRational (App e) = compile e +compileRational (Cast (e :: Expr a)) + = compile e >>= compileCast (TY :: TY (a, Rational)) 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 + domain _ = (: []) <$> mkSort (TY :: TY a) + range _ = mkSort (TY :: TY b) instance (IsTy a, IsFun (b -> c)) => IsFun (a -> b -> c) where + domain _ = do + srt <- mkSort (TY :: TY a) + lst <- domain (TY :: TY (b -> c)) + return (srt : lst) + range _ = range (TY :: TY (b -> c)) 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!" +app2AST :: IsTy a => FunApp a -> Z3 Base.AST +app2AST f = doApp2AST f [] + where doApp2AST :: FunApp t -> [Base.AST] -> Z3 Base.AST + doApp2AST (FuncDecl fd) acc = mkApp fd acc + doApp2AST (PApp e1 e2) acc = compile e2 >>= doApp2AST e1 . (: acc) + +---------------------------------------------------------------------- +-- Patterns + +instance Compilable Pattern where + compile (Pat e) = compile e + diff --git a/Z3/Lang/TY.hs b/Z3/Lang/TY.hs --- a/Z3/Lang/TY.hs +++ b/Z3/Lang/TY.hs @@ -16,8 +16,7 @@ -- | An alternative to 'undefined' to fake type parameters. --- --- Example: @TY :: TY Integer@ instead of @undefined :: Integer@ -- +-- 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 new file mode 100644 --- /dev/null +++ b/Z3/Monad.hs @@ -0,0 +1,546 @@ + +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- TODO: Error handling + +-- | +-- Module : Z3.Monad +-- Copyright : (c) Iago Abal, 2013 +-- (c) David Castro, 2013 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- +-- A simple monadic wrapper for 'Z3.Base'. + +module Z3.Monad + ( MonadZ3(..) + , Z3 + , module Z3.Opts + , Logic(..) + , evalZ3 + , evalZ3With + + -- * Types + , Symbol + , AST + , Sort + , FuncDecl + , App + , Pattern + , Model + + -- ** Satisfiability result + , Result(..) + + -- * Symbols + , mkStringSymbol + + -- * Sorts + , mkBoolSort + , mkIntSort + , mkRealSort + + -- * Constants and Applications + , mkFuncDecl + , mkApp + , mkConst + , mkTrue + , mkFalse + , mkEq + , mkNot + , mkIte + , mkIff + , mkImplies + , mkXor + , mkAnd + , mkOr + , mkDistinct + , mkAdd + , mkMul + , mkSub + , mkUnaryMinus + , mkDiv + , mkMod + , mkRem + , mkLt + , mkLe + , mkGt + , mkGe + , mkInt2Real + , mkReal2Int + , mkIsInt + + -- * Numerals + , mkNumeral + , mkInt + , mkReal + + -- * Quantifiers + , mkPattern + , mkBound + , mkForall + , mkExists + + -- * Accessors + , getBool + , getInt + , getReal + + -- * Models + , eval + , evalT + , showModel + , showContext + + -- * Constraints + , assertCnstr + , check + , getModel + , delModel + , withModel + , push + , pop + + -- * String Conversion + , ASTPrintMode(..) + , setASTPrintMode + , astToString + , patternToString + , sortToString + , funcDeclToString + ) + where + +import Z3.Opts +import Z3.Base + ( Symbol + , AST + , Sort + , FuncDecl + , App + , Pattern + , Model + , Result(..) + , Logic(..) + , ASTPrintMode(..) + ) +import qualified Z3.Base as Base + +import Control.Applicative ( Applicative ) +import Control.Monad ( void ) +import Control.Monad.Reader ( ReaderT, runReaderT, asks ) +import Control.Monad.Trans ( MonadIO, liftIO ) +import Data.Traversable ( Traversable ) +import qualified Data.Traversable as T + +--------------------------------------------------------------------- +-- The Z3 monad-class + +class (Monad m, MonadIO m) => MonadZ3 m where + getSolver :: m (Maybe Base.Solver) + getContext :: m Base.Context + +------------------------------------------------- +-- Lifting + +liftScalar :: MonadZ3 z3 => (Base.Context -> IO b) -> z3 b +liftScalar f = liftIO . f =<< getContext + +liftFun1 :: MonadZ3 z3 => (Base.Context -> a -> IO b) -> a -> z3 b +liftFun1 f a = getContext >>= \ctx -> liftIO (f ctx a) + +liftFun2 :: MonadZ3 z3 => (Base.Context -> a -> b -> IO c) -> a -> b -> z3 c +liftFun2 f a b = getContext >>= \ctx -> liftIO (f ctx a b) + +liftFun3 :: MonadZ3 z3 => (Base.Context -> a -> b -> c -> IO d) + -> a -> b -> c -> z3 d +liftFun3 f a b c = getContext >>= \ctx -> liftIO (f ctx a b c) + +liftFun4 :: MonadZ3 z3 => (Base.Context -> a -> b -> c -> d -> IO e) + -> a -> b -> c -> d -> z3 e +liftFun4 f a b c d = getContext >>= \ctx -> liftIO (f ctx a b c d) + +liftSolver0 :: MonadZ3 z3 => + (Base.Context -> Base.Solver -> IO b) + -> (Base.Context -> IO b) + -> z3 b +liftSolver0 f_s f_no_s = + do ctx <- getContext + liftIO . maybe (f_no_s ctx) (f_s ctx) =<< getSolver + +liftSolver1 :: MonadZ3 z3 => + (Base.Context -> Base.Solver -> a -> IO b) + -> (Base.Context -> a -> IO b) + -> a -> z3 b +liftSolver1 f_s f_no_s a = + do ctx <- getContext + liftIO . maybe (f_no_s ctx a) (\s -> f_s ctx s a) =<< getSolver + +------------------------------------------------- +-- A simple Z3 monad. + +newtype Z3 a = Z3 { _unZ3 :: ReaderT Z3Env IO a } + deriving (Functor, Applicative, Monad, MonadIO) + +data Z3Env + = Z3Env { + envSolver :: Maybe Base.Solver + , envContext :: Base.Context + } + +instance MonadZ3 Z3 where + getSolver = Z3 $ asks envSolver + getContext = Z3 $ asks envContext + +-- | Eval a Z3 script. +evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a +evalZ3With mbLogic opts (Z3 s) = + Base.withConfig $ \cfg -> do + setOpts cfg opts + Base.withContext cfg $ \ctx -> do + mbSolver <- T.mapM (Base.mkSolverForLogic ctx) mbLogic + runReaderT s (Z3Env mbSolver ctx) + +-- | Eval a Z3 script with default configuration options. +evalZ3 :: Z3 a -> IO a +evalZ3 = evalZ3With Nothing stdOpts + +--------------------------------------------------------------------- +-- Symbols + +-- | Create a Z3 symbol using a string. +-- +-- Reference: +mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol +mkStringSymbol = liftFun1 Base.mkStringSymbol + +--------------------------------------------------------------------- +-- Sorts + +-- | Create the /boolean/ type. +-- +-- Reference: +mkBoolSort :: MonadZ3 z3 => z3 Sort +mkBoolSort = liftScalar Base.mkBoolSort + +-- | Create the /integer/ type. +-- +-- Reference: +mkIntSort :: MonadZ3 z3 => z3 Sort +mkIntSort = liftScalar Base.mkIntSort + +-- | Create the /real/ type. +-- +-- Reference: +mkRealSort :: MonadZ3 z3 => z3 Sort +mkRealSort = liftScalar Base.mkRealSort + +--------------------------------------------------------------------- +-- Constants and Applications + +-- | A Z3 function +mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl +mkFuncDecl = liftFun3 Base.mkFuncDecl + +-- | Create a constant or function application. +-- +-- Reference: +mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST +mkApp = liftFun2 Base.mkApp + +-- | Declare and create a constant. +-- +-- Reference: +mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST +mkConst = liftFun2 Base.mkConst + +-- | Create an AST node representing /true/. +-- +-- Reference: +mkTrue :: MonadZ3 z3 => z3 AST +mkTrue = liftScalar Base.mkTrue + +-- | Create an AST node representing /false/. +-- +-- Reference: +mkFalse :: MonadZ3 z3 => z3 AST +mkFalse = liftScalar Base.mkFalse + +-- | Create an AST node representing /l = r/. +-- +-- Reference: +mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST +mkEq = liftFun2 Base.mkEq + +-- | The distinct construct is used for declaring the arguments pairwise +-- distinct. +-- +-- Reference: +mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST +mkDistinct = liftFun1 Base.mkDistinct + +-- | Create an AST node representing /not(a)/. +-- +-- Reference: +mkNot :: MonadZ3 z3 => AST -> z3 AST +mkNot = liftFun1 Base.mkNot + +-- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/. +-- +-- Reference: +mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST +mkIte = liftFun3 Base.mkIte + +-- | Create an AST node representing /t1 iff t2/. +-- +-- Reference: +mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST +mkIff = liftFun2 Base.mkIff + +-- | Create an AST node representing /t1 implies t2/. +-- +-- Reference: +mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST +mkImplies = liftFun2 Base.mkImplies + +-- | Create an AST node representing /t1 xor t2/. +-- +-- Reference: +mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST +mkXor = liftFun2 Base.mkXor + +-- | Create an AST node representing args[0] and ... and args[num_args-1]. +-- +-- Reference: +mkAnd :: MonadZ3 z3 => [AST] -> z3 AST +mkAnd = liftFun1 Base.mkAnd + +-- | Create an AST node representing args[0] or ... or args[num_args-1]. +-- +-- Reference: +mkOr :: MonadZ3 z3 => [AST] -> z3 AST +mkOr = liftFun1 Base.mkOr + +-- | Create an AST node representing args[0] + ... + args[num_args-1]. +-- +-- Reference: +mkAdd :: MonadZ3 z3 => [AST] -> z3 AST +mkAdd = liftFun1 Base.mkAdd + +-- | Create an AST node representing args[0] * ... * args[num_args-1]. +-- +-- Reference: +mkMul :: MonadZ3 z3 => [AST] -> z3 AST +mkMul = liftFun1 Base.mkMul + +-- | Create an AST node representing args[0] - ... - args[num_args - 1]. +-- +-- Reference: +mkSub :: MonadZ3 z3 => [AST] -> z3 AST +mkSub = liftFun1 Base.mkSub + +-- | Create an AST node representing -arg. +-- +-- Reference: +mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST +mkUnaryMinus = liftFun1 Base.mkUnaryMinus + +-- | Create an AST node representing arg1 div arg2. +-- +-- Reference: +mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST +mkDiv = liftFun2 Base.mkDiv + +-- | Create an AST node representing arg1 mod arg2. +-- +-- Reference: +mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST +mkMod = liftFun2 Base.mkMod + +-- | Create an AST node representing arg1 rem arg2. +-- +-- Reference: +mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST +mkRem = liftFun2 Base.mkRem + +-- | Create less than. +-- +-- Reference: +mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST +mkLt = liftFun2 Base.mkLt + +-- | Create less than or equal to. +-- +-- Reference: +mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST +mkLe = liftFun2 Base.mkLe + +-- | Create greater than. +-- +-- Reference: +mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST +mkGt = liftFun2 Base.mkGt + +-- | Create greater than or equal to. +-- +-- Reference: +mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST +mkGe = liftFun2 Base.mkGe + +-- | Coerce an integer to a real. +-- +-- Reference: +mkInt2Real :: MonadZ3 z3 => AST -> z3 AST +mkInt2Real = liftFun1 Base.mkInt2Real + +-- | Coerce a real to an integer. +-- +-- Reference: +mkReal2Int :: MonadZ3 z3 => AST -> z3 AST +mkReal2Int = liftFun1 Base.mkReal2Int + +-- | Check if a real number is an integer. +-- +-- Reference: +mkIsInt :: MonadZ3 z3 => AST -> z3 AST +mkIsInt = liftFun1 Base.mkIsInt + +--------------------------------------------------------------------- +-- Numerals + +-- | Create a numeral of a given sort. +-- +-- Reference: +mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST +mkNumeral = liftFun2 Base.mkNumeral + +------------------------------------------------- +-- Numerals / Integers + +-- | Create a numeral of sort /int/. +mkInt :: (MonadZ3 z3, Integral a) => a -> z3 AST +mkInt = liftFun1 Base.mkInt + +------------------------------------------------- +-- Numerals / Reals + +-- | Create a numeral of sort /real/. +mkReal :: (MonadZ3 z3, Real r) => r -> z3 AST +mkReal = liftFun1 Base.mkReal + +--------------------------------------------------------------------- +-- Quantifiers + +mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern +mkPattern = liftFun1 Base.mkPattern + +mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST +mkBound = liftFun2 Base.mkBound + +mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST +mkForall = liftFun4 Base.mkForall + +mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST +mkExists = liftFun4 Base.mkExists + +--------------------------------------------------------------------- +-- Accessors + +-- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/. +-- +-- Reference: +getBool :: MonadZ3 z3 => AST -> z3 (Maybe Bool) +getBool = liftFun1 Base.getBool + +-- | Return the integer value +getInt :: MonadZ3 z3 => AST -> z3 Integer +getInt = liftFun1 Base.getInt + +-- | Return rational value +getReal :: MonadZ3 z3 => AST -> z3 Rational +getReal = liftFun1 Base.getReal + +--------------------------------------------------------------------- +-- Models + +-- | Evaluate an AST node in the given model. +eval :: MonadZ3 z3 => Model -> AST -> z3 (Maybe AST) +eval = liftFun2 Base.eval + +-- | Evaluate a collection of AST nodes in the given model. +evalT :: (MonadZ3 z3,Traversable t) => Model -> t AST -> z3 (Maybe (t AST)) +evalT = liftFun2 Base.evalT + +--------------------------------------------------------------------- +-- Constraints + +-- | Create a backtracking point. +push :: MonadZ3 z3 => z3 () +push = liftSolver0 Base.solverPush Base.push + +-- | Backtrack /n/ backtracking points. +pop :: MonadZ3 z3 => Int -> z3 () +pop = liftSolver1 Base.solverPop Base.pop + +-- | Assert a constraing into the logical context. +-- +-- Reference: +assertCnstr :: MonadZ3 z3 => AST -> z3 () +assertCnstr = liftSolver1 Base.solverAssertCnstr Base.assertCnstr + +-- | Get model. +-- +-- Reference : +getModel :: MonadZ3 z3 => z3 (Result, Maybe Model) +getModel = liftSolver0 Base.solverCheckAndGetModel Base.getModel + +-- | Delete a model object. +-- +-- Reference: +delModel :: MonadZ3 z3 => Model -> z3 () +delModel = liftFun1 Base.delModel + +withModel :: (Applicative z3, MonadZ3 z3) => + (Base.Model -> z3 a) -> z3 (Result, Maybe a) +withModel f = do + (r,mb_m) <- getModel + mb_e <- T.traverse f mb_m + void $ T.traverse delModel mb_m + return (r, mb_e) + +-- | Convert the given model into a string. +showModel :: MonadZ3 z3 => Model -> z3 String +showModel = liftFun1 Base.showModel + +-- | Convert Z3's logical context into a string. +showContext :: MonadZ3 z3 => z3 String +showContext = liftScalar Base.showContext + +-- | Check whether the given logical context is consistent or not. +check :: MonadZ3 z3 => z3 Result +check = liftSolver0 Base.solverCheck Base.check + +--------------------------------------------------------------------- +-- String Conversion + +-- | Set the mode for converting expressions to strings. +setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 () +setASTPrintMode = liftFun1 Base.setASTPrintMode + +-- | Convert an AST to a string. +astToString :: MonadZ3 z3 => AST -> z3 String +astToString = liftFun1 Base.astToString + +-- | Convert a pattern to a string. +patternToString :: MonadZ3 z3 => Pattern -> z3 String +patternToString = liftFun1 Base.patternToString + +-- | Convert a sort to a string. +sortToString :: MonadZ3 z3 => Sort -> z3 String +sortToString = liftFun1 Base.sortToString + +-- | Convert a FuncDecl to a string. +funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String +funcDeclToString = liftFun1 Base.funcDeclToString + diff --git a/Z3/Opts.hs b/Z3/Opts.hs new file mode 100644 --- /dev/null +++ b/Z3/Opts.hs @@ -0,0 +1,81 @@ + +-- | +-- Module : Z3.Opts +-- Copyright : (c) Iago Abal, 2013 +-- (c) David Castro, 2013 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- +-- High-level interface to configuration options. + +module Z3.Opts + ( Opts + , setOpts + , stdOpts + , (+?) + , opt + , OptValue + ) + where + +import qualified Z3.Base as Base + +import Data.Monoid ( Monoid(..) ) + +--------------------------------------------------------------------- +-- Configuration + +-- | Z3 configuration. +newtype Opts = Opts [Opt] + +instance Monoid Opts where + mempty = Opts [] + mappend (Opts ps1) (Opts ps2) = Opts (ps1++ps2) + +-- | Default configuration. +stdOpts :: Opts +stdOpts = mempty + +-- | Append configurations. +(+?) :: Opts -> Opts -> Opts +(+?) = mappend + +-- | Set a configuration option. +opt :: OptValue val => String -> val -> Opts +opt oid val = Opts [option oid val] + +-- | Set configuration. +setOpts :: Base.Config -> Opts -> IO () +setOpts baseCfg (Opts params) = mapM_ (setOpt baseCfg) params + +------------------------------------------------- +-- Options + +-- | Configuration option. +data Opt = Opt String -- id + String -- value + +-- | Set an option. +setOpt :: Base.Config -> Opt -> IO () +setOpt baseCfg (Opt oid val) = Base.setParamValue baseCfg oid val + +-- | Values for Z3 options. +class OptValue val where + option :: String -> val -> Opt + +instance OptValue Bool where + option oid True = Opt oid "true" + option oid False = Opt oid "false" + +instance OptValue Int where + option oid = Opt oid . show + +instance OptValue Integer where + option oid = Opt oid . show + +instance OptValue Double where + option oid = Opt oid . show + +instance OptValue [Char] where + option = Opt diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -1,23 +1,27 @@ Name: z3 -Version: 0.2.0 +Version: 0.3.0 Synopsis: Bindings for the Z3 Theorem Prover -Description: - Bindings for the Z3 Theorem Prover. +Description: + Bindings for the Z3 Theorem Prover (). . - 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.Lang") is still very experimental and likely to change. + Low-level bindings to the Z3 API are provided by "Z3.Base", this API is + still incomplete but pretty much stable. . - 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. + A simple but convenient wrapper for "Z3.Base" is provided by "Z3.Monad". . - Haddock documentation: + The "Z3.Lang" API provides a high-level interface to Z3, but it is still + very experimental and likely to change. . - More information about Z3: + Important notes: . - * + * 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 --extra-lib-dirs and --extra-include-dirs Cabal flags. + . + * Hackage fails to compile this package because of the z3 dependency. + . + * Haddock documentation can be found at + Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE @@ -25,7 +29,7 @@ David Castro Maintainer: Iago Abal , David Castro -Copyright: 2012, Iago Abal, David Castro +Copyright: 2012-2013, Iago Abal, David Castro Category: Math, Theorem Provers, Formal Methods Build-type: Simple Cabal-version: >= 1.6 @@ -35,11 +39,14 @@ location: https://bitbucket.org/iago/z3-haskell Library - Exposed-modules: + Exposed-modules: Z3.Base - Z3.Base.C + Z3.Opts + + Z3.Monad + Z3.Lang Z3.Lang.Prelude Z3.Lang.Nat @@ -47,16 +54,27 @@ Z3.Lang.Pow2 Other-modules: - + + Z3.Base.C + Z3.Lang.Exprs Z3.Lang.Monad Z3.Lang.TY ghc-options: -Wall - Build-depends: base > 3 && < 5, containers, mtl +-- modify in MonadState causes <> in mtl-2.1, so we forbide this mtl +-- version in this library. + Build-depends: base > 3 && < 5, containers, mtl < 2.1 || > 2.1 Build-tools: hsc2hs - Extensions: ForeignFunctionInterface + Extensions: FlexibleInstances + ForeignFunctionInterface + includes: z3.h - extra-libraries: gomp z3 gomp + + -- In OS X libz3 is linked statically against libgomp + if os(darwin) + extra-libraries: z3 + else + extra-libraries: gomp z3 gomp