{-# LANGUAGE DeriveDataTypeable #-} {-# 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) ptrToMaybe ptr | ptr == nullPtr = Nothing | otherwise = Just ptr