diff --git a/Z3/Base.hs b/Z3/Base.hs --- a/Z3/Base.hs +++ b/Z3/Base.hs @@ -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 , --- David Castro --- --- Low-level bindings to Z3 API. - --- TODO Rename showModel and showContext to match Z3 C API names. -module Z3.Base ( - - -- * Types - Config - , Context - , Symbol - , AST - , Sort - , FuncDecl - , App - , Pattern - , Model - , 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: -mkConfig :: IO Config -mkConfig = Config <$> z3_mk_config - --- | Delete a configuration. --- --- Reference: -delConfig :: Config -> IO () -delConfig = z3_del_config . unConfig - --- | Run a computation using a temporally created configuration. -withConfig :: (Config -> IO a) -> IO a -withConfig = bracket mkConfig delConfig - --- | Set a configuration parameter. --- --- Reference: --- --- See: -setParamValue :: Config -> String -> String -> IO () -setParamValue cfg s1 s2 = - withCString s1 $ \cs1 -> - withCString s2 $ \cs2 -> - z3_set_param_value (unConfig cfg) cs1 cs2 - ---------------------------------------------------------------------- --- Context - --- | Create a context using the given configuration. --- --- Reference: -mkContext :: Config -> IO Context -mkContext cfg = do - ctxPtr <- z3_mk_context (unConfig cfg) - z3_set_error_handler ctxPtr nullFunPtr - return $ Context ctxPtr - --- | Delete the given logical context. --- --- Reference: -delContext :: Context -> IO () -delContext = z3_del_context . unContext - --- | Run a computation using a temporally created context. -withContext :: Config -> (Context -> IO a) -> IO a -withContext cfg = bracket (mkContext cfg) delContext - --- | Convert the given logical context into a string. --- --- Reference: -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: -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: -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: -mkUninterpretedSort :: Context -> Symbol -> IO Sort -mkUninterpretedSort c sy = checkError c $ - Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy) - --- | Create the /Boolean/ type. --- --- Reference: -mkBoolSort :: Context -> IO Sort -mkBoolSort c = checkError c $ Sort <$> z3_mk_bool_sort (unContext c) - --- | Create an /integer/ type. --- --- Reference: -mkIntSort :: Context -> IO Sort -mkIntSort c = checkError c $ Sort <$> z3_mk_int_sort (unContext c) - --- | Create a /real/ type. --- --- Reference: -mkRealSort :: Context -> IO Sort -mkRealSort c = checkError c $ Sort <$> z3_mk_real_sort (unContext c) - --- | Create a bit-vector type of the given size. --- --- This type can also be seen as a machine integer. --- --- Reference: -mkBvSort :: Context -> Int -> IO Sort -mkBvSort c n = checkError c $ Sort <$> z3_mk_bv_sort (unContext c) (fromIntegral n) - --- | Create an array type --- --- Reference: --- -mkArraySort :: Context -> Sort -> Sort -> IO Sort -mkArraySort c dom rng = checkError c $ Sort <$> z3_mk_array_sort (unContext c) (unSort dom) (unSort rng) - --- | Create a tuple type --- --- Reference: -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: -mkApp :: Context -> FuncDecl -> [AST] -> IO AST -mkApp ctx fd args = - withArray (map unAST args) $ \pargs -> - checkError ctx $ - AST <$> z3_mk_app ctxPtr fdPtr numArgs pargs - where ctxPtr = unContext ctx - fdPtr = unFuncDecl fd - numArgs = genericLength args - --- | Declare and create a constant. --- --- Reference: -mkConst :: Context -> Symbol -> Sort -> IO AST -mkConst c x s = checkError c $ AST <$> z3_mk_const (unContext c) (unSymbol x) (unSort s) - --- TODO Constants and Applications: Z3_mk_fresh_func_decl --- TODO Constants and Applications: Z3_mk_fresh_const - --- | Create an AST node representing /true/. --- --- Reference: -mkTrue :: Context -> IO AST -mkTrue c = checkError c $ AST <$> z3_mk_true (unContext c) - --- | Create an AST node representing /false/. --- --- Reference: -mkFalse :: Context -> IO AST -mkFalse c = checkError c $ AST <$> z3_mk_false (unContext c) - --- | Create an AST node representing /l = r/. --- --- Reference: -mkEq :: Context -> AST -> AST -> IO AST -mkEq c e1 e2 = checkError c $ AST <$> z3_mk_eq (unContext c) (unAST e1) (unAST e2) - --- | The distinct construct is used for declaring the arguments pairwise --- distinct. --- --- Reference: -mkDistinct :: Context -> [AST] -> IO AST -mkDistinct _ [] = error "Z3.Base.mkDistinct: empty list of expressions" -mkDistinct c es = - withArray (map unAST es) $ \aptr -> - checkError c $ - AST <$> z3_mk_distinct (unContext c) n aptr - where n = genericLength es - --- | Create an AST node representing /not(a)/. --- --- Reference: -mkNot :: Context -> AST -> IO AST -mkNot c e = checkError c $ AST <$> z3_mk_not (unContext c) (unAST e) - --- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/. --- --- Reference: -mkIte :: Context -> AST -> AST -> AST -> IO AST -mkIte c g e1 e2 = - checkError c $ AST <$> z3_mk_ite (unContext c) (unAST g) (unAST e1) (unAST e2) - --- | Create an AST node representing /t1 iff t2/. --- --- Reference: -mkIff :: Context -> AST -> AST -> IO AST -mkIff c p q = checkError c $ AST <$> z3_mk_iff (unContext c) (unAST p) (unAST q) - --- | Create an AST node representing /t1 implies t2/. --- --- Reference: -mkImplies :: Context -> AST -> AST -> IO AST -mkImplies c p q = checkError c $ AST <$> z3_mk_implies (unContext c) (unAST p) (unAST q) - --- | Create an AST node representing /t1 xor t2/. --- --- Reference: -mkXor :: Context -> AST -> AST -> IO AST -mkXor c p q = checkError c $ AST <$> z3_mk_xor (unContext c) (unAST p) (unAST q) - --- | Create an AST node representing args[0] and ... and args[num_args-1]. --- --- Reference: -mkAnd :: Context -> [AST] -> IO AST -mkAnd _ [] = error "Z3.Base.mkAnd: empty list of expressions" -mkAnd c es = - withArray (map unAST es) $ \aptr -> - checkError c $ - AST <$> z3_mk_and (unContext c) n aptr - where n = genericLength es - --- | Create an AST node representing args[0] or ... or args[num_args-1]. --- --- Reference: -mkOr :: Context -> [AST] -> IO AST -mkOr _ [] = error "Z3.Base.mkOr: empty list of expressions" -mkOr c es = - withArray (map unAST es) $ \aptr -> - checkError c $ - AST <$> z3_mk_or (unContext c) n aptr - where n = genericLength es - --- | Create an AST node representing args[0] + ... + args[num_args-1]. --- --- Reference: -mkAdd :: Context -> [AST] -> IO AST -mkAdd _ [] = error "Z3.Base.mkAdd: empty list of expressions" -mkAdd c es = - withArray (map unAST es) $ \aptr -> - checkError c $ - AST <$> z3_mk_add (unContext c) n aptr - where n = genericLength es - --- | Create an AST node representing args[0] * ... * args[num_args-1]. --- --- Reference: -mkMul :: Context -> [AST] -> IO AST -mkMul _ [] = error "Z3.Base.mkMul: empty list of expressions" -mkMul c es = - withArray (map unAST es) $ \aptr -> - checkError c $ - AST <$> z3_mk_mul (unContext c) n aptr - where n = genericLength es - --- | Create an AST node representing args[0] - ... - args[num_args - 1]. --- --- Reference: -mkSub :: Context -> [AST] -> IO AST -mkSub _ [] = error "Z3.Base.mkSub: empty list of expressions" -mkSub c es = - withArray (map unAST es) $ \aptr -> - checkError c $ - AST <$> z3_mk_sub (unContext c) n aptr - where n = genericLength es - --- | Create an AST node representing -arg. --- --- Reference: -mkUnaryMinus :: Context -> AST -> IO AST -mkUnaryMinus c e = checkError c $ AST <$> z3_mk_unary_minus (unContext c) (unAST e) - --- | Create an AST node representing arg1 div arg2. --- --- Reference: -mkDiv :: Context -> AST -> AST -> IO AST -mkDiv c e1 e2 = checkError c $ AST <$> z3_mk_div (unContext c) (unAST e1) (unAST e2) - --- | Create an AST node representing arg1 mod arg2. --- --- Reference: -mkMod :: Context -> AST -> AST -> IO AST -mkMod c e1 e2 = checkError c $ AST <$> z3_mk_mod (unContext c) (unAST e1) (unAST e2) - --- | Create an AST node representing arg1 rem arg2. --- --- Reference: -mkRem :: Context -> AST -> AST -> IO AST -mkRem c e1 e2 = checkError c $ AST <$> z3_mk_rem (unContext c) (unAST e1) (unAST e2) - --- | Create less than. --- --- Reference: -mkLt :: Context -> AST -> AST -> IO AST -mkLt c e1 e2 = checkError c $ AST <$> z3_mk_lt (unContext c) (unAST e1) (unAST e2) - --- | Create less than or equal to. --- --- Reference: -mkLe :: Context -> AST -> AST -> IO AST -mkLe c e1 e2 = checkError c $ AST <$> z3_mk_le (unContext c) (unAST e1) (unAST e2) - --- | Create greater than. --- --- Reference: -mkGt :: Context -> AST -> AST -> IO AST -mkGt c e1 e2 = checkError c $ AST <$> z3_mk_gt (unContext c) (unAST e1) (unAST e2) - --- | Create greater than or equal to. --- --- Reference: -mkGe :: Context -> AST -> AST -> IO AST -mkGe c e1 e2 = checkError c $ AST <$> z3_mk_ge (unContext c) (unAST e1) (unAST e2) - --- | Coerce an integer to a real. --- --- Reference: -mkInt2Real :: Context -> AST -> IO AST -mkInt2Real c e = checkError c $ AST <$> z3_mk_int2real (unContext c) (unAST e) - --- | Coerce a real to an integer. --- --- Reference: -mkReal2Int :: Context -> AST -> IO AST -mkReal2Int c e = checkError c $ AST <$> z3_mk_real2int (unContext c) (unAST e) - --- | Check if a real number is an integer. --- --- Reference: -mkIsInt :: Context -> AST -> IO AST -mkIsInt c e = checkError c $ AST <$> z3_mk_is_int (unContext c) (unAST e) - ---------------------------------------------------------------------- --- Bit-vectors - --- | Bitwise negation. --- --- Reference: -mkBvnot :: Context -> AST -> IO AST -mkBvnot c e = checkError c $ AST <$> z3_mk_bvnot (unContext c) (unAST e) - --- | Take conjunction of bits in vector, return vector of length 1. --- --- Reference: -mkBvredand :: Context -> AST -> IO AST -mkBvredand c e = checkError c $ AST <$> z3_mk_bvredand (unContext c) (unAST e) - --- | Take disjunction of bits in vector, return vector of length 1. --- --- Reference: -mkBvredor :: Context -> AST -> IO AST -mkBvredor c e = checkError c $ AST <$> z3_mk_bvredor (unContext c) (unAST e) - --- | Bitwise and. --- --- Reference: -mkBvand :: Context -> AST -> AST -> IO AST -mkBvand c e1 e2 = checkError c $ AST <$> z3_mk_bvand (unContext c) (unAST e1) (unAST e2) - --- | Bitwise or. --- --- Reference: -mkBvor :: Context -> AST -> AST -> IO AST -mkBvor c e1 e2 = checkError c $ AST <$> z3_mk_bvor (unContext c) (unAST e1) (unAST e2) - --- | Bitwise exclusive-or. --- --- Reference: -mkBvxor :: Context -> AST -> AST -> IO AST -mkBvxor c e1 e2 = checkError c $ AST <$> z3_mk_bvxor (unContext c) (unAST e1) (unAST e2) - --- | Bitwise nand. --- --- Reference: -mkBvnand :: Context -> AST -> AST -> IO AST -mkBvnand c e1 e2 = checkError c $ AST <$> z3_mk_bvnand (unContext c) (unAST e1) (unAST e2) - --- | Bitwise nor. --- --- Reference: -mkBvnor :: Context -> AST -> AST -> IO AST -mkBvnor c e1 e2 = checkError c $ AST <$> z3_mk_bvnor (unContext c) (unAST e1) (unAST e2) - --- | Bitwise xnor. --- --- Reference: -mkBvxnor :: Context -> AST -> AST -> IO AST -mkBvxnor c e1 e2 = checkError c $ AST <$> z3_mk_bvxnor (unContext c) (unAST e1) (unAST e2) - --- | Standard two's complement unary minus. --- --- Reference: AST -> IO AST -mkBvneg c e = checkError c $ AST <$> z3_mk_bvneg (unContext c) (unAST e) - --- | Standard two's complement addition. --- --- Reference: -mkBvadd :: Context -> AST -> AST -> IO AST -mkBvadd c e1 e2 = checkError c $ AST <$> z3_mk_bvadd (unContext c) (unAST e1) (unAST e2) - --- | Standard two's complement subtraction. --- --- Reference: -mkBvsub :: Context -> AST -> AST -> IO AST -mkBvsub c e1 e2 = checkError c $ AST <$> z3_mk_bvsub (unContext c) (unAST e1) (unAST e2) - --- | Standard two's complement multiplication. --- --- Reference: -mkBvmul :: Context -> AST -> AST -> IO AST -mkBvmul c e1 e2 = checkError c $ AST <$> z3_mk_bvmul (unContext c) (unAST e1) (unAST e2) - --- | Unsigned division. --- --- Reference: -mkBvudiv :: Context -> AST -> AST -> IO AST -mkBvudiv c e1 e2 = checkError c $ AST <$> z3_mk_bvudiv (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed division. --- --- Reference: -mkBvsdiv :: Context -> AST -> AST -> IO AST -mkBvsdiv c e1 e2 = checkError c $ AST <$> z3_mk_bvsdiv (unContext c) (unAST e1) (unAST e2) - --- | Unsigned remainder. --- --- Reference: -mkBvurem :: Context -> AST -> AST -> IO AST -mkBvurem c e1 e2 = checkError c $ AST <$> z3_mk_bvurem (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed remainder (sign follows dividend). --- --- Reference: -mkBvsrem :: Context -> AST -> AST -> IO AST -mkBvsrem c e1 e2 = checkError c $ AST <$> z3_mk_bvsrem (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed remainder (sign follows divisor). --- --- Reference: -mkBvsmod :: Context -> AST -> AST -> IO AST -mkBvsmod c e1 e2 = checkError c $ AST <$> z3_mk_bvsmod (unContext c) (unAST e1) (unAST e2) - --- | Unsigned less than. --- --- Reference: -mkBvult :: Context -> AST -> AST -> IO AST -mkBvult c e1 e2 = checkError c $ AST <$> z3_mk_bvult (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed less than. --- --- Reference: -mkBvslt :: Context -> AST -> AST -> IO AST -mkBvslt c e1 e2 = checkError c $ AST <$> z3_mk_bvslt (unContext c) (unAST e1) (unAST e2) - --- | Unsigned less than or equal to. --- --- Reference: -mkBvule :: Context -> AST -> AST -> IO AST -mkBvule c e1 e2 = checkError c $ AST <$> z3_mk_bvule (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed less than or equal to. --- --- Reference: -mkBvsle :: Context -> AST -> AST -> IO AST -mkBvsle c e1 e2 = checkError c $ AST <$> z3_mk_bvsle (unContext c) (unAST e1) (unAST e2) - --- | Unsigned greater than or equal to. --- --- Reference: -mkBvuge :: Context -> AST -> AST -> IO AST -mkBvuge c e1 e2 = checkError c $ AST <$> z3_mk_bvuge (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed greater than or equal to. --- --- Reference: -mkBvsge :: Context -> AST -> AST -> IO AST -mkBvsge c e1 e2 = checkError c $ AST <$> z3_mk_bvsge (unContext c) (unAST e1) (unAST e2) - --- | Unsigned greater than. --- --- Reference: -mkBvugt :: Context -> AST -> AST -> IO AST -mkBvugt c e1 e2 = checkError c $ AST <$> z3_mk_bvugt (unContext c) (unAST e1) (unAST e2) - --- | Two's complement signed greater than. --- --- Reference: -mkBvsgt :: Context -> AST -> AST -> IO AST -mkBvsgt c e1 e2 = checkError c $ AST <$> z3_mk_bvsgt (unContext c) (unAST e1) (unAST e2) - --- | Concatenate the given bit-vectors. --- --- Reference: -mkConcat :: Context -> AST -> AST -> IO AST -mkConcat c e1 e2 = checkError c $ AST <$> z3_mk_concat (unContext c) (unAST e1) (unAST e2) - --- | Extract the bits high down to low from a bitvector of size m to yield a new --- bitvector of size /n/, where /n = high - low + 1/. --- --- Reference: -mkExtract :: Context -> Int -> Int -> AST -> IO AST -mkExtract c j i e - = checkError c $ AST <$> z3_mk_extract (unContext c) (fromIntegral j) (fromIntegral i) (unAST e) - --- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector --- of size /m+i/, where /m/ is the size of the given bit-vector. --- --- Reference: -mkSignExt :: Context -> Int -> AST -> IO AST -mkSignExt c i e - = checkError c $ AST <$> z3_mk_sign_ext (unContext c) (fromIntegral i) (unAST e) - --- | Extend the given bit-vector with zeros to the (unsigned) equivalent --- bitvector of size /m+i/, where /m/ is the size of the given bit-vector. --- --- Reference: -mkZeroExt :: Context -> Int -> AST -> IO AST -mkZeroExt c i e - = checkError c $ AST <$> z3_mk_zero_ext (unContext c) (fromIntegral i) (unAST e) - --- | Repeat the given bit-vector up length /i/. --- --- Reference: -mkRepeat :: Context -> Int -> AST -> IO AST -mkRepeat c i e - = checkError c $ AST <$> z3_mk_repeat (unContext c) (fromIntegral i) (unAST e) - --- | Shift left. --- --- Reference: -mkBvshl :: Context -> AST -> AST -> IO AST -mkBvshl c e1 e2 = checkError c $ AST <$> z3_mk_bvshl (unContext c) (unAST e1) (unAST e2) - --- | Logical shift right. --- --- Reference: -mkBvlshr :: Context -> AST -> AST -> IO AST -mkBvlshr c e1 e2 = checkError c $ AST <$> z3_mk_bvlshr (unContext c) (unAST e1) (unAST e2) - --- | Arithmetic shift right. --- --- Reference: -mkBvashr :: Context -> AST -> AST -> IO AST -mkBvashr c e1 e2 = checkError c $ AST <$> z3_mk_bvashr (unContext c) (unAST e1) (unAST e2) - --- | Rotate bits of /t1/ to the left /i/ times. --- --- Reference: -mkRotateLeft :: Context -> Int -> AST -> IO AST -mkRotateLeft c i e - = checkError c $ AST <$> z3_mk_rotate_left (unContext c) (fromIntegral i) (unAST e) - --- | Rotate bits of /t1/ to the right /i/ times. --- --- Reference: -mkRotateRight :: Context -> Int -> AST -> IO AST -mkRotateRight c i e - = checkError c $ AST <$> z3_mk_rotate_right (unContext c) (fromIntegral i) (unAST e) - --- | Rotate bits of /t1/ to the left /t2/ times. --- --- Reference: -mkExtRotateLeft :: Context -> AST -> AST -> IO AST -mkExtRotateLeft c e1 e2 - = checkError c $ AST <$> z3_mk_ext_rotate_left (unContext c) (unAST e1) (unAST e2) - --- | Rotate bits of /t1/ to the right /t2/ times. --- --- Reference: -mkExtRotateRight :: Context -> AST -> AST -> IO AST -mkExtRotateRight c e1 e2 - = checkError c $ AST <$> z3_mk_ext_rotate_right (unContext c) (unAST e1) (unAST e2) - --- | Create an /n/ bit bit-vector from the integer argument /t1/. --- --- Reference: -mkInt2bv :: Context -> Int -> AST -> IO AST -mkInt2bv c i e - = checkError c $ AST <$> z3_mk_int2bv (unContext c) (fromIntegral i) (unAST e) - --- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false, --- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative --- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/. --- If /is_signed/ is true, /t1/ is treated as a signed bit-vector. --- --- Reference: -mkBv2int :: Context -> AST -> Bool -> IO AST -mkBv2int c e is_signed - = checkError c $ AST <$> z3_mk_bv2int (unContext c) (unAST e) (unBool is_signed) - --- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/ --- does not overflow. --- --- Reference: -mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST -mkBvaddNoOverflow c e1 e2 is_signed = - checkError c $ AST <$> z3_mk_bvadd_no_overflow (unContext c) (unAST e1) (unAST e2) - (unBool is_signed) - --- | Create a predicate that checks that the bit-wise signed addition of /t1/ --- and /t2/ does not underflow. --- --- Reference: -mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST -mkBvaddNoUnderflow c e1 e2 = - checkError c $ AST <$> z3_mk_bvadd_no_underflow (unContext c) (unAST e1) (unAST e2) - --- | Create a predicate that checks that the bit-wise signed subtraction of /t1/ --- and /t2/ does not overflow. --- --- Reference: -mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST -mkBvsubNoOverflow c e1 e2 = - checkError c $ AST <$> z3_mk_bvsub_no_overflow (unContext c) (unAST e1) (unAST e2) - --- | Create a predicate that checks that the bit-wise subtraction of /t1/ and --- /t2/ does not underflow. --- --- Reference: -mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST -mkBvsubNoUnderflow c e1 e2 = - checkError c $ AST <$> z3_mk_bvsub_no_underflow (unContext c) (unAST e1) (unAST e2) - --- | Create a predicate that checks that the bit-wise signed division of /t1/ --- and /t2/ does not overflow. --- --- Reference: -mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST -mkBvsdivNoOverflow c e1 e2 = - checkError c $ AST <$> z3_mk_bvsdiv_no_overflow (unContext c) (unAST e1) (unAST e2) - --- | Check that bit-wise negation does not overflow when /t1/ is interpreted as --- a signed bit-vector. --- --- Reference: -mkBvnegNoOverflow :: Context -> AST -> IO AST -mkBvnegNoOverflow c e = - checkError c $ AST <$> z3_mk_bvneg_no_overflow (unContext c) (unAST e) - --- | Create a predicate that checks that the bit-wise multiplication of /t1/ and --- /t2/ does not overflow. --- --- Reference: -mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST -mkBvmulNoOverflow c e1 e2 is_signed = - checkError c $ AST <$> z3_mk_bvmul_no_overflow (unContext c) (unAST e1) (unAST e2) - (unBool is_signed) - --- | Create a predicate that checks that the bit-wise signed multiplication of --- /t1/ and /t2/ does not underflow. --- --- Reference: -mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST -mkBvmulNoUnderflow c e1 e2 = - checkError c $ AST <$> z3_mk_bvmul_no_underflow (unContext c) (unAST e1) (unAST e2) - ---------------------------------------------------------------------- --- Arrays - --- | Array read. The argument a is the array and i is the index of the array --- that gets read. --- --- Reference: -mkSelect :: Context -> AST -> AST -> IO AST -mkSelect c a1 a2 = checkError c $ AST <$> z3_mk_select (unContext c) (unAST a1) (unAST a2) - --- | Array update.   --- --- Reference: -mkStore :: Context -> AST -> AST -> AST -> IO AST -mkStore c a1 a2 a3 = checkError c $ AST <$> z3_mk_store (unContext c) (unAST a1) (unAST a2) (unAST a3) - --- | Create the constant array. --- --- Reference: -mkConstArray :: Context -> Sort -> AST -> IO AST -mkConstArray c s a = checkError c $ AST <$> z3_mk_const_array (unContext c) (unSort s) (unAST a) - --- | map f on the the argument arrays. --- --- Reference: -mkMap :: Context -> FuncDecl -> Int -> [AST] -> IO AST -mkMap c f n args = withArray (map unAST args) $ \args' -> - checkError c $ AST <$> z3_mk_map (unContext c) (unFuncDecl f) (fromIntegral n) args' - --- | Access the array default value. Produces the default range value, for --- arrays that can be represented as finite maps with a default range value. --- --- Reference: -mkArrayDefault :: Context -> AST -> IO AST -mkArrayDefault c a = checkError c $ AST <$> z3_mk_array_default (unContext c) (unAST a) - --- TODO Sets - ---------------------------------------------------------------------- --- Numerals - --- | Create a numeral of a given sort. --- --- Reference: -mkNumeral :: Context -> String -> Sort -> IO AST -mkNumeral c str s = - withCString str $ \cstr-> - checkError c $ AST <$> z3_mk_numeral (unContext c) cstr (unSort s) - -------------------------------------------------- --- Numerals / Integers - --- | Create a numeral of sort /int/. -mkInt :: Integral a => Context -> a -> IO AST -mkInt c n = mkIntSort c >>= mkNumeral c n_str - where n_str = show $ toInteger n - -{-# INLINE mkIntZ3 #-} -mkIntZ3 :: Context -> Int32 -> Sort -> IO AST -mkIntZ3 c n s = checkError c $ AST <$> z3_mk_int (unContext c) cn (unSort s) - where cn = fromIntegral n :: CInt - -{-# INLINE mkUnsignedIntZ3 #-} -mkUnsignedIntZ3 :: Context -> Word32 -> Sort -> IO AST -mkUnsignedIntZ3 c n s = checkError c $ AST <$> z3_mk_unsigned_int (unContext c) cn (unSort s) - where cn = fromIntegral n :: CUInt - -{-# INLINE mkInt64Z3 #-} -mkInt64Z3 :: Context -> Int64 -> Sort -> IO AST -mkInt64Z3 c n s = checkError c $ AST <$> z3_mk_int64 (unContext c) cn (unSort s) - where cn = fromIntegral n :: CLLong - -{-# INLINE mkUnsignedInt64Z3 #-} -mkUnsignedInt64Z3 :: Context -> Word64 -> Sort -> IO AST -mkUnsignedInt64Z3 c n s = - checkError c $ AST <$> z3_mk_unsigned_int64 (unContext c) cn (unSort s) - where cn = fromIntegral n :: CULLong - -{-# RULES "mkInt/mkInt_IntZ3" mkInt = mkInt_IntZ3 #-} -mkInt_IntZ3 :: Context -> Int32 -> IO AST -mkInt_IntZ3 c n = mkIntSort c >>= mkIntZ3 c n - -{-# RULES "mkInt/mkInt_UnsignedIntZ3" mkInt = mkInt_UnsignedIntZ3 #-} -mkInt_UnsignedIntZ3 :: Context -> Word32 -> IO AST -mkInt_UnsignedIntZ3 c n = mkIntSort c >>= mkUnsignedIntZ3 c n - -{-# RULES "mkInt/mkInt_Int64Z3" mkInt = mkInt_Int64Z3 #-} -mkInt_Int64Z3 :: Context -> Int64 -> IO AST -mkInt_Int64Z3 c n = mkIntSort c >>= mkInt64Z3 c n - -{-# RULES "mkInt/mkInt_UnsignedInt64Z3" mkInt = mkInt_UnsignedInt64Z3 #-} -mkInt_UnsignedInt64Z3 :: Context -> Word64 -> IO AST -mkInt_UnsignedInt64Z3 c n = mkIntSort c >>= mkUnsignedInt64Z3 c n - -------------------------------------------------- --- Numerals / Reals - --- | Create a numeral of sort /real/. -mkReal :: Real r => Context -> r -> IO AST -mkReal c n = mkRealSort c >>= mkNumeral c n_str - where r = toRational n - r_n = toInteger $ numerator r - r_d = toInteger $ denominator r - n_str = show r_n ++ " / " ++ show r_d - -{-# RULES "mkReal/mkRealZ3" mkReal = mkRealZ3 #-} -mkRealZ3 :: Context -> Ratio Int32 -> IO AST -mkRealZ3 c r = checkError c $ AST <$> z3_mk_real (unContext c) n d - where n = (fromIntegral $ numerator r) :: CInt - d = (fromIntegral $ denominator r) :: CInt - -{-# RULES "mkReal/mkReal_IntZ3" mkReal = mkReal_IntZ3 #-} -mkReal_IntZ3 :: Context -> Int32 -> IO AST -mkReal_IntZ3 c n = mkRealSort c >>= mkIntZ3 c n - -{-# RULES "mkReal/mkReal_UnsignedIntZ3" mkReal = mkReal_UnsignedIntZ3 #-} -mkReal_UnsignedIntZ3 :: Context -> Word32 -> IO AST -mkReal_UnsignedIntZ3 c n = mkRealSort c >>= mkUnsignedIntZ3 c n - -{-# RULES "mkReal/mkReal_Int64Z3" mkReal = mkReal_Int64Z3 #-} -mkReal_Int64Z3 :: Context -> Int64 -> IO AST -mkReal_Int64Z3 c n = mkRealSort c >>= mkInt64Z3 c n - -{-# RULES "mkReal/mkReal_UnsignedInt64Z3" mkReal = mkReal_UnsignedInt64Z3 #-} -mkReal_UnsignedInt64Z3 :: Context -> Word64 -> IO AST -mkReal_UnsignedInt64Z3 c n = mkRealSort c >>= mkUnsignedInt64Z3 c n - ---------------------------------------------------------------------- --- Quantifiers - -mkPattern :: Context -> [AST] -> IO Pattern -mkPattern _ [] = error "Z3.Base.mkPattern: empty list of expressions" -mkPattern c es = - withArray (map unAST es) $ \aptr -> - checkError c $ Pattern <$> z3_mk_pattern (unContext c) n aptr - where n = genericLength es - -mkBound :: Context -> Int -> Sort -> IO AST -mkBound c i s - | i >= 0 = checkError c $ AST <$> z3_mk_bound (unContext c) (fromIntegral i) (unSort s) - | otherwise = error "Z3.Base.mkBound: negative de-Bruijn index" - -mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST -mkForall c pats x s p - = withArray (map unPattern pats) $ \patsPtr -> - withArray (map unSymbol x ) $ \xptr -> - withArray (map unSort s ) $ \sptr -> - checkError c $ AST <$> z3_mk_forall cptr 0 n patsPtr len sptr xptr (unAST p) - where n = genericLength pats - cptr = unContext c - len - | l == 0 = error "Z3.Base.mkForall:\ - \ forall with 0 bound variables" - | l /= length x = error "Z3.Base.mkForall:\ - \ different number of symbols and sorts" - | otherwise = fromIntegral l - where l = length s - -mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST -mkExists c pats x s p - = withArray (map unPattern pats) $ \patsPtr -> - withArray (map unSymbol x ) $ \xptr -> - withArray (map unSort s ) $ \sptr -> - checkError c $ AST <$> z3_mk_exists cptr 0 n patsPtr len sptr xptr (unAST p) - where n = fromIntegral $ length pats - cptr = unContext c - len - | l == 0 = error "Z3.Base.mkForall:\ - \ forall with 0 bound variables" - | l /= length x = error "Z3.Base.mkForall:\ - \ different number of symbols and sorts" - | otherwise = fromIntegral l - where l = length s - ---------------------------------------------------------------------- --- Accessors - --- | Return the size of the given bit-vector sort. --- --- Reference: -getBvSortSize :: Context -> Sort -> IO Int -getBvSortSize c s = - checkError c $ fromIntegral <$> z3_get_bv_sort_size (unContext c) (unSort s) - --- | Return the sort of an AST node. --- --- Reference: -getSort :: Context -> AST -> IO Sort -getSort c e = checkError c $ Sort <$> z3_get_sort (unContext c) (unAST e) - --- | Cast a 'Z3_lbool' from Z3.Base.C to @Bool@. -castLBool :: Z3_lbool -> Maybe Bool -castLBool lb - | lb == z3_l_true = Just True - | lb == z3_l_false = Just False - | lb == z3_l_undef = Nothing - | otherwise = error "Z3.Base.castLBool: illegal `Z3_lbool' value" - --- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF --- otherwise. --- --- Reference: -getBool :: Context -> AST -> IO (Maybe Bool) -getBool c a = checkError c $ - castLBool <$> z3_get_bool_value (unContext c) (unAST a) - --- | Return numeral value, as a string of a numeric constant term. --- --- Reference: -getNumeralString :: Context -> AST -> IO String -getNumeralString c a = checkError c $ peekCString =<< z3_get_numeral_string ctxPtr (unAST a) - where ctxPtr = unContext c - --- | Return 'Z3Int' value -getInt :: Context -> AST -> IO Integer -getInt c a = read <$> getNumeralString c a - --- | Return 'Z3Real' value -getReal :: Context -> AST -> IO Rational -getReal c a = parse <$> getNumeralString c a - where parse :: String -> Rational - parse s - | [(i, sj)] <- reads s = i % parseDen (dropWhile (== ' ') sj) - | otherwise = error "Z3.Base.getReal: no parse" - - parseDen :: String -> Integer - parseDen "" = 1 - parseDen ('/':sj) = read sj - parseDen _ = error "Z3.Base.getReal: no parse" - - --- TODO Modifiers - ---------------------------------------------------------------------- --- Models - --- | Evaluate an AST node in the given model. -eval :: Context -> Model -> AST -> IO (Maybe AST) -eval ctx m a = - alloca $ \aptr2 -> - checkError ctx $ z3_eval ctxPtr (unModel m) (unAST a) aptr2 >>= peekAST aptr2 . toBool - where peekAST :: Ptr (Ptr Z3_ast) -> Bool -> IO (Maybe AST) - peekAST _p False = return Nothing - peekAST p True = Just . AST <$> peek p - - ctxPtr = unContext ctx - --- | Evaluate a collection of AST nodes in the given model. -evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST)) -evalT c m = fmap T.sequence . T.mapM (eval c m) - --- | 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: -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: -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: -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: -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: -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: -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: -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: -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: -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: -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: -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: -push :: Context -> IO () -push c = checkError c $ z3_push $ unContext c - --- | Backtrack /n/ backtracking points. --- --- Reference: -pop :: Context -> Int -> IO () -pop ctx cnt = checkError ctx $ z3_pop (unContext ctx) $ fromIntegral cnt - --- TODO Constraints: Z3_get_num_scopes --- TODO Constraints: Z3_persist_ast - --- | Assert a constraing into the logical context. --- --- Reference: -assertCnstr :: Context -> AST -> IO () -assertCnstr ctx ast = checkError ctx $ - z3_assert_cnstr (unContext ctx) (unAST ast) - --- | Get model (logical context is consistent) --- --- Reference : -getModel :: Context -> IO (Result, Maybe Model) -getModel c = - alloca $ \mptr -> - checkError c (z3_check_and_get_model (unContext c) mptr) >>= \lb -> - (toResult lb,) <$> peekModel mptr - where peekModel :: Ptr (Ptr Z3_model) -> IO (Maybe Model) - peekModel p | p == nullPtr = return Nothing - | otherwise = mkModel <$> peek p - mkModel :: Ptr Z3_model -> Maybe Model - mkModel = fmap Model . ptrToMaybe - --- | Delete a model object. --- --- Reference: -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: -check :: Context -> IO Result -check ctx = checkError ctx $ toResult <$> z3_check (unContext ctx) - --- TODO Constraints: Z3_check_assumptions --- TODO Constraints: Z3_get_implied_equalities - --- TODO From section 'Constraints' on. - - ---------------------------------------------------------------------- --- * Parameters - -mkParams :: Context -> IO Params -mkParams c = checkError c $ Params <$> z3_mk_params (unContext c) - -paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO () -paramsSetBool c params sym b = checkError c $ - z3_params_set_bool (unContext c) (unParams params) (unSymbol sym) (unBool b) - -paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO () -paramsSetUInt c params sym v = checkError c $ - z3_params_set_uint (unContext c) (unParams params) - (unSymbol sym) (fromIntegral v) - -paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO () -paramsSetDouble c params sym v = checkError c $ - z3_params_set_double (unContext c) (unParams params) - (unSymbol sym) (realToFrac v) - -paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO () -paramsSetSymbol c params sym v = - checkError c $ z3_params_set_symbol (unContext c) (unParams params) (unSymbol sym) - (unSymbol v) - -paramsToString :: Context -> Params -> IO String -paramsToString c (Params params) = - checkError c (z3_params_to_string (unContext c) params) >>= peekCString - - ---------------------------------------------------------------------- --- Solvers - -{-# WARNING Logic - , mkSolver - , mkSimpleSolver - , mkSolverForLogic - , solverSetParams - , solverPush - , solverPop - , solverReset - , solverAssertCnstr - , solverAssertAndTrack - , solverCheck - , solverCheckAndGetModel - , solverGetReasonUnknown - "New Z3 API support is still incomplete and fragile: \ - \you may experience segmentation faults!" - #-} - --- | Solvers available in Z3. --- --- These are described at --- --- /WARNING/: Support for solvers is fragile, you may experience segmentation --- faults! -data Logic - = AUFLIA - -- ^ Closed formulas over the theory of linear integer arithmetic - -- and arrays extended with free sort and function symbols but - -- restricted to arrays with integer indices and values. - - | AUFLIRA - -- ^ Closed linear formulas with free sort and function symbols over - -- one- and two-dimentional arrays of integer index and real - -- value. - - | AUFNIRA - -- ^ Closed formulas with free function and predicate symbols over a - -- theory of arrays of arrays of integer index and real value. - - | LRA - -- ^ Closed linear formulas in linear real arithmetic. - - | QF_ABV - -- ^ Closed quantifier-free formulas over the theory of bitvectors - -- and bitvector arrays. - - | QF_AUFBV - -- ^ Closed quantifier-free formulas over the theory of bitvectors - -- and bitvector arrays extended with free sort and function - -- symbols. - - | QF_AUFLIA - -- ^ Closed quantifier-free linear formulas over the theory of - -- integer arrays extended with free sort and function symbols. - - | QF_AX - -- ^ Closed quantifier-free formulas over the theory of arrays with - -- extensionality. - - | QF_BV - -- ^ Closed quantifier-free formulas over the theory of fixed-size - -- bitvectors. - - | QF_IDL - -- ^ Difference Logic over the integers. In essence, Boolean - -- combinations of inequations of the form x - y < b where x and y - -- are integer variables and b is an integer constant. - - | QF_LIA - -- ^ Unquantified linear integer arithmetic. In essence, Boolean - -- combinations of inequations between linear polynomials over - -- integer variables. - - | QF_LRA - -- ^ Unquantified linear real arithmetic. In essence, Boolean - -- combinations of inequations between linear polynomials over - -- real variables. - - | QF_NIA - -- ^ Quantifier-free integer arithmetic. - - | QF_NRA - -- ^ Quantifier-free real arithmetic. - - | QF_RDL - -- ^ Difference Logic over the reals. In essence, Boolean - -- combinations of inequations of the form x - y < b where x and y - -- are real variables and b is a rational constant. - - | QF_UF - -- ^ Unquantified formulas built over a signature of uninterpreted - -- (i.e., free) sort and function symbols. - - | QF_UFBV - -- ^ Unquantified formulas over bitvectors with uninterpreted sort - -- function and symbols. - - | QF_UFIDL - -- ^ Difference Logic over the integers (in essence) but with - -- uninterpreted sort and function symbols. - - | QF_UFLIA - -- ^ Unquantified linear integer arithmetic with uninterpreted sort - -- and function symbols. - - | QF_UFLRA - -- ^ Unquantified linear real arithmetic with uninterpreted sort and - -- function symbols. - - | QF_UFNRA - -- ^ Unquantified non-linear real arithmetic with uninterpreted sort - -- and function symbols. - - | UFLRA - -- ^ Linear real arithmetic with uninterpreted sort and function - -- symbols. - - | UFNIA - -- ^ Non-linear integer arithmetic with uninterpreted sort and - -- function symbols. - -instance Show Logic where - show AUFLIA = "AUFLIA" - show AUFLIRA = "AUFLIRA" - show AUFNIRA = "AUFNIRA" - show LRA = "LRA" - show QF_ABV = "QF_ABV" - show QF_AUFBV = "QF_AUFBV" - show QF_AUFLIA = "QF_AUFLIA" - show QF_AX = "QF_AX" - show QF_BV = "QF_BV" - show QF_IDL = "QF_IDL" - show QF_LIA = "QF_LIA" - show QF_LRA = "QF_LRA" - show QF_NIA = "QF_NIA" - show QF_NRA = "QF_NRA" - show QF_RDL = "QF_RDL" - show QF_UF = "QF_UF" - show QF_UFBV = "QF_UFBV" - show QF_UFIDL = "QF_UFIDL" - show QF_UFLIA = "QF_UFLIA" - show QF_UFLRA = "QF_UFLRA" - show QF_UFNRA = "QF_UFNRA" - show UFLRA = "UFLRA" - show UFNIA = "UFNIA" - -mkSolver :: Context -> IO Solver -mkSolver c = checkError c $ Solver <$> z3_mk_solver (unContext c) - -mkSimpleSolver :: Context -> IO Solver -mkSimpleSolver c = checkError c $ Solver <$> z3_mk_simple_solver (unContext c) - -mkSolverForLogic :: Context -> Logic -> IO Solver -mkSolverForLogic c logic = - do sym <- mkStringSymbol c (show logic) - checkError c $ Solver <$> z3_mk_solver_for_logic (unContext c) (unSymbol sym) - -solverSetParams :: Context -> Solver -> Params -> IO () -solverSetParams c solver params = - checkError c $ z3_solver_set_params (unContext c) (unSolver solver) (unParams params) - -solverPush :: Context -> Solver -> IO () -solverPush c solver = checkError c $ z3_solver_push (unContext c) (unSolver solver) - -solverPop :: Context -> Solver -> Int -> IO () -solverPop c solver i = - checkError c $ z3_solver_pop (unContext c) (unSolver solver) (fromIntegral i) - -solverReset :: Context -> Solver -> IO () -solverReset c solver = checkError c $ z3_solver_reset (unContext c) (unSolver solver) - -solverAssertCnstr :: Context -> Solver -> AST -> IO () -solverAssertCnstr c solver ast = - checkError c $ z3_solver_assert (unContext c) (unSolver solver) (unAST ast) - -solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO () -solverAssertAndTrack c solver constraint var = - checkError c $ z3_solver_assert_and_track (unContext c) (unSolver solver) - (unAST constraint) (unAST var) - -solverCheck :: Context -> Solver -> IO Result -solverCheck c solver = - checkError c $ toResult <$> z3_solver_check (unContext c) (unSolver solver) - -solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model) -solverCheckAndGetModel c (Solver s) = - do res <- checkError c $ toResult <$> z3_solver_check cptr s - mmodel <- case res of - Sat -> checkError c $ (Just . Model) <$> z3_solver_get_model cptr s - _ -> return Nothing - return (res, mmodel) - where cptr = unContext c - -solverGetReasonUnknown :: Context -> Solver -> IO String -solverGetReasonUnknown c solver = - checkError c $ z3_solver_get_reason_unknown (unContext c) (unSolver solver) >>= peekCString - ---------------------------------------------------------------------- --- String Conversion - --- | Pretty-printing mode for converting ASTs to strings. The mode --- can be one of the following: --- --- * Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format. --- --- * Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format. --- --- * Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x --- compliant format. --- --- * Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x --- compliant format. -data ASTPrintMode - = Z3_PRINT_SMTLIB_FULL - | Z3_PRINT_LOW_LEVEL - | Z3_PRINT_SMTLIB_COMPLIANT - | Z3_PRINT_SMTLIB2_COMPLIANT - --- | Set the pretty-printing mode for converting ASTs to strings. -setASTPrintMode :: Context -> ASTPrintMode -> IO () -setASTPrintMode ctx Z3_PRINT_SMTLIB_FULL = - checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_smtlib_full -setASTPrintMode ctx Z3_PRINT_LOW_LEVEL = - checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_low_level -setASTPrintMode ctx Z3_PRINT_SMTLIB_COMPLIANT = - checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_smtlib_compliant -setASTPrintMode ctx Z3_PRINT_SMTLIB2_COMPLIANT = - checkError ctx $ z3_set_ast_print_mode (unContext ctx) z3_print_smtlib2_compliant - --- | Convert an AST to a string. -astToString :: Context -> AST -> IO String -astToString ctx ast = - checkError ctx $ z3_ast_to_string (unContext ctx) (unAST ast) >>= peekCString - --- | Convert a pattern to a string. -patternToString :: Context -> Pattern -> IO String -patternToString ctx pattern = - checkError ctx $ z3_pattern_to_string (unContext ctx) (unPattern pattern) >>= peekCString - --- | Convert a sort to a string. -sortToString :: Context -> Sort -> IO String -sortToString ctx sort = - checkError ctx $ z3_sort_to_string (unContext ctx) (unSort sort) >>= peekCString - --- | Convert a FuncDecl to a string. -funcDeclToString :: Context -> FuncDecl -> IO String -funcDeclToString ctx funcDecl = - checkError ctx $ z3_func_decl_to_string (unContext ctx) (unFuncDecl funcDecl) >>= peekCString - --- | Convert the given benchmark into SMT-LIB formatted string. --- --- The output format can be configured via 'setASTPrintMode'. --- --- Reference: -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 , +-- David Castro +-- +-- Low-level bindings to Z3 API. +-- +-- There is (mostly) a one-to-one correspondence with Z3 C API, thus see +-- +-- 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 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 +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 +-- +-- /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) diff --git a/Z3/Base/C.hsc b/Z3/Base/C.hsc --- a/Z3/Base/C.hsc +++ b/Z3/Base/C.hsc @@ -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 , +-- Maintainer: Iago Abal , -- David Castro -- --- 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: +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: +newtype Z3_bool = Z3_bool CInt + deriving Eq --- | Z3 custom error handler +-- | Reference: 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: +z3_true = Z3_bool(#const Z3_TRUE) +-- | Reference: +z3_false = Z3_bool(#const Z3_FALSE) --- | Z3 String type +-- | Reference: type Z3_string = CString --- | Z3 pretty-printing modes +-- | Reference: 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: type Z3_error_code = CInt #{enum Z3_error_code, , z3_ok = Z3_OK @@ -122,21 +118,15 @@ --------------------------------------------------------------------- -- * Create configuration --- | Create a configuration. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_config" z3_mk_config :: IO (Ptr Z3_config) --- | Delete the given configuration object. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_del_config" z3_del_config :: Ptr Z3_config -> IO () --- | Set a configuration parameter. --- --- Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_context" z3_mk_context :: Ptr Z3_config -> IO (Ptr Z3_context) --- | Delete the given logical context. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_del_context" z3_del_context :: Ptr Z3_context -> IO () --------------------------------------------------------------------- -- * Symbols --- | Create a Z3 symbol using an integer. --- --- Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_bool_sort" z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Create an integer type. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int_sort" z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Create a real type. --- --- Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_bv_sort" z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort) --- | Create an array type --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_array_sort" z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort) --- | Create a tuple type --- --- Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_true" z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) --- | Create an AST node representing /false/. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_false" z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast) --- | Create an AST node representing l = r. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_eq" z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- TODO: Z3_mk_distinct +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_not" z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing an if-then-else: ite(t1, t2, t3). --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_ite" z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing t1 iff t2. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_iff" z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing t1 implies t2. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_implies" z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing t1 xor t2. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_xor" z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing args[0] and ... and args[num_args-1]. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_and" z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Create an AST node representing args[0] or ... or args[num_args-1]. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_or" z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Arithmetic: Integers and Reals --- | Create an AST node representing args[0] + ... + args[num_args-1]. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_add" z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Create an AST node representing args[0] * ... * args[num_args-1]. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_mul" z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Create an AST node representing args[0] - ... - args[num_args - 1]. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_sub" z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Create an AST node representing -arg. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_unary_minus" z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing arg1 div arg2. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_div" z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing arg1 mod arg2. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_mod" z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an AST node representing arg1 rem arg2. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_rem" z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create less than. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_lt" z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create less than or equal to. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_le" z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create greater than. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_gt" z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create greater than or equal to. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_ge" z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Coerce an integer to a real. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int2real" z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Coerce a real to an integer. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_real2int" z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Check if a real number is an integer. --- --- Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvnot" z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Take conjunction of bits in vector, return vector of length 1. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvredand" z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Take disjunction of bits in vector, return vector of length 1. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvredor" z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Bitwise and. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvand" z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Bitwise or. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvor" z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Bitwise exclusive-or. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvxor" z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Bitwise nand. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvnand" z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Bitwise nor. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvnor" z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Bitwise xnor. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvxnor" z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Standard two's complement unary minus. --- --- Reference: Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Standard two's complement addition. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvadd" z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Standard two's complement subtraction. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsub" z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Standard two's complement multiplication. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvmul" z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Unsigned division. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvudiv" z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed division. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsdiv" z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Unsigned remainder. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvurem" z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed remainder (sign follows dividend). --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsrem" z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed remainder (sign follows divisor). --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsmod" z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Unsigned less than. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvult" z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed less than. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvslt" z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Unsigned less than or equal to. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvule" z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed less than or equal to. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsle" z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Unsigned greater than or equal to. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvuge" z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed greater than or equal to. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsge" z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Unsigned greater than. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvugt" z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Two's complement signed greater than. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsgt" z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Concatenate the given bit-vectors. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_concat" z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Extract the bits high down to low from a bitvector of size m to yield a new --- bitvector of size /n/, where /n = high - low + 1/. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_extract" z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector --- of size /m+i/, where /m/ is the size of the given bit-vector. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_sign_ext" z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Extend the given bit-vector with zeros to the (unsigned) equivalent --- bitvector of size /m+i/, where /m/ is the size of the given bit-vector. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_zero_ext" z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Repeat the given bit-vector up length /i/. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_repeat" z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Shift left. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvshl" z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Logical shift right. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvlshr" z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Arithmetic shift right. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_bvashr" z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Rotate bits of /t1/ to the left /i/ times. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_rotate_left" z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Rotate bits of /t1/ to the right /i/ times. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_rotate_right" z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Rotate bits of /t1/ to the left /t2/ times. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_ext_rotate_left" z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Rotate bits of /t1/ to the right /t2/ times. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_ext_rotate_right" z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an /n/ bit bit-vector from the integer argument /t1/. --- --- Reference: --- +-- | Reference: foreign import ccall unsafe "Z3_mk_int2bv" z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false, --- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative --- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/. --- If /is_signed/ is true, /t1/ is treated as a signed bit-vector. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bv2int" z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/ --- does not overflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvadd_no_overflow" z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise signed addition of /t1/ --- and /t2/ does not underflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvadd_no_underflow" z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise signed subtraction of /t1/ --- and /t2/ does not overflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsub_no_overflow" z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise subtraction of /t1/ and --- /t2/ does not underflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsub_no_underflow" z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise signed division of /t1/ --- and /t2/ does not overflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsdiv_no_overflow" z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Check that bit-wise negation does not overflow when /t1/ is interpreted as --- a signed bit-vector. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvneg_no_overflow" z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise multiplication of /t1/ and --- /t2/ does not overflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvmul_no_overflow" z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Create a predicate that checks that the bit-wise signed multiplication of --- /t1/ and /t2/ does not underflow. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvmul_no_underflow" z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -------------------------------------------------------------------------------- -- * Arrays --- | Array read. The argument a is the array and i is the index of the array --- that gets read. --- --- Reference: + +-- | Reference: foreign import ccall unsafe "Z3_mk_select" z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Array update.   --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_store" z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Create the constant array. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_const_array" z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | map f on the the argument arrays. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_map" z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Access the array default value. Produces the default range value, for --- arrays that can be represented as finite maps with a default range value. --- --- Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_numeral" z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Create a real from a fraction. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_real" z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast) --- | Create a numeral of a given sort. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int" z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Create a numeral of a given sort. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_unsigned_int" z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Create a numeral of a given sort. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int64" z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Create a numeral of a given sort. --- --- Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_pattern" z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) --- | Create a bound variable. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bound" z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Create a forall formula. --- --- Reference: +-- | Reference: 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: 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 +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: +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: +-- | Reference: foreign import ccall unsafe "Z3_get_bv_sort_size" z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt --- | Return the sort of an AST node. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_sort" z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) --- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF --- otherwise. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_bool_value" z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool --- | Return numeral value, as a string of a numeric constant term. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_numeral_string" z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string +-- | Reference: +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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: + +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: foreign import ccall unsafe "Z3_push" z3_push :: Ptr Z3_context -> IO () --- TODO Constraints: Z3_pop +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_assert_cnstr" z3_assert_cnstr :: Ptr Z3_context -> Ptr Z3_ast -> IO () --- | Check whether the given logical context is consistent or not. --- --- Reference : +-- | Reference : foreign import ccall unsafe "Z3_check_and_get_model" z3_check_and_get_model :: Ptr Z3_context -> Ptr (Ptr Z3_model) -> IO Z3_lbool --- | Check whether the given logical context is consistent or not. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_check" z3_check :: Ptr Z3_context -> IO Z3_lbool -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities --- | Delete a model object. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_del_model" z3_del_model :: Ptr Z3_context -> Ptr Z3_model -> IO () +-- | Reference: foreign import ccall unsafe "Z3_model_to_string" z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO CString +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_params" z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params) --- | Increment the reference counter of the given parameter set. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_inc_ref" z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () --- | Decrement the reference counter of the given parameter set. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_dec_ref" z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () --- | Add a Boolean parameter k with value v to the parameter set p. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_set_bool" z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Z3_bool -> IO () --- | Add an unsigned parameter k with value v to the parameter set p. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_set_uint" z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO () --- | Add a double parameter k with value v to the parameter set p. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_set_double" z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO () --- | Add a symbol parameter k with value v to the parameter set p. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_set_symbol" z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Ptr Z3_symbol -> IO () --- | Convert a parameter set into a string. This function is mainly --- used for printing the contents of a parameter set. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_to_string" z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string -{- --- | Validate the parameter set p against the parameter description --- set d. --- --- Reference: -foreign import ccall unsafe "Z3_params_validate" - z3_params_validate :: Ptr Z3_context -> Ptr Z3_params -> Z3_param_descrs -> IO () --} - --------------------------------------------------------------------- -- * Solvers --- | Create an SMT solver that uses a set of builtin tactics. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_solver" z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) --- | Create a simple solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_simple_solver" z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) --- | Create a solver for a particular logic, as given by the SMTLIB --- standard here: --- --- --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_solver_for_logic" z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver) --- | Set the parameters for a solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_set_params" z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO () --- | Increment the reference counter of the given solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_inc_ref" z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Decrement the reference counter of the given solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_dec_ref" z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Create a backtracking point in a solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_push" z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Backtrack to the nth-most recent backtracking point. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_pop" z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO () --- | Remove all assertions from a solver. --- --- Reference: +-- | Reference: +foreign import ccall unsafe "Z3_solver_get_num_scopes" + z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt + +-- | Reference: foreign import ccall unsafe "Z3_solver_reset" z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Add a constraint to a solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_assert" z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO () --- | Add a constraint to a solver and track it using a Boolean --- constant, given as the last argument. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_assert_and_track" z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> Ptr Z3_ast -> IO () --- | Check whether the assertions in a given solver are consistent. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_check" z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool --- | Retrieve the model for the last call to Z3_solver_check or --- Z3_solver_check_assumptions on the given solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_get_model" z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) --- | Return a brief justification for an "unknown" result (i.e., --- Z3_L_UNDEF) for the last call to Z3_solver_check or --- Z3_solver_check_assumptions on the given solver. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_get_reason_unknown" z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string +-- | Reference: +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: +-- | Reference: foreign import ccall unsafe "Z3_set_ast_print_mode" z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO () --- | Convert an AST into a string using the current print mode. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_ast_to_string" z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string --- | Convert a pattern into a string using the current print mode. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_pattern_to_string" z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string --- | Convert a sort into a string using the current print mode. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_sort_to_string" z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string --- | Convert a func_decl into a string using the current print mode. --- --- Reference: +-- | Reference: foreign import ccall unsafe "Z3_func_decl_to_string" z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string --- | Convert the given benchmark into SMT-LIB formatted string. --- --- Reference: +-- | Reference: 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 : +-- | Reference: foreign import ccall unsafe "Z3_get_error_code" z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code --- | Register a Z3 error handler. --- --- Reference : +-- | Reference: foreign import ccall unsafe "Z3_set_error_handler" z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO () --- | Set an error. --- --- Reference : +-- | Reference: foreign import ccall unsafe "Z3_set_error" z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO () --- | Return a string describing the given error code. --- --- Reference : +-- | Reference: foreign import ccall unsafe "Z3_get_error_msg" z3_get_error_msg :: Z3_error_code -> IO Z3_string --- | Return a string describing the given error code. --- --- Reference : +-- | Reference: 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: +foreign import ccall unsafe "Z3_get_version" + z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO () diff --git a/Z3/Lang.hs b/Z3/Lang.hs --- a/Z3/Lang.hs +++ b/Z3/Lang.hs @@ -8,8 +8,14 @@ -- David Castro -- 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 diff --git a/Z3/Lang/Lg2.hs b/Z3/Lang/Lg2.hs --- a/Z3/Lang/Lg2.hs +++ b/Z3/Lang/Lg2.hs @@ -9,7 +9,13 @@ -- Maintainer: Iago Abal , -- David Castro +{-# 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 diff --git a/Z3/Lang/Monad.hs b/Z3/Lang/Monad.hs --- a/Z3/Lang/Monad.hs +++ b/Z3/Lang/Monad.hs @@ -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 diff --git a/Z3/Lang/Nat.hs b/Z3/Lang/Nat.hs --- a/Z3/Lang/Nat.hs +++ b/Z3/Lang/Nat.hs @@ -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 module Z3.Lang.Nat + {-# DEPRECATED + "The Z3.Lang interface will be moved to a dedicated package." + #-} ( Nat ) where diff --git a/Z3/Lang/Pow2.hs b/Z3/Lang/Pow2.hs --- a/Z3/Lang/Pow2.hs +++ b/Z3/Lang/Pow2.hs @@ -9,8 +9,14 @@ -- Maintainer: Iago Abal , -- David Castro +{-# 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 diff --git a/Z3/Lang/Prelude.hs b/Z3/Lang/Prelude.hs --- a/Z3/Lang/Prelude.hs +++ b/Z3/Lang/Prelude.hs @@ -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 diff --git a/Z3/Monad.hs b/Z3/Monad.hs --- a/Z3/Monad.hs +++ b/Z3/Monad.hs @@ -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: -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: @@ -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 diff --git a/Z3/Opts.hs b/Z3/Opts.hs --- a/Z3/Opts.hs +++ b/Z3/Opts.hs @@ -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 , -- David Castro -- --- 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" diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -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 + . + . * Hackage fails to compile this package because of the (unsatisfied) /libz3/ dependency. . - * Haddock documentation can be found at - . + A changelog is available at Homepage: http://bitbucket.org/iago/z3-haskell License: BSD3 License-file: LICENSE -Author: Iago Abal , +Author: Iago Abal , David Castro -Maintainer: Iago Abal , +Maintainer: Iago Abal , David Castro -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