module Z3.Base (
Config
, Context
, Symbol
, AST
, Sort
, FuncDecl
, App
, Pattern
, Constructor
, Model
, FuncInterp
, FuncEntry
, Params
, Solver
, SortKind(..)
, ASTKind(..)
, Tactic
, ApplyResult
, Goal
, Result(..)
, mkConfig
, delConfig
, setParamValue
, withConfig
, mkContext
, withContext
, mkParams
, paramsSetBool
, paramsSetUInt
, paramsSetDouble
, paramsSetSymbol
, paramsToString
, mkIntSymbol
, mkStringSymbol
, mkUninterpretedSort
, mkBoolSort
, mkIntSort
, mkRealSort
, mkBvSort
, mkFiniteDomainSort
, mkArraySort
, mkTupleSort
, mkConstructor
, mkDatatype
, mkDatatypes
, mkSetSort
, mkFuncDecl
, mkApp
, mkConst
, mkFreshFuncDecl
, mkFreshConst
, mkVar
, mkBoolVar
, mkRealVar
, mkIntVar
, mkBvVar
, mkFreshVar
, mkFreshBoolVar
, mkFreshRealVar
, mkFreshIntVar
, mkFreshBvVar
, mkTrue
, mkFalse
, mkEq
, mkNot
, mkIte
, mkIff
, mkImplies
, mkXor
, mkAnd
, mkOr
, mkDistinct
, mkDistinct1
, mkBool
, mkAdd
, mkMul
, mkSub
, mkSub1
, 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
, mkEmptySet
, mkFullSet
, mkSetAdd
, mkSetDel
, mkSetUnion
, mkSetIntersect
, mkSetDifference
, mkSetComplement
, mkSetMember
, mkSetSubset
, mkNumeral
, mkReal
, mkInt
, mkUnsignedInt
, mkInt64
, mkUnsignedInt64
, mkIntegral
, mkRational
, mkFixed
, mkRealNum
, mkInteger
, mkIntNum
, mkBitvector
, mkBvNum
, mkPattern
, mkBound
, mkForall
, mkExists
, mkForallConst
, mkExistsConst
, getSymbolString
, getSortKind
, getBvSortSize
, getDatatypeSortConstructors
, getDatatypeSortRecognizers
, getDatatypeSortConstructorAccessors
, getDeclName
, getArity
, getDomain
, getRange
, appToAst
, getAppDecl
, getAppNumArgs
, getAppArg
, getAppArgs
, getSort
, getArraySortDomain
, getArraySortRange
, getBoolValue
, getAstKind
, isApp
, toApp
, getNumeralString
, simplify
, simplifyEx
, getIndexValue
, isQuantifierForall
, isQuantifierExists
, getQuantifierWeight
, getQuantifierNumPatterns
, getQuantifierPatternAST
, getQuantifierPatterns
, getQuantifierNumNoPatterns
, getQuantifierNoPatternAST
, getQuantifierNoPatterns
, getQuantifierNumBound
, getQuantifierBoundName
, getQuantifierBoundSort
, getQuantifierBoundVars
, getQuantifierBody
, getBool
, getInt
, getReal
, getBv
, substituteVars
, modelEval
, evalArray
, getConstInterp
, getFuncInterp
, hasInterp
, numConsts
, numFuncs
, getConstDecl
, getFuncDecl
, getConsts
, getFuncs
, isAsArray
, addFuncInterp
, addConstInterp
, getAsArrayFuncDecl
, funcInterpGetNumEntries
, funcInterpGetEntry
, funcInterpGetElse
, funcInterpGetArity
, funcEntryGetValue
, funcEntryGetNumArgs
, funcEntryGetArg
, modelToString
, showModel
, EvalAst
, eval
, evalBool
, evalInt
, evalReal
, evalBv
, mapEval
, evalT
, FuncModel (..)
, evalFunc
, mkTactic
, andThenTactic
, orElseTactic
, skipTactic
, tryForTactic
, mkQuantifierEliminationTactic
, mkAndInverterGraphTactic
, applyTactic
, getApplyResultNumSubgoals
, getApplyResultSubgoal
, getApplyResultSubgoals
, mkGoal
, goalAssert
, getGoalSize
, getGoalFormula
, getGoalFormulas
, ASTPrintMode(..)
, setASTPrintMode
, astToString
, patternToString
, sortToString
, funcDeclToString
, benchmarkToSMTLibString
, parseSMTLib2String
, parseSMTLib2File
, Z3Error(..)
, Z3ErrorCode(..)
, Version(..)
, getVersion
, Fixedpoint (..)
, mkFixedpoint
, fixedpointPush
, fixedpointPop
, fixedpointAddRule
, fixedpointSetParams
, fixedpointRegisterRelation
, fixedpointQueryRelations
, fixedpointGetAnswer
, fixedpointGetAssertions
, Logic(..)
, mkSolver
, mkSimpleSolver
, mkSolverForLogic
, solverGetHelp
, solverSetParams
, solverPush
, solverPop
, solverReset
, solverGetNumScopes
, solverAssertCnstr
, solverAssertAndTrack
, solverCheck
, solverCheckAssumptions
, solverGetModel
, solverGetUnsatCore
, solverGetReasonUnknown
, solverToString
, solverCheckAndGetModel
) where
import Z3.Base.C
import Control.Applicative ( (<$>), (<*>), (<*), pure )
import Control.Exception ( Exception, bracket, throw )
import Control.Monad ( join, when, forM )
import Data.Fixed ( Fixed, HasResolution )
import Data.Foldable ( Foldable (..) )
import Data.Int
import Data.IORef ( IORef, newIORef, atomicModifyIORef' )
import Data.List.NonEmpty (NonEmpty (..), nonEmpty)
import Data.Maybe ( fromJust )
import Data.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
data Context =
Context {
unContext :: ForeignPtr Z3_context
, refCount :: !(IORef Word)
}
deriving Eq
newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol }
deriving (Eq, Ord, Show, Storable)
newtype AST = AST { unAST :: ForeignPtr Z3_ast }
deriving (Eq, Ord, Show, Typeable)
newtype Sort = Sort { unSort :: ForeignPtr Z3_sort }
deriving (Eq, Ord, Show)
newtype FuncDecl = FuncDecl { unFuncDecl :: ForeignPtr Z3_func_decl }
deriving (Eq, Ord, Show, Typeable)
newtype App = App { unApp :: ForeignPtr Z3_app }
deriving (Eq, Ord, Show)
newtype Pattern = Pattern { unPattern :: ForeignPtr Z3_pattern }
deriving (Eq, Ord, Show)
newtype Constructor = Constructor { unConstructor :: ForeignPtr Z3_constructor }
deriving (Eq, Ord, Show)
newtype ConstructorList = ConstructorList { unConstructorList :: ForeignPtr Z3_constructor_list }
deriving (Eq, Ord, Show)
newtype Model = Model { unModel :: ForeignPtr Z3_model }
deriving Eq
newtype FuncInterp = FuncInterp { unFuncInterp :: ForeignPtr Z3_func_interp }
deriving Eq
newtype FuncEntry = FuncEntry { unFuncEntry :: ForeignPtr Z3_func_entry }
deriving Eq
newtype Tactic = Tactic { unTactic :: ForeignPtr Z3_tactic }
deriving Eq
newtype Goal = Goal { unGoal :: ForeignPtr Z3_goal }
deriving Eq
newtype ApplyResult = ApplyResult { unApplyResult :: ForeignPtr Z3_apply_result }
deriving Eq
newtype Params = Params { unParams :: ForeignPtr Z3_params }
deriving Eq
newtype Solver = Solver { unSolver :: ForeignPtr Z3_solver }
deriving Eq
data Result
= Sat
| Unsat
| Undef
deriving (Eq, Ord, Read, Show)
data SortKind
= Z3_UNINTERPRETED_SORT
| Z3_BOOL_SORT
| Z3_INT_SORT
| Z3_REAL_SORT
| Z3_BV_SORT
| Z3_ARRAY_SORT
| Z3_DATATYPE_SORT
| Z3_RELATION_SORT
| Z3_FINITE_DOMAIN_SORT
| Z3_FLOATING_POINT_SORT
| Z3_ROUNDING_MODE_SORT
| Z3_UNKNOWN_SORT
deriving (Eq, Show)
data ASTKind
= Z3_NUMERAL_AST
| Z3_APP_AST
| Z3_VAR_AST
| Z3_QUANTIFIER_AST
| Z3_SORT_AST
| Z3_FUNC_DECL_AST
| Z3_UNKNOWN_AST
deriving (Eq, Show)
mkConfig :: IO Config
mkConfig = Config <$> z3_mk_config
delConfig :: Config -> IO ()
delConfig = z3_del_config . unConfig
setParamValue :: Config -> String -> String -> IO ()
setParamValue cfg s1 s2 =
withCString s1 $ \cs1 ->
withCString s2 $ \cs2 ->
z3_set_param_value (unConfig cfg) cs1 cs2
withConfig :: (Config -> IO a) -> IO a
withConfig = bracket mkConfig delConfig
mkContextWith :: (Ptr Z3_config -> IO (Ptr Z3_context)) -> Config -> IO Context
mkContextWith mkCtx cfg = do
ctxPtr <- mkCtx (unConfig cfg)
z3_set_error_handler ctxPtr nullFunPtr
count <- newIORef 1
Context <$> newForeignPtr ctxPtr (contextDecRef ctxPtr count)
<*> pure count
mkContext :: Config -> IO Context
mkContext = mkContextWith z3_mk_context_rc
contextIncRef :: Context -> IO ()
contextIncRef ctx = atomicModifyIORef' (refCount ctx) $ \n ->
(n+1, ())
contextDecRef :: Ptr Z3_context -> IORef Word -> IO ()
contextDecRef ctxPtr count = join $ atomicModifyIORef' count $ \n ->
if n > 1
then (n1, return ())
else ( 0, z3_del_context ctxPtr)
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 -> Word -> 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
mkIntSymbol :: Integral int => Context -> int -> IO Symbol
mkIntSymbol c i
| 0 <= i && i <= 2^(30::Int)1
= liftFun1 z3_mk_int_symbol c 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 :: Integral int => Context -> int -> IO Sort
mkBvSort c i
| i >= 0 = liftFun1 z3_mk_bv_sort c i
| otherwise = error "Z3.Base.mkBvSort: negative size"
mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort
mkFiniteDomainSort = liftFun2 z3_mk_finite_domain_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 = withContextError c $ \cPtr ->
h2c sym $ \symPtr ->
marshalArrayLen syms $ \ n symsPtr ->
marshalArray sorts $ \ sortsPtr ->
alloca $ \ outConstrPtr ->
allocaArray n $ \ outProjsPtr -> do
srtPtr <- checkError cPtr $ z3_mk_tuple_sort cPtr symPtr
(fromIntegral n) symsPtr sortsPtr
outConstrPtr outProjsPtr
outConstr <- peek outConstrPtr
outProjs <- peekArray n outProjsPtr
sort <- c2h c srtPtr
constrFd <- c2h c outConstr
projsFds <- mapM (c2h c) outProjs
return (sort, constrFd, projsFds)
where (syms, sorts) = unzip symSorts
mkConstructor :: Context
-> Symbol
-> Symbol
-> [(Symbol, Maybe Sort, Int)]
-> IO Constructor
mkConstructor c sym recog symSortsRefs =
withContextError c $ \cPtr ->
h2c sym $ \symPtr ->
h2c recog $ \recogPtr ->
marshalArrayLen syms $ \ n symsPtr ->
marshalArray maybeSorts $ \ sortsPtr ->
marshalArray (map toInteger refs) $ \ refsPtr -> do
constructor <- checkError cPtr $ z3_mk_constructor
cPtr symPtr recogPtr n symsPtr sortsPtr refsPtr
c2h c constructor
where (syms, maybeSorts, refs) = unzip3 symSortsRefs
mkDatatype :: Context
-> Symbol
-> [Constructor]
-> IO Sort
mkDatatype c sym consList = marshalArrayLen consList $ \ n consPtrs -> do
toHsCheckError c $ \cPtr -> z3_mk_datatype cPtr (unSymbol sym) n consPtrs
mkConstructorList :: Context
-> [Constructor]
-> IO ConstructorList
mkConstructorList c consList = marshalArrayLen consList $ \ n consPtrs -> do
toHsCheckError c $ \cPtr -> z3_mk_constructor_list cPtr n consPtrs
mkDatatypes :: Context
-> [Symbol]
-> [[Constructor]]
-> IO ([Sort])
mkDatatypes c syms consLists =
if length consLists == n then do
consLists' <- mapM (mkConstructorList c) consLists
withContextError c $ \cPtr ->
marshalArrayLen syms $ \ symLen symsPtr ->
marshalArray consLists' $ \ consPtr ->
allocaArray n $ \ sortsPtr -> do
z3_mk_datatypes cPtr symLen symsPtr sortsPtr consPtr
peekArrayToHs c n sortsPtr
else
error "Z3.Base.mkDatatypes: lists of different length"
where n = length syms
mkSetSort :: Context -> Sort -> IO Sort
mkSetSort = liftFun1 z3_mk_set_sort
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
mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl
mkFreshFuncDecl ctx str dom rng =
withCString str $ \cstr ->
marshal z3_mk_fresh_func_decl ctx $ \f ->
marshalArrayLen dom $ \domNum domArr ->
h2c rng $ \ptrRange ->
f cstr domNum domArr ptrRange
mkFreshConst :: Context
-> String
-> Sort
-> IO AST
mkFreshConst = liftFun2 z3_mk_fresh_const
mkVar :: Context -> Symbol -> Sort -> IO AST
mkVar = mkConst
mkBoolVar :: Context -> Symbol -> IO AST
mkBoolVar ctx sym = mkVar ctx sym =<< mkBoolSort ctx
mkRealVar :: Context -> Symbol -> IO AST
mkRealVar ctx sym = mkVar ctx sym =<< mkRealSort ctx
mkIntVar :: Context -> Symbol -> IO AST
mkIntVar ctx sym = mkVar ctx sym =<< mkIntSort ctx
mkBvVar :: Context -> Symbol
-> Int
-> IO AST
mkBvVar ctx sym sz = mkVar ctx sym =<< mkBvSort ctx sz
mkFreshVar :: Context -> String -> Sort -> IO AST
mkFreshVar = mkFreshConst
mkFreshBoolVar :: Context -> String -> IO AST
mkFreshBoolVar ctx str = mkFreshVar ctx str =<< mkBoolSort ctx
mkFreshRealVar :: Context -> String -> IO AST
mkFreshRealVar ctx str = mkFreshVar ctx str =<< mkRealSort ctx
mkFreshIntVar :: Context -> String -> IO AST
mkFreshIntVar ctx str = mkFreshVar ctx str =<< mkIntSort ctx
mkFreshBvVar :: Context -> String
-> Int
-> IO AST
mkFreshBvVar ctx str sz = mkFreshVar ctx str =<< mkBvSort ctx sz
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_err "Z3.Base.mkDistinct: empty list of expressions" z3_mk_distinct
mkDistinct1 :: Context -> NonEmpty AST -> IO AST
mkDistinct1 = liftAstN1 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_mk_true z3_mk_and
mkOr :: Context -> [AST] -> IO AST
mkOr = liftAstN z3_mk_false z3_mk_or
mkBool :: Context -> Bool -> IO AST
mkBool ctx False = mkFalse ctx
mkBool ctx True = mkTrue ctx
mkAdd :: Context -> [AST] -> IO AST
mkAdd ctx = maybe (mkInteger ctx 0) (liftAstN1 z3_mk_add ctx) . nonEmpty
mkMul :: Context -> [AST] -> IO AST
mkMul ctx = maybe (mkInteger ctx 1) (liftAstN1 z3_mk_mul ctx) . nonEmpty
mkSub :: Context -> [AST] -> IO AST
mkSub = liftAstN_err "Z3.Base.mkSub: empty list of expressions" z3_mk_sub
mkSub1 :: Context -> NonEmpty AST -> IO AST
mkSub1 = liftAstN1 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
mkEmptySet :: Context
-> Sort
-> IO AST
mkEmptySet = liftFun1 z3_mk_empty_set
mkFullSet :: Context
-> Sort
-> IO AST
mkFullSet = liftFun1 z3_mk_full_set
mkSetAdd :: Context
-> AST
-> AST
-> IO AST
mkSetAdd = liftFun2 z3_mk_set_add
mkSetDel :: Context
-> AST
-> AST
-> IO AST
mkSetDel = liftFun2 z3_mk_set_del
mkSetUnion :: Context -> [AST] -> IO AST
mkSetUnion ctx args = marshal z3_mk_set_union ctx $ \f ->
marshalArrayLen args $ \argsNum argsArr ->
f argsNum argsArr
mkSetIntersect :: Context -> [AST] -> IO AST
mkSetIntersect ctx args = marshal z3_mk_set_intersect ctx $ \f ->
marshalArrayLen args $ \argsNum argsArr ->
f argsNum argsArr
mkSetDifference :: Context
-> AST
-> AST
-> IO AST
mkSetDifference = liftFun2 z3_mk_set_difference
mkSetComplement :: Context
-> AST
-> IO AST
mkSetComplement = liftFun1 z3_mk_set_complement
mkSetMember :: Context
-> AST
-> AST
-> IO AST
mkSetMember = liftFun2 z3_mk_set_member
mkSetSubset :: Context
-> AST
-> AST
-> IO AST
mkSetSubset = liftFun2 z3_mk_set_subset
mkNumeral :: Context -> String -> Sort -> IO AST
mkNumeral = liftFun2 z3_mk_numeral
mkReal :: Context -> Int
-> Int
-> IO AST
mkReal ctx num den
| den /= 0 = liftFun2 z3_mk_real ctx num den
| otherwise = error "Z3.Base.mkReal: zero denominator"
mkInt :: Context -> Int -> Sort -> IO AST
mkInt = liftFun2 z3_mk_int
mkUnsignedInt :: Context -> Word -> Sort -> IO AST
mkUnsignedInt = liftFun2 z3_mk_unsigned_int
mkInt64 :: Context -> Int64 -> Sort -> IO AST
mkInt64 = liftFun2 z3_mk_int64
mkUnsignedInt64 :: Context -> Word64 -> Sort -> IO AST
mkUnsignedInt64 = liftFun2 z3_mk_unsigned_int64
mkIntegral :: Integral a => Context -> a -> Sort -> IO AST
mkIntegral c n s = mkNumeral c n_str s
where n_str = show $ toInteger n
mkRational :: Context -> Rational -> IO AST
mkRational = mkRealNum
mkFixed :: HasResolution a => Context -> Fixed a -> IO AST
mkFixed ctx = mkRational ctx . toRational
mkRealNum :: Real r => Context -> r -> IO AST
mkRealNum c n = mkNumeral c n_str =<< mkRealSort c
where r = toRational n
r_n = toInteger $ numerator r
r_d = toInteger $ denominator r
n_str = show r_n ++ " / " ++ show r_d
mkInteger :: Context -> Integer -> IO AST
mkInteger = mkIntNum
mkIntNum :: Integral a => Context -> a -> IO AST
mkIntNum ctx n = mkIntegral ctx n =<< mkIntSort ctx
mkBitvector :: Context -> Int
-> Integer
-> IO AST
mkBitvector = mkBvNum
mkBvNum :: Integral i => Context -> Int
-> i
-> IO AST
mkBvNum ctx s n = mkIntegral ctx n =<< mkBvSort ctx s
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
getSymbolString :: Context -> Symbol -> IO String
getSymbolString = liftFun1 z3_get_symbol_string
getSortKind :: Context -> Sort -> IO SortKind
getSortKind ctx sort = toSortKind <$> liftFun1 z3_get_sort_kind ctx sort
where toSortKind :: Z3_sort_kind -> SortKind
toSortKind k
| k == z3_uninterpreted_sort = Z3_UNINTERPRETED_SORT
| k == z3_bool_sort = Z3_BOOL_SORT
| k == z3_int_sort = Z3_INT_SORT
| k == z3_real_sort = Z3_REAL_SORT
| k == z3_bv_sort = Z3_BV_SORT
| k == z3_array_sort = Z3_ARRAY_SORT
| k == z3_datatype_sort = Z3_DATATYPE_SORT
| k == z3_relation_sort = Z3_RELATION_SORT
| k == z3_finite_domain_sort = Z3_FINITE_DOMAIN_SORT
| k == z3_floating_point_sort = Z3_FLOATING_POINT_SORT
| k == z3_rounding_mode_sort = Z3_ROUNDING_MODE_SORT
| k == z3_unknown_sort = Z3_UNKNOWN_SORT
| otherwise =
error "Z3.Base.getSortKind: unknown `Z3_sort_kind'"
getBvSortSize :: Context -> Sort -> IO Int
getBvSortSize = liftFun1 z3_get_bv_sort_size
getArraySortDomain :: Context -> Sort -> IO Sort
getArraySortDomain = liftFun1 z3_get_array_sort_domain
getArraySortRange :: Context -> Sort -> IO Sort
getArraySortRange = liftFun1 z3_get_array_sort_range
getDatatypeSortConstructors :: Context
-> Sort
-> IO [FuncDecl]
getDatatypeSortConstructors c dtSort =
withContextError c $ \cPtr ->
h2c dtSort $ \dtSortPtr -> do
numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr
T.mapM (getConstructor dtSortPtr) [0..(numCons1)]
where
getConstructor dtSortPtr idx =
toHsCheckError c $ \cPtr -> z3_get_datatype_sort_constructor cPtr dtSortPtr idx
getDatatypeSortRecognizers :: Context
-> Sort
-> IO [FuncDecl]
getDatatypeSortRecognizers c dtSort =
withContextError c $ \cPtr ->
h2c dtSort $ \dtSortPtr -> do
numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr
T.mapM (getRecognizer dtSortPtr) [0..(numCons1)]
where
getRecognizer dtSortPtr idx =
toHsCheckError c $ \cPtr -> z3_get_datatype_sort_recognizer cPtr dtSortPtr idx
getDatatypeSortConstructorAccessors :: Context
-> Sort
-> IO [[FuncDecl]]
getDatatypeSortConstructorAccessors c dtSort =
withContextError c $ \cPtr ->
h2c dtSort $ \dtSortPtr -> do
numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr
T.mapM (getAccessors dtSortPtr) [0..(numCons1)]
where
getConstructor dtSortPtr idx_c =
withContext c $ \cPtr -> z3_get_datatype_sort_constructor cPtr dtSortPtr idx_c
getAccessors dtSortPtr idx_c = do
consPtr <- getConstructor dtSortPtr idx_c
numAs <- toHsCheckError c $ \cPtr -> z3_get_arity cPtr consPtr
if numAs > 0
then T.mapM (\idx_a -> getAccessors' dtSortPtr idx_c idx_a) [0..(numAs 1)]
else return []
getAccessors' dtSortPtr idx_c idx_a =
toHsCheckError c $ \cPtr -> z3_get_datatype_sort_constructor_accessor cPtr dtSortPtr idx_c idx_a
getDeclName :: Context -> FuncDecl -> IO Symbol
getDeclName c decl = h2c decl $ \declPtr ->
Symbol <$> withContextError c (\cPtr -> z3_get_decl_name cPtr declPtr)
getArity :: Context -> FuncDecl -> IO Int
getArity = liftFun1 z3_get_arity
getDomain :: Context
-> FuncDecl
-> Int
-> IO Sort
getDomain = liftFun2 z3_get_domain
getRange :: Context -> FuncDecl -> IO Sort
getRange = liftFun1 z3_get_range
appToAst :: Context -> App -> IO AST
appToAst = liftFun1 z3_app_to_ast
getAppDecl :: Context -> App -> IO FuncDecl
getAppDecl = liftFun1 z3_get_app_decl
getAppNumArgs :: Context -> App -> IO Int
getAppNumArgs = liftFun1 z3_get_app_num_args
getAppArg :: Context -> App -> Int -> IO AST
getAppArg = liftFun2 z3_get_app_arg
getAppArgs :: Context -> App -> IO [AST]
getAppArgs ctx a = do
n <- getAppNumArgs ctx a
T.forM [0..n1] (getAppArg ctx a)
getSort :: Context -> AST -> IO Sort
getSort = liftFun1 z3_get_sort
getBoolValue :: Context -> AST -> IO (Maybe Bool)
getBoolValue c a = h2c a $ \astPtr ->
castLBool <$> withContextError c (\cPtr -> z3_get_bool_value cPtr astPtr)
where 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"
getAstKind :: Context -> AST -> IO ASTKind
getAstKind ctx ast = toAstKind <$> liftFun1 z3_get_ast_kind ctx ast
where toAstKind :: Z3_ast_kind -> ASTKind
toAstKind k
| k == z3_numeral_ast = Z3_NUMERAL_AST
| k == z3_app_ast = Z3_APP_AST
| k == z3_var_ast = Z3_VAR_AST
| k == z3_quantifier_ast = Z3_QUANTIFIER_AST
| k == z3_sort_ast = Z3_SORT_AST
| k == z3_func_decl_ast = Z3_FUNC_DECL_AST
| k == z3_unknown_ast = Z3_UNKNOWN_AST
| otherwise =
error "Z3.Base.getAstKind: unknown `Z3_ast_kind'"
isApp :: Context -> AST -> IO Bool
isApp = liftFun1 z3_is_app
toApp :: Context -> AST -> IO App
toApp = liftFun1 z3_to_app
getNumeralString :: Context -> AST -> IO String
getNumeralString = liftFun1 z3_get_numeral_string
getIndexValue :: Context -> AST -> IO Int
getIndexValue = liftFun1 z3_get_index_value
isQuantifierForall :: Context -> AST -> IO Bool
isQuantifierForall = liftFun1 z3_is_quantifier_forall
isQuantifierExists :: Context -> AST -> IO Bool
isQuantifierExists ctx = fmap not . isQuantifierForall ctx
getQuantifierWeight :: Context -> AST -> IO Int
getQuantifierWeight = liftFun1 z3_get_quantifier_weight
getQuantifierNumPatterns :: Context -> AST -> IO Int
getQuantifierNumPatterns = liftFun1 z3_get_quantifier_num_patterns
getQuantifierPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierPatternAST = liftFun2 z3_get_quantifier_pattern_ast
getQuantifierPatterns :: Context -> AST -> IO [AST]
getQuantifierPatterns ctx a = do
n <- getQuantifierNumPatterns ctx a
T.forM [0..n1] (getQuantifierPatternAST ctx a)
getQuantifierNumNoPatterns :: Context -> AST -> IO Int
getQuantifierNumNoPatterns = liftFun1 z3_get_quantifier_num_no_patterns
getQuantifierNoPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierNoPatternAST = liftFun2 z3_get_quantifier_no_pattern_ast
getQuantifierNoPatterns :: Context -> AST -> IO [AST]
getQuantifierNoPatterns ctx a = do
n <- getQuantifierNumNoPatterns ctx a
T.forM [0..n1] (getQuantifierNoPatternAST ctx a)
getQuantifierNumBound :: Context -> AST -> IO Int
getQuantifierNumBound = liftFun1 z3_get_quantifier_num_bound
getQuantifierBoundName :: Context -> AST -> Int -> IO Symbol
getQuantifierBoundName = liftFun2 z3_get_quantifier_bound_name
getQuantifierBoundSort :: Context -> AST -> Int -> IO Sort
getQuantifierBoundSort = liftFun2 z3_get_quantifier_bound_sort
getQuantifierBoundVars :: Context -> AST -> IO [AST]
getQuantifierBoundVars ctx a = do
n <- getQuantifierNumBound ctx a
T.forM [0..n1] $ \i -> do
b <- getQuantifierBoundName ctx a i
s <- getQuantifierBoundSort ctx a i
mkVar ctx b s
getQuantifierBody :: Context -> AST -> IO AST
getQuantifierBody = liftFun1 z3_get_quantifier_body
simplify :: Context -> AST -> IO AST
simplify = liftFun1 z3_simplify
simplifyEx :: Context -> AST -> Params -> IO AST
simplifyEx = liftFun2 z3_simplify_ex
getBool :: Context -> AST -> IO Bool
getBool c a = fromJust <$> getBoolValue c a
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"
getBv :: Context -> AST
-> Bool
-> IO Integer
getBv c a signed = getInt c =<< mkBv2int c a signed
substituteVars :: Context -> AST -> [AST] -> IO AST
substituteVars ctx a vars =
marshal z3_substitute_vars ctx $ \f ->
h2c a $ \aPtr ->
marshalArrayLen vars $ \varsNum varsArr ->
f aPtr varsNum varsArr
modelEval :: Context
-> Model
-> AST
-> Bool
-> IO (Maybe AST)
modelEval ctx m a b =
withContext ctx $ \ctxPtr ->
alloca $ \aptr2 ->
h2c a $ \astPtr ->
h2c m $ \mPtr ->
h2c b $ \b' ->
checkError ctxPtr
(z3_model_eval ctxPtr mPtr astPtr b' aptr2) >>= peekAST aptr2 . toBool
where peekAST :: Ptr (Ptr Z3_ast) -> Bool -> IO (Maybe AST)
peekAST _p False = return Nothing
peekAST p True = fmap Just . c2h ctx =<< peek p
getConstInterp :: Context -> Model -> FuncDecl -> IO (Maybe AST)
getConstInterp ctx m fd = marshal z3_model_get_const_interp ctx $ \f ->
h2c m $ \mPtr ->
h2c fd $ \fdPtr ->
f mPtr fdPtr
hasInterp :: Context -> Model -> FuncDecl -> IO Bool
hasInterp = liftFun2 z3_model_has_interp
numConsts :: Context -> Model -> IO Word
numConsts = liftFun1 z3_model_get_num_consts
numFuncs :: Context -> Model -> IO Word
numFuncs = liftFun1 z3_model_get_num_funcs
getConstDecl :: Context -> Model -> Word -> IO FuncDecl
getConstDecl = liftFun2 z3_model_get_const_decl
getFuncDecl :: Context -> Model -> Word -> IO FuncDecl
getFuncDecl = liftFun2 z3_model_get_func_decl
getConsts :: Context -> Model -> IO [FuncDecl]
getConsts ctx m = do
n <- numConsts ctx m
forM [0..n1] $ \i -> getConstDecl ctx m i
getFuncs :: Context -> Model -> IO [FuncDecl]
getFuncs ctx m = do
n <- numFuncs ctx m
forM [0..n1] $ \i -> getFuncDecl ctx m i
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
addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp
addFuncInterp = liftFun3 z3_add_func_interp
addConstInterp :: Context -> Model -> FuncDecl -> AST -> IO ()
addConstInterp = liftFun3 z3_add_const_interp
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
type EvalAst a = Model -> AST -> IO (Maybe a)
eval :: Context -> EvalAst AST
eval ctx m a = modelEval ctx m a True
evalBool :: Context -> EvalAst Bool
evalBool ctx m ast = eval ctx m ast >>= T.traverse (getBool ctx)
evalInt :: Context -> EvalAst Integer
evalInt ctx m ast = eval ctx m ast >>= T.traverse (getInt ctx)
evalReal :: Context -> EvalAst Rational
evalReal ctx m ast = eval ctx m ast >>= T.traverse (getReal ctx)
evalBv :: Context -> Bool
-> EvalAst Integer
evalBv ctx signed m ast =
eval ctx m ast >>= T.traverse (\a -> getBv ctx a signed)
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
evalT c = mapEval (eval c)
mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (Maybe (t a))
mapEval f m = fmap T.sequence . T.mapM (f 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)
data ASTPrintMode
= Z3_PRINT_SMTLIB_FULL
| Z3_PRINT_LOW_LEVEL
| Z3_PRINT_SMTLIB2_COMPLIANT
setASTPrintMode :: Context -> ASTPrintMode -> IO ()
setASTPrintMode ctx mode = withContextError ctx $ \ctxPtr ->
case mode of
Z3_PRINT_SMTLIB_FULL ->
z3_set_ast_print_mode ctxPtr z3_print_smtlib_full
Z3_PRINT_LOW_LEVEL ->
z3_set_ast_print_mode ctxPtr z3_print_low_level
Z3_PRINT_SMTLIB2_COMPLIANT ->
z3_set_ast_print_mode ctxPtr 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
mkTactic :: Context -> String -> IO Tactic
mkTactic = liftFun1 z3_mk_tactic
andThenTactic :: Context -> Tactic -> Tactic -> IO Tactic
andThenTactic = liftFun2 z3_tactic_and_then
orElseTactic :: Context -> Tactic -> Tactic -> IO Tactic
orElseTactic = liftFun2 z3_tactic_or_else
skipTactic :: Context -> IO Tactic
skipTactic = liftFun0 z3_tactic_skip
tryForTactic :: Context -> Tactic -> Int -> IO Tactic
tryForTactic = liftFun2 z3_tactic_try_for
mkQuantifierEliminationTactic :: Context -> IO Tactic
mkQuantifierEliminationTactic ctx = mkTactic ctx "qe"
mkAndInverterGraphTactic :: Context -> IO Tactic
mkAndInverterGraphTactic ctx = mkTactic ctx "aig"
applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult
applyTactic = liftFun2 z3_tactic_apply
getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int
getApplyResultNumSubgoals = liftFun1 z3_apply_result_get_num_subgoals
getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal
getApplyResultSubgoal = liftFun2 z3_apply_result_get_subgoal
getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal]
getApplyResultSubgoals ctx a = do
n <- getApplyResultNumSubgoals ctx a
T.forM [0..n1] (getApplyResultSubgoal ctx a)
mkGoal :: Context -> Bool -> Bool -> Bool -> IO Goal
mkGoal = liftFun3 z3_mk_goal
goalAssert :: Context -> Goal -> AST -> IO ()
goalAssert = liftFun2 z3_goal_assert
getGoalSize :: Context -> Goal -> IO Int
getGoalSize = liftFun1 z3_goal_size
getGoalFormula :: Context -> Goal -> Int -> IO AST
getGoalFormula = liftFun2 z3_goal_formula
getGoalFormulas :: Context -> Goal -> IO [AST]
getGoalFormulas ctx g = do
n <- getGoalSize ctx g
T.forM [0..n1] (getGoalFormula ctx g)
parseSMTLib2String :: Context
-> String
-> [Symbol]
-> [Sort]
-> [Symbol]
-> [FuncDecl]
-> IO AST
parseSMTLib2String ctx str sortNames sorts declNames decls =
marshal z3_parse_smtlib2_string ctx $ \f ->
withCString str $ \cstr ->
marshalArrayLen sorts $ \sortNum sortArr ->
marshalArray sortNames $ \sortNameArr ->
marshalArrayLen decls $ \declNum declArr ->
marshalArray declNames $ \declNameArr ->
f cstr sortNum sortNameArr sortArr declNum declNameArr declArr
parseSMTLib2File :: Context
-> String
-> [Symbol]
-> [Sort]
-> [Symbol]
-> [FuncDecl]
-> IO AST
parseSMTLib2File ctx file sortNames sorts declNames decls =
marshal z3_parse_smtlib2_string ctx $ \f ->
withCString file $ \fileName ->
marshalArrayLen sorts $ \sortNum sortArr ->
marshalArray sortNames $ \sortNameArr ->
marshalArrayLen decls $ \declNum declArr ->
marshalArray declNames $ \declNameArr ->
f fileName sortNum sortNameArr sortArr declNum declNameArr declArr
data Z3Error = Z3Error
{ errCode :: Z3ErrorCode
, errMsg :: String
}
deriving Typeable
instance Show Z3Error where
show (Z3Error _ s) = "Z3 error: " ++ 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 :: Ptr Z3_context -> IO a -> IO a
checkError cPtr m = do
m <* (z3_get_error_code cPtr >>= throwZ3Exn)
where getErrStr i = peekCString =<< z3_get_error_msg_ex cPtr i
throwZ3Exn i = when (i /= z3_ok) $ getErrStr i >>= z3Error (toZ3Error 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
newtype Fixedpoint = Fixedpoint { unFixedpoint :: ForeignPtr Z3_fixedpoint }
deriving Eq
instance Marshal Fixedpoint (Ptr Z3_fixedpoint) where
c2h = mkC2hRefCount Fixedpoint z3_fixedpoint_inc_ref z3_fixedpoint_dec_ref
h2c fp = withForeignPtr (unFixedpoint fp)
mkFixedpoint :: Context -> IO Fixedpoint
mkFixedpoint = liftFun0 z3_mk_fixedpoint
fixedpointPush :: Context -> Fixedpoint -> IO ()
fixedpointPush = liftFun1 z3_fixedpoint_push
fixedpointPop :: Context -> Fixedpoint -> IO ()
fixedpointPop = liftFun1 z3_fixedpoint_pop
fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO ()
fixedpointAddRule = liftFun3 z3_fixedpoint_add_rule
fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO ()
fixedpointSetParams = liftFun2 z3_fixedpoint_set_params
fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO ()
fixedpointRegisterRelation = liftFun2 z3_fixedpoint_register_relation
fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result
fixedpointQueryRelations ctx fixedpoint fds =
marshal z3_fixedpoint_query_relations ctx $ \f ->
h2c fixedpoint $ \fixedpointPtr ->
marshalArrayLen fds $ \fdsNum fdsArr ->
f fixedpointPtr fdsNum fdsArr
fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST
fixedpointGetAnswer = liftFun1 z3_fixedpoint_get_answer
fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST]
fixedpointGetAssertions = liftFun1 z3_fixedpoint_get_assertions
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 = liftFun0 z3_mk_solver
mkSimpleSolver :: Context -> IO Solver
mkSimpleSolver = liftFun0 z3_mk_simple_solver
mkSolverForLogic :: Context -> Logic -> IO Solver
mkSolverForLogic c logic = mkStringSymbol c (show logic) >>= \sym ->
toHsCheckError c $ \cPtr -> z3_mk_solver_for_logic cPtr $ unSymbol sym
solverGetHelp :: Context -> Solver -> IO String
solverGetHelp = liftFun1 z3_solver_get_help
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 $ h2c solver
solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result
solverCheckAssumptions ctx solver assump =
marshal z3_solver_check_assumptions ctx $ \f ->
h2c solver $ \solverPtr ->
marshalArrayLen assump $ \assumpNum assumpArr ->
f solverPtr assumpNum assumpArr
solverGetModel :: Context -> Solver -> IO Model
solverGetModel ctx solver = marshal z3_solver_get_model ctx $ \f ->
h2c solver $ \solverPtr ->
f solverPtr
solverGetUnsatCore :: Context -> Solver -> IO [AST]
solverGetUnsatCore = liftFun1 z3_solver_get_unsat_core
solverGetReasonUnknown :: Context -> Solver -> IO String
solverGetReasonUnknown = liftFun1 z3_solver_get_reason_unknown
solverToString :: Context -> Solver -> IO String
solverToString = liftFun1 z3_solver_to_string
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)
withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r
withContext c = withForeignPtr (unContext c)
withContextError :: Context -> (Ptr Z3_context -> IO r) -> IO r
withContextError c f = withContext c $ \cPtr -> checkError cPtr (f cPtr)
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_err :: String
-> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))
-> Context -> [AST] -> IO AST
liftAstN_err s _ _ [] = error s
liftAstN_err _ f c es = marshal f c $ marshalArrayLen es
liftAstN :: (Ptr Z3_context -> IO (Ptr Z3_ast))
-> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))
-> Context -> [AST] -> IO AST
liftAstN s f c = maybe (liftFun0 s c) (liftAstN1 f c) . nonEmpty
liftAstN1 :: (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast))
-> Context -> NonEmpty AST -> IO AST
liftAstN1 f c = marshal f c . marshalArrayLen . toList
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)
cs2hs :: Marshal h c => Context -> [c] -> IO [h]
cs2hs ctx = mapM (c2h ctx)
peekArrayToHs :: (Marshal h c, Storable c) => Context -> Int -> Ptr c -> IO [h]
peekArrayToHs c n dPtr =
cs2hs c =<< peekArray n dPtr
toHsCheckError :: Marshal h c => Context -> (Ptr Z3_context -> IO c) -> IO h
toHsCheckError c f = withContext c $ \cPtr ->
c2h c =<< checkError cPtr (f cPtr)
type Z3SetRefCount c = Ptr Z3_context -> Ptr c -> IO ()
type Z3IncRefFun c = Z3SetRefCount c
type Z3DecRefFun c = Z3SetRefCount c
mkC2hRefCount :: (ForeignPtr c -> h)
-> Z3IncRefFun c
-> Z3DecRefFun c
-> Context -> Ptr c -> IO h
mkC2hRefCount mk incRef decRef ctx xPtr =
withContext ctx $ \ctxPtr -> do
incRef ctxPtr xPtr
contextIncRef ctx
let xFinalizer = do
decRef ctxPtr xPtr
contextDecRef ctxPtr (refCount ctx)
mk <$> newForeignPtr xPtr xFinalizer
dummy_inc_ref :: Z3IncRefFun c
dummy_inc_ref _ _ = return ()
on_ast_ptr :: Z3SetRefCount Z3_ast
-> (Ptr Z3_context -> Ptr a -> IO (Ptr Z3_ast))
-> Z3SetRefCount a
f `on_ast_ptr` t = \ctxPtr ptr -> f ctxPtr =<< t ctxPtr ptr
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 = mkC2hRefCount App
(z3_inc_ref `on_ast_ptr` z3_app_to_ast)
(z3_dec_ref `on_ast_ptr` z3_app_to_ast)
h2c app = withForeignPtr (unApp app)
instance Marshal Params (Ptr Z3_params) where
c2h = mkC2hRefCount Params z3_params_inc_ref z3_params_dec_ref
h2c prm = withForeignPtr (unParams prm)
instance Marshal Symbol (Ptr Z3_symbol) where
c2h _ = return . Symbol
h2c s f = f (unSymbol s)
instance Marshal AST (Ptr Z3_ast) where
c2h = mkC2hRefCount AST z3_inc_ref z3_dec_ref
h2c a f = withForeignPtr (unAST a) f
instance Marshal [AST] (Ptr Z3_ast_vector) where
c2h ctx vecPtr = withContext ctx $ \ctxPtr -> do
z3_ast_vector_inc_ref ctxPtr vecPtr
n <- z3_ast_vector_size ctxPtr vecPtr
res <- if n == 0
then return []
else mapM (\i -> z3_ast_vector_get ctxPtr vecPtr i >>= c2h ctx) [0 .. (n 1)]
z3_ast_vector_dec_ref ctxPtr vecPtr
return res
h2c _ _ = error "Marshal [AST] (Ptr Z3_ast_vector) => h2c not implemented"
instance Marshal Sort (Ptr Z3_sort) where
c2h = mkC2hRefCount Sort
(z3_inc_ref `on_ast_ptr` z3_sort_to_ast)
(z3_dec_ref `on_ast_ptr` z3_sort_to_ast)
h2c srt = withForeignPtr (unSort srt)
instance Marshal FuncDecl (Ptr Z3_func_decl) where
c2h = mkC2hRefCount FuncDecl
(z3_inc_ref `on_ast_ptr` z3_func_decl_to_ast)
(z3_dec_ref `on_ast_ptr` z3_func_decl_to_ast)
h2c fnd = withForeignPtr (unFuncDecl fnd)
instance Marshal FuncEntry (Ptr Z3_func_entry) where
c2h = mkC2hRefCount FuncEntry z3_func_entry_inc_ref
z3_func_entry_dec_ref
h2c fne = withForeignPtr (unFuncEntry fne)
instance Marshal FuncInterp (Ptr Z3_func_interp) where
c2h = mkC2hRefCount FuncInterp z3_func_interp_inc_ref
z3_func_interp_dec_ref
h2c fni = withForeignPtr (unFuncInterp fni)
instance Marshal Model (Ptr Z3_model) where
c2h = mkC2hRefCount Model z3_model_inc_ref z3_model_dec_ref
h2c m = withForeignPtr (unModel m)
instance Marshal Pattern (Ptr Z3_pattern) where
c2h = mkC2hRefCount Pattern
(z3_inc_ref `on_ast_ptr` z3_pattern_to_ast)
(z3_dec_ref `on_ast_ptr` z3_pattern_to_ast)
h2c pat = withForeignPtr (unPattern pat)
instance Marshal Constructor (Ptr Z3_constructor) where
c2h = mkC2hRefCount Constructor dummy_inc_ref z3_del_constructor
h2c cns = withForeignPtr (unConstructor cns)
instance Marshal ConstructorList (Ptr Z3_constructor_list) where
c2h = mkC2hRefCount ConstructorList dummy_inc_ref z3_del_constructor_list
h2c cl = withForeignPtr (unConstructorList cl)
instance Marshal Solver (Ptr Z3_solver) where
c2h = mkC2hRefCount Solver z3_solver_inc_ref z3_solver_dec_ref
h2c slv = withForeignPtr (unSolver slv)
instance Marshal Tactic (Ptr Z3_tactic) where
c2h = mkC2hRefCount Tactic z3_tactic_inc_ref z3_tactic_dec_ref
h2c tac = withForeignPtr (unTactic tac)
instance Marshal ApplyResult (Ptr Z3_apply_result) where
c2h = mkC2hRefCount ApplyResult z3_apply_result_inc_ref z3_apply_result_dec_ref
h2c apl = withForeignPtr (unApplyResult apl)
instance Marshal Goal (Ptr Z3_goal) where
c2h = mkC2hRefCount Goal z3_goal_inc_ref z3_goal_dec_ref
h2c goa = withForeignPtr (unGoal goa)
marshal :: Marshal rh rc => (Ptr Z3_context -> t) ->
Context -> (t -> IO rc) -> IO rh
marshal f c cont = toHsCheckError c $ \cPtr -> cont $ f cPtr
liftFun0 :: Marshal rh rc => (Ptr Z3_context -> IO rc) ->
Context -> IO rh
liftFun0 = flip toHsCheckError
liftFun1 :: (Marshal ah ac, Marshal rh rc) =>
(Ptr Z3_context -> ac -> IO rc) ->
Context -> ah -> IO rh
liftFun1 f c x = h2c x $ \a ->
toHsCheckError c $ \cPtr -> f cPtr 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 = h2c x $ \a -> h2c y $ \b ->
toHsCheckError c $ \cPtr -> f cPtr 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 = h2c x $ \x1 -> h2c y $ \y1 -> h2c z $ \z1 ->
toHsCheckError c $ \cPtr -> f cPtr 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_false = False
| otherwise = True
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