z3 0.3.1 → 0.3.2
raw patch · 11 files changed
+2361/−2449 lines, 11 files
Files
- Z3/Base.hs +1953/−1838
- Z3/Base/C.hsc +241/−584
- Z3/Lang.hs +8/−2
- Z3/Lang/Lg2.hs +6/−0
- Z3/Lang/Monad.hs +2/−1
- Z3/Lang/Nat.hs +6/−0
- Z3/Lang/Pow2.hs +6/−0
- Z3/Lang/Prelude.hs +6/−3
- Z3/Monad.hs +97/−8
- Z3/Opts.hs +24/−6
- z3.cabal +12/−7
Z3/Base.hs view
@@ -1,1842 +1,1957 @@ {-# 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- , FuncInterp- , FuncEntry- , Params- , Solver-- -- ** Satisfiability result- , Result(..)-- -- * Configuration- , mkConfig- , delConfig- , withConfig- , setParamValue-- -- * Context- , mkContext- , delContext- , withContext- , contextToString- , showContext-- -- * Symbols- , mkIntSymbol- , mkStringSymbol-- -- * Sorts- , mkUninterpretedSort- , mkBoolSort- , mkIntSort- , mkRealSort- , mkBvSort- , mkArraySort- , mkTupleSort-- -- * 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- , FuncModel (..)- , eval- , evalT- , evalFunc- , evalArray- , getFuncInterp- , isAsArray- , getAsArrayFuncDecl- , funcInterpGetNumEntries- , funcInterpGetEntry- , funcInterpGetElse- , funcInterpGetArity- , funcEntryGetValue- , funcEntryGetNumArgs- , funcEntryGetArg- , modelToString- , showModel-- -- * 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- , benchmarkToSMTLibString-- -- * 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 interpretation of a function.-newtype FuncInterp = FuncInterp { unFuncInterp :: Ptr Z3_func_interp }- deriving Eq---- | An entry in an interpreted function-newtype FuncEntry = FuncEntry { unFuncEntry :: Ptr Z3_func_entry }- 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---- | Convert the given logical context into a string.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216>-contextToString :: Context -> IO String-contextToString c =- checkError c $ z3_context_to_string (unContext c) >>= peekCString---- | Alias for 'contextToString'.-showContext :: Context -> IO String-showContext = contextToString-------------------------------------------------------------------------- Symbols---- | Create a Z3 symbol using an integer.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3df806baf6124df3e63a58cf23e12411>-mkIntSymbol :: Integral int => Context -> int -> IO Symbol-mkIntSymbol ctx i- | 0 <= i && i <= 2^(30::Int)-1- = Symbol <$> z3_mk_int_symbol (unContext ctx) (fromIntegral i)- | otherwise- = error "Z3.Base.mkIntSymbol: invalid range"--{-# SPECIALIZE mkIntSymbol :: Context -> Int -> IO Symbol #-}-{-# SPECIALIZE mkIntSymbol :: Context -> Integer -> IO Symbol #-}---- | 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---- | Create a free (uninterpreted) type using the given name (symbol).------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>-mkUninterpretedSort :: Context -> Symbol -> IO Sort-mkUninterpretedSort c sy = checkError c $- Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy)---- | 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)---- | Create a tuple type------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>-mkTupleSort :: Context -- ^ Context- -> Symbol -- ^ Name of the sort- -> [(Symbol, Sort)] -- ^ Name and sort of each field- -> IO (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function- -- declarations for the- -- constructor and projections.-mkTupleSort c sym symSorts = checkError c $- let (syms, sorts) = unzip symSorts- in withArrayLen (map unSymbol syms) $ \ n symsPtr ->- withArray (map unSort sorts) $ \ sortsPtr ->- alloca $ \ outConstrPtr ->- allocaArray n $ \ outProjsPtr -> do- sort <- checkError c $ z3_mk_tuple_sort- (unContext c) (unSymbol sym)- (fromIntegral n) symsPtr sortsPtr- outConstrPtr outProjsPtr- outConstr <- peek outConstrPtr- outProjs <- peekArray n outProjsPtr- return (Sort sort, FuncDecl outConstr, map FuncDecl outProjs)----- 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)---- | The interpretation of a function is a mapping part (arguments to values)--- and an 'else' part.-data FuncModel = FuncModel- { interpMap :: [([AST], AST)]- , interpElse :: AST- }---- | Evaluate a function declaration to a list of argument/value pairs.-evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)-evalFunc ctx m fDecl =- do interpMb <- getFuncInterp ctx m fDecl- case interpMb of- Nothing -> return Nothing- Just interp ->- do funcMap <- getMapFromInterp ctx interp- elsePart <- funcInterpGetElse ctx interp- return (Just $ FuncModel funcMap elsePart)---- | Evaluate an array as a function, if possible.-evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)-evalArray ctx model array =- do -- The array must first be evaluated normally, to get it into- -- 'as-array' form, which is required to acquire the FuncDecl.- evaldArrayMb <- eval ctx model array- case evaldArrayMb of- Nothing -> return Nothing- Just evaldArray ->- do canConvert <- isAsArray ctx evaldArray- if canConvert- then- do arrayDecl <- getAsArrayFuncDecl ctx evaldArray- evalFunc ctx model arrayDecl- else return Nothing----- | Return the function declaration f associated with a (_ as_array f) node.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>-getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl-getAsArrayFuncDecl ctx a = checkError ctx $- FuncDecl <$> z3_get_as_array_func_decl (unContext ctx) (unAST a)---- | The (_ as-array f) AST node is a construct for assigning interpretations--- for arrays in Z3. It is the array such that forall indices i we have that--- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE--- if the a is an as-array AST node.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>-isAsArray :: Context -> AST -> IO Bool-isAsArray ctx a = toBool <$> z3_is_as_array (unContext ctx) (unAST a)---getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)]-getMapFromInterp ctx interp =- do n <- funcInterpGetNumEntries ctx interp- entries <- mapM (funcInterpGetEntry ctx interp) [0..n-1]- mapM (getEntry ctx) entries--getEntry :: Context -> FuncEntry -> IO ([AST], AST)-getEntry ctx entry =- do val <- funcEntryGetValue ctx entry- args <- getEntryArgs ctx entry- return (args, val)--getEntryArgs :: Context -> FuncEntry -> IO [AST]-getEntryArgs ctx entry =- do n <- funcEntryGetNumArgs ctx entry- mapM (funcEntryGetArg ctx entry) [0..n-1]---- | Return the interpretation of the function f in the model m.--- Return NULL, if the model does not assign an interpretation for f.--- That should be interpreted as: the f does not matter.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>-getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)-getFuncInterp c m fd = do- ptr <- checkError c $- z3_model_get_func_interp (unContext c) (unModel m) (unFuncDecl fd)- return $ FuncInterp <$> ptrToMaybe ptr---- | Return the number of entries in the given function interpretation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>-funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int-funcInterpGetNumEntries ctx fi = checkError ctx $ fromIntegral <$>- z3_func_interp_get_num_entries (unContext ctx) (unFuncInterp fi)---- | Return a _point_ of the given function intepretation.--- It represents the value of f in a particular point.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>-funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry-funcInterpGetEntry ctx fi i = checkError ctx $ FuncEntry <$>- z3_func_interp_get_entry (unContext ctx) (unFuncInterp fi) (fromIntegral i)---- | Return the 'else' value of the given function interpretation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>-funcInterpGetElse :: Context -> FuncInterp -> IO AST-funcInterpGetElse ctx fi = checkError ctx $- AST <$> z3_func_interp_get_else (unContext ctx) (unFuncInterp fi)---- | Return the arity (number of arguments) of the given function--- interpretation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>-funcInterpGetArity :: Context -> FuncInterp -> IO Int-funcInterpGetArity ctx fi = checkError ctx $- fromIntegral <$> z3_func_interp_get_arity (unContext ctx) (unFuncInterp fi)---- | Return the value of this point.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>-funcEntryGetValue :: Context -> FuncEntry -> IO AST-funcEntryGetValue ctx entry = checkError ctx $- AST <$> z3_func_entry_get_value (unContext ctx) (unFuncEntry entry)---- | Return the number of arguments in a Z3_func_entry object.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>-funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int-funcEntryGetNumArgs ctx entry = checkError ctx $ fromIntegral <$>- z3_func_entry_get_num_args (unContext ctx) (unFuncEntry entry)---- | Return an argument of a Z3_func_entry object.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>-funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST-funcEntryGetArg ctx entry i = checkError ctx $ AST <$>- z3_func_entry_get_arg (unContext ctx) (unFuncEntry entry) (fromIntegral i)---- | Convert the given model into a string.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>-modelToString :: Context -> Model -> IO String-modelToString c m = checkError c $- z3_model_to_string (unContext c) (unModel m) >>= peekCString---- | Alias for 'modelToString'.-showModel :: Context -> Model -> IO String-showModel = modelToString-------------------------------------------------------------------------- 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 = fmap Model . ptrToMaybe---- | 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)---- | 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---- | Convert the given benchmark into SMT-LIB formatted string.------ The output format can be configured via 'setASTPrintMode'.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4>-benchmarkToSMTLibString :: Context- -> String -- ^ name- -> String -- ^ logic- -> String -- ^ status- -> String -- ^ attributes- -> [AST] -- ^ assumptions- -> AST -- ^ formula- -> IO String-benchmarkToSMTLibString c name logic st attr assump f =- withCString name $ \cname ->- withCString logic $ \clogic ->- withCString st $ \cst ->- withCString attr $ \cattr ->- withArray (map unAST assump) $ \cassump ->- z3_benchmark_to_smtlib_string (unContext c) cname clogic cst cattr- numAssump cassump (unAST f)- >>= peekCString- where numAssump = genericLength assump-------------------------------------------------------------------------- Utils+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}++-- |+-- Module : Z3.Base+-- Copyright : (c) Iago Abal, 2012-2014+-- (c) David Castro, 2012-2013+-- License : BSD3+-- Maintainer: Iago Abal <mail@iagoabal.eu>,+-- David Castro <david.castro.dcp@gmail.com>+--+-- Low-level bindings to Z3 API.+--+-- There is (mostly) a one-to-one correspondence with Z3 C API, thus see+-- <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html>+-- for further details.+--+-- Note that these bindings still focus on the old Z3 3.x API, and will not+-- handle reference counting for you if you decide to use Z3 4.x API functions.+-- Mixing both API is known to cause some segmentation faults!+--+-- Supporting Z3 4.x API (and removing support for 3.x) is planned for+-- the 0.4 version of these bindings.++{- HACKING++Add here the IO-based wrapper for a new Z3 API function:++* Take a look to a few others API functions and follow the same coding style.+ * 2-space wide indentation, no tabs.+ * No trailing spaces, please.+ * ...+* Place the API function in the right section, according to the Z3's API documentation.+* Annotate the API function with a short but concise haddock comment.+ * Look at the Z3 API documentation for inspiration.+* Add the API function to the module export list, (only) if needed.++This should be straightforward for most cases using [MARSHALLING HELPERS].+-}++module Z3.Base (++ -- * Types+ Config+ , Context+ , Symbol+ , AST+ , Sort+ , FuncDecl+ , App+ , Pattern+ , Model+ , FuncInterp+ , FuncEntry+ , Params+ , Solver++ -- ** Satisfiability result+ , Result(..)++ -- * Configuration+ , mkConfig+ , delConfig+ , withConfig+ , setParamValue++ -- * Context+ , mkContext+ , delContext+ , withContext+ , contextToString+ , showContext++ -- * Symbols+ , mkIntSymbol+ , mkStringSymbol++ -- * Sorts+ , mkUninterpretedSort+ , mkBoolSort+ , mkIntSort+ , mkRealSort+ , mkBvSort+ , mkArraySort+ , mkTupleSort++ -- * 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+ , mkForallConst+ , mkExistsConst++ -- * Accessors+ , getBvSortSize+ , getSort+ , getBool+ , getInt+ , getReal+ , toApp++ -- * Models+ , FuncModel (..)+ , eval+ , evalT+ , evalFunc+ , evalArray+ , getFuncInterp+ , isAsArray+ , getAsArrayFuncDecl+ , funcInterpGetNumEntries+ , funcInterpGetEntry+ , funcInterpGetElse+ , funcInterpGetArity+ , funcEntryGetValue+ , funcEntryGetNumArgs+ , funcEntryGetArg+ , modelToString+ , showModel++ -- * Constraints+ , assertCnstr+ , check+ , checkAndGetModel+ , getModel+ , delModel+ , push+ , pop++ -- * Parameters+ , mkParams+ , paramsSetBool+ , paramsSetUInt+ , paramsSetDouble+ , paramsSetSymbol+ , paramsToString++ -- * Solvers+ -- /EXPERIMENTAL/ support for solvers,+ -- very fragile and likely to cause crashes!!!+ --+ -- Yet, there are people using it, so you may want to give it a try.+ , Logic(..)+ , mkSolver+ , mkSimpleSolver+ , mkSolverForLogic+ , solverSetParams+ , solverPush+ , solverPop+ , solverReset+ , solverGetNumScopes+ , solverAssertCnstr+ , solverAssertAndTrack+ , solverCheck+ , solverGetModel+ , solverCheckAndGetModel+ , solverGetReasonUnknown+ , solverToString++ -- * String Conversion+ , ASTPrintMode(..)+ , setASTPrintMode+ , astToString+ , patternToString+ , sortToString+ , funcDeclToString+ , benchmarkToSMTLibString++ -- * Miscellaneous+ , Version(..)+ , getVersion++ -- * Error Handling+ , Z3Error(..)+ , Z3ErrorCode(..)+ ) where++import Z3.Base.C++import Control.Applicative ( (<$>), (<*) )+import Control.Exception ( Exception, bracket, throw )+import Control.Monad ( when )+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, newForeignPtr )+import Foreign.C+ ( CDouble, CInt, CUInt, CLLong, CULLong, CString+ , peekCString+ , withCString )+import Foreign.Concurrent++---------------------------------------------------------------------+-- 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 /symbol/.+--+-- Used to name types, constants and functions.+newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol }+ deriving (Eq, Ord, Show, Storable)++-- | A Z3 /AST node/.+--+-- This is the data-structure used in Z3 to represent terms, formulas and types.+newtype AST = AST { unAST :: Ptr Z3_ast }+ deriving (Eq, Ord, Show, Storable, Typeable)++-- | A kind of AST representing /types/.+newtype Sort = Sort { unSort :: Ptr Z3_sort }+ deriving (Eq, Ord, Show, Storable)++-- | A kind of AST representing function symbols.+newtype FuncDecl = FuncDecl { unFuncDecl :: Ptr Z3_func_decl }+ deriving (Eq, Ord, Show, Storable, Typeable)++-- | A kind of AST representing constant and function declarations.+newtype App = App { unApp :: Ptr Z3_app }+ deriving (Eq, Ord, Show, Storable)++-- | A kind of AST representing pattern and multi-patterns 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++-- | An interpretation of a function in a model.+newtype FuncInterp = FuncInterp { unFuncInterp :: Ptr Z3_func_interp }+ deriving Eq++-- | Representation of the value of a 'Z3_func_interp' at a particular point.+newtype FuncEntry = FuncEntry { unFuncEntry :: Ptr Z3_func_entry }+ 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.+--+-- A(n) (incremental) solver, possibly specialized by a particular tactic+-- or logic.+newtype Solver = Solver { _unSolver :: ForeignPtr Z3_solver }+ deriving Eq++-- | Result of a satisfiability check.+--+-- This corresponds to the /z3_lbool/ type in the C API.+data Result+ = Sat+ | Unsat+ | Undef+ deriving (Eq, Ord, Read, Show)++---------------------------------------------------------------------+-- Configuration++-- | Create a configuration.+mkConfig :: IO Config+mkConfig = Config <$> z3_mk_config++-- | Delete a configuration.+delConfig :: Config -> IO ()+delConfig = z3_del_config . unConfig++-- | Run a computation using a temporally created configuration.+--+-- Note that the configuration object can be thrown away once+-- it has been used to create the Z3 'Context'.+withConfig :: (Config -> IO a) -> IO a+withConfig = bracket mkConfig delConfig++-- | Set a configuration parameter.+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.+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.+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++-- | Convert the given logical context into a string.+contextToString :: Context -> IO String+contextToString = liftFun0 z3_context_to_string++-- | Alias for 'contextToString'.+showContext :: Context -> IO String+showContext = contextToString+{-# DEPRECATED showContext "Use contextToString instead." #-}++---------------------------------------------------------------------+-- Symbols++-- | Create a Z3 symbol using an integer.+--+-- @mkIntSymbol c i@ /requires/ @0 <= i < 2^30@+mkIntSymbol :: Integral int => Context -> int -> IO Symbol+mkIntSymbol c i+ | 0 <= i && i <= 2^(30::Int)-1+ = marshal z3_mk_int_symbol c $ h2c i+ | otherwise+ = error "Z3.Base.mkIntSymbol: invalid range"++{-# SPECIALIZE mkIntSymbol :: Context -> Int -> IO Symbol #-}+{-# SPECIALIZE mkIntSymbol :: Context -> Integer -> IO Symbol #-}++-- | Create a Z3 symbol using a string.+mkStringSymbol :: Context -> String -> IO Symbol+mkStringSymbol = liftFun1 z3_mk_string_symbol++---------------------------------------------------------------------+-- Sorts++-- | Create a free (uninterpreted) type using the given name (symbol).+--+-- Two free types are considered the same iff the have the same name.+mkUninterpretedSort :: Context -> Symbol -> IO Sort+mkUninterpretedSort = liftFun1 z3_mk_uninterpreted_sort++-- | Create the /boolean/ type.+--+-- This type is used to create propositional variables and predicates.+mkBoolSort :: Context -> IO Sort+mkBoolSort = liftFun0 z3_mk_bool_sort++-- | Create an /integer/ type.+--+-- This is the type of arbitrary precision integers.+-- A machine integer can be represented using bit-vectors, see 'mkBvSort'.+mkIntSort :: Context -> IO Sort+mkIntSort = liftFun0 z3_mk_int_sort++-- | Create a /real/ type.+--+-- This type is not a floating point number.+-- Z3 does not have support for floating point numbers yet.+mkRealSort :: Context -> IO Sort+mkRealSort = liftFun0 z3_mk_real_sort++-- | Create a bit-vector type of the given size.+--+-- This type can also be seen as a machine integer.+--+-- @mkBvSort c sz@ /requires/ @sz >= 0@+mkBvSort :: Context -> Int -> IO Sort+mkBvSort = liftFun1 z3_mk_bv_sort++-- TODO: Z3_mk_finite_domain_sort++-- | Create an array type+--+-- We usually represent the array type as: [domain -> range].+-- Arrays are usually used to model the heap/memory in software verification.+mkArraySort :: Context -> Sort -> Sort -> IO Sort+mkArraySort = liftFun2 z3_mk_array_sort++-- | Create a tuple type+--+-- A tuple with n fields has a constructor and n projections.+-- This function will also declare the constructor and projection functions.+mkTupleSort :: Context -- ^ Context+ -> Symbol -- ^ Name of the sort+ -> [(Symbol, Sort)] -- ^ Name and sort of each field+ -> IO (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function+ -- declarations for the+ -- constructor and projections.+mkTupleSort c sym symSorts = checkError c $+ h2c sym $ \symPtr ->+ marshalArrayLen syms $ \ n symsPtr ->+ marshalArray sorts $ \ sortsPtr ->+ alloca $ \ outConstrPtr ->+ allocaArray n $ \ outProjsPtr -> do+ sort <- z3_mk_tuple_sort (unContext c) symPtr+ (fromIntegral n) symsPtr sortsPtr+ outConstrPtr outProjsPtr+ outConstr <- peek outConstrPtr+ outProjs <- peekArray n outProjsPtr+ return (Sort sort, FuncDecl outConstr, map FuncDecl outProjs)+ where (syms, sorts) = unzip symSorts++-- TODO Sorts: from Z3_mk_enumeration_sort on++---------------------------------------------------------------------+-- Constants and Applications++-- | Declare a constant or function.+mkFuncDecl :: Context -- ^ Logical context.+ -> Symbol -- ^ Name of the function (or constant).+ -> [Sort] -- ^ Function domain (empty for constants).+ -> Sort -- ^ Return sort of the function.+ -> IO FuncDecl+mkFuncDecl ctx smb dom rng =+ marshal z3_mk_func_decl ctx $ \f ->+ h2c smb $ \ptrSym ->+ marshalArrayLen dom $ \domNum domArr ->+ h2c rng $ \ptrRange ->+ f ptrSym domNum domArr ptrRange++-- | Create a constant or function application.+mkApp :: Context -> FuncDecl -> [AST] -> IO AST+mkApp ctx fd args = marshal z3_mk_app ctx $ \f ->+ h2c fd $ \fdPtr ->+ marshalArrayLen args $ \argsNum argsArr ->+ f fdPtr argsNum argsArr++-- | Declare and create a constant.+--+-- This is a shorthand for:+-- @do xd <- mkFunDecl c x [] s; mkApp c xd []@+mkConst :: Context -> Symbol -> Sort -> IO AST+mkConst = liftFun2 z3_mk_const++-- TODO Constants and Applications: Z3_mk_fresh_func_decl+-- TODO Constants and Applications: Z3_mk_fresh_const++-- | Create an AST node representing /true/.+mkTrue :: Context -> IO AST+mkTrue = liftFun0 z3_mk_true++-- | Create an AST node representing /false/.+mkFalse :: Context -> IO AST+mkFalse = liftFun0 z3_mk_false++-- | Create an AST node representing /l = r/.+mkEq :: Context -> AST -> AST -> IO AST+mkEq = liftFun2 z3_mk_eq++-- | The distinct construct is used for declaring the arguments pairwise+-- distinct.+--+-- That is, @and [ args!!i /= args!!j | i <- [0..length(args)-1], j <- [i+1..length(args)-1] ]@+mkDistinct :: Context -> [AST] -> IO AST+mkDistinct =+ liftAstN "Z3.Base.mkDistinct: empty list of expressions" z3_mk_distinct++-- | Create an AST node representing /not(a)/.+mkNot :: Context -> AST -> IO AST+mkNot = liftFun1 z3_mk_not++-- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/.+mkIte :: Context -> AST -> AST -> AST -> IO AST+mkIte = liftFun3 z3_mk_ite++-- | Create an AST node representing /t1 iff t2/.+mkIff :: Context -> AST -> AST -> IO AST+mkIff = liftFun2 z3_mk_iff++-- | Create an AST node representing /t1 implies t2/.+mkImplies :: Context -> AST -> AST -> IO AST+mkImplies = liftFun2 z3_mk_implies++-- | Create an AST node representing /t1 xor t2/.+mkXor :: Context -> AST -> AST -> IO AST+mkXor = liftFun2 z3_mk_xor++-- | Create an AST node representing args[0] and ... and args[num_args-1].+mkAnd :: Context -> [AST] -> IO AST+mkAnd = liftAstN "Z3.Base.mkAnd: empty list of expressions" z3_mk_and++-- | Create an AST node representing args[0] or ... or args[num_args-1].+mkOr :: Context -> [AST] -> IO AST+mkOr = liftAstN "Z3.Base.mkOr: empty list of expressions" z3_mk_or++-- | Create an AST node representing args[0] + ... + args[num_args-1].+mkAdd :: Context -> [AST] -> IO AST+mkAdd = liftAstN "Z3.Base.mkAdd: empty list of expressions" z3_mk_add++-- | Create an AST node representing args[0] * ... * args[num_args-1].+mkMul :: Context -> [AST] -> IO AST+mkMul = liftAstN "Z3.Base.mkMul: empty list of expressions" z3_mk_mul++-- | Create an AST node representing args[0] - ... - args[num_args - 1].+mkSub :: Context -> [AST] -> IO AST+mkSub = liftAstN "Z3.Base.mkSub: empty list of expressions" z3_mk_sub++-- | Create an AST node representing -arg.+mkUnaryMinus :: Context -> AST -> IO AST+mkUnaryMinus = liftFun1 z3_mk_unary_minus++-- | Create an AST node representing arg1 div arg2.+mkDiv :: Context -> AST -> AST -> IO AST+mkDiv = liftFun2 z3_mk_div++-- | Create an AST node representing arg1 mod arg2.+mkMod :: Context -> AST -> AST -> IO AST+mkMod = liftFun2 z3_mk_mod++-- | Create an AST node representing arg1 rem arg2.+mkRem :: Context -> AST -> AST -> IO AST+mkRem = liftFun2 z3_mk_rem++-- | Create less than.+mkLt :: Context -> AST -> AST -> IO AST+mkLt = liftFun2 z3_mk_lt++-- | Create less than or equal to.+mkLe :: Context -> AST -> AST -> IO AST+mkLe = liftFun2 z3_mk_le++-- | Create greater than.+mkGt :: Context -> AST -> AST -> IO AST+mkGt = liftFun2 z3_mk_gt++-- | Create greater than or equal to.+mkGe :: Context -> AST -> AST -> IO AST+mkGe = liftFun2 z3_mk_ge++-- | Coerce an integer to a real.+mkInt2Real :: Context -> AST -> IO AST+mkInt2Real = liftFun1 z3_mk_int2real++-- | Coerce a real to an integer.+mkReal2Int :: Context -> AST -> IO AST+mkReal2Int = liftFun1 z3_mk_real2int++-- | Check if a real number is an integer.+mkIsInt :: Context -> AST -> IO AST+mkIsInt = liftFun1 z3_mk_is_int++---------------------------------------------------------------------+-- Bit-vectors++-- | Bitwise negation.+mkBvnot :: Context -> AST -> IO AST+mkBvnot = liftFun1 z3_mk_bvnot++-- | Take conjunction of bits in vector, return vector of length 1.+mkBvredand :: Context -> AST -> IO AST+mkBvredand = liftFun1 z3_mk_bvredand++-- | Take disjunction of bits in vector, return vector of length 1.+mkBvredor :: Context -> AST -> IO AST+mkBvredor = liftFun1 z3_mk_bvredor++-- | Bitwise and.+mkBvand :: Context -> AST -> AST -> IO AST+mkBvand = liftFun2 z3_mk_bvand++-- | Bitwise or.+mkBvor :: Context -> AST -> AST -> IO AST+mkBvor = liftFun2 z3_mk_bvor++-- | Bitwise exclusive-or.+mkBvxor :: Context -> AST -> AST -> IO AST+mkBvxor = liftFun2 z3_mk_bvxor++-- | Bitwise nand.+mkBvnand :: Context -> AST -> AST -> IO AST+mkBvnand = liftFun2 z3_mk_bvnand++-- | Bitwise nor.+mkBvnor :: Context -> AST -> AST -> IO AST+mkBvnor = liftFun2 z3_mk_bvnor++-- | Bitwise xnor.+mkBvxnor :: Context -> AST -> AST -> IO AST+mkBvxnor = liftFun2 z3_mk_bvxnor++-- | Standard two's complement unary minus.+mkBvneg :: Context -> AST -> IO AST+mkBvneg = liftFun1 z3_mk_bvneg++-- | Standard two's complement addition.+mkBvadd :: Context -> AST -> AST -> IO AST+mkBvadd = liftFun2 z3_mk_bvadd++-- | Standard two's complement subtraction.+mkBvsub :: Context -> AST -> AST -> IO AST+mkBvsub = liftFun2 z3_mk_bvsub++-- | Standard two's complement multiplication.+mkBvmul :: Context -> AST -> AST -> IO AST+mkBvmul = liftFun2 z3_mk_bvmul++-- | Unsigned division.+mkBvudiv :: Context -> AST -> AST -> IO AST+mkBvudiv = liftFun2 z3_mk_bvudiv++-- | Two's complement signed division.+mkBvsdiv :: Context -> AST -> AST -> IO AST+mkBvsdiv = liftFun2 z3_mk_bvsdiv++-- | Unsigned remainder.+mkBvurem :: Context -> AST -> AST -> IO AST+mkBvurem = liftFun2 z3_mk_bvurem++-- | Two's complement signed remainder (sign follows dividend).+mkBvsrem :: Context -> AST -> AST -> IO AST+mkBvsrem = liftFun2 z3_mk_bvsrem++-- | Two's complement signed remainder (sign follows divisor).+mkBvsmod :: Context -> AST -> AST -> IO AST+mkBvsmod = liftFun2 z3_mk_bvsmod++-- | Unsigned less than.+mkBvult :: Context -> AST -> AST -> IO AST+mkBvult = liftFun2 z3_mk_bvult++-- | Two's complement signed less than.+mkBvslt :: Context -> AST -> AST -> IO AST+mkBvslt = liftFun2 z3_mk_bvslt++-- | Unsigned less than or equal to.+mkBvule :: Context -> AST -> AST -> IO AST+mkBvule = liftFun2 z3_mk_bvule++-- | Two's complement signed less than or equal to.+mkBvsle :: Context -> AST -> AST -> IO AST+mkBvsle = liftFun2 z3_mk_bvsle++-- | Unsigned greater than or equal to.+mkBvuge :: Context -> AST -> AST -> IO AST+mkBvuge = liftFun2 z3_mk_bvuge++-- | Two's complement signed greater than or equal to.+mkBvsge :: Context -> AST -> AST -> IO AST+mkBvsge = liftFun2 z3_mk_bvsge++-- | Unsigned greater than.+mkBvugt :: Context -> AST -> AST -> IO AST+mkBvugt = liftFun2 z3_mk_bvugt++-- | Two's complement signed greater than.+mkBvsgt :: Context -> AST -> AST -> IO AST+mkBvsgt = liftFun2 z3_mk_bvsgt++-- | Concatenate the given bit-vectors.+mkConcat :: Context -> AST -> AST -> IO AST+mkConcat = liftFun2 z3_mk_concat++-- | 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/.+mkExtract :: Context -> Int -> Int -> AST -> IO AST+mkExtract = liftFun3 z3_mk_extract++-- | 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.+mkSignExt :: Context -> Int -> AST -> IO AST+mkSignExt = liftFun2 z3_mk_sign_ext++-- | 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.+mkZeroExt :: Context -> Int -> AST -> IO AST+mkZeroExt = liftFun2 z3_mk_zero_ext++-- | Repeat the given bit-vector up length /i/.+mkRepeat :: Context -> Int -> AST -> IO AST+mkRepeat = liftFun2 z3_mk_repeat++-- | Shift left.+mkBvshl :: Context -> AST -> AST -> IO AST+mkBvshl = liftFun2 z3_mk_bvshl++-- | Logical shift right.+mkBvlshr :: Context -> AST -> AST -> IO AST+mkBvlshr = liftFun2 z3_mk_bvlshr++-- | Arithmetic shift right.+mkBvashr :: Context -> AST -> AST -> IO AST+mkBvashr = liftFun2 z3_mk_bvashr++-- | Rotate bits of /t1/ to the left /i/ times.+mkRotateLeft :: Context -> Int -> AST -> IO AST+mkRotateLeft = liftFun2 z3_mk_rotate_left++-- | Rotate bits of /t1/ to the right /i/ times.+mkRotateRight :: Context -> Int -> AST -> IO AST+mkRotateRight = liftFun2 z3_mk_rotate_right++-- | Rotate bits of /t1/ to the left /t2/ times.+mkExtRotateLeft :: Context -> AST -> AST -> IO AST+mkExtRotateLeft = liftFun2 z3_mk_ext_rotate_left++-- | Rotate bits of /t1/ to the right /t2/ times.+mkExtRotateRight :: Context -> AST -> AST -> IO AST+mkExtRotateRight = liftFun2 z3_mk_ext_rotate_right++-- | Create an /n/ bit bit-vector from the integer argument /t1/.+mkInt2bv :: Context -> Int -> AST -> IO AST+mkInt2bv = liftFun2 z3_mk_int2bv++-- | 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.+mkBv2int :: Context -> AST -> Bool -> IO AST+mkBv2int = liftFun2 z3_mk_bv2int++-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/+-- does not overflow.+mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST+mkBvaddNoOverflow = liftFun3 z3_mk_bvadd_no_overflow++-- | Create a predicate that checks that the bit-wise signed addition of /t1/+-- and /t2/ does not underflow.+mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST+mkBvaddNoUnderflow = liftFun2 z3_mk_bvadd_no_underflow++-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/+-- and /t2/ does not overflow.+mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST+mkBvsubNoOverflow = liftFun2 z3_mk_bvsub_no_overflow++-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and+-- /t2/ does not underflow.+mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST+mkBvsubNoUnderflow = liftFun2 z3_mk_bvsub_no_underflow++-- | Create a predicate that checks that the bit-wise signed division of /t1/+-- and /t2/ does not overflow.+mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST+mkBvsdivNoOverflow = liftFun2 z3_mk_bvsdiv_no_overflow++-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as+-- a signed bit-vector.+mkBvnegNoOverflow :: Context -> AST -> IO AST+mkBvnegNoOverflow = liftFun1 z3_mk_bvneg_no_overflow++-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and+-- /t2/ does not overflow.+mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST+mkBvmulNoOverflow = liftFun3 z3_mk_bvmul_no_overflow++-- | Create a predicate that checks that the bit-wise signed multiplication of+-- /t1/ and /t2/ does not underflow.+mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST+mkBvmulNoUnderflow = liftFun2 z3_mk_bvmul_no_underflow++---------------------------------------------------------------------+-- Arrays++-- | Array read. The argument a is the array and i is the index of the array+-- that gets read.+mkSelect :: Context+ -> AST -- ^ Array.+ -> AST -- ^ Index of the array to read.+ -> IO AST+mkSelect = liftFun2 z3_mk_select++-- | Array update.+--+-- The result of this function is an array that is equal to the input array+-- (with respect to select) on all indices except for i, where it maps to v.+--+-- The semantics of this function is given by the theory of arrays described+-- in the SMT-LIB standard. See <http://smtlib.org> for more details.+mkStore :: Context+ -> AST -- ^ Array.+ -> AST -- ^ Index /i/ of the array.+ -> AST -- ^ New value for /i/.+ -> IO AST+mkStore = liftFun3 z3_mk_store++-- | Create the constant array.+--+-- The resulting term is an array, such that a select on an arbitrary index+-- produces the value /v/.+mkConstArray :: Context+ -> Sort -- ^ Domain sort of the array.+ -> AST -- ^ Value /v/ that the array maps to.+ -> IO AST+mkConstArray = liftFun2 z3_mk_const_array++-- | Map a function /f/ on the the argument arrays.+--+-- The /n/ nodes args must be of array sorts [domain -> range_i].+-- The function declaration /f/ must have type range_1 .. range_n -> range.+-- The sort of the result is [domain -> range].+mkMap :: Context+ -> FuncDecl -- ^ Function /f/.+ -> [AST] -- ^ List of arrays.+ -> IO AST+mkMap ctx fun args = marshal z3_mk_map ctx $ \f ->+ h2c fun $ \funPtr ->+ marshalArrayLen args $ \argsNum argsArr ->+ f funPtr argsNum argsArr++-- | Access the array default value.+--+-- Produces the default range value, for arrays that can be represented as+-- finite maps with a default range value.+mkArrayDefault :: Context+ -> AST -- ^ Array.+ -> IO AST+mkArrayDefault = liftFun1 z3_mk_array_default++-- TODO: Sets++---------------------------------------------------------------------+-- Numerals++-- | Create a numeral of a given sort.+mkNumeral :: Context -> String -> Sort -> IO AST+mkNumeral = liftFun2 z3_mk_numeral++-------------------------------------------------+-- 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 = marshal z3_mk_int c $ h2c s . withIntegral n++{-# INLINE mkUnsignedIntZ3 #-}+mkUnsignedIntZ3 :: Context -> Word32 -> Sort -> IO AST+mkUnsignedIntZ3 c n s = marshal z3_mk_unsigned_int c $+ h2c s . withIntegral n++{-# INLINE mkInt64Z3 #-}+mkInt64Z3 :: Context -> Int64 -> Sort -> IO AST+mkInt64Z3 = liftFun2 z3_mk_int64++{-# INLINE mkUnsignedInt64Z3 #-}+mkUnsignedInt64Z3 :: Context -> Word64 -> Sort -> IO AST+mkUnsignedInt64Z3 = liftFun2 z3_mk_unsigned_int64++{-# 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 $ c2h c =<< 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++-- | Create a pattern for quantifier instantiation.+--+-- Z3 uses pattern matching to instantiate quantifiers.+-- If a pattern is not provided for a quantifier, then Z3 will automatically+-- compute a set of patterns for it. However, for optimal performance,+-- the user should provide the patterns.+--+-- Patterns comprise a list of terms.+-- The list should be non-empty.+-- If the list comprises of more than one term, it is a called a multi-pattern.+--+-- In general, one can pass in a list of (multi-)patterns in the quantifier+-- constructor.+mkPattern :: Context+ -> [AST] -- ^ Terms.+ -> IO Pattern+mkPattern _ [] = error "Z3.Base.mkPattern: empty list of expressions"+mkPattern c es = marshal z3_mk_pattern c $ marshalArrayLen es++-- | Create a bound variable.+--+-- Bound variables are indexed by de-Bruijn indices.+--+-- See <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e>+mkBound :: Context+ -> Int -- ^ de-Bruijn index.+ -> Sort+ -> IO AST+mkBound c i s+ | i >= 0 = liftFun2 z3_mk_bound c i s+ | otherwise = error "Z3.Base.mkBound: negative de-Bruijn index"++type MkZ3Quantifier = 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: Allow the user to specify the quantifier weight!+marshalMkQ :: MkZ3Quantifier+ -> Context+ -> [Pattern]+ -> [Symbol]+ -> [Sort]+ -> AST+ -> IO AST+marshalMkQ z3_mk_Q ctx pats x s body = marshal z3_mk_Q ctx $ \f ->+ marshalArrayLen pats $ \n patsArr ->+ marshalArray x $ \xArr ->+ marshalArray s $ \sArr ->+ h2c body $ \bodyPtr ->+ f 0 n patsArr len sArr xArr bodyPtr+ where len+ | l == 0 = error "Z3.Base.mkQuantifier:\+ \ quantifier with 0 bound variables"+ | l /= length x = error "Z3.Base.mkQuantifier:\+ \ different number of symbols and sorts"+ | otherwise = fromIntegral l+ where l = length s++-- | Create a forall formula.+--+-- The bound variables are de-Bruijn indices created using 'mkBound'.+--+-- Z3 applies the convention that the last element in /xs/ refers to the+-- variable with index 0, the second to last element of /xs/ refers to the+-- variable with index 1, etc.+mkForall :: Context+ -> [Pattern] -- ^ Instantiation patterns (see 'mkPattern').+ -> [Symbol] -- ^ Bound (quantified) variables /xs/.+ -> [Sort] -- ^ Sorts of the bound variables.+ -> AST -- ^ Body of the quantifier.+ -> IO AST+mkForall = marshalMkQ z3_mk_forall++-- | Create an exists formula.+--+-- Similar to 'mkForall'.+mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST+mkExists = marshalMkQ z3_mk_exists++type MkZ3QuantifierConst = Ptr Z3_context+ -> CUInt+ -> CUInt+ -> Ptr (Ptr Z3_app)+ -> CUInt+ -> Ptr (Ptr Z3_pattern)+ -> Ptr Z3_ast+ -> IO (Ptr Z3_ast)++marshalMkQConst :: MkZ3QuantifierConst+ -> Context+ -> [Pattern]+ -> [App]+ -> AST+ -> IO AST+marshalMkQConst z3_mk_Q_const ctx pats apps body =+ marshal z3_mk_Q_const ctx $ \f ->+ marshalArrayLen pats $ \patsNum patsArr ->+ marshalArray apps $ \appsArr ->+ h2c body $ \bodyPtr ->+ f 0 len appsArr patsNum patsArr bodyPtr+ where len+ | l == 0 = error "Z3.Base.mkQuantifierConst:\+ \ quantifier with 0 bound variables"+ | otherwise = fromIntegral l+ where l = length apps+-- TODO: Allow the user to specify the quantifier weight!++-- | Create a universal quantifier using a list of constants that will form the+-- set of bound variables.+mkForallConst :: Context+ -> [Pattern] -- ^ Instantiation patterns (see 'mkPattern').+ -> [App] -- ^ Constants to be abstracted into bound variables.+ -> AST -- ^ Quantifier body.+ -> IO AST+mkForallConst = marshalMkQConst z3_mk_forall_const++-- | Create a existential quantifier using a list of constants that will form+-- the set of bound variables.+mkExistsConst :: Context+ -> [Pattern] -- ^ Instantiation patterns (see 'mkPattern').+ -> [App] -- ^ Constants to be abstracted into bound variables.+ -> AST -- ^ Quantifier body.+ -> IO AST+mkExistsConst = marshalMkQConst z3_mk_exists_const++---------------------------------------------------------------------+-- Accessors++-- | Return the size of the given bit-vector sort.+getBvSortSize :: Context -> Sort -> IO Int+getBvSortSize = liftFun1 z3_get_bv_sort_size++-- | Return the sort of an AST node.+getSort :: Context -> AST -> IO Sort+getSort = liftFun1 z3_get_sort++-- | 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.+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.+getNumeralString :: Context -> AST -> IO String+getNumeralString = liftFun1 z3_get_numeral_string++-- | 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"+++-- | Convert an ast into an APP_AST. This is just type casting.+toApp :: Context -> AST -> IO App+toApp = liftFun1 z3_to_app++-- TODO Modifiers++---------------------------------------------------------------------+-- Models++-- | Evaluate an AST node in the given model.+--+-- The evaluation may fail for the following reasons:+--+-- * /t/ contains a quantifier.+-- * the model m is partial.+-- * /t/ is type incorrect.+eval :: Context+ -> Model -- ^ Model /m/.+ -> AST -- ^ Expression to evaluate /t/.+ -> 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)++-- | The interpretation of a function.+data FuncModel = FuncModel+ { interpMap :: [([AST], AST)]+ -- ^ Mapping from arguments to values.+ , interpElse :: AST+ -- ^ Default value.+ }++-- | Evaluate a function declaration to a list of argument/value pairs.+evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)+evalFunc ctx m fDecl =+ do interpMb <- getFuncInterp ctx m fDecl+ case interpMb of+ Nothing -> return Nothing+ Just interp ->+ do funcMap <- getMapFromInterp ctx interp+ elsePart <- funcInterpGetElse ctx interp+ return (Just $ FuncModel funcMap elsePart)++-- | Evaluate an array as a function, if possible.+evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)+evalArray ctx model array =+ do -- The array must first be evaluated normally, to get it into+ -- 'as-array' form, which is required to acquire the FuncDecl.+ evaldArrayMb <- eval ctx model array+ case evaldArrayMb of+ Nothing -> return Nothing+ Just evaldArray ->+ do canConvert <- isAsArray ctx evaldArray+ if canConvert+ then+ do arrayDecl <- getAsArrayFuncDecl ctx evaldArray+ evalFunc ctx model arrayDecl+ else return Nothing+++-- | Return the function declaration f associated with a (_ as_array f) node.+getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl+getAsArrayFuncDecl = liftFun1 z3_get_as_array_func_decl++-- | The (_ as-array f) AST node is a construct for assigning interpretations+-- for arrays in Z3. It is the array such that forall indices i we have that+-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE+-- if the a is an as-array AST node.+isAsArray :: Context -> AST -> IO Bool+isAsArray = liftFun1 z3_is_as_array+++getMapFromInterp :: Context -> FuncInterp -> IO [([AST], AST)]+getMapFromInterp ctx interp =+ do n <- funcInterpGetNumEntries ctx interp+ entries <- mapM (funcInterpGetEntry ctx interp) [0..n-1]+ mapM (getEntry ctx) entries++getEntry :: Context -> FuncEntry -> IO ([AST], AST)+getEntry ctx entry =+ do val <- funcEntryGetValue ctx entry+ args <- getEntryArgs ctx entry+ return (args, val)++getEntryArgs :: Context -> FuncEntry -> IO [AST]+getEntryArgs ctx entry =+ do n <- funcEntryGetNumArgs ctx entry+ mapM (funcEntryGetArg ctx entry) [0..n-1]++-- | Return the interpretation of the function f in the model m.+-- Return NULL, if the model does not assign an interpretation for f.+-- That should be interpreted as: the f does not matter.+getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)+getFuncInterp ctx m fd = marshal z3_model_get_func_interp ctx $ \f ->+ h2c m $ \mPtr ->+ h2c fd $ \fdPtr ->+ f mPtr fdPtr++-- | Return the number of entries in the given function interpretation.+funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int+funcInterpGetNumEntries = liftFun1 z3_func_interp_get_num_entries++-- | Return a _point_ of the given function intepretation.+-- It represents the value of f in a particular point.+funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry+funcInterpGetEntry = liftFun2 z3_func_interp_get_entry++-- | Return the 'else' value of the given function interpretation.+funcInterpGetElse :: Context -> FuncInterp -> IO AST+funcInterpGetElse = liftFun1 z3_func_interp_get_else++-- | Return the arity (number of arguments) of the given function+-- interpretation.+funcInterpGetArity :: Context -> FuncInterp -> IO Int+funcInterpGetArity = liftFun1 z3_func_interp_get_arity++-- | Return the value of this point.+funcEntryGetValue :: Context -> FuncEntry -> IO AST+funcEntryGetValue = liftFun1 z3_func_entry_get_value++-- | Return the number of arguments in a Z3_func_entry object.+funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int+funcEntryGetNumArgs = liftFun1 z3_func_entry_get_num_args++-- | Return an argument of a Z3_func_entry object.+funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST+funcEntryGetArg = liftFun2 z3_func_entry_get_arg++-- | Convert the given model into a string.+modelToString :: Context -> Model -> IO String+modelToString = liftFun1 z3_model_to_string++-- | Alias for 'modelToString'.+showModel :: Context -> Model -> IO String+showModel = modelToString+{-# DEPRECATED showModel "Use modelToString instead." #-}++---------------------------------------------------------------------+-- Constraints++-- | Create a backtracking point.+push :: Context -> IO ()+push = liftFun0 z3_push++-- | Backtrack /n/ backtracking points.+pop :: Context -> Int -> IO ()+pop = liftFun1 z3_pop++-- TODO Constraints: Z3_get_num_scopes++-- TODO Constraints: Z3_persist_ast++-- | Assert a constraing into the logical context.+assertCnstr :: Context -> AST -> IO ()+assertCnstr = liftFun1 z3_assert_cnstr++-- | Check whether the given logical context is consistent or not.+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 = fmap Model . ptrToMaybe+{-# DEPRECATED getModel "Use checkAndGetModel instead." #-}++-- | Check whether the given logical context is consistent or not.+--+-- If the logical context is not unsatisfiable and model construction is+-- enabled (via 'mkConfig'), then a model is returned. The caller is+-- responsible for deleting the model using the function 'delModel'.+checkAndGetModel :: Context -> IO (Result, Maybe Model)+checkAndGetModel = getModel++-- | Delete a model object.+delModel :: Context -> Model -> IO ()+delModel = liftFun1 z3_del_model++-- | Check whether the given logical context is consistent or not.+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++{-# WARNING mkParams+ , paramsSetBool+ , paramsSetUInt+ , paramsSetDouble+ , paramsSetSymbol+ , paramsToString+ "New Z3 API support is still incomplete and fragile: \+ \you may experience segmentation faults!"+ #-}++mkParams :: Context -> IO Params+mkParams = liftFun0 z3_mk_params++paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()+paramsSetBool = liftFun3 z3_params_set_bool++paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()+paramsSetUInt = liftFun3 z3_params_set_uint++paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()+paramsSetDouble = liftFun3 z3_params_set_double++paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()+paramsSetSymbol = liftFun3 z3_params_set_symbol++paramsToString :: Context -> Params -> IO String+paramsToString = liftFun1 z3_params_to_string++---------------------------------------------------------------------+-- Solvers++{-# WARNING Logic+ , mkSolver+ , mkSimpleSolver+ , mkSolverForLogic+ , solverSetParams+ , solverPush+ , solverPop+ , solverReset+ , solverGetNumScopes+ , 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"++mkSolverForeign :: Context -> Ptr Z3_solver -> IO Solver+mkSolverForeign c ptr =+ do z3_solver_inc_ref cPtr ptr+ Solver <$> newForeignPtr ptr (z3_solver_dec_ref cPtr ptr)+ where cPtr = unContext c++mkSolver :: Context -> IO Solver+mkSolver = liftFun0 z3_mk_solver++mkSimpleSolver :: Context -> IO Solver+mkSimpleSolver = liftFun0 z3_mk_simple_solver++mkSolverForLogic :: Context -> Logic -> IO Solver+mkSolverForLogic c logic =+ do sym <- mkStringSymbol c (show logic)+ checkError c $+ mkSolverForeign c =<< z3_mk_solver_for_logic (unContext c) (unSymbol sym)++solverSetParams :: Context -> Solver -> Params -> IO ()+solverSetParams = liftFun2 z3_solver_set_params++solverPush :: Context -> Solver -> IO ()+solverPush = liftFun1 z3_solver_push++solverPop :: Context -> Solver -> Int -> IO ()+solverPop = liftFun2 z3_solver_pop++solverReset :: Context -> Solver -> IO ()+solverReset = liftFun1 z3_solver_reset++-- | Number of backtracking points.+solverGetNumScopes :: Context -> Solver -> IO Int+solverGetNumScopes = liftFun1 z3_solver_get_num_scopes++solverAssertCnstr :: Context -> Solver -> AST -> IO ()+solverAssertCnstr = liftFun2 z3_solver_assert++solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()+solverAssertAndTrack = liftFun3 z3_solver_assert_and_track++-- | Check whether the assertions in a given solver are consistent or not.+solverCheck :: Context -> Solver -> IO Result+solverCheck ctx solver = marshal z3_solver_check ctx $ withSolverPtr solver++-- Retrieve the model for the last 'Z3_solver_check'.+--+-- The error handler is invoked if a model is not available because+-- the commands above were not invoked for the given solver,+-- or if the result was 'Unsat'.+solverGetModel :: Context -> Solver -> IO Model+solverGetModel ctx solver = marshal z3_solver_get_model ctx $ \f ->+ h2c solver $ \solverPtr ->+ f solverPtr++solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)+solverCheckAndGetModel ctx solver =+ do res <- solverCheck ctx solver+ mbModel <- case res of+ Unsat -> return Nothing+ _ -> Just <$> solverGetModel ctx solver+ return (res, mbModel)++solverGetReasonUnknown :: Context -> Solver -> IO String+solverGetReasonUnknown = liftFun1 z3_solver_get_reason_unknown++-- | Convert the given solver into a string.+solverToString :: Context -> Solver -> IO String+solverToString = liftFun1 z3_solver_to_string++---------------------------------------------------------------------+-- 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 = liftFun1 z3_ast_to_string++-- | Convert a pattern to a string.+patternToString :: Context -> Pattern -> IO String+patternToString = liftFun1 z3_pattern_to_string++-- | Convert a sort to a string.+sortToString :: Context -> Sort -> IO String+sortToString = liftFun1 z3_sort_to_string++-- | Convert a FuncDecl to a string.+funcDeclToString :: Context -> FuncDecl -> IO String+funcDeclToString = liftFun1 z3_func_decl_to_string++-- | Convert the given benchmark into SMT-LIB formatted string.+--+-- The output format can be configured via 'setASTPrintMode'.+benchmarkToSMTLibString :: Context+ -> String -- ^ name+ -> String -- ^ logic+ -> String -- ^ status+ -> String -- ^ attributes+ -> [AST] -- ^ assumptions+ -> AST -- ^ formula+ -> IO String+benchmarkToSMTLibString ctx name logic status attr assump form =+ marshal z3_benchmark_to_smtlib_string ctx $ \f ->+ withCString name $ \namePtr ->+ withCString logic $ \logicPtr ->+ withCString status $ \statusPtr ->+ withCString attr $ \attrPtr ->+ marshalArrayLen assump $ \assumpNum assumpArr ->+ h2c form $ \formPtr ->+ f namePtr logicPtr statusPtr attrPtr assumpNum assumpArr formPtr++---------------------------------------------------------------------+-- Error handling++-- | 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++---------------------------------------------------------------------+-- Miscellaneous++data Version+ = Version {+ z3Major :: !Int+ , z3Minor :: !Int+ , z3Build :: !Int+ , z3Revision :: !Int+ }+ deriving (Eq,Ord)++instance Show Version where+ show (Version major minor build _) =+ show major ++ "." ++ show minor ++ "." ++ show build++-- | Return Z3 version number information.+getVersion :: IO Version+getVersion =+ alloca $ \ptrMinor ->+ alloca $ \ptrMajor ->+ alloca $ \ptrBuild ->+ alloca $ \ptrRevision -> do+ z3_get_version ptrMinor ptrMajor ptrBuild ptrRevision+ minor <- fromIntegral <$> peek ptrMinor+ major <- fromIntegral <$> peek ptrMajor+ build <- fromIntegral <$> peek ptrBuild+ revision <- fromIntegral <$> peek ptrRevision+ return $ Version minor major build revision++---------------------------------------------------------------------+-- Marshalling++{- MARSHALLING HELPERS++We try to get rid of most of the marshalling boilerplate which, by the way,+is going to be essential for transitioning to Z3 4 API.++Most API functions can be lifted using 'liftFun'{0-3} helpers. Otherwise try+using 'marshal'. Worst case scenario, write the marshalling code yourself.++-}++withSolverPtr :: Solver -> (Ptr Z3_solver -> IO a) -> IO a+withSolverPtr (Solver fptr) = withForeignPtr fptr++withIntegral :: (Integral a, Integral b) => a -> (b -> r) -> r+withIntegral x f = f (fromIntegral x)++marshalArray :: (Marshal h c, Storable c) => [h] -> (Ptr c -> IO a) -> IO a+marshalArray hs f = hs2cs hs $ \cs -> withArray cs f++marshalArrayLen :: (Marshal h c, Storable c, Integral i) =>+ [h] -> (i -> Ptr c -> IO a) -> IO a+marshalArrayLen hs f =+ hs2cs hs $ \cs -> withArrayLen cs $ \n -> f (fromIntegral n)++liftAstN :: String+ -> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))+ -> Context -> [AST] -> IO AST+liftAstN s _ _ [] = error s+liftAstN _ f c es = marshal f c $ marshalArrayLen es+{-# INLINE liftAstN #-}++class Marshal h c where+ c2h :: Context -> c -> IO h+ h2c :: h -> (c -> IO r) -> IO r++hs2cs :: Marshal h c => [h] -> ([c] -> IO r) -> IO r+hs2cs [] f = f []+hs2cs (h:hs) f =+ h2c h $ \c ->+ hs2cs hs $ \cs -> f (c:cs)++instance Marshal h (Ptr x) => Marshal (Maybe h) (Ptr x) where+ c2h c = T.mapM (c2h c) . ptrToMaybe+ h2c Nothing f = f nullPtr+ h2c (Just x) f = h2c x f++instance Marshal () () where+ c2h _ = return+ h2c x f = f x++instance Marshal Bool Z3_bool where+ c2h _ = return . toBool+ h2c b f = f (unBool b)++instance Marshal Result Z3_lbool where+ c2h _ = return . toResult+ h2c = error "Marshal Result Z3_lbool => h2c not implemented"++instance Integral h => Marshal h CInt where+ c2h _ = return . fromIntegral+ h2c i f = f (fromIntegral i)++instance Integral h => Marshal h CUInt where+ c2h _ = return . fromIntegral+ h2c i f = f (fromIntegral i)++instance Integral h => Marshal h CLLong where+ c2h _ = return . fromIntegral+ h2c i f = f (fromIntegral i)++instance Integral h => Marshal h CULLong where+ c2h _ = return . fromIntegral+ h2c i f = f (fromIntegral i)++instance Marshal Double CDouble where+ c2h _ = return . realToFrac+ h2c d f = f (realToFrac d)++instance Marshal String CString where+ c2h _ = peekCString+ h2c = withCString++instance Marshal App (Ptr Z3_app) where+ c2h _ = return . App+ h2c a f = f (unApp a)++instance Marshal Params (Ptr Z3_params) where+ c2h _ = return . Params+ h2c p f = f (unParams p)++instance Marshal Symbol (Ptr Z3_symbol) where+ c2h _ = return . Symbol+ h2c s f = f (unSymbol s)++instance Marshal AST (Ptr Z3_ast) where+ c2h _ = return . AST+ h2c a f = f (unAST a)++instance Marshal Sort (Ptr Z3_sort) where+ c2h _ = return . Sort+ h2c a f = f (unSort a)++instance Marshal FuncDecl (Ptr Z3_func_decl) where+ c2h _ = return . FuncDecl+ h2c a f = f (unFuncDecl a)++instance Marshal FuncEntry (Ptr Z3_func_entry) where+ c2h _ = return . FuncEntry+ h2c e f = f (unFuncEntry e)++instance Marshal FuncInterp (Ptr Z3_func_interp) where+ c2h _ = return . FuncInterp+ h2c a f = f (unFuncInterp a)++instance Marshal Model (Ptr Z3_model) where+ c2h _ = return . Model+ h2c m f = f (unModel m)++instance Marshal Pattern (Ptr Z3_pattern) where+ c2h _ = return . Pattern+ h2c a f = f (unPattern a)++instance Marshal Solver (Ptr Z3_solver) where+ c2h = mkSolverForeign+ h2c = withSolverPtr++marshal :: Marshal rh rc => (Ptr Z3_context -> t) ->+ Context -> (t -> IO rc) -> IO rh+marshal f c cont = checkError c $ cont (f (unContext c)) >>= c2h c++liftFun0 :: Marshal rh rc => (Ptr Z3_context -> IO rc) ->+ Context -> IO rh+liftFun0 f c = checkError c $ c2h c =<< f (unContext c)+{-# INLINE liftFun0 #-}++liftFun1 :: (Marshal ah ac, Marshal rh rc) =>+ (Ptr Z3_context -> ac -> IO rc) ->+ Context -> ah -> IO rh+liftFun1 f c x = checkError c $ h2c x $ \a ->+ c2h c =<< f (unContext c) a+{-# INLINE liftFun1 #-}++liftFun2 :: (Marshal ah ac, Marshal bh bc, Marshal rh rc) =>+ (Ptr Z3_context -> ac -> bc -> IO rc) ->+ Context -> ah -> bh -> IO rh+liftFun2 f c x y = checkError c $ h2c x $ \a -> h2c y $ \b ->+ c2h c =<< f (unContext c) a b+{-# INLINE liftFun2 #-}++liftFun3 :: (Marshal ah ac, Marshal bh bc, Marshal ch cc, Marshal rh rc) =>+ (Ptr Z3_context -> ac -> bc -> cc -> IO rc) ->+ Context -> ah -> bh -> ch -> IO rh+liftFun3 f c x y z = checkError c $+ h2c x $ \x1 -> h2c y $ \y1 -> h2c z $ \z1 ->+ c2h c =<< f (unContext c) x1 y1 z1+{-# INLINE liftFun3 #-}++---------------------------------------------------------------------+-- Utils++-- | 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 -- | Wraps a non-null pointer with 'Just', or else returns 'Nothing'. ptrToMaybe :: Ptr a -> Maybe (Ptr a)
Z3/Base/C.hsc view
@@ -1,17 +1,28 @@-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE ForeignFunctionInterface #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE ForeignFunctionInterface #-} -- | -- Module : Z3.Base.C--- Copyright : (c) Iago Abal, 2012-2013+-- Copyright : (c) Iago Abal, 2012-2014 -- (c) David Castro, 2012-2013 -- License : BSD3--- Maintainer: Iago Abal <iago.abal@gmail.com>,+-- Maintainer: Iago Abal <mail@iagoabal.eu>, -- David Castro <david.castro.dcp@gmail.com> ----- Low-level bindings, highly inspired by yices-painless.+-- Z3 API foreign imports. +{- HACKING +Add here the foreign import to support a new API function:++* Take a look to a few others foreign imports and follow the same coding style.+ * 2-space wide indentation, no tabs.+ * No trailing spaces, please.+ * ...+* Place the foreign import in the right section, according to the Z3's API documentation.+* Include a reference to the function's API documentation.+-}+ module Z3.Base.C where import Foreign@@ -24,73 +35,58 @@ --------------------------------------------------------------------- -- * Types --- | A configuration object used to initialize logical contexts. data Z3_config --- | Logical context. This is the main Z3 data-structure. data Z3_context --- | A Lisp-link symbol. It is used to name types, constants, and functions.--- A symbol can be created using string or integers. data Z3_symbol --- | Abstract syntax tree node. That is, the data-structure used in Z3 to--- represent terms, formulas and types. data Z3_ast --- | A kind of AST used to represent types. data Z3_sort --- | A kind of AST used to represent function symbols. data Z3_func_decl --- | A kind of AST used to represent constant and function declarations. data Z3_app --- | A kind of AST used to represent pattern and multi-patterns used to--- guide quantifier instantiation. data Z3_pattern --- | A model for the constraints asserted into the logical context. data Z3_model --- | The interpretation of a function returned from the model. data Z3_func_interp --- | An entry in a function interpretation. data Z3_func_entry --- | 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+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6c2de6ea89b244e37c3ffb17a9ea2a89>+newtype Z3_lbool = Z3_lbool CInt+ deriving Eq --- | Values of lifted boolean type z3_l_true, z3_l_false, z3_l_undef :: Z3_lbool-z3_l_true = #const Z3_L_TRUE-z3_l_false = #const Z3_L_FALSE-z3_l_undef = #const Z3_L_UNDEF+z3_l_true = Z3_lbool (#const Z3_L_TRUE)+z3_l_false = Z3_lbool (#const Z3_L_FALSE)+z3_l_undef = Z3_lbool (#const Z3_L_UNDEF) --- | Boolean type. It is just an alias for int.-type Z3_bool = CInt+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a65ded0ada3ee285865759a21140eeb>+newtype Z3_bool = Z3_bool CInt+ deriving Eq --- | Z3 custom error handler+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga311274c8a65a5d25cf715ebdf0c68747> 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-z3_false = #const Z3_FALSE+z3_true, z3_false :: Z3_bool+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad86c8730a2e4e61bac585b240a6288d4>+z3_true = Z3_bool(#const Z3_TRUE)+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d9cee57472b2c7623642f123b8f1781>+z3_false = Z3_bool(#const Z3_FALSE) --- | Z3 String type+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga49f047b93b0282e686956678da5b86b1> type Z3_string = CString --- | Z3 pretty-printing modes+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0112dc1e8e08a19bf7a4299bb09a9727> type Z3_ast_print_mode = CInt z3_print_smtlib_full :: Z3_ast_print_mode z3_print_smtlib_full = #const Z3_PRINT_SMTLIB_FULL@@ -101,7 +97,7 @@ z3_print_smtlib2_compliant :: Z3_ast_print_mode z3_print_smtlib2_compliant = #const Z3_PRINT_SMTLIB2_COMPLIANT --- | Z3 error codes+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9f9e7b1b5b81381fab96debbaaa638f> type Z3_error_code = CInt #{enum Z3_error_code, , z3_ok = Z3_OK@@ -122,21 +118,15 @@ --------------------------------------------------------------------- -- * Create configuration --- | Create a configuration.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>+-- | 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>+-- | 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>+-- | 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 () @@ -144,30 +134,22 @@ --------------------------------------------------------------------- -- * Create context --- | Create a context using the given configuration.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46>+-- | 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>+-- | 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 an integer.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3df806baf6124df3e63a58cf23e12411>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3df806baf6124df3e63a58cf23e12411> foreign import ccall unsafe "Z3_mk_int_symbol" z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol) --- | Create a Z3 symbol using a C string.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>+-- | 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) @@ -176,47 +158,31 @@ -- TODO Sorts: Z3_is_eq_sort --- | Create a free (uninterpreted) type using the given name (symbol).------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de> foreign import ccall unsafe "Z3_mk_uninterpreted_sort" z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort) --- | Create the Boolean type.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>+-- | 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>+-- | 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>+-- | 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) --- | 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>+-- | 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>+-- | 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) --- | Create a tuple type------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1> foreign import ccall unsafe "Z3_mk_tuple_sort" z3_mk_tuple_sort :: Ptr Z3_context -> Ptr Z3_symbol@@ -233,9 +199,7 @@ --------------------------------------------------------------------- -- * Constants and Applications --- | Declare a constant or function.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2>+-- | 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@@ -244,9 +208,7 @@ -> Ptr Z3_sort -> IO (Ptr Z3_func_decl) --- | Create a constant or function application.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>+-- | 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@@ -254,9 +216,7 @@ -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Declare and create a constant.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>+-- | 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) @@ -266,510 +226,324 @@ --------------------------------------------------------------------- -- * Propositional Logic and Equality --- | Create an AST node representing /true/.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>+-- | 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>+-- | 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>+-- | 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+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7> 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>+-- | 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>+-- | 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.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>+-- | 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.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>+-- | 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.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>+-- | 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>+-- | 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].------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>+-- | 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].------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>+-- | 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].------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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) --------------------------------------------------------------------- -- * Bit-vectors --- | Bitwise negation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>---+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>++-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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) @@ -778,60 +552,42 @@ --------------------------------------------------------------------- -- * Numerals --- | Create a numeral of a given sort.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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) --------------------------------------------------------------------- -- * Quantifiers --- | Create a pattern for quantifier instantiation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85>+-- | 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>+-- | 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>+-- | 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)@@ -839,9 +595,7 @@ -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an exists formula.------ Referece: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407+-- | 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)@@ -849,46 +603,61 @@ -> 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+-- TODO: Z3_mk_quantifier, Z3_mk_quantifier_ex +-- | Reference <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabdb40b3ac220bce5a3801e6d29fb3bb6>+foreign import ccall unsafe "Z3_mk_forall_const"+ z3_mk_forall_const :: Ptr Z3_context+ -> CUInt+ -> CUInt+ -> Ptr (Ptr Z3_app)+ -> CUInt+ -> Ptr (Ptr Z3_pattern)+ -> Ptr Z3_ast+ -> IO (Ptr Z3_ast)++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2011bea0f4445d58ec4d7cefe4499ceb>+foreign import ccall unsafe "Z3_mk_exists_const"+ z3_mk_exists_const :: Ptr Z3_context+ -> CUInt+ -> CUInt+ -> Ptr (Ptr Z3_app)+ -> CUInt+ -> Ptr (Ptr Z3_pattern)+ -> Ptr Z3_ast+ -> IO (Ptr Z3_ast)++-- TODO: 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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 +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf9345fd0822d7e9928dd4ab14a09765b>+foreign import ccall unsafe "Z3_to_app"+ z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app)+ -- TODO Modifiers --------------------------------------------------------------------- -- * Models --- | Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded,--- and store the result in v.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga47d3655283564918c85bda0b423b7f67>+-- | 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@@ -896,88 +665,63 @@ -> Ptr (Ptr Z3_ast) -> IO Z3_bool --- | The (_ as-array f) AST node is a construct for assigning interpretations for--- arrays in Z3. It is the array such that forall indices i we have that--- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE if--- the a is an as-array AST node.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa> foreign import ccall unsafe "Z3_is_as_array" z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool --- | Return the function declaration f associated with a (_ as_array f) node.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda> foreign import ccall unsafe "Z3_get_as_array_func_decl" z3_get_as_array_func_decl :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_func_decl) --- | Return the interpretation of the function f in the model m.--- Return NULL, if the model does not assign an interpretation for f.--- That should be interpreted as: the f does not matter.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633> foreign import ccall unsafe "Z3_model_get_func_interp" z3_model_get_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_func_interp) --- | Return the number of entries in the given function interpretation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844> foreign import ccall unsafe "Z3_func_interp_get_num_entries" z3_func_interp_get_num_entries :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt --- | Return a "point" of the given function intepretation.--- It represents the value of f in a particular point.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da> foreign import ccall unsafe "Z3_func_interp_get_entry" z3_func_interp_get_entry :: Ptr Z3_context -> Ptr Z3_func_interp -> CUInt -> IO (Ptr Z3_func_entry) --- | Return the 'else' value of the given function interpretation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64> foreign import ccall unsafe "Z3_func_interp_get_else" z3_func_interp_get_else :: Ptr Z3_context -> Ptr Z3_func_interp -> IO (Ptr Z3_ast)--- | Return the arity (number of arguments) of the given function interpretation.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8> foreign import ccall unsafe "Z3_func_interp_get_arity" z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt --- | Return the value of this point.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da> foreign import ccall unsafe "Z3_func_entry_get_value" z3_func_entry_get_value :: Ptr Z3_context -> Ptr Z3_func_entry -> IO (Ptr Z3_ast) --- | Return the number of arguments in a Z3_func_entry object.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a> foreign import ccall unsafe "Z3_func_entry_get_num_args" z3_func_entry_get_num_args :: Ptr Z3_context -> Ptr Z3_func_entry -> IO CUInt --- | Return an argument of a Z3_func_entry object.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab> foreign import ccall unsafe "Z3_func_entry_get_arg" z3_func_entry_get_arg :: Ptr Z3_context -> Ptr Z3_func_entry@@ -987,264 +731,180 @@ --------------------------------------------------------------------- -- * Constraints +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad651ad68c7a060cbb5616349233cb10f> foreign import ccall unsafe "Z3_push" z3_push :: Ptr Z3_context -> IO () --- TODO Constraints: Z3_pop+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab2b3a542006c86c8d86dc37872f88b61> 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>+-- | 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>+-- | 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.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>+-- | 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 -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities --- | Delete a model object.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee>+-- | 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 () +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af> foreign import ccall unsafe "Z3_model_to_string" z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO CString +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216> 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd4b4a6465601835341b477b75725b28>+foreign import ccall unsafe "Z3_solver_get_num_scopes"+ z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt++-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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 +-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf52e41db4b12a84188b80255454d3abb>+foreign import ccall unsafe "Z3_solver_to_string"+ z3_solver_to_string :: 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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 --- | Convert the given benchmark into SMT-LIB formatted string.------ Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4>+-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4> foreign import ccall unsafe "Z3_benchmark_to_smtlib_string" z3_benchmark_to_smtlib_string :: Ptr Z3_context -> Z3_string -- ^ name@@ -1259,32 +919,29 @@ --------------------------------------------------------------------- -- * 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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>+-- | 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++---------------------------------------------------------------------+-- * Miscellaneous++-- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga45fcd18a00379b13a536c5b6117190ae>+foreign import ccall unsafe "Z3_get_version"+ z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO ()
Z3/Lang.hs view
@@ -8,8 +8,14 @@ -- David Castro <david.castro.dcp@gmail.com> -- Stability : experimental -module Z3.Lang (- module Z3.Lang.Prelude+{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}+ -- Imports deprecated modules, but it is a depcrecated module itself.++module Z3.Lang+ {-# DEPRECATED+ "The Z3.Lang interface will be moved to a dedicated package."+ #-}+ ( module Z3.Lang.Prelude , module Z3.Lang.Nat ) where
Z3/Lang/Lg2.hs view
@@ -9,7 +9,13 @@ -- Maintainer: Iago Abal <iago.abal@gmail.com>, -- David Castro <david.castro.dcp@gmail.com> +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}+ -- Imports deprecated modules, but it is a depcrecated module itself.+ module Z3.Lang.Lg2+ {-# DEPRECATED+ "The Z3.Lang interface will be moved to a dedicated package."+ #-} ( declareLg2 ) where
Z3/Lang/Monad.hs view
@@ -59,6 +59,7 @@ import Control.Applicative ( Applicative ) import Control.Monad.State+import Data.Maybe ( fromMaybe ) import qualified Data.Traversable as T ---------------------------------------------------------------------@@ -136,7 +137,7 @@ 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+ where soft_timeout_val = show $ fromMaybe 0 $ softTimeout args ------------------------------------------------- -- HOAX-deBruijn conversion
Z3/Lang/Nat.hs view
@@ -5,6 +5,9 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}+ -- Imports deprecated modules, but it is a depcrecated module itself.+ -- | -- Module : Z3.Lang.Nat -- Copyright : (c) Iago Abal, 2012@@ -14,6 +17,9 @@ -- David Castro <david.castro.dcp@gmail.com> module Z3.Lang.Nat+ {-# DEPRECATED+ "The Z3.Lang interface will be moved to a dedicated package."+ #-} ( Nat ) where
Z3/Lang/Pow2.hs view
@@ -9,8 +9,14 @@ -- Maintainer: Iago Abal <iago.abal@gmail.com>, -- David Castro <david.castro.dcp@gmail.com> +{-# OPTIONS_GHC -fno-warn-warnings-deprecations #-}+ -- Imports deprecated modules, but it is a depcrecated module itself.+ -- TODO generalize for x^y module Z3.Lang.Pow2+ {-# DEPRECATED+ "The Z3.Lang interface will be moved to a dedicated package."+ #-} ( declarePow2 ) where
Z3/Lang/Prelude.hs view
@@ -26,9 +26,11 @@ -- TODO: Pretty-printing of expressions -module Z3.Lang.Prelude (-- -- * Z3 script+module Z3.Lang.Prelude+ {-# DEPRECATED+ "The Z3.Lang interface will be moved to a dedicated package."+ #-}+ ( -- * Z3 script Z3 , Base.Result , evalZ3@@ -47,6 +49,7 @@ , showContext , exprToString , push, pop+ , getVersion -- ** Models , Model
Z3/Monad.hs view
@@ -18,12 +18,18 @@ -- A simple monadic wrapper for 'Z3.Base'. module Z3.Monad- ( MonadZ3(..)+ ( -- * Z3 monad+ MonadZ3(..) , Z3 , module Z3.Opts , Logic(..) , evalZ3 , evalZ3With+ -- ** Z3 enviroments+ , Z3Env+ , newEnv+ , delEnv+ , evalZ3WithEnv -- * Types , Symbol@@ -33,9 +39,11 @@ , App , Pattern , Model+ , Base.Context , FuncInterp , FuncEntry , FuncModel(..)+ , Base.Solver -- ** Satisfiability result , Result(..)@@ -154,12 +162,15 @@ , mkBound , mkForall , mkExists+ , mkForallConst+ , mkExistsConst -- * Accessors , getBvSortSize , getBool , getInt , getReal+ , toApp -- * Models , eval@@ -187,6 +198,9 @@ , withModel , push , pop+ , local+ , reset+ , getNumScopes -- * String Conversion , ASTPrintMode(..)@@ -195,7 +209,12 @@ , patternToString , sortToString , funcDeclToString+ , solverToString , benchmarkToSMTLibString++ -- * Miscellaneous+ , Version(..)+ , getVersion ) where @@ -214,10 +233,12 @@ , Result(..) , Logic(..) , ASTPrintMode(..)+ , Version(..) ) import qualified Z3.Base as Base import Control.Applicative ( Applicative )+import qualified Control.Exception as E import Control.Monad ( void ) import Control.Monad.Reader ( ReaderT, runReaderT, asks ) import Control.Monad.Trans ( MonadIO, liftIO )@@ -279,6 +300,7 @@ newtype Z3 a = Z3 { _unZ3 :: ReaderT Z3Env IO a } deriving (Functor, Applicative, Monad, MonadIO) +-- | Z3 environment. data Z3Env = Z3Env { envSolver :: Maybe Base.Solver@@ -292,16 +314,41 @@ -- | 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)+ E.bracket (newEnv mbLogic opts) delEnv $ runReaderT s -- | Eval a Z3 script with default configuration options. evalZ3 :: Z3 a -> IO a evalZ3 = evalZ3With Nothing stdOpts +-- | Create a new Z3 environment.+--+-- Until we move to Z3 API 4.0 you need to manually freed this+-- environment using 'delEnv'.+newEnv :: Maybe Logic -> Opts -> IO Z3Env+newEnv mbLogic opts =+ Base.withConfig $ \cfg -> do+ setOpts cfg opts+ ctx <- Base.mkContext cfg+ mbSolver <- T.mapM (Base.mkSolverForLogic ctx) mbLogic+ return $ Z3Env mbSolver ctx++-- | Free a Z3 environment.+delEnv :: Z3Env -> IO ()+delEnv = Base.delContext . envContext++-- | Eval a Z3 script with a given environment.+--+-- Environments may facilitate running many queries under the same+-- logical context.+--+-- Note that an environment may change after each query.+-- If you want to preserve the same environment then use 'local', as in+-- @evalZ3WithEnv /env/ (local /query/)@.+evalZ3WithEnv :: Z3 a+ -> Z3Env+ -> IO a+evalZ3WithEnv (Z3 s) = runReaderT s+ --------------------------------------------------------------------- -- Contexts @@ -879,8 +926,8 @@ -- | map f on the the argument arrays. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>-mkMap :: MonadZ3 z3 => FuncDecl -> Int -> [AST] -> z3 AST-mkMap = liftFun3 Base.mkMap+mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST+mkMap = liftFun2 Base.mkMap -- | Access the array default value. Produces the default range value, for -- arrays that can be represented as finite maps with a default range value.@@ -924,6 +971,12 @@ mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST mkForall = liftFun4 Base.mkForall +mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST+mkForallConst = liftFun3 Base.mkForallConst++mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST+mkExistsConst = liftFun3 Base.mkExistsConst+ mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST mkExists = liftFun4 Base.mkExists @@ -950,6 +1003,10 @@ getReal :: MonadZ3 z3 => AST -> z3 Rational getReal = liftFun1 Base.getReal +-- | Cast AST into an App.+toApp :: MonadZ3 z3 => AST -> z3 App+toApp = liftFun1 Base.toApp+ --------------------------------------------------------------------- -- Models @@ -1056,6 +1113,26 @@ pop :: MonadZ3 z3 => Int -> z3 () pop = liftSolver1 Base.solverPop Base.pop +-- | Run a query and restore the initial logical context.+--+-- This is a shorthand for 'push', run the query, and 'pop'.+local :: MonadZ3 z3 => z3 a -> z3 a+local q = do+ push+ r <- q+ pop 1+ return r++-- | Backtrack all the way.+reset :: MonadZ3 z3 => z3 ()+reset = liftSolver0 Base.solverReset+ (error "reset requires solver")++-- | Get number of backtracking points.+getNumScopes :: MonadZ3 z3 => z3 Int+getNumScopes = liftSolver0 Base.solverGetNumScopes+ (error "getNumScopes requires solver")+ -- | Assert a constraing into the logical context. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>@@ -1109,6 +1186,11 @@ funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String funcDeclToString = liftFun1 Base.funcDeclToString +-- | Convert the solver to a string.+solverToString :: MonadZ3 z3 => z3 String+solverToString = liftSolver0 Base.solverToString+ (error "solverToString requires solver")+ -- | Convert the given benchmark into SMT-LIB formatted string. -- -- The output format can be configured via 'setASTPrintMode'.@@ -1121,3 +1203,10 @@ -> AST -- ^ formula -> z3 String benchmarkToSMTLibString = liftFun6 Base.benchmarkToSMTLibString++---------------------------------------------------------------------+-- Miscellaneous++-- | Return Z3 version number information.+getVersion :: MonadZ3 z3 => z3 Version+getVersion = liftIO Base.getVersion
Z3/Opts.hs view
@@ -1,19 +1,25 @@ -- | -- Module : Z3.Opts--- Copyright : (c) Iago Abal, 2013+-- Copyright : (c) Iago Abal, 2013-2014 -- (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.+-- Configuring Z3.+--+-- Z3 has plenty of configuration options and these vary quite a lot+-- across Z3 versions, being hard to design a proper abstraction.+-- We decided to keep this simple. module Z3.Opts- ( Opts+ ( -- * Z3 configuration+ Opts , setOpts , stdOpts , (+?)+ -- * Z3 options , opt , OptValue )@@ -33,6 +39,9 @@ mempty = Opts [] mappend (Opts ps1) (Opts ps2) = Opts (ps1++ps2) +singleton :: Opt -> Opts+singleton o = Opts [o]+ -- | Default configuration. stdOpts :: Opts stdOpts = mempty@@ -43,9 +52,12 @@ -- | Set a configuration option. opt :: OptValue val => String -> val -> Opts-opt oid val = Opts [option oid val]+opt oid val = singleton $ option oid val -- | Set configuration.+--+-- If you are using 'Z3.Lang' or 'Z3.Monad' interfaces, you don't need+-- to call this function directly, just pass your 'Opts' to /evalZ3*/. setOpts :: Base.Config -> Opts -> IO () setOpts baseCfg (Opts params) = mapM_ (setOpt baseCfg) params @@ -65,8 +77,7 @@ option :: String -> val -> Opt instance OptValue Bool where- option oid True = Opt oid "true"- option oid False = Opt oid "false"+ option oid = Opt oid . boolVal instance OptValue Int where option oid = Opt oid . show@@ -79,3 +90,10 @@ instance OptValue [Char] where option = Opt++-------------------------------------------------+-- Utils++boolVal :: Bool -> String+boolVal True = "true"+boolVal False = "false"
z3.cabal view
@@ -1,5 +1,5 @@ Name: z3-Version: 0.3.1+Version: 0.3.2 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 Theorem Prover (<http://z3.codeplex.com>).@@ -12,26 +12,31 @@ The "Z3.Lang" API provides a high-level interface to Z3, but it is still very experimental and likely to change. .+ * In version 0.3.2 the "Z3.Lang" interface has been deprecated, we will move+ it to a dedicated package.+ . Important notes: . * Installation (Unix-like): Just be sure to use the standard locations for dynamic libraries (\/usr\/lib) and header files (\/usr\/include), or else use the --extra-lib-dirs and --extra-include-dirs Cabal flags. .+ * Haddock documentation can be found at+ <http://www.iagoabal.eu/z3-haskell/doc/0.3.2>.+ . * Hackage fails to compile this package because of the (unsatisfied) /libz3/ dependency. .- * Haddock documentation can be found at- <http://www.iagoabal.eu/z3-haskell/doc/0.3.1>.+ A changelog is available at <https://bitbucket.org/iago/z3-haskell/src/tip/CHANGES.md> Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE-Author: Iago Abal <iago.abal@gmail.com>,+Author: Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>-Maintainer: Iago Abal <iago.abal@gmail.com>,+Maintainer: Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>-Copyright: 2012-2013, Iago Abal, David Castro-Category: Math, Theorem Provers, Formal Methods+Copyright: 2012-2014, Iago Abal, David Castro+Category: Math, SMT, Theorem Provers, Formal Methods Build-type: Simple Cabal-version: >= 1.6