module Z3.Base (
Config
, Context
, Symbol
, AST
, Sort
, FuncDecl
, App
, Pattern
, Model
, FuncInterp
, FuncEntry
, Params
, Solver
, Result(..)
, mkConfig
, delConfig
, withConfig
, setParamValue
, mkContext
, delContext
, withContext
, contextToString
, showContext
, mkIntSymbol
, mkStringSymbol
, mkUninterpretedSort
, mkBoolSort
, mkIntSort
, mkRealSort
, mkBvSort
, mkArraySort
, mkTupleSort
, 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
, 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
, mkSelect
, mkStore
, mkConstArray
, mkMap
, mkArrayDefault
, mkNumeral
, mkInt
, mkReal
, mkPattern
, mkBound
, mkForall
, mkExists
, getBvSortSize
, getSort
, getBool
, getInt
, getReal
, FuncModel (..)
, eval
, evalT
, evalFunc
, evalArray
, getFuncInterp
, isAsArray
, getAsArrayFuncDecl
, funcInterpGetNumEntries
, funcInterpGetEntry
, funcInterpGetElse
, funcInterpGetArity
, funcEntryGetValue
, funcEntryGetNumArgs
, funcEntryGetArg
, modelToString
, showModel
, assertCnstr
, check
, getModel
, delModel
, push
, pop
, mkParams
, paramsSetBool
, paramsSetUInt
, paramsSetDouble
, paramsSetSymbol
, paramsToString
, Logic(..)
, mkSolver
, mkSimpleSolver
, mkSolverForLogic
, solverSetParams
, solverPush
, solverPop
, solverReset
, solverAssertCnstr
, solverAssertAndTrack
, solverCheck
, solverCheckAndGetModel
, solverGetReasonUnknown
, ASTPrintMode(..)
, setASTPrintMode
, astToString
, patternToString
, sortToString
, funcDeclToString
, benchmarkToSMTLibString
, 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 )
newtype Config = Config { unConfig :: Ptr Z3_config }
deriving Eq
newtype Context = Context { unContext :: Ptr Z3_context }
deriving Eq
newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol }
deriving (Eq, Ord, Show, Storable)
newtype AST = AST { unAST :: Ptr Z3_ast }
deriving (Eq, Ord, Show, Storable, Typeable)
newtype Sort = Sort { unSort :: Ptr Z3_sort }
deriving (Eq, Ord, Show, Storable)
newtype FuncDecl = FuncDecl { unFuncDecl :: Ptr Z3_func_decl }
deriving (Eq, Ord, Show, Storable, Typeable)
newtype App = App { _unApp :: Ptr Z3_app }
deriving (Eq, Ord, Show, Storable)
newtype Pattern = Pattern { unPattern :: Ptr Z3_pattern }
deriving (Eq, Ord, Show, Storable)
newtype Model = Model { unModel :: Ptr Z3_model }
deriving Eq
newtype FuncInterp = FuncInterp { unFuncInterp :: Ptr Z3_func_interp }
deriving Eq
newtype FuncEntry = FuncEntry { unFuncEntry :: Ptr Z3_func_entry }
deriving Eq
newtype Params = Params { unParams :: Ptr Z3_params }
deriving Eq
newtype Solver = Solver { unSolver :: Ptr Z3_solver }
deriving Eq
data Result
= Sat
| Unsat
| Undef
deriving (Eq, Ord, Read, Show)
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"
toBool :: Z3_bool -> Bool
toBool b
| b == z3_true = True
| b == z3_false = False
| otherwise = error "Z3.Base.toBool: illegal `Z3_bool' value"
unBool :: Bool -> Z3_bool
unBool True = z3_true
unBool False = z3_false
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
z3Error :: Z3ErrorCode -> String -> IO ()
z3Error cd = throw . Z3Error cd
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
mkConfig :: IO Config
mkConfig = Config <$> z3_mk_config
delConfig :: Config -> IO ()
delConfig = z3_del_config . unConfig
withConfig :: (Config -> IO a) -> IO a
withConfig = bracket mkConfig delConfig
setParamValue :: Config -> String -> String -> IO ()
setParamValue cfg s1 s2 =
withCString s1 $ \cs1 ->
withCString s2 $ \cs2 ->
z3_set_param_value (unConfig cfg) cs1 cs2
mkContext :: Config -> IO Context
mkContext cfg = do
ctxPtr <- z3_mk_context (unConfig cfg)
z3_set_error_handler ctxPtr nullFunPtr
return $ Context ctxPtr
delContext :: Context -> IO ()
delContext = z3_del_context . unContext
withContext :: Config -> (Context -> IO a) -> IO a
withContext cfg = bracket (mkContext cfg) delContext
contextToString :: Context -> IO String
contextToString c =
checkError c $ z3_context_to_string (unContext c) >>= peekCString
showContext :: Context -> IO String
showContext = contextToString
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"
mkStringSymbol :: Context -> String -> IO Symbol
mkStringSymbol ctx s =
withCString s $ \cs ->
checkError ctx $
Symbol <$> z3_mk_string_symbol (unContext ctx) cs
mkUninterpretedSort :: Context -> Symbol -> IO Sort
mkUninterpretedSort c sy = checkError c $
Sort <$> z3_mk_uninterpreted_sort (unContext c) (unSymbol sy)
mkBoolSort :: Context -> IO Sort
mkBoolSort c = checkError c $ Sort <$> z3_mk_bool_sort (unContext c)
mkIntSort :: Context -> IO Sort
mkIntSort c = checkError c $ Sort <$> z3_mk_int_sort (unContext c)
mkRealSort :: Context -> IO Sort
mkRealSort c = checkError c $ Sort <$> z3_mk_real_sort (unContext c)
mkBvSort :: Context -> Int -> IO Sort
mkBvSort c n = checkError c $ Sort <$> z3_mk_bv_sort (unContext c) (fromIntegral n)
mkArraySort :: Context -> Sort -> Sort -> IO Sort
mkArraySort c dom rng = checkError c $ Sort <$> z3_mk_array_sort (unContext c) (unSort dom) (unSort rng)
mkTupleSort :: Context
-> Symbol
-> [(Symbol, Sort)]
-> IO (Sort, FuncDecl, [FuncDecl])
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)
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)
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
mkConst :: Context -> Symbol -> Sort -> IO AST
mkConst c x s = checkError c $ AST <$> z3_mk_const (unContext c) (unSymbol x) (unSort s)
mkTrue :: Context -> IO AST
mkTrue c = checkError c $ AST <$> z3_mk_true (unContext c)
mkFalse :: Context -> IO AST
mkFalse c = checkError c $ AST <$> z3_mk_false (unContext c)
mkEq :: Context -> AST -> AST -> IO AST
mkEq c e1 e2 = checkError c $ AST <$> z3_mk_eq (unContext c) (unAST e1) (unAST e2)
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
mkNot :: Context -> AST -> IO AST
mkNot c e = checkError c $ AST <$> z3_mk_not (unContext c) (unAST e)
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)
mkIff :: Context -> AST -> AST -> IO AST
mkIff c p q = checkError c $ AST <$> z3_mk_iff (unContext c) (unAST p) (unAST q)
mkImplies :: Context -> AST -> AST -> IO AST
mkImplies c p q = checkError c $ AST <$> z3_mk_implies (unContext c) (unAST p) (unAST q)
mkXor :: Context -> AST -> AST -> IO AST
mkXor c p q = checkError c $ AST <$> z3_mk_xor (unContext c) (unAST p) (unAST q)
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
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
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
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
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
mkUnaryMinus :: Context -> AST -> IO AST
mkUnaryMinus c e = checkError c $ AST <$> z3_mk_unary_minus (unContext c) (unAST e)
mkDiv :: Context -> AST -> AST -> IO AST
mkDiv c e1 e2 = checkError c $ AST <$> z3_mk_div (unContext c) (unAST e1) (unAST e2)
mkMod :: Context -> AST -> AST -> IO AST
mkMod c e1 e2 = checkError c $ AST <$> z3_mk_mod (unContext c) (unAST e1) (unAST e2)
mkRem :: Context -> AST -> AST -> IO AST
mkRem c e1 e2 = checkError c $ AST <$> z3_mk_rem (unContext c) (unAST e1) (unAST e2)
mkLt :: Context -> AST -> AST -> IO AST
mkLt c e1 e2 = checkError c $ AST <$> z3_mk_lt (unContext c) (unAST e1) (unAST e2)
mkLe :: Context -> AST -> AST -> IO AST
mkLe c e1 e2 = checkError c $ AST <$> z3_mk_le (unContext c) (unAST e1) (unAST e2)
mkGt :: Context -> AST -> AST -> IO AST
mkGt c e1 e2 = checkError c $ AST <$> z3_mk_gt (unContext c) (unAST e1) (unAST e2)
mkGe :: Context -> AST -> AST -> IO AST
mkGe c e1 e2 = checkError c $ AST <$> z3_mk_ge (unContext c) (unAST e1) (unAST e2)
mkInt2Real :: Context -> AST -> IO AST
mkInt2Real c e = checkError c $ AST <$> z3_mk_int2real (unContext c) (unAST e)
mkReal2Int :: Context -> AST -> IO AST
mkReal2Int c e = checkError c $ AST <$> z3_mk_real2int (unContext c) (unAST e)
mkIsInt :: Context -> AST -> IO AST
mkIsInt c e = checkError c $ AST <$> z3_mk_is_int (unContext c) (unAST e)
mkBvnot :: Context -> AST -> IO AST
mkBvnot c e = checkError c $ AST <$> z3_mk_bvnot (unContext c) (unAST e)
mkBvredand :: Context -> AST -> IO AST
mkBvredand c e = checkError c $ AST <$> z3_mk_bvredand (unContext c) (unAST e)
mkBvredor :: Context -> AST -> IO AST
mkBvredor c e = checkError c $ AST <$> z3_mk_bvredor (unContext c) (unAST e)
mkBvand :: Context -> AST -> AST -> IO AST
mkBvand c e1 e2 = checkError c $ AST <$> z3_mk_bvand (unContext c) (unAST e1) (unAST e2)
mkBvor :: Context -> AST -> AST -> IO AST
mkBvor c e1 e2 = checkError c $ AST <$> z3_mk_bvor (unContext c) (unAST e1) (unAST e2)
mkBvxor :: Context -> AST -> AST -> IO AST
mkBvxor c e1 e2 = checkError c $ AST <$> z3_mk_bvxor (unContext c) (unAST e1) (unAST e2)
mkBvnand :: Context -> AST -> AST -> IO AST
mkBvnand c e1 e2 = checkError c $ AST <$> z3_mk_bvnand (unContext c) (unAST e1) (unAST e2)
mkBvnor :: Context -> AST -> AST -> IO AST
mkBvnor c e1 e2 = checkError c $ AST <$> z3_mk_bvnor (unContext c) (unAST e1) (unAST e2)
mkBvxnor :: Context -> AST -> AST -> IO AST
mkBvxnor c e1 e2 = checkError c $ AST <$> z3_mk_bvxnor (unContext c) (unAST e1) (unAST e2)
mkBvneg :: Context -> AST -> IO AST
mkBvneg c e = checkError c $ AST <$> z3_mk_bvneg (unContext c) (unAST e)
mkBvadd :: Context -> AST -> AST -> IO AST
mkBvadd c e1 e2 = checkError c $ AST <$> z3_mk_bvadd (unContext c) (unAST e1) (unAST e2)
mkBvsub :: Context -> AST -> AST -> IO AST
mkBvsub c e1 e2 = checkError c $ AST <$> z3_mk_bvsub (unContext c) (unAST e1) (unAST e2)
mkBvmul :: Context -> AST -> AST -> IO AST
mkBvmul c e1 e2 = checkError c $ AST <$> z3_mk_bvmul (unContext c) (unAST e1) (unAST e2)
mkBvudiv :: Context -> AST -> AST -> IO AST
mkBvudiv c e1 e2 = checkError c $ AST <$> z3_mk_bvudiv (unContext c) (unAST e1) (unAST e2)
mkBvsdiv :: Context -> AST -> AST -> IO AST
mkBvsdiv c e1 e2 = checkError c $ AST <$> z3_mk_bvsdiv (unContext c) (unAST e1) (unAST e2)
mkBvurem :: Context -> AST -> AST -> IO AST
mkBvurem c e1 e2 = checkError c $ AST <$> z3_mk_bvurem (unContext c) (unAST e1) (unAST e2)
mkBvsrem :: Context -> AST -> AST -> IO AST
mkBvsrem c e1 e2 = checkError c $ AST <$> z3_mk_bvsrem (unContext c) (unAST e1) (unAST e2)
mkBvsmod :: Context -> AST -> AST -> IO AST
mkBvsmod c e1 e2 = checkError c $ AST <$> z3_mk_bvsmod (unContext c) (unAST e1) (unAST e2)
mkBvult :: Context -> AST -> AST -> IO AST
mkBvult c e1 e2 = checkError c $ AST <$> z3_mk_bvult (unContext c) (unAST e1) (unAST e2)
mkBvslt :: Context -> AST -> AST -> IO AST
mkBvslt c e1 e2 = checkError c $ AST <$> z3_mk_bvslt (unContext c) (unAST e1) (unAST e2)
mkBvule :: Context -> AST -> AST -> IO AST
mkBvule c e1 e2 = checkError c $ AST <$> z3_mk_bvule (unContext c) (unAST e1) (unAST e2)
mkBvsle :: Context -> AST -> AST -> IO AST
mkBvsle c e1 e2 = checkError c $ AST <$> z3_mk_bvsle (unContext c) (unAST e1) (unAST e2)
mkBvuge :: Context -> AST -> AST -> IO AST
mkBvuge c e1 e2 = checkError c $ AST <$> z3_mk_bvuge (unContext c) (unAST e1) (unAST e2)
mkBvsge :: Context -> AST -> AST -> IO AST
mkBvsge c e1 e2 = checkError c $ AST <$> z3_mk_bvsge (unContext c) (unAST e1) (unAST e2)
mkBvugt :: Context -> AST -> AST -> IO AST
mkBvugt c e1 e2 = checkError c $ AST <$> z3_mk_bvugt (unContext c) (unAST e1) (unAST e2)
mkBvsgt :: Context -> AST -> AST -> IO AST
mkBvsgt c e1 e2 = checkError c $ AST <$> z3_mk_bvsgt (unContext c) (unAST e1) (unAST e2)
mkConcat :: Context -> AST -> AST -> IO AST
mkConcat c e1 e2 = checkError c $ AST <$> z3_mk_concat (unContext c) (unAST e1) (unAST e2)
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)
mkSignExt :: Context -> Int -> AST -> IO AST
mkSignExt c i e
= checkError c $ AST <$> z3_mk_sign_ext (unContext c) (fromIntegral i) (unAST e)
mkZeroExt :: Context -> Int -> AST -> IO AST
mkZeroExt c i e
= checkError c $ AST <$> z3_mk_zero_ext (unContext c) (fromIntegral i) (unAST e)
mkRepeat :: Context -> Int -> AST -> IO AST
mkRepeat c i e
= checkError c $ AST <$> z3_mk_repeat (unContext c) (fromIntegral i) (unAST e)
mkBvshl :: Context -> AST -> AST -> IO AST
mkBvshl c e1 e2 = checkError c $ AST <$> z3_mk_bvshl (unContext c) (unAST e1) (unAST e2)
mkBvlshr :: Context -> AST -> AST -> IO AST
mkBvlshr c e1 e2 = checkError c $ AST <$> z3_mk_bvlshr (unContext c) (unAST e1) (unAST e2)
mkBvashr :: Context -> AST -> AST -> IO AST
mkBvashr c e1 e2 = checkError c $ AST <$> z3_mk_bvashr (unContext c) (unAST e1) (unAST e2)
mkRotateLeft :: Context -> Int -> AST -> IO AST
mkRotateLeft c i e
= checkError c $ AST <$> z3_mk_rotate_left (unContext c) (fromIntegral i) (unAST e)
mkRotateRight :: Context -> Int -> AST -> IO AST
mkRotateRight c i e
= checkError c $ AST <$> z3_mk_rotate_right (unContext c) (fromIntegral i) (unAST e)
mkExtRotateLeft :: Context -> AST -> AST -> IO AST
mkExtRotateLeft c e1 e2
= checkError c $ AST <$> z3_mk_ext_rotate_left (unContext c) (unAST e1) (unAST e2)
mkExtRotateRight :: Context -> AST -> AST -> IO AST
mkExtRotateRight c e1 e2
= checkError c $ AST <$> z3_mk_ext_rotate_right (unContext c) (unAST e1) (unAST e2)
mkInt2bv :: Context -> Int -> AST -> IO AST
mkInt2bv c i e
= checkError c $ AST <$> z3_mk_int2bv (unContext c) (fromIntegral i) (unAST e)
mkBv2int :: Context -> AST -> Bool -> IO AST
mkBv2int c e is_signed
= checkError c $ AST <$> z3_mk_bv2int (unContext c) (unAST e) (unBool is_signed)
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)
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvaddNoUnderflow c e1 e2 =
checkError c $ AST <$> z3_mk_bvadd_no_underflow (unContext c) (unAST e1) (unAST e2)
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
mkBvsubNoOverflow c e1 e2 =
checkError c $ AST <$> z3_mk_bvsub_no_overflow (unContext c) (unAST e1) (unAST e2)
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvsubNoUnderflow c e1 e2 =
checkError c $ AST <$> z3_mk_bvsub_no_underflow (unContext c) (unAST e1) (unAST e2)
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
mkBvsdivNoOverflow c e1 e2 =
checkError c $ AST <$> z3_mk_bvsdiv_no_overflow (unContext c) (unAST e1) (unAST e2)
mkBvnegNoOverflow :: Context -> AST -> IO AST
mkBvnegNoOverflow c e =
checkError c $ AST <$> z3_mk_bvneg_no_overflow (unContext c) (unAST e)
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)
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvmulNoUnderflow c e1 e2 =
checkError c $ AST <$> z3_mk_bvmul_no_underflow (unContext c) (unAST e1) (unAST e2)
mkSelect :: Context -> AST -> AST -> IO AST
mkSelect c a1 a2 = checkError c $ AST <$> z3_mk_select (unContext c) (unAST a1) (unAST a2)
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)
mkConstArray :: Context -> Sort -> AST -> IO AST
mkConstArray c s a = checkError c $ AST <$> z3_mk_const_array (unContext c) (unSort s) (unAST a)
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'
mkArrayDefault :: Context -> AST -> IO AST
mkArrayDefault c a = checkError c $ AST <$> z3_mk_array_default (unContext c) (unAST a)
mkNumeral :: Context -> String -> Sort -> IO AST
mkNumeral c str s =
withCString str $ \cstr->
checkError c $ AST <$> z3_mk_numeral (unContext c) cstr (unSort s)
mkInt :: Integral a => Context -> a -> IO AST
mkInt c n = mkIntSort c >>= mkNumeral c n_str
where n_str = show $ toInteger n
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
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
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
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
mkInt_IntZ3 :: Context -> Int32 -> IO AST
mkInt_IntZ3 c n = mkIntSort c >>= mkIntZ3 c n
mkInt_UnsignedIntZ3 :: Context -> Word32 -> IO AST
mkInt_UnsignedIntZ3 c n = mkIntSort c >>= mkUnsignedIntZ3 c n
mkInt_Int64Z3 :: Context -> Int64 -> IO AST
mkInt_Int64Z3 c n = mkIntSort c >>= mkInt64Z3 c n
mkInt_UnsignedInt64Z3 :: Context -> Word64 -> IO AST
mkInt_UnsignedInt64Z3 c n = mkIntSort c >>= mkUnsignedInt64Z3 c n
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
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
mkReal_IntZ3 :: Context -> Int32 -> IO AST
mkReal_IntZ3 c n = mkRealSort c >>= mkIntZ3 c n
mkReal_UnsignedIntZ3 :: Context -> Word32 -> IO AST
mkReal_UnsignedIntZ3 c n = mkRealSort c >>= mkUnsignedIntZ3 c n
mkReal_Int64Z3 :: Context -> Int64 -> IO AST
mkReal_Int64Z3 c n = mkRealSort c >>= mkInt64Z3 c n
mkReal_UnsignedInt64Z3 :: Context -> Word64 -> IO AST
mkReal_UnsignedInt64Z3 c n = mkRealSort c >>= mkUnsignedInt64Z3 c n
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
getBvSortSize :: Context -> Sort -> IO Int
getBvSortSize c s =
checkError c $ fromIntegral <$> z3_get_bv_sort_size (unContext c) (unSort s)
getSort :: Context -> AST -> IO Sort
getSort c e = checkError c $ Sort <$> z3_get_sort (unContext c) (unAST e)
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"
getBool :: Context -> AST -> IO (Maybe Bool)
getBool c a = checkError c $
castLBool <$> z3_get_bool_value (unContext c) (unAST a)
getNumeralString :: Context -> AST -> IO String
getNumeralString c a = checkError c $ peekCString =<< z3_get_numeral_string ctxPtr (unAST a)
where ctxPtr = unContext c
getInt :: Context -> AST -> IO Integer
getInt c a = read <$> getNumeralString c a
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"
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
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
evalT c m = fmap T.sequence . T.mapM (eval c m)
data FuncModel = FuncModel
{ interpMap :: [([AST], AST)]
, interpElse :: AST
}
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)
evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
evalArray ctx model array =
do
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
getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
getAsArrayFuncDecl ctx a = checkError ctx $
FuncDecl <$> z3_get_as_array_func_decl (unContext ctx) (unAST a)
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..n1]
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..n1]
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
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
funcInterpGetNumEntries ctx fi = checkError ctx $ fromIntegral <$>
z3_func_interp_get_num_entries (unContext ctx) (unFuncInterp fi)
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
funcInterpGetEntry ctx fi i = checkError ctx $ FuncEntry <$>
z3_func_interp_get_entry (unContext ctx) (unFuncInterp fi) (fromIntegral i)
funcInterpGetElse :: Context -> FuncInterp -> IO AST
funcInterpGetElse ctx fi = checkError ctx $
AST <$> z3_func_interp_get_else (unContext ctx) (unFuncInterp fi)
funcInterpGetArity :: Context -> FuncInterp -> IO Int
funcInterpGetArity ctx fi = checkError ctx $
fromIntegral <$> z3_func_interp_get_arity (unContext ctx) (unFuncInterp fi)
funcEntryGetValue :: Context -> FuncEntry -> IO AST
funcEntryGetValue ctx entry = checkError ctx $
AST <$> z3_func_entry_get_value (unContext ctx) (unFuncEntry entry)
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
funcEntryGetNumArgs ctx entry = checkError ctx $ fromIntegral <$>
z3_func_entry_get_num_args (unContext ctx) (unFuncEntry entry)
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
funcEntryGetArg ctx entry i = checkError ctx $ AST <$>
z3_func_entry_get_arg (unContext ctx) (unFuncEntry entry) (fromIntegral i)
modelToString :: Context -> Model -> IO String
modelToString c m = checkError c $
z3_model_to_string (unContext c) (unModel m) >>= peekCString
showModel :: Context -> Model -> IO String
showModel = modelToString
push :: Context -> IO ()
push c = checkError c $ z3_push $ unContext c
pop :: Context -> Int -> IO ()
pop ctx cnt = checkError ctx $ z3_pop (unContext ctx) $ fromIntegral cnt
assertCnstr :: Context -> AST -> IO ()
assertCnstr ctx ast = checkError ctx $
z3_assert_cnstr (unContext ctx) (unAST ast)
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
delModel :: Context -> Model -> IO ()
delModel c m = checkError c $ z3_del_model (unContext c) (unModel m)
check :: Context -> IO Result
check ctx = checkError ctx $ toResult <$> z3_check (unContext ctx)
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
data Logic
= AUFLIA
| AUFLIRA
| AUFNIRA
| LRA
| QF_ABV
| QF_AUFBV
| QF_AUFLIA
| QF_AX
| QF_BV
| QF_IDL
| QF_LIA
| QF_LRA
| QF_NIA
| QF_NRA
| QF_RDL
| QF_UF
| QF_UFBV
| QF_UFIDL
| QF_UFLIA
| QF_UFLRA
| QF_UFNRA
| UFLRA
| UFNIA
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
data ASTPrintMode
= Z3_PRINT_SMTLIB_FULL
| Z3_PRINT_LOW_LEVEL
| Z3_PRINT_SMTLIB_COMPLIANT
| Z3_PRINT_SMTLIB2_COMPLIANT
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
astToString :: Context -> AST -> IO String
astToString ctx ast =
checkError ctx $ z3_ast_to_string (unContext ctx) (unAST ast) >>= peekCString
patternToString :: Context -> Pattern -> IO String
patternToString ctx pattern =
checkError ctx $ z3_pattern_to_string (unContext ctx) (unPattern pattern) >>= peekCString
sortToString :: Context -> Sort -> IO String
sortToString ctx sort =
checkError ctx $ z3_sort_to_string (unContext ctx) (unSort sort) >>= peekCString
funcDeclToString :: Context -> FuncDecl -> IO String
funcDeclToString ctx funcDecl =
checkError ctx $ z3_func_decl_to_string (unContext ctx) (unFuncDecl funcDecl) >>= peekCString
benchmarkToSMTLibString :: Context
-> String
-> String
-> String
-> String
-> [AST]
-> AST
-> 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
ptrToMaybe :: Ptr a -> Maybe (Ptr a)
ptrToMaybe ptr | ptr == nullPtr = Nothing
| otherwise = Just ptr