z3 0.2.0 → 0.3.0
raw patch · 14 files changed
+3376/−1459 lines, 14 filesdep ~mtl
Dependency ranges changed: mtl
Files
- LICENSE +1/−1
- Z3/Base.hs +1598/−953
- Z3/Base/C.hsc +702/−69
- Z3/Lang.hs +0/−1
- Z3/Lang/Exprs.hs +50/−51
- Z3/Lang/Lg2.hs +7/−8
- Z3/Lang/Monad.hs +80/−184
- Z3/Lang/Nat.hs +19/−8
- Z3/Lang/Pow2.hs +8/−8
- Z3/Lang/Prelude.hs +245/−154
- Z3/Lang/TY.hs +1/−2
- Z3/Monad.hs +546/−0
- Z3/Opts.hs +81/−0
- z3.cabal +38/−20
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c)2012, Iago Abal, David Castro+Copyright (c)2012-2013, Iago Abal, David Castro All rights reserved.
Z3/Base.hs view
@@ -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 <iago.abal@gmail.com>,--- David Castro <david.castro.dcp@gmail.com>------ 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>----mkConfig :: IO Config-mkConfig = do- ptr <- z3_mk_config- fptr <- newForeignPtr ptr (z3_del_config ptr)- return $! Config fptr---- | Set a configuration parameter.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3>------ See: <http://research.microsoft.com/en-us/um/redmond/projects/z3/config.html>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>----mkBoolSort :: Context -> IO (Sort Bool)-mkBoolSort c = withContext c $ \cptr ->- Sort <$> z3_mk_bool_sort cptr---- | Create an integer type.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>----mkIntSort :: Context -> IO (Sort Integer)-mkIntSort c = withContext c $ \cptr ->- Sort <$> z3_mk_int_sort cptr---- | Create a real type.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>----mkApp1 :: (Z3Type a, Z3Type b)- => Context- -> FuncDecl (a -> b)- -> AST a- -> IO (AST b)-mkApp1 ctx fd a- = AST <$> mkApp ctx fd [unAST a]--mkApp2 :: (Z3Type a, Z3Type b, Z3Type c)- => Context- -> FuncDecl (a -> b -> c)- -> AST a -> AST b- -> IO (AST c)-mkApp2 ctx fd a b- = AST <$> mkApp ctx fd [unAST a,unAST b]--mkApp3 :: (Z3Type a, Z3Type b, Z3Type c , Z3Type d)- => Context- -> FuncDecl (a -> b -> c -> d)- -> AST a -> AST b -> AST c- -> IO (AST d)-mkApp3 ctx fd a b c- = AST <$> mkApp ctx fd [unAST a,unAST b,unAST c]--mkApp4 :: (Z3Type a, Z3Type b, Z3Type c , Z3Type d, Z3Type e)- => Context- -> FuncDecl (a -> b -> c -> d -> e)- -> AST a -> AST b -> AST c -> AST d- -> IO (AST e)-mkApp4 ctx fd a b c d- = AST <$> mkApp ctx fd [unAST a,unAST b,unAST c,unAST d]--mkApp5 :: (Z3Type a, Z3Type b, Z3Type c , Z3Type d, Z3Type e, Z3Type f)- => Context- -> FuncDecl (a -> b -> c -> d -> e -> f)- -> AST a -> AST b -> AST c -> AST d -> AST e- -> IO (AST f)-mkApp5 ctx fd a b c d e- = AST <$> mkApp ctx fd [unAST a,unAST b ,unAST c,unAST d ,unAST e]---mkApp :: Context -> FuncDecl t -> [Ptr Z3_ast] -> IO (Ptr Z3_ast)-mkApp ctx fd args =- withContext ctx $ \ctxPtr ->- withArray args $ \pargs ->- z3_mk_app ctxPtr (unFuncDecl fd) (fromIntegral $ length args) pargs----- | Declare and create a constant.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>----mkConst :: 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>----mkTrue :: Context -> IO (AST Bool)-mkTrue c = withContext c $ \cptr ->- AST <$> z3_mk_true cptr---- | Create an AST node representing /false/.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>----mkFalse :: Context -> IO (AST Bool)-mkFalse c = withContext c $ \cptr ->- AST <$> z3_mk_false cptr---- | Create an AST node representing l = r.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>----mkEq :: 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>----mkIte :: Context -> AST Bool -> AST a -> AST a -> IO (AST a)-mkIte c g e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_ite cptr (unAST g) (unAST e1) (unAST e2)---- | Create an AST node representing t1 iff t2.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>----mkIff :: Context -> AST Bool -> AST Bool -> IO (AST Bool)-mkIff c p q = withContext c $ \cptr ->- AST <$> z3_mk_iff cptr (unAST p) (unAST q)---- | Create an AST node representing t1 implies t2.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>----mkImplies :: Context -> AST Bool -> AST Bool -> IO (AST Bool)-mkImplies c p q = withContext c $ \cptr ->- AST <$> z3_mk_implies cptr (unAST p) (unAST q)---- | Create an AST node representing t1 xor t2.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>----mkXor :: Context -> AST Bool -> AST Bool -> IO (AST Bool)-mkXor c p q = 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>----mkOr :: Context -> [AST Bool] -> IO (AST Bool)-mkOr _ [] = error "Z3.Base.mkOr: empty list of expressions"-mkOr c es =- withArray es $ \aptr ->- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>----mkAdd :: Z3Num a => Context -> [AST a] -> IO (AST a)-mkAdd _ [] = error "Z3.Base.mkAdd: empty list of expressions"-mkAdd c es =- withArray es $ \aptr ->- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>----mkMul :: Z3Num a => Context -> [AST a] -> IO (AST a)-mkMul _ [] = error "Z3.Base.mkMul: empty list of expressions"-mkMul c es =- withArray es $ \aptr ->- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>----mkUnaryMinus :: Z3Num a => Context -> AST a -> IO (AST a)-mkUnaryMinus c e = withContext c $ \cptr ->- AST <$> z3_mk_unary_minus cptr (unAST e)---- | Create an AST node representing arg1 div arg2.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>----mkDiv :: Z3Num a => Context -> AST a -> AST a -> IO (AST a)-mkDiv c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_div cptr (unAST e1) (unAST e2)---- | Create an AST node representing arg1 mod arg2.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>----mkMod :: Context -> AST Integer -> AST Integer -> IO (AST Integer)-mkMod c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_mod cptr (unAST e1) (unAST e2)---- | Create an AST node representing arg1 rem arg2.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>----mkRem :: Context -> AST Integer -> AST Integer -> IO (AST Integer)-mkRem c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_rem cptr (unAST e1) (unAST e2)---- | Create less than.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>----mkLt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)-mkLt c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_lt cptr (unAST e1) (unAST e2)---- | Create less than or equal to.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>----mkLe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)-mkLe c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_le cptr (unAST e1) (unAST e2)---- | Create greater than.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>----mkGt :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)-mkGt c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_gt cptr (unAST e1) (unAST e2)---- | Create greater than or equal to.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>----mkGe :: Z3Num a => Context -> AST a -> AST a -> IO (AST Bool)-mkGe c e1 e2 = withContext c $ \cptr ->- AST <$> z3_mk_ge cptr (unAST e1) (unAST e2)---- | Coerce an integer to a real.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>----mkInt2Real :: Context -> AST Integer -> IO (AST Rational)-mkInt2Real c e = withContext c $ \cptr ->- AST <$> z3_mk_int2real cptr (unAST e)---- | Coerce a real to an integer.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>----mkReal2Int :: Context -> AST Rational -> IO (AST Integer)-mkReal2Int c e = withContext c $ \cptr ->- AST <$> z3_mk_real2int cptr (unAST e)---- | Check if a real number is an integer.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>----mkIsInt :: Context -> AST Rational -> IO (AST Bool)-mkIsInt c e = 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>----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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>----getNumeralString :: Z3Num a => Context -> AST a -> IO String-getNumeralString c a = 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>----assertCnstr :: Context -> AST Bool -> IO ()-assertCnstr ctx ast = withContext ctx $ \ctxPtr ->- z3_assert_cnstr ctxPtr (unAST ast)---- | Get model (logical context is consistent)------ Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>----getModel :: Context -> IO (Result 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>----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 <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+--+-- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>+mkConfig :: IO Config+mkConfig = Config <$> z3_mk_config++-- | Delete a configuration.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3>+--+-- See: <http://research.microsoft.com/en-us/um/redmond/projects/z3/config.html>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>+mkBoolSort :: Context -> IO Sort+mkBoolSort c = checkError c $ Sort <$> z3_mk_bool_sort (unContext c)++-- | Create an /integer/ type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>+mkIntSort :: Context -> IO Sort+mkIntSort c = checkError c $ Sort <$> z3_mk_int_sort (unContext c)++-- | Create a /real/ type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>+mkBvSort :: Context -> Int -> IO Sort+mkBvSort c n = checkError c $ Sort <$> z3_mk_bv_sort (unContext c) (fromIntegral n)++-- | Create an array type+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>+mkTrue :: Context -> IO AST+mkTrue c = checkError c $ AST <$> z3_mk_true (unContext c)++-- | Create an AST node representing /false/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>+mkFalse :: Context -> IO AST+mkFalse c = checkError c $ AST <$> z3_mk_false (unContext c)++-- | Create an AST node representing /l = r/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>+mkIsInt :: Context -> AST -> IO AST+mkIsInt c e = checkError c $ AST <$> z3_mk_is_int (unContext c) (unAST e)++---------------------------------------------------------------------+-- Bit-vectors++-- | Bitwise negation.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>+mkBvredor :: Context -> AST -> IO AST+mkBvredor c e = checkError c $ AST <$> z3_mk_bvredor (unContext c) (unAST e)++-- | Bitwise and.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7+mkBvneg :: Context -> AST -> IO AST+mkBvneg c e = checkError c $ AST <$> z3_mk_bvneg (unContext c) (unAST e)++-- | Standard two's complement addition.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad651ad68c7a060cbb5616349233cb10f>+push :: Context -> IO ()+push c = checkError c $ z3_push $ unContext c++-- | Backtrack /n/ backtracking points.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab2b3a542006c86c8d86dc37872f88b61>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>+assertCnstr :: Context -> AST -> IO ()+assertCnstr ctx ast = checkError ctx $ z3_assert_cnstr (unContext ctx) (unAST ast)++-- | Get model (logical context is consistent)+--+-- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>+getModel :: Context -> IO (Result, Maybe Model)+getModel c =+ 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee>+delModel :: Context -> Model -> IO ()+delModel c m = checkError c $ z3_del_model (unContext c) (unModel m)++-- | Convert the given model into a string.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>+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 <http://smtlib.cs.uiowa.edu/logics.html>+--+-- /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
Z3/Base/C.hsc view
@@ -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 <iago.abal@gmail.com>, -- David Castro <david.castro.dcp@gmail.com> -- -- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>--- foreign import ccall unsafe "Z3_mk_config" z3_mk_config :: IO (Ptr Z3_config) -- | Delete the given configuration object. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774>--- foreign import ccall unsafe "Z3_del_config" z3_del_config :: Ptr Z3_config -> IO () -- | Set a configuration parameter. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46>--- foreign import ccall unsafe "Z3_mk_context" z3_mk_context :: Ptr Z3_config -> IO (Ptr Z3_context) -- | Delete the given logical context. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200>--- foreign import ccall unsafe "Z3_del_context" z3_del_context :: Ptr Z3_context -> IO () - --------------------------------------------------------------------- -- * Symbols -- | Create a Z3 symbol using a C string. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>--- foreign import ccall unsafe "Z3_mk_bool_sort" z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Create an integer type. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>--- foreign import ccall unsafe "Z3_mk_int_sort" z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) -- | Create a real type. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2>--- foreign import ccall unsafe "Z3_mk_func_decl" z3_mk_func_decl :: Ptr Z3_context -> Ptr Z3_symbol@@ -177,7 +218,6 @@ -- | Create a constant or function application. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>--- foreign import ccall unsafe "Z3_mk_app" z3_mk_app :: Ptr Z3_context -> Ptr Z3_func_decl@@ -188,7 +228,6 @@ -- | Declare and create a constant. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>--- foreign import ccall unsafe "Z3_mk_true" z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) -- | Create an AST node representing /false/. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>+foreign import ccall unsafe "Z3_mk_bvredor"+ z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Bitwise and.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7+foreign import ccall unsafe "Z3_mk_bvneg"+ z3_mk_bvneg :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Standard two's complement addition.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>+--+foreign import ccall unsafe "Z3_mk_repeat"+ z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Shift left.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>+--+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabe0bbc1e01a084a75506a62e5e6900b3>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8779204998136569c3e166c34cfd3e2c>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7201b6231b61421c005457206760a121>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga42cc319787d485d9cb665d80e02d206f>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88a165138162a8bac401672f0a1b7891>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85>--- foreign import ccall unsafe "Z3_mk_pattern" z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) -- | Create a bound variable. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e>--- foreign import ccall unsafe "Z3_mk_bound" z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- | Create a forall formula. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7e975b7d7ac96de1db73d8f71166c663>--- foreign import ccall unsafe "Z3_mk_forall" z3_mk_forall :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_pattern)@@ -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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga47d3655283564918c85bda0b423b7f67>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>--- 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 : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>--- foreign import ccall unsafe "Z3_check" z3_check :: Ptr Z3_context -> IO Z3_lbool @@ -518,9 +904,256 @@ -- | Delete a model object. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee>--- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac7f883536538ab0ad234fde58988e673>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a91c9f749b89e1dcf1493177d395d0c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae4df28ba713b81ee99abd929e32484ea>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga39e3df967eaad45b343256d56c54e91c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4974397cb652c7f7f479012eb465e250>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga11498ce4b25d294f5f89ab7ac1b74c62>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac2e899a4906b6133a23fdb60ef992ec9>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga624e692e180a8b2f617156b1e1ae9722>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ae64e7f89201589424191a9b824d3ca>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c>+foreign import ccall unsafe "Z3_mk_solver"+ z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)++-- | Create a simple solver.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c>+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:+--+-- <http://smtlib.cs.uiowa.edu/logics.html>+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga54244cfc9d9cd2ca8f08c3909d700628>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga887441b3468a1bc605bbf564ddebf2ae>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga388e25a8b477abbd49f08c6c29dfa12d>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2362dcef4e9b8ede41298a50428902ff>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae41bebe15b1b1105f9abb8690188d1e2>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40aa98e15aceffa5be3afad2e065478a>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4a4a215b9130d7980e3c393fe857335f>+foreign import ccall unsafe "Z3_solver_reset"+ z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO ()++-- | Add a constraint to a solver.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72afadf5e8b216f2c6ae675e872b8be4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46fb6f3aa3ef451d6be01a737697810>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga000e369de7b71caa4ee701089709c526>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf14a54d904a7e45eecc00c5fb8a9d5c9>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaed5d19000004b43dd75e487682e91b55>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga20d66dac19b6d6a06537843d0e25f761>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab1aa4b78298fe00b3167bf7bfd88aea3>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51b048ddbbcd88708e7aa4fe1c2462d6>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf90c72f63eab298e1dd750f6a26fb945>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga15243dcad77f5571e28e8aa1da465675>+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 : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ac771e68b28d2c86f40aa84889b3807>+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 : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadaa12e9990f37b0c1e2bf1dd502dbf39>+foreign import ccall unsafe "Z3_set_error_handler"+ z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO ()++-- | Set an error.+--+-- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga41cf70319c4802ab7301dd168d6f5e45>+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 : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6>+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 : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92>+foreign import ccall unsafe "Z3_get_error_msg_ex"+ z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string
Z3/Lang.hs view
@@ -7,7 +7,6 @@ -- Maintainer: Iago Abal <iago.abal@gmail.com>, -- David Castro <david.castro.dcp@gmail.com> -- Stability : experimental--- module Z3.Lang ( module Z3.Lang.Prelude
Z3/Lang/Exprs.hs view
@@ -3,6 +3,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeFamilies #-} @@ -14,25 +15,26 @@ -- Maintainer: Iago Abal <iago.abal@gmail.com>, -- David Castro <david.castro.dcp@gmail.com> -- 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.
Z3/Lang/Lg2.hs view
@@ -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+
Z3/Lang/Monad.hs view
@@ -13,6 +13,7 @@ -- David Castro <david.castro.dcp@gmail.com> -- 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 <http://smtlib.cs.uiowa.edu/logics.html>+ , 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
Z3/Lang/Nat.hs view
@@ -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
Z3/Lang/Pow2.hs view
@@ -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
Z3/Lang/Prelude.hs view
@@ -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 <iago.abal@gmail.com>, -- David Castro <david.castro.dcp@gmail.com> -- 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+
Z3/Lang/TY.hs view
@@ -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)
+ Z3/Monad.hs view
@@ -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 <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+--+-- 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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>+mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol+mkStringSymbol = liftFun1 Base.mkStringSymbol++---------------------------------------------------------------------+-- Sorts++-- | Create the /boolean/ type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>+mkBoolSort :: MonadZ3 z3 => z3 Sort+mkBoolSort = liftScalar Base.mkBoolSort++-- | Create the /integer/ type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>+mkIntSort :: MonadZ3 z3 => z3 Sort+mkIntSort = liftScalar Base.mkIntSort++-- | Create the /real/ type.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>+mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST+mkApp = liftFun2 Base.mkApp++-- | Declare and create a constant.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>+mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST+mkConst = liftFun2 Base.mkConst++-- | Create an AST node representing /true/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>+mkTrue :: MonadZ3 z3 => z3 AST+mkTrue = liftScalar Base.mkTrue++-- | Create an AST node representing /false/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>+mkFalse :: MonadZ3 z3 => z3 AST+mkFalse = liftScalar Base.mkFalse++-- | Create an AST node representing /l = r/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>+mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST+mkEq = liftFun2 Base.mkEq++-- | The distinct construct is used for declaring the arguments pairwise+-- distinct.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7>+mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST+mkDistinct = liftFun1 Base.mkDistinct++-- | Create an AST node representing /not(a)/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>+mkNot :: MonadZ3 z3 => AST -> z3 AST+mkNot = liftFun1 Base.mkNot++-- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>+mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST+mkIte = liftFun3 Base.mkIte++-- | Create an AST node representing /t1 iff t2/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>+mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST+mkIff = liftFun2 Base.mkIff++-- | Create an AST node representing /t1 implies t2/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>+mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST+mkImplies = liftFun2 Base.mkImplies++-- | Create an AST node representing /t1 xor t2/.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>+mkAnd :: MonadZ3 z3 => [AST] -> z3 AST+mkAnd = liftFun1 Base.mkAnd++-- | Create an AST node representing args[0] or ... or args[num_args-1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>+mkOr :: MonadZ3 z3 => [AST] -> z3 AST+mkOr = liftFun1 Base.mkOr++-- | Create an AST node representing args[0] + ... + args[num_args-1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>+mkAdd :: MonadZ3 z3 => [AST] -> z3 AST+mkAdd = liftFun1 Base.mkAdd++-- | Create an AST node representing args[0] * ... * args[num_args-1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>+mkMul :: MonadZ3 z3 => [AST] -> z3 AST+mkMul = liftFun1 Base.mkMul++-- | Create an AST node representing args[0] - ... - args[num_args - 1].+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>+mkSub :: MonadZ3 z3 => [AST] -> z3 AST+mkSub = liftFun1 Base.mkSub++-- | Create an AST node representing -arg.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>+mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST+mkUnaryMinus = liftFun1 Base.mkUnaryMinus++-- | Create an AST node representing arg1 div arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>+mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST+mkDiv = liftFun2 Base.mkDiv++-- | Create an AST node representing arg1 mod arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>+mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST+mkMod = liftFun2 Base.mkMod++-- | Create an AST node representing arg1 rem arg2.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>+mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST+mkRem = liftFun2 Base.mkRem++-- | Create less than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>+mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST+mkLt = liftFun2 Base.mkLt++-- | Create less than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>+mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST+mkLe = liftFun2 Base.mkLe++-- | Create greater than.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>+mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST+mkGt = liftFun2 Base.mkGt++-- | Create greater than or equal to.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>+mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST+mkGe = liftFun2 Base.mkGe++-- | Coerce an integer to a real.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>+mkInt2Real :: MonadZ3 z3 => AST -> z3 AST+mkInt2Real = liftFun1 Base.mkInt2Real++-- | Coerce a real to an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>+mkReal2Int :: MonadZ3 z3 => AST -> z3 AST+mkReal2Int = liftFun1 Base.mkReal2Int++-- | Check if a real number is an integer.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>+mkIsInt :: MonadZ3 z3 => AST -> z3 AST+mkIsInt = liftFun1 Base.mkIsInt++---------------------------------------------------------------------+-- Numerals++-- | Create a numeral of a given sort.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>+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: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>+assertCnstr :: MonadZ3 z3 => AST -> z3 ()+assertCnstr = liftSolver1 Base.solverAssertCnstr Base.assertCnstr++-- | Get model.+--+-- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>+getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)+getModel = liftSolver0 Base.solverCheckAndGetModel Base.getModel++-- | Delete a model object.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee>+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+
+ Z3/Opts.hs view
@@ -0,0 +1,81 @@++-- |+-- Module : Z3.Opts+-- Copyright : (c) Iago Abal, 2013+-- (c) David Castro, 2013+-- License : BSD3+-- Maintainer: Iago Abal <iago.abal@gmail.com>,+-- David Castro <david.castro.dcp@gmail.com>+--+-- 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
z3.cabal view
@@ -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 (<http://z3.codeplex.com>). .- 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: <http://www.iagoabal.eu/z3-haskell/doc>+ 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: .- * <http://z3.codeplex.com>+ * 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+ <http://www.iagoabal.eu/z3-haskell/doc/0.3.0> Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE@@ -25,7 +29,7 @@ David Castro <david.castro.dcp@gmail.com> Maintainer: Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>-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 <<loop>> 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