diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,31 @@ +Copyright (c)2012, Iago Abal, David Castro + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the names of Iago Abal and David Castro nor the names of + other contributors may be used to endorse or promote products + derived from this software without specific prior written + permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Z3/Base.hs b/Z3/Base.hs new file mode 100644 --- /dev/null +++ b/Z3/Base.hs @@ -0,0 +1,827 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} + +-- | +-- 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 + , App + , Pattern + , Model + + , castAST + + -- ** Satisfiability result + , Result(..) + + -- ** Z3 types + , Z3Type(..) + , Z3Scalar(..) + , Z3Num + + -- * Configuration + , mkConfig + , setParamValue + , set_MODEL + , set_MODEL_PARTIAL + , set_WELL_SORTED_CHECK + + -- * Context + , mkContext + + -- * Symbols + , mkStringSymbol + + -- * Sorts + , mkBoolSort + , mkIntSort + , mkRealSort + + -- * Constants and Applications + , 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 + + -- * Accessors + , getBool + , getInt + , getReal + + -- * Models + , eval + + -- * Constraints + , assertCnstr + , check + , getModel + + ) where + +import Z3.Base.C +import Z3.Types.TY + +import Control.Applicative ( (<$>) ) +import Control.Monad ( liftM2 ) +import Data.Typeable ( Typeable ) +import Data.Int +import Data.Ratio ( Ratio, numerator, denominator, (%) ) +import Data.Word +import Data.Typeable ( Typeable, typeOf ) +import Foreign hiding ( newForeignPtr, toBool ) +import Foreign.C + ( CInt, CUInt, CLLong, CULLong + , peekCString + , withCString ) +import Foreign.Concurrent ( newForeignPtr ) + +--------------------------------------------------------------------- +-- 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 + +-- | 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 + +-- | 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) + +-- | 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) + +-- | 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. +-- +data Model + = Model { + modelContext :: Context + , unModel :: ForeignPtr Z3_model + } + deriving Eq + +-- | Result of a satisfiability check. +-- +data Result + = Sat + | Unsat + | Undef + deriving (Eq, Ord, Enum, Bounded, 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 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 Typeable a => Z3Type a where + mkSort :: Context -> IO (Sort a) + +instance Z3Type Bool where + mkSort = mkBoolSort + +instance Z3Type Integer where + mkSort = mkIntSort + +instance Z3Type Rational where + mkSort = mkRealSort + +-- | A Z3 scalar type +-- +class (Eq a, Show a, Z3Type a) => Z3Scalar a where + mkValue :: Context -> a -> IO (AST a) + getValue :: Context -> AST a -> IO (Maybe a) + +instance Z3Scalar Bool where + mkValue ctx True = mkTrue ctx + mkValue ctx False = mkFalse ctx + getValue = getBool + +instance Z3Scalar Integer where + mkValue ctx = mkInt ctx + getValue ctx ast = Just <$> getInt ctx ast + +instance Z3Scalar Rational where + mkValue ctx = mkReal ctx + getValue ctx ast = Just <$> getReal ctx ast + +-- | A Z3 numeric type +-- +class (Z3Scalar a, Num a) => Z3Num a where +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 = + withForeignPtr (unConfig 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 "MWELL_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 = withForeignPtr (unConfig 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 = + withForeignPtr (unContext 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 = withForeignPtr (unContext c) $ \cptr -> + Sort <$> z3_mk_bool_sort cptr + +-- | Create an integer type. +-- +-- Reference: +-- +mkIntSort :: Context -> IO (Sort Integer) +mkIntSort c = withForeignPtr (unContext c) $ \cptr -> + Sort <$> z3_mk_int_sort cptr + +-- | Create a real type. +-- +-- Reference: +-- +mkRealSort :: Context -> IO (Sort Rational) +mkRealSort c = withForeignPtr (unContext c) $ \cptr -> + Sort <$> z3_mk_real_sort cptr + +-- TODO Sorts: from Z3_mk_real_sort on + +--------------------------------------------------------------------- +-- Constants and Applications + +-- TODO Constants and Applications: Z3_mk_func_decl +-- TODO Constants and Applications: Z3_mk_app + +-- | Declare and create a constant. +-- +-- Reference: +-- +mkConst :: Context -> Symbol -> Sort a -> IO (AST a) +mkConst c x s = withForeignPtr (unContext 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 = withForeignPtr (unContext c) $ \cptr -> + AST <$> z3_mk_true cptr + +-- | Create an AST node representing /false/. +-- +-- Reference: +-- +mkFalse :: Context -> IO (AST Bool) +mkFalse c = withForeignPtr (unContext c) $ \cptr -> + AST <$> z3_mk_false cptr + +-- | Create an AST node representing l = r. +-- +-- Reference: +-- +mkEq :: Z3Scalar a => Context -> AST a -> AST a -> IO (AST Bool) +mkEq c e1 e2 = withForeignPtr (unContext c) $ \cptr -> + 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 -> + withForeignPtr (unContext 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 -> + withForeignPtr (unContext 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 -> + withForeignPtr (unContext 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 -> + withForeignPtr (unContext 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 -> + withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext 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 = + withForeignPtr (unContext 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 = + withForeignPtr (unContext c) $ \ctxPtr -> + AST <$> z3_mk_int ctxPtr cn (unSort s) + where cn = fromIntegral n :: CInt + +{-# INLINE mkUnsignedIntZ3 #-} +mkUnsignedIntZ3 :: Z3Num a => Context -> Word32 -> Sort a -> IO (AST a) +mkUnsignedIntZ3 c n s = + withForeignPtr (unContext c) $ \ctxPtr -> + AST <$> z3_mk_unsigned_int ctxPtr cn (unSort s) + where cn = fromIntegral n :: CUInt + +{-# INLINE mkInt64Z3 #-} +mkInt64Z3 :: Z3Num a => Context -> Int64 -> Sort a -> IO (AST a) +mkInt64Z3 c n s = + withForeignPtr (unContext c) $ \ctxPtr -> + AST <$> z3_mk_int64 ctxPtr cn (unSort s) + where cn = fromIntegral n :: CLLong + +{-# INLINE mkUnsignedInt64Z3 #-} +mkUnsignedInt64Z3 :: Z3Num a => Context -> Word64 -> Sort a -> IO (AST a) +mkUnsignedInt64Z3 c n s = + withForeignPtr (unContext c) $ \ctxPtr -> + AST <$> z3_mk_unsigned_int64 ctxPtr cn (unSort s) + where cn = fromIntegral n :: CULLong + +{-# 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 = + withForeignPtr (unContext 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 + +-- TODO Quantifiers + +--------------------------------------------------------------------- +-- 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 = withForeignPtr (unContext 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 = withForeignPtr (unContext c) $ \ctxPtr -> + peekCString =<< z3_get_numeral_string ctxPtr (unAST a) + +-- | Return 'Z3Int' value +-- +getInt :: Num a => Context -> AST Integer -> IO a +getInt c a = fromInteger . read <$> getNumeralString c a + +-- | Return the numerator (as a numeral AST) of a numeral AST of sort /real/. +-- +-- Reference: +-- +getNumerator :: Context -> AST Rational -> IO Integer +getNumerator c a = withForeignPtr (unContext c) $ \ctxPtr -> + z3_get_numerator ctxPtr (unAST a) >>= getInt c . AST + +-- | Return the denominator (as a numeral AST) of a numeral AST of sort /real/. +-- +-- Reference: +-- +getDenominator :: Context -> AST Rational -> IO Integer +getDenominator c a = withForeignPtr (unContext c) $ \ctxPtr -> + z3_get_denominator ctxPtr (unAST a) >>= getInt c . AST + +-- | Return 'Z3Real' value +-- +getReal :: Fractional a => Context -> AST Rational -> IO a +getReal c a = fromRational <$> + liftM2 (%) (getNumerator c a) (getDenominator c a) + +-- TODO Modifiers + +--------------------------------------------------------------------- +-- Models + +mkModel :: Context -> Ptr Z3_model -> IO Model +mkModel ctx ptr = withForeignPtr (unContext ctx) $ \ctxPtr -> + Model ctx <$> newForeignPtr ptr (z3_del_model ctxPtr ptr) + +-- | Evaluate an AST node in the given model. +eval :: Model -> AST a -> IO (Maybe (AST a)) +eval m a + = withForeignPtr (unContext $ modelContext m) $ \ctxPtr -> + withForeignPtr (unModel m) $ \mdlPtr -> + alloca $ \aptr2 -> + z3_eval ctxPtr mdlPtr (unAST a) aptr2 >>= peekAST aptr2 . toBool + 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 = + withForeignPtr (unContext ctx) $ \ctxPtr -> + z3_assert_cnstr ctxPtr (unAST ast) + +-- | Get model (logical context is consistent) +-- +-- Reference : +-- +getModel :: Context -> IO (Result, Maybe Model) +getModel c = withForeignPtr (unContext c) $ \ctxPtr -> + alloca $ \mptr -> + z3_check_and_get_model ctxPtr mptr >>= peekModel mptr . toResult + where peekModel :: Ptr (Ptr Z3_model) + -> Result + -> IO (Result, Maybe Model) + peekModel p r | p == nullPtr = return (r, Nothing) + | otherwise = do z3m <- peek p + m <- mkModel c z3m + return (r, Just m) + +-- | Check whether the given logical context is consistent or not. +-- +-- Reference: +-- +check :: Context -> IO Result +check ctx = toResult <$> withForeignPtr (unContext ctx) z3_check + +-- TODO Constraints: Z3_check_assumptions +-- TODO Constraints: Z3_get_implied_equalities + +-- TODO From section 'Constraints' on. diff --git a/Z3/Base/C.hsc b/Z3/Base/C.hsc new file mode 100644 --- /dev/null +++ b/Z3/Base/C.hsc @@ -0,0 +1,489 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE ForeignFunctionInterface #-} + +-- | +-- Module : Z3.Base.C +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- +-- Low-level bindings, highly inspired by yices-painless. +-- + + +module Z3.Base.C where + +import Foreign +import Foreign.C.Types +import Foreign.C.String + +#include + + +--------------------------------------------------------------------- +-- * Types + +-- | A configuration object used to initialize logical contexts. +data Z3_config + +-- | Logical context. This is the main Z3 data-structure. +data Z3_context + +-- | A Lisp-link symbol. It is used to name types, constants, and functions. +-- A symbol can be created using string or integers. +data Z3_symbol + +-- | Abstract syntax tree node. That is, the data-structure used in Z3 to +-- represent terms, formulas and types. +data Z3_ast + +-- | A kind of AST used to represent types. +data Z3_sort + +-- | 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 +-- guide quantifier instantiation. +data Z3_pattern + +-- | A model for the constraints asserted into the logical context. +data Z3_model + +-- | Lifted Boolean type: false, undefined, true. +type Z3_lbool = CInt + +-- | Values of lifted boolean type +z3_l_true, z3_l_false, z3_l_undef :: Z3_lbool +z3_l_true = #const Z3_L_TRUE +z3_l_false = #const Z3_L_FALSE +z3_l_undef = #const Z3_L_UNDEF + +-- | Boolean type. It is just an alias for int. +type Z3_bool = CInt + +-- | Z3_bool values +z3_true, z3_false :: Z3_lbool +z3_true = #const Z3_TRUE +z3_false = #const Z3_FALSE + +-- | Z3 String type +type Z3_string = CString + +--------------------------------------------------------------------- +-- * 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 () + + +--------------------------------------------------------------------- +-- * Create context + +-- | 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) + + +--------------------------------------------------------------------- +-- * Sorts + +-- TODO Sorts: Z3_is_eq_sort +-- TODO Sorts: Z3_mk_uninterpreted_sort + +-- | 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 + + +--------------------------------------------------------------------- +-- * Constants and Applications + +-- TODO Constants and Applications: Z3_mk_func_decl +-- TODO Constants and Applications: Z3_mk_app + +-- | 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) + +-- TODO Constants and Applications: Z3_mk_fresh_func_decl +-- TODO Constants and Applications: Z3_mk_fresh_const + +--------------------------------------------------------------------- +-- * Propositional Logic and Equality + +-- | 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 + +-- | 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. +-- +-- 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. +-- +-- 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. +-- +-- 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]. +-- +-- 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]. +-- +-- 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]. +-- +-- 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 + +--------------------------------------------------------------------- +-- * 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) + +-- TODO Quantifiers + +--------------------------------------------------------------------- +-- * Accessors + +-- | 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 + +-- | Return the numerator (as a numeral AST) of a numeral AST of sort Int. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_get_numerator" + z3_get_numerator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Return the denominator (as a numeral AST) of a numeral AST of sort Real. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_get_denominator" + z3_get_denominator :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- TODO Modifiers + +--------------------------------------------------------------------- +-- * Models + +-- | Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, +-- and store the result in v. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_eval" + z3_eval :: Ptr Z3_context + -> Ptr Z3_model + -> Ptr Z3_ast + -> Ptr (Ptr Z3_ast) + -> IO Z3_bool + +--------------------------------------------------------------------- +-- * 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: +-- +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. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_check" + z3_check :: Ptr Z3_context -> IO Z3_lbool + +-- TODO Constraints: Z3_check_assumptions +-- TODO Constraints: Z3_get_implied_equalities + +-- | Delete a model object. +-- +-- Reference: +-- +foreign import ccall unsafe "Z3_del_model" + z3_del_model :: Ptr Z3_context -> Ptr Z3_model -> IO () + + +-- TODO From section 'Constraints' on. diff --git a/Z3/Exprs.hs b/Z3/Exprs.hs new file mode 100644 --- /dev/null +++ b/Z3/Exprs.hs @@ -0,0 +1,211 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} + +-- | +-- Module : Z3.Exprs +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental + +-- TODO: Pretty-printing of expressions + +module Z3.Exprs ( + + module Z3.Types + + -- * Abstract syntax + , Expr + + -- * Constructing expressions + , true + , false + , not_ + , and_, (&&*) + , or_, (||*) + , xor + , implies, (==>) + , iff, (<=>) + , (//), (%*), (%%) + , (==*), (/=*) + , (<=*), (<*) + , (>=*), (>*) + , ite + + ) where + + +import Z3.Exprs.Internal +import Z3.Types + +import Data.Typeable ( Typeable1(..), typeOf ) +import Unsafe.Coerce ( unsafeCoerce ) + + +deriving instance Show (Expr a) +deriving instance Typeable1 Expr + +instance Eq (Expr a) where + (Lit l1) == (Lit l2) = l1 == l2 + (Const a) == (Const b) = a == b + (Not e1) == (Not e2) = e1 == e2 + (BoolBin op1 p1 q1) == (BoolBin op2 p2 q2) + = op1 == op2 && p1 == p2 && q1 == q2 + (BoolMulti op1 ps) == (BoolMulti op2 qs) + | length ps == length qs = op1 == op2 && and (zipWith (==) ps qs) + (Neg e1) == (Neg e2) = e1 == e2 + (CRingArith op1 as) == (CRingArith op2 bs) + | length as == length bs = op1 == op2 && and (zipWith (==) as bs) + (IntArith op1 a1 b1) == (IntArith op2 a2 b2) + = op1 == op2 && a1 == a2 && b1 == b2 + (RealArith op1 a1 b1) == (RealArith op2 a2 b2) + = op1 == op2 && a1 == a2 && b1 == b2 + (CmpE op1 a1 b1) == (CmpE op2 a2 b2) + | op1 == op2 && typeOf a1 == typeOf a2 + = a1 == unsafeCoerce a2 && b1 == unsafeCoerce b2 + (CmpI op1 a1 b1) == (CmpI op2 a2 b2) + | op1 == op2 && typeOf a1 == typeOf a2 + = a1 == unsafeCoerce a2 && b1 == unsafeCoerce b2 + (Ite g1 a1 b1) == (Ite g2 a2 b2) = g1 == g2 && a1 == a2 && b1 == b2 + _e1 == _e2 = False + + +-- * Constructing expressions + +instance IsNum a => Num (Expr a) where + (CRingArith Add as) + (CRingArith Add bs) = CRingArith Add (as ++ bs) + (CRingArith Add as) + b = CRingArith Add (b:as) + a + (CRingArith Add bs) = CRingArith Add (a:bs) + a + b = CRingArith Add [a,b] + (CRingArith Mul as) * (CRingArith Mul bs) = CRingArith Mul (as ++ bs) + (CRingArith Mul as) * b = CRingArith Mul (b:as) + a * (CRingArith Mul bs) = CRingArith Mul (a:bs) + a * b = CRingArith Mul [a,b] + (CRingArith Sub as) - b = CRingArith Sub (as ++ [b]) + a - b = CRingArith Sub [a,b] + negate = Neg + abs e = ite (e >=* 0) e (-e) + signum e = ite (e >* 0) 1 (ite (e ==* 0) 0 (-1)) + fromInteger = literal . fromInteger + +instance IsReal a => Fractional (Expr a) where + (/) = RealArith Div + fromRational = literal . fromRational + +infixl 7 //, %*, %% +infix 4 ==*, /=*, <*, <=*, >=*, >* +infixr 3 &&*, ||*, `xor` +infixr 2 `implies`, `iff`, ==>, <=> + +-- | /literal/ constructor. +-- +literal :: IsScalar a => a -> Expr a +literal = Lit + +-- | Boolean literals. +-- +true, false :: Expr Bool +true = Lit True +false = Lit False + +-- | Boolean negation +-- +not_ :: Expr Bool -> Expr Bool +not_ = Not + +-- | Boolean binary /xor/. +-- +xor :: Expr Bool -> Expr Bool -> Expr Bool +xor = BoolBin Xor +-- | Boolean implication +-- +implies :: Expr Bool -> Expr Bool -> Expr Bool +implies = BoolBin Implies +-- | An alias for 'implies'. +-- +(==>) :: Expr Bool -> Expr Bool -> Expr Bool +(==>) = implies +-- | Boolean /if and only if/. +-- +iff :: Expr Bool -> Expr Bool -> Expr Bool +iff = BoolBin Iff +-- | An alias for 'iff'. +-- +(<=>) :: Expr Bool -> Expr Bool -> Expr Bool +(<=>) = iff + +-- | Boolean variadic /and/. +-- +and_ :: [Expr Bool] -> Expr Bool +and_ = BoolMulti And +-- | Boolean variadic /or/. +-- +or_ :: [Expr Bool] -> Expr Bool +or_ = BoolMulti Or + +-- | Boolean binary /and/. +-- +(&&*) :: Expr Bool -> Expr Bool -> Expr Bool +(BoolMulti And ps) &&* (BoolMulti And qs) = and_ (ps ++ qs) +(BoolMulti And ps) &&* q = and_ (q:ps) +p &&* (BoolMulti And qs) = and_ (p:qs) +p &&* q = and_ [p,q] +-- | Boolean binary /or/. +-- +(||*) :: Expr Bool -> Expr Bool -> Expr Bool +(BoolMulti Or ps) ||* (BoolMulti Or qs) = or_ (ps ++ qs) +(BoolMulti Or ps) ||* q = or_ (q:ps) +p ||* (BoolMulti Or qs) = or_ (p:qs) +p ||* q = or_ [p,q] + +-- | Integer division. +-- +(//) :: IsInt a => Expr a -> Expr a -> Expr a +(//) = IntArith Quot +-- | Integer modulo. +-- +(%*) :: IsInt a => Expr a -> Expr a -> Expr a +(%*) = IntArith Mod +-- | Integer remainder. +-- +(%%) :: IsInt a => Expr a -> Expr a -> Expr a +(%%) = IntArith Rem + + +-- | Equals. +-- +(==*) :: IsScalar a => Expr a -> Expr a -> Expr Bool +(==*) = CmpE Eq +-- | Not equals. +-- +(/=*) :: IsScalar a => Expr a -> Expr a -> Expr Bool +(/=*) = CmpE Neq + + +-- | Less or equals than. +-- +(<=*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(<=*) = CmpI Le +-- | Less than. +-- +(<*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(<*) = CmpI Lt +-- | Greater or equals than. +-- +(>=*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(>=*) = CmpI Ge +-- | Greater than. +-- +(>*) :: IsNum a => Expr a -> Expr a -> Expr Bool +(>*) = CmpI Gt + +-- | /if-then-else/. +-- +ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a +ite = Ite diff --git a/Z3/Exprs/Internal.hs b/Z3/Exprs/Internal.hs new file mode 100644 --- /dev/null +++ b/Z3/Exprs/Internal.hs @@ -0,0 +1,109 @@ + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} + +-- | +-- Module : Z3.Exprs.Internal +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental + +module Z3.Exprs.Internal where + + +import Z3.Types + +import Data.Typeable ( Typeable ) + + +-- | Unique identifiers +-- +type Uniq = Int + +{-# WARNING Lit + , Const + , Not + , BoolBin + , BoolMulti + , Neg + , CRingArith + , IntArith + , RealArith + , CmpE + , CmpI + , Ite + "You are using a constructor of type Expr, \ + \which you should NOT be using! \ + \In fact, you should not be importing this \ + \module at all! Import Z3.Exprs instead!" #-} + +-- | Abstract syntax. +-- +data Expr :: * -> * where + -- | Literals + Lit :: IsScalar a => a -> Expr a + -- | Constants + Const :: !Uniq -> Expr a + -- | Logical negation + Not :: Expr Bool -> Expr Bool + -- | Binary boolean expressions + BoolBin :: BoolBinOp -> Expr Bool -> Expr Bool -> Expr Bool + -- | Variadic boolean expressions + BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool + -- | Arithmetic negation + Neg :: IsNum a => Expr a -> Expr a + -- | Arithmetic expressions for commutative rings + CRingArith :: IsNum a => CRingOp -> [Expr a] -> Expr a + -- | Integer arithmetic + IntArith :: IsInt a => IntOp -> Expr a -> Expr a -> Expr a + -- | Real arithmetic + RealArith :: IsReal a => RealOp -> Expr a -> Expr a -> Expr a + -- | Comparison expressions + CmpE :: IsScalar a => CmpOpE -> Expr a -> Expr a -> Expr Bool + CmpI :: IsNum a => CmpOpI -> Expr a -> Expr a -> Expr Bool + -- | if-then-else expressions + Ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a + +{-# WARNING BoolBinOp + , BoolMultiOp + , CRingOp + , IntOp + , RealOp + , CmpOpE + , CmpOpI + "You should NOT be using this type or data constructor! \ + \In fact, you should not be importing this \ + \module at all! Import Z3.Exprs instead!" #-} + +-- | Boolean binary operations. +data BoolBinOp = Xor | Implies | Iff + deriving (Eq,Show) + +-- | Boolean variadic operations. +data BoolMultiOp = And | Or + deriving (Eq,Show) + +-- | Commutative ring operations. +data CRingOp = Add | Mul | Sub + deriving (Eq,Show) + +-- | Operations for sort /int/. +data IntOp = Quot | Mod | Rem + deriving (Eq,Show) + +-- | Operations for sort /real/. +data RealOp = Div + deriving (Eq,Show) + +-- | Equality testing. +data CmpOpE = Eq | Neq + deriving (Eq, Show, Typeable) + +-- | Inequality comparisons. +data CmpOpI = Le | Lt | Ge | Gt + deriving (Eq, Show, Typeable) diff --git a/Z3/Monad.hs b/Z3/Monad.hs new file mode 100644 --- /dev/null +++ b/Z3/Monad.hs @@ -0,0 +1,284 @@ +{-# OPTIONS_GHC -funbox-strict-fields #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-} + +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | +-- Module : Z3.Monad +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro +-- Stability : experimental + + +module Z3.Monad ( + -- * Z3 Monad + Z3 + , evalZ3 + + -- * Satisfiability result + , Base.Result(..) + + -- * Z3 actions + , var + , assert + , let_ + , check + + , module Z3.Exprs + + ) where + +import qualified Z3.Base as Base +import Z3.Exprs +import Z3.Exprs.Internal + +import Control.Monad +import Control.Monad.State.Strict +import Data.Maybe ( fromMaybe ) +import qualified Data.IntMap as Map + +--------------------------------------------------------------------- +-- The Z3 Monad + +-- | Z3 monad. +-- +newtype Z3 a = Z3 (StateT Z3State IO a) + deriving (Functor, Monad) + +instance MonadState Z3State Z3 where + get = Z3 $ StateT $ \s -> return (s,s) + put st = Z3 $ StateT $ \_ -> return ((), st) + +-- | Existential type. Used to store constants keeping sort info. +-- +data AnyAST = forall a. Base.Z3Type a => AnyAST (Base.AST a) + +-- | Internal state of Z3 monad. +-- +data Z3State + = Z3State { uniqVal :: !Uniq + , context :: Base.Context + , consts :: Map.IntMap AnyAST + } + +-- | Eval a Z3 script. +-- +evalZ3 :: Z3 a -> IO a +evalZ3 (Z3 s) = do + cfg <- Base.mkConfig + Base.set_MODEL cfg True + Base.set_MODEL_PARTIAL cfg False + ctx <- Base.mkContext cfg + evalStateT s Z3State { uniqVal = 0 + , context = ctx + , consts = Map.empty + } + +-- | Fresh symbol name. +-- +fresh :: Z3 (Uniq, String) +fresh = do + st <- get + let i = uniqVal st + put st { uniqVal = i + 1 } + return (uniqVal st, 'v':show i) + +-- | Add a constant of type @Base.AST a@ to the state. +-- +addConst :: Base.Z3Type a => Uniq -> Base.AST a -> Z3 () +addConst u ast = do + st <- get + put st { consts = Map.insert u (AnyAST ast) (consts st) } + +-- | Get a 'Base.AST' stored in the Z3State. +-- +{- TODO: I believe that getConst return type should be Z3 (Base.AST a) + instead. If Map.lookup returns nothing then we "panic" because + an undefined constant, if Base.castAST returns nothing then we + panic because of type mismatch. We have the duty to guarantee + that none of these errors would ever happen. + - Iago +-} +getConst :: forall a. Base.Z3Type a => Uniq -> Z3 (Maybe (Base.AST a)) +getConst u = liftM mlookup (gets consts) + where mlookup :: Map.IntMap AnyAST -> Maybe (Base.AST a) + mlookup m = Map.lookup u m >>= \(AnyAST e) -> Base.castAST e + +--------------------------------------------------------------------- +-- Constructing expressions + +-- | Declare skolem variables. +-- +var :: forall a. IsTy a => Z3 (Expr a) +var = do + ctx <- gets context + (u, str) <- fresh + smb <- mkStringSymbol_ ctx str + (srt :: Base.Sort (TypeZ3 a)) <- Z3 . lift $ Base.mkSort ctx + addConst u =<< mkConst_ ctx smb srt + return $ Const u + +-- | Make assertion in current context. +-- +assert :: Expr Bool -> Z3 () +assert = join . liftM2 assertCnstr_ (gets context) . compile + +-- | Introduce an auxiliary declaration to name a given expression. +-- +-- If you really want sharing use this instead of Haskell's /let/. +-- +let_ :: IsScalar a => Expr a -> Z3 (Expr a) +let_ e = do + aux <- var + assert (aux ==* e) + return aux + +-- | Check current context. +-- +check :: Z3 Base.Result +check = check_ =<< gets context + +-- | Create a 'Base.AST' from a 'Expr'. +-- +compile :: IsTy a => Expr a -> Z3 (Base.AST (TypeZ3 a)) +compile (Lit a) + = flip mkLiteral_ (toZ3Type a) =<< gets context +compile (Const u) + = liftM (fromMaybe $ error uNDEFINED_CONST) $ getConst u +compile (Not b) + = do ctx <- gets context + b' <- compile b + mkNot_ ctx b' +compile (BoolBin op e1 e2) + = do ctx <- gets context + e1' <- compile e1 + e2' <- compile e2 + mkBoolBin_ ctx op e1' e2' +compile (BoolMulti op es) + = do ctx <- gets context + es' <- mapM compile es + mkBoolMulti_ ctx op es' +compile (Neg e) + = do ctx <- gets context + e' <- compile e + mkUnaryMinus_ ctx e' +compile (CRingArith op es) + = do ctx <- gets context + es' <- mapM compile es + mkCRingArith_ ctx op es' +compile (IntArith op e1 e2) + = do ctx <- gets context + e1' <- compile e1 + e2' <- compile e2 + mkIntArith_ ctx op e1' e2' +compile (RealArith op e1 e2) + = do ctx <- gets context + e1' <- compile e1 + e2' <- compile e2 + mkRealArith_ ctx op e1' e2' +compile (CmpE op e1 e2) + = do ctx <- gets context + e1' <- compile e1 + e2' <- compile e2 + mkEq_ ctx op e1' e2' +compile (CmpI op e1 e2) + = do ctx <- gets context + e1' <- compile e1 + e2' <- compile e2 + mkCmp_ ctx op e1' e2' +compile (Ite b e1 e2) + = do ctx <- gets context + b' <- compile b + e1' <- compile e1 + e2' <- compile e2 + mkIte_ ctx b' e1' e2' + +--------------------------------------------------------------------- +-- Internal lifted Base functions + +assertCnstr_ :: Base.Context -> Base.AST Bool -> Z3 () +assertCnstr_ ctx = Z3 . lift . Base.assertCnstr ctx + +check_ :: Base.Context -> Z3 Base.Result +check_ = Z3 . lift . Base.check + +mkStringSymbol_ :: Base.Context -> String -> Z3 Base.Symbol +mkStringSymbol_ ctx = Z3 . lift . Base.mkStringSymbol ctx + +mkLiteral_ :: forall a. Base.Z3Scalar a => Base.Context -> a -> Z3 (Base.AST a) +mkLiteral_ ctx = Z3 . lift . Base.mkValue ctx + +mkNot_ :: Base.Context -> Base.AST Bool -> Z3 (Base.AST Bool) +mkNot_ ctx = Z3 . lift . Base.mkNot ctx + +mkBoolBin_ :: Base.Context -> BoolBinOp -> + Base.AST Bool -> Base.AST Bool -> Z3 (Base.AST Bool) +mkBoolBin_ ctx Xor b1 = Z3 . lift . Base.mkXor ctx b1 +mkBoolBin_ ctx Implies b1 = Z3 . lift . Base.mkImplies ctx b1 +mkBoolBin_ ctx Iff b1 = Z3 . lift . Base.mkIff ctx b1 + +mkBoolMulti_ :: Base.Context -> BoolMultiOp -> + [Base.AST Bool] -> Z3 (Base.AST Bool) +mkBoolMulti_ ctx And = Z3 . lift . Base.mkAnd ctx +mkBoolMulti_ ctx Or = Z3 . lift . Base.mkAnd ctx + +mkEq_ :: Base.Z3Scalar a => Base.Context -> CmpOpE -> + Base.AST a -> Base.AST a -> Z3 (Base.AST Bool) +mkEq_ ctx Eq e1 = Z3 . lift . Base.mkEq ctx e1 +mkEq_ ctx Neq e1 = Z3 . lift . (Base.mkNot ctx <=< Base.mkEq ctx e1) + +mkCmp_ :: Base.Z3Num a => Base.Context -> CmpOpI -> + Base.AST a -> Base.AST a -> Z3 (Base.AST Bool) +mkCmp_ ctx Le e1 = Z3 . lift . Base.mkLe ctx e1 +mkCmp_ ctx Lt e1 = Z3 . lift . Base.mkLt ctx e1 +mkCmp_ ctx Ge e1 = Z3 . lift . Base.mkGe ctx e1 +mkCmp_ ctx Gt e1 = Z3 . lift . Base.mkGt ctx e1 + +mkConst_ :: Base.Z3Type a => Base.Context + -> Base.Symbol -> Base.Sort a -> Z3 (Base.AST a) +mkConst_ ctx smb = Z3 . lift . Base.mkConst ctx smb + +mkUnaryMinus_ :: Base.Z3Num a => Base.Context -> Base.AST a -> Z3 (Base.AST a) +mkUnaryMinus_ ctx = Z3 . lift . Base.mkUnaryMinus ctx + +mkCRingArith_ :: Base.Z3Num a => Base.Context + -> CRingOp -> [Base.AST a] -> Z3 (Base.AST a) +mkCRingArith_ ctx Add = Z3 . lift . Base.mkAdd ctx +mkCRingArith_ ctx Mul = Z3 . lift . Base.mkMul ctx +mkCRingArith_ ctx Sub = Z3 . lift . Base.mkSub ctx + +mkIntArith_ :: Base.Context + -> IntOp + -> Base.AST Integer -> Base.AST Integer + -> Z3 (Base.AST Integer) +mkIntArith_ ctx Quot e1 = Z3 . lift . Base.mkDiv ctx e1 +mkIntArith_ ctx Mod e1 = Z3 . lift . Base.mkMod ctx e1 +mkIntArith_ ctx Rem e1 = Z3 . lift . Base.mkRem ctx e1 + +mkRealArith_ :: Base.Context + -> RealOp + -> Base.AST Rational -> Base.AST Rational + -> Z3 (Base.AST Rational) +mkRealArith_ ctx Div e1 = Z3 . lift . Base.mkDiv ctx e1 + +mkIte_ :: Base.Context + -> Base.AST Bool + -> Base.AST a -> Base.AST a + -> Z3 (Base.AST a) +mkIte_ ctx b e1 = Z3 . lift . Base.mkIte ctx b e1 + +--------------------------------------------------------------------- +-- Error messages + +uNDEFINED_CONST :: String +uNDEFINED_CONST = "Panic! Undefined constant or unexpected\ + \constant sort." diff --git a/Z3/Types.hs b/Z3/Types.hs new file mode 100644 --- /dev/null +++ b/Z3/Types.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} + + +-- | +-- Module : Z3.Types +-- Copyright : (c) Iago Abal, 2012 +-- (c) David Castro, 2012 +-- License : BSD3 +-- Maintainer: Iago Abal , +-- David Castro + + +module Z3.Types ( + + -- * Types + TypeZ3 + , IsTy + , IsScalar(..) + + -- ** Numeric types + , IsNum + , IsInt + , IsReal + + ) where + +import Z3.Base ( Z3Type, Z3Scalar, Z3Num ) + +import Data.Typeable ( Typeable ) + +---------------------------------------------------------------------- +-- Types + +-- | Maps a type to the underlying Z3 type. +-- +type family TypeZ3 a + +type instance TypeZ3 Bool = Bool +type instance TypeZ3 Integer = Integer +type instance TypeZ3 Rational = Rational + +-- | Types for expressions. +-- +class (Typeable a, Z3Type (TypeZ3 a)) => IsTy a where + +instance IsTy Bool where +instance IsTy Integer where +instance IsTy Rational where + +-- | Scalar types. +-- +class (Eq a, Show a, IsTy a, Z3Scalar(TypeZ3 a)) => IsScalar a where + fromZ3Type :: TypeZ3 a -> a + toZ3Type :: a -> TypeZ3 a + +instance IsScalar Bool where + fromZ3Type = id + toZ3Type = id + +instance IsScalar Integer where + fromZ3Type = id + toZ3Type = id + +instance IsScalar Rational where + fromZ3Type = id + toZ3Type = id + +------------------------------------------------------------ +-- Numeric types +-- +-- Future Work: We would like to instance 'IsInt' with 'Int32' to provide +-- support for reasoning about 32-bit integer arithmetic with overflow. +-- It would be also interesting (but perhaps more tricky) to support +-- floating point arithmetic by creating an instance of 'IsReal' for +-- 'Double'. +-- + +-- | Numeric types. +-- +class (IsScalar a, Num a, Z3Num (TypeZ3 a)) => IsNum a where +instance IsNum Integer where +instance IsNum Rational where + +-- | Typeclass for Haskell Z3 numbers of /int/ sort in Z3. +-- +class (IsNum a, Integral a, TypeZ3 a ~ Integer) => IsInt a where +instance IsInt Integer where + +-- | Typeclass for Haskell Z3 numbers of /real/ sort in Z3. +-- +class (IsNum a, Fractional a, Real a, TypeZ3 a ~ Rational) => IsReal a where +instance IsReal Rational where diff --git a/z3.cabal b/z3.cabal new file mode 100644 --- /dev/null +++ b/z3.cabal @@ -0,0 +1,54 @@ +Name: z3 +Version: 0.1.1 +Synopsis: 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.Monad") is still very experimental. + . + More information about Z3: + . + * +Homepage: http://bitbucket.org/iago/z3-haskell +License: BSD3 +License-file: LICENSE +Author: Iago Abal , + David Castro +Maintainer: Iago Abal , + David Castro +Copyright: 2012, Iago Abal, David Castro +Category: Math, Theorem Provers, Formal Methods +Build-type: Simple +Cabal-version: >= 1.6 + +source-repository head + type: mercurial + location: https://bitbucket.org/iago/z3-haskell + +Library + Exposed-modules: + + Z3.Base + Z3.Base.C + + Z3.Exprs + + Z3.Monad + + Z3.Types + + Other-modules: + + Z3.Exprs.Internal + + ghc-options: -Wall + + Build-depends: base > 3 && < 5, containers, mtl + + Build-tools: hsc2hs + Extensions: ForeignFunctionInterface + includes: z3.h + extra-libraries: gomp z3 gomp