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
, mkForallConst
, mkExistsConst
, getBvSortSize
, getSort
, getBool
, getInt
, getReal
, toApp
, FuncModel (..)
, eval
, evalT
, evalFunc
, evalArray
, getFuncInterp
, isAsArray
, getAsArrayFuncDecl
, funcInterpGetNumEntries
, funcInterpGetEntry
, funcInterpGetElse
, funcInterpGetArity
, funcEntryGetValue
, funcEntryGetNumArgs
, funcEntryGetArg
, modelToString
, showModel
, assertCnstr
, check
, checkAndGetModel
, getModel
, delModel
, push
, pop
, mkParams
, paramsSetBool
, paramsSetUInt
, paramsSetDouble
, paramsSetSymbol
, paramsToString
, Logic(..)
, mkSolver
, mkSimpleSolver
, mkSolverForLogic
, solverSetParams
, solverPush
, solverPop
, solverReset
, solverGetNumScopes
, solverAssertCnstr
, solverAssertAndTrack
, solverCheck
, solverGetModel
, solverCheckAndGetModel
, solverGetReasonUnknown
, solverToString
, ASTPrintMode(..)
, setASTPrintMode
, astToString
, patternToString
, sortToString
, funcDeclToString
, benchmarkToSMTLibString
, Version(..)
, getVersion
, 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
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 :: ForeignPtr Z3_solver }
deriving Eq
data Result
= Sat
| Unsat
| Undef
deriving (Eq, Ord, Read, Show)
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 = liftFun0 z3_context_to_string
showContext :: Context -> IO String
showContext = contextToString
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"
mkStringSymbol :: Context -> String -> IO Symbol
mkStringSymbol = liftFun1 z3_mk_string_symbol
mkUninterpretedSort :: Context -> Symbol -> IO Sort
mkUninterpretedSort = liftFun1 z3_mk_uninterpreted_sort
mkBoolSort :: Context -> IO Sort
mkBoolSort = liftFun0 z3_mk_bool_sort
mkIntSort :: Context -> IO Sort
mkIntSort = liftFun0 z3_mk_int_sort
mkRealSort :: Context -> IO Sort
mkRealSort = liftFun0 z3_mk_real_sort
mkBvSort :: Context -> Int -> IO Sort
mkBvSort = liftFun1 z3_mk_bv_sort
mkArraySort :: Context -> Sort -> Sort -> IO Sort
mkArraySort = liftFun2 z3_mk_array_sort
mkTupleSort :: Context
-> Symbol
-> [(Symbol, Sort)]
-> IO (Sort, FuncDecl, [FuncDecl])
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
mkFuncDecl :: Context
-> Symbol
-> [Sort]
-> Sort
-> 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
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
mkConst :: Context -> Symbol -> Sort -> IO AST
mkConst = liftFun2 z3_mk_const
mkTrue :: Context -> IO AST
mkTrue = liftFun0 z3_mk_true
mkFalse :: Context -> IO AST
mkFalse = liftFun0 z3_mk_false
mkEq :: Context -> AST -> AST -> IO AST
mkEq = liftFun2 z3_mk_eq
mkDistinct :: Context -> [AST] -> IO AST
mkDistinct =
liftAstN "Z3.Base.mkDistinct: empty list of expressions" z3_mk_distinct
mkNot :: Context -> AST -> IO AST
mkNot = liftFun1 z3_mk_not
mkIte :: Context -> AST -> AST -> AST -> IO AST
mkIte = liftFun3 z3_mk_ite
mkIff :: Context -> AST -> AST -> IO AST
mkIff = liftFun2 z3_mk_iff
mkImplies :: Context -> AST -> AST -> IO AST
mkImplies = liftFun2 z3_mk_implies
mkXor :: Context -> AST -> AST -> IO AST
mkXor = liftFun2 z3_mk_xor
mkAnd :: Context -> [AST] -> IO AST
mkAnd = liftAstN "Z3.Base.mkAnd: empty list of expressions" z3_mk_and
mkOr :: Context -> [AST] -> IO AST
mkOr = liftAstN "Z3.Base.mkOr: empty list of expressions" z3_mk_or
mkAdd :: Context -> [AST] -> IO AST
mkAdd = liftAstN "Z3.Base.mkAdd: empty list of expressions" z3_mk_add
mkMul :: Context -> [AST] -> IO AST
mkMul = liftAstN "Z3.Base.mkMul: empty list of expressions" z3_mk_mul
mkSub :: Context -> [AST] -> IO AST
mkSub = liftAstN "Z3.Base.mkSub: empty list of expressions" z3_mk_sub
mkUnaryMinus :: Context -> AST -> IO AST
mkUnaryMinus = liftFun1 z3_mk_unary_minus
mkDiv :: Context -> AST -> AST -> IO AST
mkDiv = liftFun2 z3_mk_div
mkMod :: Context -> AST -> AST -> IO AST
mkMod = liftFun2 z3_mk_mod
mkRem :: Context -> AST -> AST -> IO AST
mkRem = liftFun2 z3_mk_rem
mkLt :: Context -> AST -> AST -> IO AST
mkLt = liftFun2 z3_mk_lt
mkLe :: Context -> AST -> AST -> IO AST
mkLe = liftFun2 z3_mk_le
mkGt :: Context -> AST -> AST -> IO AST
mkGt = liftFun2 z3_mk_gt
mkGe :: Context -> AST -> AST -> IO AST
mkGe = liftFun2 z3_mk_ge
mkInt2Real :: Context -> AST -> IO AST
mkInt2Real = liftFun1 z3_mk_int2real
mkReal2Int :: Context -> AST -> IO AST
mkReal2Int = liftFun1 z3_mk_real2int
mkIsInt :: Context -> AST -> IO AST
mkIsInt = liftFun1 z3_mk_is_int
mkBvnot :: Context -> AST -> IO AST
mkBvnot = liftFun1 z3_mk_bvnot
mkBvredand :: Context -> AST -> IO AST
mkBvredand = liftFun1 z3_mk_bvredand
mkBvredor :: Context -> AST -> IO AST
mkBvredor = liftFun1 z3_mk_bvredor
mkBvand :: Context -> AST -> AST -> IO AST
mkBvand = liftFun2 z3_mk_bvand
mkBvor :: Context -> AST -> AST -> IO AST
mkBvor = liftFun2 z3_mk_bvor
mkBvxor :: Context -> AST -> AST -> IO AST
mkBvxor = liftFun2 z3_mk_bvxor
mkBvnand :: Context -> AST -> AST -> IO AST
mkBvnand = liftFun2 z3_mk_bvnand
mkBvnor :: Context -> AST -> AST -> IO AST
mkBvnor = liftFun2 z3_mk_bvnor
mkBvxnor :: Context -> AST -> AST -> IO AST
mkBvxnor = liftFun2 z3_mk_bvxnor
mkBvneg :: Context -> AST -> IO AST
mkBvneg = liftFun1 z3_mk_bvneg
mkBvadd :: Context -> AST -> AST -> IO AST
mkBvadd = liftFun2 z3_mk_bvadd
mkBvsub :: Context -> AST -> AST -> IO AST
mkBvsub = liftFun2 z3_mk_bvsub
mkBvmul :: Context -> AST -> AST -> IO AST
mkBvmul = liftFun2 z3_mk_bvmul
mkBvudiv :: Context -> AST -> AST -> IO AST
mkBvudiv = liftFun2 z3_mk_bvudiv
mkBvsdiv :: Context -> AST -> AST -> IO AST
mkBvsdiv = liftFun2 z3_mk_bvsdiv
mkBvurem :: Context -> AST -> AST -> IO AST
mkBvurem = liftFun2 z3_mk_bvurem
mkBvsrem :: Context -> AST -> AST -> IO AST
mkBvsrem = liftFun2 z3_mk_bvsrem
mkBvsmod :: Context -> AST -> AST -> IO AST
mkBvsmod = liftFun2 z3_mk_bvsmod
mkBvult :: Context -> AST -> AST -> IO AST
mkBvult = liftFun2 z3_mk_bvult
mkBvslt :: Context -> AST -> AST -> IO AST
mkBvslt = liftFun2 z3_mk_bvslt
mkBvule :: Context -> AST -> AST -> IO AST
mkBvule = liftFun2 z3_mk_bvule
mkBvsle :: Context -> AST -> AST -> IO AST
mkBvsle = liftFun2 z3_mk_bvsle
mkBvuge :: Context -> AST -> AST -> IO AST
mkBvuge = liftFun2 z3_mk_bvuge
mkBvsge :: Context -> AST -> AST -> IO AST
mkBvsge = liftFun2 z3_mk_bvsge
mkBvugt :: Context -> AST -> AST -> IO AST
mkBvugt = liftFun2 z3_mk_bvugt
mkBvsgt :: Context -> AST -> AST -> IO AST
mkBvsgt = liftFun2 z3_mk_bvsgt
mkConcat :: Context -> AST -> AST -> IO AST
mkConcat = liftFun2 z3_mk_concat
mkExtract :: Context -> Int -> Int -> AST -> IO AST
mkExtract = liftFun3 z3_mk_extract
mkSignExt :: Context -> Int -> AST -> IO AST
mkSignExt = liftFun2 z3_mk_sign_ext
mkZeroExt :: Context -> Int -> AST -> IO AST
mkZeroExt = liftFun2 z3_mk_zero_ext
mkRepeat :: Context -> Int -> AST -> IO AST
mkRepeat = liftFun2 z3_mk_repeat
mkBvshl :: Context -> AST -> AST -> IO AST
mkBvshl = liftFun2 z3_mk_bvshl
mkBvlshr :: Context -> AST -> AST -> IO AST
mkBvlshr = liftFun2 z3_mk_bvlshr
mkBvashr :: Context -> AST -> AST -> IO AST
mkBvashr = liftFun2 z3_mk_bvashr
mkRotateLeft :: Context -> Int -> AST -> IO AST
mkRotateLeft = liftFun2 z3_mk_rotate_left
mkRotateRight :: Context -> Int -> AST -> IO AST
mkRotateRight = liftFun2 z3_mk_rotate_right
mkExtRotateLeft :: Context -> AST -> AST -> IO AST
mkExtRotateLeft = liftFun2 z3_mk_ext_rotate_left
mkExtRotateRight :: Context -> AST -> AST -> IO AST
mkExtRotateRight = liftFun2 z3_mk_ext_rotate_right
mkInt2bv :: Context -> Int -> AST -> IO AST
mkInt2bv = liftFun2 z3_mk_int2bv
mkBv2int :: Context -> AST -> Bool -> IO AST
mkBv2int = liftFun2 z3_mk_bv2int
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
mkBvaddNoOverflow = liftFun3 z3_mk_bvadd_no_overflow
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvaddNoUnderflow = liftFun2 z3_mk_bvadd_no_underflow
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
mkBvsubNoOverflow = liftFun2 z3_mk_bvsub_no_overflow
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvsubNoUnderflow = liftFun2 z3_mk_bvsub_no_underflow
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
mkBvsdivNoOverflow = liftFun2 z3_mk_bvsdiv_no_overflow
mkBvnegNoOverflow :: Context -> AST -> IO AST
mkBvnegNoOverflow = liftFun1 z3_mk_bvneg_no_overflow
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
mkBvmulNoOverflow = liftFun3 z3_mk_bvmul_no_overflow
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvmulNoUnderflow = liftFun2 z3_mk_bvmul_no_underflow
mkSelect :: Context
-> AST
-> AST
-> IO AST
mkSelect = liftFun2 z3_mk_select
mkStore :: Context
-> AST
-> AST
-> AST
-> IO AST
mkStore = liftFun3 z3_mk_store
mkConstArray :: Context
-> Sort
-> AST
-> IO AST
mkConstArray = liftFun2 z3_mk_const_array
mkMap :: Context
-> FuncDecl
-> [AST]
-> IO AST
mkMap ctx fun args = marshal z3_mk_map ctx $ \f ->
h2c fun $ \funPtr ->
marshalArrayLen args $ \argsNum argsArr ->
f funPtr argsNum argsArr
mkArrayDefault :: Context
-> AST
-> IO AST
mkArrayDefault = liftFun1 z3_mk_array_default
mkNumeral :: Context -> String -> Sort -> IO AST
mkNumeral = liftFun2 z3_mk_numeral
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 = marshal z3_mk_int c $ h2c s . withIntegral n
mkUnsignedIntZ3 :: Context -> Word32 -> Sort -> IO AST
mkUnsignedIntZ3 c n s = marshal z3_mk_unsigned_int c $
h2c s . withIntegral n
mkInt64Z3 :: Context -> Int64 -> Sort -> IO AST
mkInt64Z3 = liftFun2 z3_mk_int64
mkUnsignedInt64Z3 :: Context -> Word64 -> Sort -> IO AST
mkUnsignedInt64Z3 = liftFun2 z3_mk_unsigned_int64
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 $ c2h c =<< 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 = marshal z3_mk_pattern c $ marshalArrayLen es
mkBound :: Context
-> Int
-> 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)
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
mkForall :: Context
-> [Pattern]
-> [Symbol]
-> [Sort]
-> AST
-> IO AST
mkForall = marshalMkQ z3_mk_forall
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
mkForallConst :: Context
-> [Pattern]
-> [App]
-> AST
-> IO AST
mkForallConst = marshalMkQConst z3_mk_forall_const
mkExistsConst :: Context
-> [Pattern]
-> [App]
-> AST
-> IO AST
mkExistsConst = marshalMkQConst z3_mk_exists_const
getBvSortSize :: Context -> Sort -> IO Int
getBvSortSize = liftFun1 z3_get_bv_sort_size
getSort :: Context -> AST -> IO Sort
getSort = liftFun1 z3_get_sort
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 = liftFun1 z3_get_numeral_string
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"
toApp :: Context -> AST -> IO App
toApp = liftFun1 z3_to_app
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 = liftFun1 z3_get_as_array_func_decl
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..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 ctx m fd = marshal z3_model_get_func_interp ctx $ \f ->
h2c m $ \mPtr ->
h2c fd $ \fdPtr ->
f mPtr fdPtr
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
funcInterpGetNumEntries = liftFun1 z3_func_interp_get_num_entries
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
funcInterpGetEntry = liftFun2 z3_func_interp_get_entry
funcInterpGetElse :: Context -> FuncInterp -> IO AST
funcInterpGetElse = liftFun1 z3_func_interp_get_else
funcInterpGetArity :: Context -> FuncInterp -> IO Int
funcInterpGetArity = liftFun1 z3_func_interp_get_arity
funcEntryGetValue :: Context -> FuncEntry -> IO AST
funcEntryGetValue = liftFun1 z3_func_entry_get_value
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
funcEntryGetNumArgs = liftFun1 z3_func_entry_get_num_args
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
funcEntryGetArg = liftFun2 z3_func_entry_get_arg
modelToString :: Context -> Model -> IO String
modelToString = liftFun1 z3_model_to_string
showModel :: Context -> Model -> IO String
showModel = modelToString
push :: Context -> IO ()
push = liftFun0 z3_push
pop :: Context -> Int -> IO ()
pop = liftFun1 z3_pop
assertCnstr :: Context -> AST -> IO ()
assertCnstr = liftFun1 z3_assert_cnstr
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
checkAndGetModel :: Context -> IO (Result, Maybe Model)
checkAndGetModel = getModel
delModel :: Context -> Model -> IO ()
delModel = liftFun1 z3_del_model
check :: Context -> IO Result
check ctx = checkError ctx $ toResult <$> z3_check (unContext ctx)
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
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"
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
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
solverCheck :: Context -> Solver -> IO Result
solverCheck ctx solver = marshal z3_solver_check ctx $ withSolverPtr solver
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
solverToString :: Context -> Solver -> IO String
solverToString = liftFun1 z3_solver_to_string
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 = liftFun1 z3_ast_to_string
patternToString :: Context -> Pattern -> IO String
patternToString = liftFun1 z3_pattern_to_string
sortToString :: Context -> Sort -> IO String
sortToString = liftFun1 z3_sort_to_string
funcDeclToString :: Context -> FuncDecl -> IO String
funcDeclToString = liftFun1 z3_func_decl_to_string
benchmarkToSMTLibString :: Context
-> String
-> String
-> String
-> String
-> [AST]
-> AST
-> 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
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
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
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
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
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)
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
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
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
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
ptrToMaybe :: Ptr a -> Maybe (Ptr a)
ptrToMaybe ptr | ptr == nullPtr = Nothing
| otherwise = Just ptr