Copyright	(c) Iago Abal 2012-2015 (c) David Castro 2012-2015
License	BSD3
Maintainer	Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Z3.Base

Contents

Types
- Satisfiability result
Algebraic Numbers
Global Parameters
Create configuration
- Helpers
Create context
Parameters
Symbols
Sorts
Constants and Applications
- Helpers
Propositional Logic and Equality
- Helpers
Arithmetic: Integers and Reals
Bit-vectors
Arrays
Sets
Numerals
- Helpers
Sequences and regular expressions
Quantifiers
Accessors
- Helpers
Modifiers
Models
- Helpers
Tactics
String Conversion
Parser interface
Error Handling
Miscellaneous
Fixedpoint
Floating-Point Arithmetic
Z3-specific floating-point extensions
Optimization
Solvers
- Helpers

Description

Low-level bindings to Z3 API.

There is (mostly) a one-to-one correspondence with Z3 C API, thus see http://z3prover.github.io/api/html/group__capi.html for further details.

Synopsis

data Config
data Context
data Symbol
data AST
data Sort
data TupleType = TupleType {
- tupleSort :: Sort
- tupleCons :: FuncDecl
- namedTupleProjs :: [(String, FuncDecl)]
}
data FuncDecl
data App
data Pattern
data Constructor
data Model
data FuncInterp
data FuncEntry
data Params
data Solver
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
data ASTKind
- = Z3_NUMERAL_AST
- | Z3_APP_AST
- | Z3_VAR_AST
- | Z3_QUANTIFIER_AST
- | Z3_SORT_AST
- | Z3_FUNC_DECL_AST
- | Z3_UNKNOWN_AST
data Tactic
data ApplyResult
data Goal
data Result
- = Sat
- | Unsat
- | Undef
algebraicIsValue :: Context -> AST -> IO Bool
algebraicIsPos :: Context -> AST -> IO Bool
algebraicIsNeg :: Context -> AST -> IO Bool
algebraicIsZero :: Context -> AST -> IO Bool
algebraicSign :: Context -> AST -> IO Int
algebraicAdd :: Context -> AST -> AST -> IO AST
algebraicSub :: Context -> AST -> AST -> IO AST
algebraicMul :: Context -> AST -> AST -> IO AST
algebraicDiv :: Context -> AST -> AST -> IO AST
algebraicRoot :: Context -> AST -> Int -> IO AST
algebraicPower :: Context -> AST -> Int -> IO AST
algebraicLt :: Context -> AST -> AST -> IO Bool
algebraicGt :: Context -> AST -> AST -> IO Bool
algebraicLe :: Context -> AST -> AST -> IO Bool
algebraicGe :: Context -> AST -> AST -> IO Bool
algebraicEq :: Context -> AST -> AST -> IO Bool
algebraicNeq :: Context -> AST -> AST -> IO Bool
algebraicRoots :: Context -> AST -> [AST] -> IO [AST]
algebraicEval :: Context -> AST -> [AST] -> IO Int
globalParamSet :: String -> String -> IO ()
globalParamResetAll :: IO ()
globalParamGet :: String -> IO (Maybe String)
mkConfig :: IO Config
delConfig :: Config -> IO ()
setParamValue :: Config -> String -> String -> IO ()
withConfig :: (Config -> IO a) -> IO a
mkContext :: Config -> IO Context
withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r
mkParams :: Context -> IO Params
paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO ()
paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
paramsToString :: Context -> Params -> IO String
mkIntSymbol :: Integral int => Context -> int -> IO Symbol
mkStringSymbol :: Context -> String -> IO Symbol
mkUninterpretedSort :: Context -> Symbol -> IO Sort
mkBoolSort :: Context -> IO Sort
mkIntSort :: Context -> IO Sort
mkRealSort :: Context -> IO Sort
mkBvSort :: Integral int => Context -> int -> IO Sort
mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort
mkArraySort :: Context -> Sort -> Sort -> IO Sort
mkArraySortN :: Context -> [Sort] -> Sort -> IO Sort
mkTupleSort :: Context -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])
mkTupleType :: Context -> Symbol -> [(String, Sort)] -> IO TupleType
mkTuple :: Context -> TupleType -> [AST] -> IO AST
mkIndexTuple :: Context -> TupleType -> Int -> AST -> IO AST
mkProjTuple :: Context -> TupleType -> String -> AST -> IO AST
mkEnumerationSort :: Context -> Symbol -> [Symbol] -> IO (Sort, [FuncDecl], [FuncDecl])
mkListSort :: Context -> Symbol -> Sort -> IO (Sort, FuncDecl, FuncDecl, FuncDecl, FuncDecl, FuncDecl, FuncDecl)
mkConstructor :: Context -> Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> IO Constructor
mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort
mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO [Sort]
mkSetSort :: Context -> Sort -> IO Sort
mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
mkApp :: Context -> FuncDecl -> [AST] -> IO AST
mkConst :: Context -> Symbol -> Sort -> IO AST
mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl
mkFreshConst :: Context -> String -> Sort -> IO AST
mkRecFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
addRecDef :: Context -> FuncDecl -> [AST] -> AST -> IO ()
mkVar :: Context -> Symbol -> Sort -> IO AST
mkBoolVar :: Context -> Symbol -> IO AST
mkRealVar :: Context -> Symbol -> IO AST
mkIntVar :: Context -> Symbol -> IO AST
mkBvVar :: Context -> Symbol -> Int -> IO AST
mkFreshVar :: Context -> String -> Sort -> IO AST
mkFreshBoolVar :: Context -> String -> IO AST
mkFreshRealVar :: Context -> String -> IO AST
mkFreshIntVar :: Context -> String -> IO AST
mkFreshBvVar :: Context -> String -> Int -> IO AST
mkTrue :: Context -> IO AST
mkFalse :: Context -> IO AST
mkEq :: Context -> AST -> AST -> IO AST
mkNot :: Context -> AST -> IO AST
mkIte :: Context -> AST -> AST -> AST -> IO AST
mkIff :: Context -> AST -> AST -> IO AST
mkImplies :: Context -> AST -> AST -> IO AST
mkXor :: Context -> AST -> AST -> IO AST
mkAnd :: Context -> [AST] -> IO AST
mkOr :: Context -> [AST] -> IO AST
mkDistinct :: Context -> [AST] -> IO AST
mkDistinct1 :: Context -> NonEmpty AST -> IO AST
mkBool :: Context -> Bool -> IO AST
mkAdd :: Context -> [AST] -> IO AST
mkMul :: Context -> [AST] -> IO AST
mkSub :: Context -> [AST] -> IO AST
mkSub1 :: Context -> NonEmpty AST -> IO AST
mkUnaryMinus :: Context -> AST -> IO AST
mkDiv :: Context -> AST -> AST -> IO AST
mkMod :: Context -> AST -> AST -> IO AST
mkRem :: Context -> AST -> AST -> IO AST
mkPower :: Context -> AST -> AST -> IO AST
mkLt :: Context -> AST -> AST -> IO AST
mkLe :: Context -> AST -> AST -> IO AST
mkGt :: Context -> AST -> AST -> IO AST
mkGe :: Context -> AST -> AST -> IO AST
mkInt2Real :: Context -> AST -> IO AST
mkReal2Int :: Context -> AST -> IO AST
mkIsInt :: Context -> AST -> IO AST
mkBvnot :: Context -> AST -> IO AST
mkBvredand :: Context -> AST -> IO AST
mkBvredor :: Context -> AST -> IO AST
mkBvand :: Context -> AST -> AST -> IO AST
mkBvor :: Context -> AST -> AST -> IO AST
mkBvxor :: Context -> AST -> AST -> IO AST
mkBvnand :: Context -> AST -> AST -> IO AST
mkBvnor :: Context -> AST -> AST -> IO AST
mkBvxnor :: Context -> AST -> AST -> IO AST
mkBvneg :: Context -> AST -> IO AST
mkBvadd :: Context -> AST -> AST -> IO AST
mkBvsub :: Context -> AST -> AST -> IO AST
mkBvmul :: Context -> AST -> AST -> IO AST
mkBvudiv :: Context -> AST -> AST -> IO AST
mkBvsdiv :: Context -> AST -> AST -> IO AST
mkBvurem :: Context -> AST -> AST -> IO AST
mkBvsrem :: Context -> AST -> AST -> IO AST
mkBvsmod :: Context -> AST -> AST -> IO AST
mkBvult :: Context -> AST -> AST -> IO AST
mkBvslt :: Context -> AST -> AST -> IO AST
mkBvule :: Context -> AST -> AST -> IO AST
mkBvsle :: Context -> AST -> AST -> IO AST
mkBvuge :: Context -> AST -> AST -> IO AST
mkBvsge :: Context -> AST -> AST -> IO AST
mkBvugt :: Context -> AST -> AST -> IO AST
mkBvsgt :: Context -> AST -> AST -> IO AST
mkConcat :: Context -> AST -> AST -> IO AST
mkExtract :: Context -> Int -> Int -> AST -> IO AST
mkSignExt :: Context -> Int -> AST -> IO AST
mkZeroExt :: Context -> Int -> AST -> IO AST
mkRepeat :: Context -> Int -> AST -> IO AST
mkBvshl :: Context -> AST -> AST -> IO AST
mkBvlshr :: Context -> AST -> AST -> IO AST
mkBvashr :: Context -> AST -> AST -> IO AST
mkRotateLeft :: Context -> Int -> AST -> IO AST
mkRotateRight :: Context -> Int -> AST -> IO AST
mkExtRotateLeft :: Context -> AST -> AST -> IO AST
mkExtRotateRight :: Context -> AST -> AST -> IO AST
mkInt2bv :: Context -> Int -> AST -> IO AST
mkBv2int :: Context -> AST -> Bool -> IO AST
mkBvnegNoOverflow :: Context -> AST -> IO AST
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
mkSelect :: Context -> AST -> AST -> IO AST
mkStore :: Context -> AST -> AST -> AST -> IO AST
mkConstArray :: Context -> Sort -> AST -> IO AST
mkMap :: Context -> FuncDecl -> [AST] -> IO AST
mkArrayDefault :: Context -> AST -> IO AST
mkEmptySet :: Context -> Sort -> IO AST
mkFullSet :: Context -> Sort -> IO AST
mkSetAdd :: Context -> AST -> AST -> IO AST
mkSetDel :: Context -> AST -> AST -> IO AST
mkSetUnion :: Context -> [AST] -> IO AST
mkSetIntersect :: Context -> [AST] -> IO AST
mkSetDifference :: Context -> AST -> AST -> IO AST
mkSetComplement :: Context -> AST -> IO AST
mkSetMember :: Context -> AST -> AST -> IO AST
mkSetSubset :: Context -> AST -> AST -> IO AST
mkNumeral :: Context -> String -> Sort -> IO AST
mkReal :: Context -> Int -> Int -> IO AST
mkInt :: Context -> Int -> Sort -> IO AST
mkUnsignedInt :: Context -> Word -> Sort -> IO AST
mkInt64 :: Context -> Int64 -> Sort -> IO AST
mkUnsignedInt64 :: Context -> Word64 -> Sort -> IO AST
mkIntegral :: Integral a => Context -> a -> Sort -> IO AST
mkRational :: Context -> Rational -> IO AST
mkFixed :: HasResolution a => Context -> Fixed a -> IO AST
mkRealNum :: Real r => Context -> r -> IO AST
mkInteger :: Context -> Integer -> IO AST
mkIntNum :: Integral a => Context -> a -> IO AST
mkBitvector :: Context -> Int -> Integer -> IO AST
mkBvNum :: Integral i => Context -> Int -> i -> IO AST
mkSeqSort :: Context -> Sort -> IO Sort
isSeqSort :: Context -> Sort -> IO Bool
mkReSort :: Context -> Sort -> IO Sort
isReSort :: Context -> Sort -> IO Bool
mkStringSort :: Context -> IO Sort
isStringSort :: Context -> Sort -> IO Bool
mkString :: Context -> String -> IO AST
isString :: Context -> AST -> IO Bool
getString :: Context -> AST -> IO String
mkSeqEmpty :: Context -> Sort -> IO AST
mkSeqUnit :: Context -> AST -> IO AST
mkSeqConcat :: Context -> [AST] -> IO AST
mkSeqPrefix :: Context -> AST -> AST -> IO AST
mkSeqSuffix :: Context -> AST -> AST -> IO AST
mkSeqContains :: Context -> AST -> AST -> IO AST
mkStrLt :: Context -> AST -> AST -> IO AST
mkStrLe :: Context -> AST -> AST -> IO AST
mkSeqExtract :: Context -> AST -> AST -> AST -> IO AST
mkSeqReplace :: Context -> AST -> AST -> AST -> IO AST
mkSeqAt :: Context -> AST -> AST -> IO AST
mkSeqLength :: Context -> AST -> IO AST
mkSeqIndex :: Context -> AST -> AST -> AST -> IO AST
mkStrToInt :: Context -> AST -> IO AST
mkIntToStr :: Context -> AST -> IO AST
mkSeqToRe :: Context -> AST -> IO AST
mkSeqInRe :: Context -> AST -> AST -> IO AST
mkRePlus :: Context -> AST -> IO AST
mkReStar :: Context -> AST -> IO AST
mkReOption :: Context -> AST -> IO AST
mkReUnion :: Integral int => Context -> int -> [AST] -> IO AST
mkReConcat :: Integral int => Context -> int -> [AST] -> IO AST
mkReRange :: Context -> AST -> AST -> IO AST
mkReLoop :: Integral int => Context -> AST -> int -> int -> IO AST
mkReIntersect :: Integral int => Context -> int -> [AST] -> IO AST
mkReComplement :: Context -> AST -> IO AST
mkReEmpty :: Context -> Sort -> IO AST
mkReFull :: Context -> Sort -> IO AST
mkPattern :: Context -> [AST] -> IO Pattern
mkBound :: Context -> Int -> Sort -> IO AST
mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
mkForallW :: Context -> Int -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
mkExistsW :: Context -> Int -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
mkForallConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
mkForallWConst :: Context -> Int -> [Pattern] -> [App] -> AST -> IO AST
mkExistsConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
mkExistsWConst :: Context -> Int -> [Pattern] -> [App] -> AST -> IO AST
getSymbolString :: Context -> Symbol -> IO String
isEqSort :: Context -> Sort -> Sort -> IO Bool
getSortName :: Context -> Sort -> IO Symbol
sortToAst :: Context -> Sort -> IO AST
getSortId :: Context -> Sort -> IO Int
getSortKind :: Context -> Sort -> IO SortKind
getBvSortSize :: Context -> Sort -> IO Int
getFiniteDomainSortSize :: Context -> Sort -> IO (Maybe Word64)
getTupleSortMkDecl :: Context -> Sort -> IO FuncDecl
getTupleSortNumFields :: Context -> Sort -> IO Int
getTupleSortFieldDecl :: Context -> Sort -> Int -> IO FuncDecl
getDatatypeSortConstructors :: Context -> Sort -> IO [FuncDecl]
getDatatypeSortRecognizers :: Context -> Sort -> IO [FuncDecl]
getDatatypeSortConstructorAccessors :: Context -> Sort -> IO [[FuncDecl]]
mkAtMost :: Context -> [AST] -> Int -> IO AST
mkAtLeast :: Context -> [AST] -> Int -> IO AST
getDeclName :: Context -> FuncDecl -> IO Symbol
getArity :: Context -> FuncDecl -> IO Int
getDomain :: Context -> FuncDecl -> Int -> IO Sort
getRange :: Context -> FuncDecl -> IO Sort
getDeclNumParameters :: Context -> FuncDecl -> IO Int
appToAst :: Context -> App -> IO AST
getAppDecl :: Context -> App -> IO FuncDecl
getAppNumArgs :: Context -> App -> IO Int
getAppArg :: Context -> App -> Int -> IO AST
getAppArgs :: Context -> App -> IO [AST]
getSort :: Context -> AST -> IO Sort
isWellSorted :: Context -> AST -> IO Bool
getArraySortDomain :: Context -> Sort -> IO Sort
getArraySortRange :: Context -> Sort -> IO Sort
getBoolValue :: Context -> AST -> IO (Maybe Bool)
getAstKind :: Context -> AST -> IO ASTKind
isApp :: Context -> AST -> IO Bool
toApp :: Context -> AST -> IO App
getNumeralString :: Context -> AST -> IO String
getNumerator :: Context -> AST -> IO AST
getDenominator :: Context -> AST -> IO AST
simplify :: Context -> AST -> IO AST
simplifyEx :: Context -> AST -> Params -> IO AST
getIndexValue :: Context -> AST -> IO Int
isQuantifierForall :: Context -> AST -> IO Bool
isQuantifierExists :: Context -> AST -> IO Bool
getQuantifierWeight :: Context -> AST -> IO Int
getQuantifierNumPatterns :: Context -> AST -> IO Int
getQuantifierPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierPatterns :: Context -> AST -> IO [AST]
getQuantifierNumNoPatterns :: Context -> AST -> IO Int
getQuantifierNoPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierNoPatterns :: Context -> AST -> IO [AST]
getQuantifierNumBound :: Context -> AST -> IO Int
getQuantifierBoundName :: Context -> AST -> Int -> IO Symbol
getQuantifierBoundSort :: Context -> AST -> Int -> IO Sort
getQuantifierBoundVars :: Context -> AST -> IO [AST]
getQuantifierBody :: Context -> AST -> IO AST
getBool :: Context -> AST -> IO Bool
getInt :: Context -> AST -> IO Integer
getReal :: Context -> AST -> IO Rational
substituteVars :: Context -> AST -> [AST] -> IO AST
substitute :: Context -> AST -> [(AST, AST)] -> IO AST
modelTranslate :: Context -> Model -> Context -> IO Model
modelEval :: Context -> Model -> AST -> Bool -> IO (Maybe AST)
evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
getConstInterp :: Context -> Model -> FuncDecl -> IO (Maybe AST)
getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
hasInterp :: Context -> Model -> FuncDecl -> IO Bool
numConsts :: Context -> Model -> IO Word
numFuncs :: Context -> Model -> IO Word
getConstDecl :: Context -> Model -> Word -> IO FuncDecl
getFuncDecl :: Context -> Model -> Word -> IO FuncDecl
getConsts :: Context -> Model -> IO [FuncDecl]
getFuncs :: Context -> Model -> IO [FuncDecl]
isAsArray :: Context -> AST -> IO Bool
isEqAST :: Context -> AST -> AST -> IO Bool
addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp
addConstInterp :: Context -> Model -> FuncDecl -> AST -> IO ()
getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
funcInterpGetElse :: Context -> FuncInterp -> IO AST
funcInterpGetArity :: Context -> FuncInterp -> IO Int
funcEntryGetValue :: Context -> FuncEntry -> IO AST
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
modelToString :: Context -> Model -> IO String
showModel :: Context -> Model -> IO String
type EvalAst a = Model -> AST -> IO (Maybe a)
eval :: Context -> EvalAst AST
evalBool :: Context -> EvalAst Bool
evalInt :: Context -> EvalAst Integer
evalReal :: Context -> EvalAst Rational
evalBv :: Context -> Bool -> EvalAst Integer
mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (Maybe (t a))
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
}
evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
mkTactic :: Context -> String -> IO Tactic
andThenTactic :: Context -> Tactic -> Tactic -> IO Tactic
orElseTactic :: Context -> Tactic -> Tactic -> IO Tactic
skipTactic :: Context -> IO Tactic
tryForTactic :: Context -> Tactic -> Int -> IO Tactic
tacticUsingParams :: Context -> Tactic -> Params -> IO Tactic
repeatTactic :: Context -> Tactic -> Int -> IO Tactic
mkQuantifierEliminationTactic :: Context -> IO Tactic
mkAndInverterGraphTactic :: Context -> IO Tactic
applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult
applyResultToString :: Context -> ApplyResult -> IO String
getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int
getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal
getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal]
mkGoal :: Context -> Bool -> Bool -> Bool -> IO Goal
goalAssert :: Context -> Goal -> AST -> IO ()
getGoalSize :: Context -> Goal -> IO Int
getGoalFormula :: Context -> Goal -> Int -> IO AST
getGoalFormulas :: Context -> Goal -> IO [AST]
goalToString :: Context -> Goal -> IO String
convertModel :: Context -> Goal -> Model -> IO Model
data ASTPrintMode
- = Z3_PRINT_SMTLIB_FULL
- | Z3_PRINT_LOW_LEVEL
- | Z3_PRINT_SMTLIB2_COMPLIANT
setASTPrintMode :: Context -> ASTPrintMode -> IO ()
astToString :: Context -> AST -> IO String
patternToString :: Context -> Pattern -> IO String
sortToString :: Context -> Sort -> IO String
funcDeclToString :: Context -> FuncDecl -> IO String
benchmarkToSMTLibString :: Context -> String -> String -> String -> String -> [AST] -> AST -> IO String
parseSMTLib2String :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO [AST]
parseSMTLib2File :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO [AST]
evalSMTLib2String :: Context -> String -> IO String
data Z3Error = Z3Error {
- errCode :: Z3ErrorCode
- errMsg :: String
}
data Z3ErrorCode
- = SortError
- | IOB
- | InvalidArg
- | ParserError
- | NoParser
- | InvalidPattern
- | MemoutFail
- | FileAccessError
- | InternalFatal
- | InvalidUsage
- | DecRefError
- | Z3Exception
data Version = Version {
- z3Major :: !Int
- z3Minor :: !Int
- z3Build :: !Int
- z3Revision :: !Int
}
getVersion :: IO Version
newtype Fixedpoint = Fixedpoint {
- unFixedpoint :: ForeignPtr Z3_fixedpoint
}
mkFixedpoint :: Context -> IO Fixedpoint
fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO ()
fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO ()
fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO ()
fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result
fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST
fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST]
mkFpaRoundingModeSort :: Context -> IO Sort
mkFpaRoundNearestTiesToEven :: Context -> IO AST
mkFpaRne :: Context -> IO AST
mkFpaRoundNearestTiesToAway :: Context -> IO AST
mkFpaRna :: Context -> IO AST
mkFpaRoundTowardPositive :: Context -> IO AST
mkFpaRtp :: Context -> IO AST
mkFpaRoundTowardNegative :: Context -> IO AST
mkFpaRtn :: Context -> IO AST
mkFpaRoundTowardZero :: Context -> IO AST
mkFpaRtz :: Context -> IO AST
mkFpaSort :: Integral int => Context -> int -> int -> IO Sort
mkFpaSortHalf :: Context -> IO Sort
mkFpaSort16 :: Context -> IO Sort
mkFpaSortSingle :: Context -> IO Sort
mkFpaSort32 :: Context -> IO Sort
mkFpaSortDouble :: Context -> IO Sort
mkFpaSort64 :: Context -> IO Sort
mkFpaSortQuadruple :: Context -> IO Sort
mkFpaSort128 :: Context -> IO Sort
mkFpaNaN :: Context -> Sort -> IO AST
mkFpaInf :: Context -> Sort -> Bool -> IO AST
mkFpaZero :: Context -> Sort -> Bool -> IO AST
mkFpaFp :: Context -> AST -> AST -> AST -> IO AST
mkFpaNumeralFloat :: Context -> Float -> Sort -> IO AST
mkFpaNumeralDouble :: Context -> Double -> Sort -> IO AST
mkFpaNumeralInt :: Integral int => Context -> int -> Sort -> IO AST
mkFpaNumeralIntUInt :: Integral int => Context -> Bool -> int -> int -> Sort -> IO AST
mkFpaNumeralInt64UInt64 :: Integral int => Context -> Bool -> int -> int -> Sort -> IO AST
mkFpaAbs :: Context -> AST -> IO AST
mkFpaNeg :: Context -> AST -> IO AST
mkFpaAdd :: Context -> AST -> AST -> AST -> IO AST
mkFpaSub :: Context -> AST -> AST -> AST -> IO AST
mkFpaMul :: Context -> AST -> AST -> AST -> IO AST
mkFpaDiv :: Context -> AST -> AST -> AST -> IO AST
mkFpaFma :: Context -> AST -> AST -> AST -> AST -> IO AST
mkFpaSqrt :: Context -> AST -> AST -> IO AST
mkFpaRem :: Context -> AST -> AST -> IO AST
mkFpaRoundToIntegral :: Context -> AST -> AST -> IO AST
mkFpaMin :: Context -> AST -> AST -> IO AST
mkFpaMax :: Context -> AST -> AST -> IO AST
mkFpaLeq :: Context -> AST -> AST -> IO AST
mkFpaLt :: Context -> AST -> AST -> IO AST
mkFpaGeq :: Context -> AST -> AST -> IO AST
mkFpaGt :: Context -> AST -> AST -> IO AST
mkFpaEq :: Context -> AST -> AST -> IO AST
mkFpaIsNormal :: Context -> AST -> IO AST
mkFpaIsSubnormal :: Context -> AST -> IO AST
mkFpaIsZero :: Context -> AST -> IO AST
mkFpaIsInfinite :: Context -> AST -> IO AST
mkFpaIsNaN :: Context -> AST -> IO AST
mkFpaIsNegative :: Context -> AST -> IO AST
mkFpaIsPositive :: Context -> AST -> IO AST
mkFpaToFpBv :: Context -> AST -> Sort -> IO AST
mkFpaToFpFloat :: Context -> AST -> AST -> Sort -> IO AST
mkFpaToFpReal :: Context -> AST -> AST -> Sort -> IO AST
mkFpaToFpSigned :: Context -> AST -> AST -> Sort -> IO AST
mkFpaToFpUnsigned :: Context -> AST -> AST -> Sort -> IO AST
mkFpaToUbv :: Integral int => Context -> AST -> AST -> int -> IO AST
mkFpaToSbv :: Integral int => Context -> AST -> AST -> int -> IO AST
mkFpaToReal :: Context -> AST -> IO AST
fpaGetEbits :: Integral int => Context -> Sort -> IO int
fpaGetSbits :: Integral int => Context -> Sort -> IO int
fpaIsNumeralNaN :: Context -> AST -> IO Bool
fpaIsNumeralInf :: Context -> AST -> IO Bool
fpaIsNumeralZero :: Context -> AST -> IO Bool
fpaIsNumeralNormal :: Context -> AST -> IO Bool
fpaIsNumeralSubnormal :: Context -> AST -> IO Bool
fpaIsNumeralPositive :: Context -> AST -> IO Bool
fpaIsNumeralNegative :: Context -> AST -> IO Bool
fpaGetNumeralSignBv :: Context -> AST -> IO AST
fpaGetNumeralSignificandBv :: Context -> AST -> IO AST
fpaGetNumeralSignificandString :: Context -> AST -> IO String
fpaGetNumeralExponentString :: Context -> AST -> Bool -> IO String
fpaGetNumeralExponentBv :: Context -> AST -> Bool -> IO AST
mkFpaToIEEEBv :: Context -> AST -> IO AST
mkFpaToFpIntReal :: Context -> AST -> AST -> AST -> Sort -> IO AST
newtype Optimize = Optimize {
- unOptimize :: ForeignPtr Z3_optimize
}
mkOptimize :: Context -> IO Optimize
optimizeAssert :: Context -> Optimize -> AST -> IO ()
optimizeAssertAndTrack :: Context -> Optimize -> AST -> AST -> IO ()
optimizeAssertSoft :: Context -> Optimize -> AST -> String -> Symbol -> IO Int
optimizeMaximize :: Context -> Optimize -> AST -> IO Int
optimizeMinimize :: Context -> Optimize -> AST -> IO Int
optimizePush :: Context -> Optimize -> IO ()
optimizePop :: Context -> Optimize -> IO ()
optimizeCheck :: Context -> Optimize -> [AST] -> IO Result
optimizeGetReasonUnknown :: Context -> Optimize -> IO String
optimizeGetModel :: Context -> Optimize -> IO Model
optimizeGetUnsatCore :: Context -> Optimize -> IO [AST]
optimizeSetParams :: Context -> Optimize -> Params -> IO ()
optimizeGetLower :: Context -> Optimize -> Int -> IO AST
optimizeGetUpper :: Context -> Optimize -> Int -> IO AST
optimizeGetUpperAsVector :: Context -> Optimize -> Int -> IO [AST]
optimizeGetLowerAsVector :: Context -> Optimize -> Int -> IO [AST]
optimizeToString :: Context -> Optimize -> IO String
optimizeFromString :: Context -> Optimize -> String -> IO ()
optimizeFromFile :: Context -> Optimize -> String -> IO ()
optimizeGetHelp :: Context -> Optimize -> IO String
optimizeGetAssertions :: Context -> Optimize -> IO [AST]
optimizeGetObjectives :: Context -> Optimize -> IO [AST]
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
mkSolver :: Context -> IO Solver
mkSimpleSolver :: Context -> IO Solver
mkSolverForLogic :: Context -> Logic -> IO Solver
solverGetHelp :: Context -> Solver -> IO String
solverSetParams :: Context -> Solver -> Params -> IO ()
solverPush :: Context -> Solver -> IO ()
solverPop :: Context -> Solver -> Int -> IO ()
solverReset :: Context -> Solver -> IO ()
solverGetNumScopes :: Context -> Solver -> IO Int
solverAssertCnstr :: Context -> Solver -> AST -> IO ()
solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
solverFromFile :: Context -> Solver -> String -> IO ()
solverFromString :: Context -> Solver -> String -> IO ()
solverGetAssertions :: Context -> Solver -> IO [AST]
solverCheck :: Context -> Solver -> IO Result
solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result
solverGetModel :: Context -> Solver -> IO Model
solverGetProof :: Context -> Solver -> IO AST
solverGetUnsatCore :: Context -> Solver -> IO [AST]
solverGetReasonUnknown :: Context -> Solver -> IO String
solverToString :: Context -> Solver -> IO String
solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)

Types

data Config Source #

A Z3 configuration object.

Instances

Instances details

Eq Config Source #
Instance details Defined in Z3.Base Methods (==) :: Config -> Config -> Bool # (/=) :: Config -> Config -> Bool #

data Context Source #

A Z3 logical context.

Instances

Instances details

Eq Context Source #
Instance details Defined in Z3.Base Methods (==) :: Context -> Context -> Bool # (/=) :: Context -> Context -> Bool #

data Symbol Source #

A Z3 symbol.

Used to name types, constants and functions.

Instances

Instances details

Storable Symbol Source #
Instance details Defined in Z3.Base Methods sizeOf :: Symbol -> Int # alignment :: Symbol -> Int # peekElemOff :: Ptr Symbol -> Int -> IO Symbol # pokeElemOff :: Ptr Symbol -> Int -> Symbol -> IO () # peekByteOff :: Ptr b -> Int -> IO Symbol # pokeByteOff :: Ptr b -> Int -> Symbol -> IO () # peek :: Ptr Symbol -> IO Symbol # poke :: Ptr Symbol -> Symbol -> IO () #
Show Symbol Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
Eq Symbol Source #
Instance details Defined in Z3.Base Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Ord Symbol Source #
Instance details Defined in Z3.Base Methods compare :: Symbol -> Symbol -> Ordering # (<) :: Symbol -> Symbol -> Bool # (<=) :: Symbol -> Symbol -> Bool # (>) :: Symbol -> Symbol -> Bool # (>=) :: Symbol -> Symbol -> Bool # max :: Symbol -> Symbol -> Symbol # min :: Symbol -> Symbol -> Symbol #

data AST Source #

A Z3 AST node.

This is the data-structure used in Z3 to represent terms, formulas and types.

Instances

Instances details

Show AST Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> AST -> ShowS # show :: AST -> String # showList :: [AST] -> ShowS #
Eq AST Source #
Instance details Defined in Z3.Base Methods (==) :: AST -> AST -> Bool # (/=) :: AST -> AST -> Bool #
Ord AST Source #
Instance details Defined in Z3.Base Methods compare :: AST -> AST -> Ordering # (<) :: AST -> AST -> Bool # (<=) :: AST -> AST -> Bool # (>) :: AST -> AST -> Bool # (>=) :: AST -> AST -> Bool # max :: AST -> AST -> AST # min :: AST -> AST -> AST #

data Sort Source #

A kind of AST representing types.

Instances

Instances details

Show Sort Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
Eq Sort Source #
Instance details Defined in Z3.Base Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Ord Sort Source #
Instance details Defined in Z3.Base Methods compare :: Sort -> Sort -> Ordering # (<) :: Sort -> Sort -> Bool # (<=) :: Sort -> Sort -> Bool # (>) :: Sort -> Sort -> Bool # (>=) :: Sort -> Sort -> Bool # max :: Sort -> Sort -> Sort # min :: Sort -> Sort -> Sort #

data TupleType Source #

A sort representing named tuples with associated functions

Constructors

TupleType
Fields tupleSort :: Sort tupleCons :: FuncDecl constructor function namedTupleProjs :: [(String, FuncDecl)] projection functions

data FuncDecl Source #

A kind of AST representing function symbols.

Instances

Instances details

Show FuncDecl Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> FuncDecl -> ShowS # show :: FuncDecl -> String # showList :: [FuncDecl] -> ShowS #
Eq FuncDecl Source #
Instance details Defined in Z3.Base Methods (==) :: FuncDecl -> FuncDecl -> Bool # (/=) :: FuncDecl -> FuncDecl -> Bool #
Ord FuncDecl Source #
Instance details Defined in Z3.Base Methods compare :: FuncDecl -> FuncDecl -> Ordering # (<) :: FuncDecl -> FuncDecl -> Bool # (<=) :: FuncDecl -> FuncDecl -> Bool # (>) :: FuncDecl -> FuncDecl -> Bool # (>=) :: FuncDecl -> FuncDecl -> Bool # max :: FuncDecl -> FuncDecl -> FuncDecl # min :: FuncDecl -> FuncDecl -> FuncDecl #

data App Source #

A kind of AST representing constant and function declarations.

Instances

Instances details

Show App Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> App -> ShowS # show :: App -> String # showList :: [App] -> ShowS #
Eq App Source #
Instance details Defined in Z3.Base Methods (==) :: App -> App -> Bool # (/=) :: App -> App -> Bool #
Ord App Source #
Instance details Defined in Z3.Base Methods compare :: App -> App -> Ordering # (<) :: App -> App -> Bool # (<=) :: App -> App -> Bool # (>) :: App -> App -> Bool # (>=) :: App -> App -> Bool # max :: App -> App -> App # min :: App -> App -> App #

data Pattern Source #

A kind of AST representing pattern and multi-patterns to guide quantifier instantiation.

Instances

Instances details

Show Pattern Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #
Eq Pattern Source #
Instance details Defined in Z3.Base Methods (==) :: Pattern -> Pattern -> Bool # (/=) :: Pattern -> Pattern -> Bool #
Ord Pattern Source #
Instance details Defined in Z3.Base Methods compare :: Pattern -> Pattern -> Ordering # (<) :: Pattern -> Pattern -> Bool # (<=) :: Pattern -> Pattern -> Bool # (>) :: Pattern -> Pattern -> Bool # (>=) :: Pattern -> Pattern -> Bool # max :: Pattern -> Pattern -> Pattern # min :: Pattern -> Pattern -> Pattern #

data Constructor Source #

A type contructor for a (recursive) datatype.

Instances

Instances details

Show Constructor Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Constructor -> ShowS # show :: Constructor -> String # showList :: [Constructor] -> ShowS #
Eq Constructor Source #
Instance details Defined in Z3.Base Methods (==) :: Constructor -> Constructor -> Bool # (/=) :: Constructor -> Constructor -> Bool #
Ord Constructor Source #
Instance details Defined in Z3.Base Methods compare :: Constructor -> Constructor -> Ordering # (<) :: Constructor -> Constructor -> Bool # (<=) :: Constructor -> Constructor -> Bool # (>) :: Constructor -> Constructor -> Bool # (>=) :: Constructor -> Constructor -> Bool # max :: Constructor -> Constructor -> Constructor # min :: Constructor -> Constructor -> Constructor #

data Model Source #

A model for the constraints asserted into the logical context.

Instances

Instances details

Eq Model Source #
Instance details Defined in Z3.Base Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #

data FuncInterp Source #

An interpretation of a function in a model.

Instances

Instances details

Eq FuncInterp Source #
Instance details Defined in Z3.Base Methods (==) :: FuncInterp -> FuncInterp -> Bool # (/=) :: FuncInterp -> FuncInterp -> Bool #

data FuncEntry Source #

Representation of the value of a Z3_func_interp at a particular point.

Instances

Instances details

Eq FuncEntry Source #
Instance details Defined in Z3.Base Methods (==) :: FuncEntry -> FuncEntry -> Bool # (/=) :: FuncEntry -> FuncEntry -> Bool #

data Params Source #

A Z3 parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

Instances

Instances details

Eq Params Source #
Instance details Defined in Z3.Base Methods (==) :: Params -> Params -> Bool # (/=) :: Params -> Params -> Bool #

data Solver Source #

A Z3 solver engine.

A(n) (incremental) solver, possibly specialized by a particular tactic or logic.

Instances

Instances details

Eq Solver Source #
Instance details Defined in Z3.Base Methods (==) :: Solver -> Solver -> Bool # (/=) :: Solver -> Solver -> Bool #

data SortKind Source #

Different kinds of Z3 types.

Constructors

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

Instances

Instances details

Show SortKind Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> SortKind -> ShowS # show :: SortKind -> String # showList :: [SortKind] -> ShowS #
Eq SortKind Source #
Instance details Defined in Z3.Base Methods (==) :: SortKind -> SortKind -> Bool # (/=) :: SortKind -> SortKind -> Bool #

data ASTKind Source #

Different kinds of Z3 AST nodes.

Constructors

Z3_NUMERAL_AST
Z3_APP_AST
Z3_VAR_AST
Z3_QUANTIFIER_AST
Z3_SORT_AST
Z3_FUNC_DECL_AST
Z3_UNKNOWN_AST

Instances

Instances details

Show ASTKind Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> ASTKind -> ShowS # show :: ASTKind -> String # showList :: [ASTKind] -> ShowS #
Eq ASTKind Source #
Instance details Defined in Z3.Base Methods (==) :: ASTKind -> ASTKind -> Bool # (/=) :: ASTKind -> ASTKind -> Bool #

data Tactic Source #

A tactic

Instances

Instances details

Eq Tactic Source #
Instance details Defined in Z3.Base Methods (==) :: Tactic -> Tactic -> Bool # (/=) :: Tactic -> Tactic -> Bool #

data ApplyResult Source #

A result of applying a tactic

Instances

Instances details

Eq ApplyResult Source #
Instance details Defined in Z3.Base Methods (==) :: ApplyResult -> ApplyResult -> Bool # (/=) :: ApplyResult -> ApplyResult -> Bool #

data Goal Source #

A goal (aka problem)

Instances

Instances details

Eq Goal Source #
Instance details Defined in Z3.Base Methods (==) :: Goal -> Goal -> Bool # (/=) :: Goal -> Goal -> Bool #

Satisfiability result

data Result Source #

Result of a satisfiability check.

This corresponds to the z3_lbool type in the C API.

Constructors

Sat
Unsat
Undef

Instances

Instances details

Read Result Source #
Instance details Defined in Z3.Base Methods readsPrec :: Int -> ReadS Result # readList :: ReadS [Result] # readPrec :: ReadPrec Result # readListPrec :: ReadPrec [Result] #
Show Result Source #
Instance details Defined in Z3.Base Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #
Eq Result Source #
Instance details Defined in Z3.Base Methods (==) :: Result -> Result -> Bool # (/=) :: Result -> Result -> Bool #
Ord Result Source #
Instance details Defined in Z3.Base Methods compare :: Result -> Result -> Ordering # (<) :: Result -> Result -> Bool # (<=) :: Result -> Result -> Bool # (>) :: Result -> Result -> Bool # (>=) :: Result -> Result -> Bool # max :: Result -> Result -> Result # min :: Result -> Result -> Result #

Algebraic Numbers

algebraicIsValue :: Context -> AST -> IO Bool Source #

algebraicIsPos :: Context -> AST -> IO Bool Source #

algebraicIsNeg :: Context -> AST -> IO Bool Source #

algebraicIsZero :: Context -> AST -> IO Bool Source #

algebraicSign :: Context -> AST -> IO Int Source #

algebraicAdd :: Context -> AST -> AST -> IO AST Source #

algebraicSub :: Context -> AST -> AST -> IO AST Source #

algebraicMul :: Context -> AST -> AST -> IO AST Source #

algebraicDiv :: Context -> AST -> AST -> IO AST Source #

algebraicRoot :: Context -> AST -> Int -> IO AST Source #

algebraicPower :: Context -> AST -> Int -> IO AST Source #

algebraicLt :: Context -> AST -> AST -> IO Bool Source #

algebraicGt :: Context -> AST -> AST -> IO Bool Source #

algebraicLe :: Context -> AST -> AST -> IO Bool Source #

algebraicGe :: Context -> AST -> AST -> IO Bool Source #

algebraicEq :: Context -> AST -> AST -> IO Bool Source #

algebraicNeq :: Context -> AST -> AST -> IO Bool Source #

algebraicRoots :: Context -> AST -> [AST] -> IO [AST] Source #

algebraicEval :: Context -> AST -> [AST] -> IO Int Source #

Global Parameters

globalParamSet :: String -> String -> IO () Source #

globalParamResetAll :: IO () Source #

globalParamGet :: String -> IO (Maybe String) Source #

Create configuration

mkConfig :: IO Config Source #

Create a configuration.

See withConfig.

delConfig :: Config -> IO () Source #

Delete a configuration.

See withConfig.

setParamValue :: Config -> String -> String -> IO () Source #

Set a configuration parameter.

Helpers

withConfig :: (Config -> IO a) -> IO a Source #

Run a computation using a temporally created configuration.

Note that the configuration object can be thrown away once it has been used to create the Z3 Context.

Create context

mkContext :: Config -> IO Context Source #

Create a context using the given configuration.

Z3_del_context is called by Haskell's garbage collector before freeing the Context object.

withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r Source #

Parameters

mkParams :: Context -> IO Params Source #

Create a Z3 (empty) parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO () Source #

Add a Boolean parameter k with value v to the parameter set p.

paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO () Source #

Add a unsigned parameter k with value v to the parameter set p.

paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO () Source #

Add a double parameter k with value v to the parameter set p.

paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO () Source #

Add a symbol parameter k with value v to the parameter set p.

paramsToString :: Context -> Params -> IO String Source #

Convert a parameter set into a string.

This function is mainly used for printing the contents of a parameter set.

Symbols

mkIntSymbol :: Integral int => Context -> int -> IO Symbol Source #

Create a Z3 symbol using an integer.

mkIntSymbol c i requires 0 <= i < 2^30

mkStringSymbol :: Context -> String -> IO Symbol Source #

Create a Z3 symbol using a String.

Sorts

mkUninterpretedSort :: Context -> Symbol -> IO Sort Source #

Create a free (uninterpreted) type using the given name (symbol).

Two free types are considered the same iff the have the same name.

mkBoolSort :: Context -> IO Sort Source #

Create the boolean type.

This type is used to create propositional variables and predicates.

mkIntSort :: Context -> IO Sort Source #

Create the integer type.

This is the type of arbitrary precision integers. A machine integer can be represented using bit-vectors, see mkBvSort.

mkRealSort :: Context -> IO Sort Source #

Create the real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

mkBvSort :: Integral int => Context -> int -> IO Sort Source #

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

mkBvSort c sz requires sz >= 0

mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort Source #

Create a finite-domain type.

mkArraySort :: Context -> Sort -> Sort -> IO Sort Source #

Create an array type

We usually represent the array type as: [domain -> range]. Arrays are usually used to model the heap/memory in software verification.

mkArraySortN :: Context -> [Sort] -> Sort -> IO Sort Source #

Create an array type with N arguments.

mkTupleSort Source #

Arguments

:: Context	Context
-> Symbol	Name of the sort
-> [(Symbol, Sort)]	Name and sort of each field
-> IO (Sort, FuncDecl, [FuncDecl])	Resulting sort, and function declarations for the constructor and projections.

Create a tuple type

A tuple with n fields has a constructor and n projections. This function will also declare the constructor and projection functions.

mkTupleType :: Context -> Symbol -> [(String, Sort)] -> IO TupleType Source #

Like mkTupleSort but wraps the result in a TupleType record

mkTuple :: Context -> TupleType -> [AST] -> IO AST Source #

Create an instance of the tuple sort wrapped in TupleType

mkIndexTuple :: Context -> TupleType -> Int -> AST -> IO AST Source #

Project the i-th field of the given tuple,

mkProjTuple :: Context -> TupleType -> String -> AST -> IO AST Source #

Project a field of the given tuple by name,

mkEnumerationSort Source #

Arguments

:: Context	logical context
-> Symbol	name of the enumeration sort
-> [Symbol]	names of the enumerated elements
-> IO (Sort, [FuncDecl], [FuncDecl])	the created enumeration sort, `enum_consts`, `enum_testers`

Create a enumeration sort.

An enumeration sort with n elements. This function will also declare the functions corresponding to the enumerations:

enum_consts: constants corresponding to the enumerated elements.
enum_testers: predicates testing if terms of the enumeration sort correspond to an enumeration.

mkListSort Source #

Arguments

:: Context	Context
-> Symbol	name of the list sort
-> Sort	sort of list elements
-> IO (Sort, FuncDecl, FuncDecl, FuncDecl, FuncDecl, FuncDecl, FuncDecl)	the created list sort, `nilDecl` `isnilDecl`, `consDecl`, `isconsDecl` `headDecl`, `tailDecl`

Create a list sort.

A list sort over elem_sort. This function declares the corresponding constructors and testers for lists:

nilDecl: declaration for the empty list
isnilDecl: test for the empty list
consDecl: declaration for a cons cell
isconsDecl: cons cell test
headDecl: list head
tailDecl: list tail

mkConstructor Source #

Arguments

:: Context	Context
-> Symbol	Name of the constructor
-> Symbol	Name of recognizer function
-> [(Symbol, Maybe Sort, Int)]	Name, sort option, and sortRefs
-> IO Constructor

Create a contructor

mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort Source #

Create datatype, such as lists, trees, records, enumerations or unions of records.

The datatype may be recursive. Returns the datatype sort.

mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO [Sort] Source #

Create mutually recursive datatypes, such as a tree and forest.

Returns the datatype sorts

mkSetSort :: Context -> Sort -> IO Sort Source #

Create an set type with a given domain type

Constants and Applications

mkFuncDecl Source #

Arguments

:: Context	Logical context.
-> Symbol	Name of the function (or constant).
-> [Sort]	Function domain (empty for constants).
-> Sort	Return sort of the function.
-> IO FuncDecl

Declare a constant or function.

mkApp :: Context -> FuncDecl -> [AST] -> IO AST Source #

Create a constant or function application.

mkConst :: Context -> Symbol -> Sort -> IO AST Source #

Declare and create a constant.

This is a shorthand for: do xd <- mkFunDecl c x [] s; mkApp c xd []

mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl Source #

Declare a fresh constant or function.

mkFreshConst Source #

Arguments

:: Context	Logical context.
-> String	Prefix.
-> Sort	Sort of the constant.
-> IO AST

Declare and create a fresh constant.

mkRecFuncDecl Source #

Arguments

:: Context	Logical context.
-> Symbol	Name of the function (or constant).
-> [Sort]	Function domain (empty for constants).
-> Sort	Return sort of the function.
-> IO FuncDecl

Declare a recursive function.

addRecDef Source #

Arguments

:: Context	Logical context.
-> FuncDecl	Declaration of the function being defined.
-> [AST]	Constants to use as the function's formal arguments.
-> AST	Body of the function to define
-> IO ()

Define the body of a recursive function. Declare it first with mkRecFuncDecl

Helpers

mkVar :: Context -> Symbol -> Sort -> IO AST Source #

Declare and create a variable (aka constant).

An alias for mkConst.

mkBoolVar :: Context -> Symbol -> IO AST Source #

Declarate and create a variable of sort bool.

See mkVar.

mkRealVar :: Context -> Symbol -> IO AST Source #

Declarate and create a variable of sort real.

See mkVar.

mkIntVar :: Context -> Symbol -> IO AST Source #

Declarate and create a variable of sort int.

See mkVar.

mkBvVar Source #

Arguments

:: Context
-> Symbol
-> Int	bit-width
-> IO AST

Declarate and create a variable of sort bit-vector.

See mkVar.

mkFreshVar :: Context -> String -> Sort -> IO AST Source #

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

mkFreshBoolVar :: Context -> String -> IO AST Source #

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

mkFreshRealVar :: Context -> String -> IO AST Source #

Declarate and create a fresh variable of sort real.

See mkFreshVar.

mkFreshIntVar :: Context -> String -> IO AST Source #

Declarate and create a fresh variable of sort int.

See mkFreshVar.

mkFreshBvVar Source #

Arguments

:: Context
-> String
-> Int	bit-width
-> IO AST

Declarate and create a fresh variable of sort bit-vector.

See mkFreshVar.

Propositional Logic and Equality

mkTrue :: Context -> IO AST Source #

Create an AST node representing true.

mkFalse :: Context -> IO AST Source #

Create an AST node representing false.

mkEq :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing l = r.

mkNot :: Context -> AST -> IO AST Source #

Create an AST node representing not(a).

mkIte :: Context -> AST -> AST -> AST -> IO AST Source #

Create an AST node representing an if-then-else: ite(t1, t2, t3).

mkIff :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing t1 iff t2.

mkImplies :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing t1 implies t2.

mkXor :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing t1 xor t2.

mkAnd :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] and ... and args[num_args-1].

mkOr :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] or ... or args[num_args-1].

mkDistinct :: Context -> [AST] -> IO AST Source #

The distinct construct is used for declaring the arguments pairwise distinct.

That is, and [ args!!i /= args!!j | i <- [0..length(args)-1], j <- [i+1..length(args)-1] ]

Requires a non-empty list.

mkDistinct1 :: Context -> NonEmpty AST -> IO AST Source #

Same as mkDistinct but type-safe.

Helpers

mkBool :: Context -> Bool -> IO AST Source #

Create an AST node representing the given boolean.

Arithmetic: Integers and Reals

mkAdd :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] + ... + args[num_args-1].

mkMul :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] * ... * args[num_args-1].

mkSub :: Context -> [AST] -> IO AST Source #

Create an AST node representing args[0] - ... - args[num_args - 1].

Requires a non-empty list.

mkSub1 :: Context -> NonEmpty AST -> IO AST Source #

Same as mkSub but type-safe.

mkUnaryMinus :: Context -> AST -> IO AST Source #

Create an AST node representing -arg.

mkDiv :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 div arg2.

mkMod :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 mod arg2.

mkRem :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 rem arg2.

mkPower :: Context -> AST -> AST -> IO AST Source #

Create an AST node representing arg1 ^ arg2.

mkLt :: Context -> AST -> AST -> IO AST Source #

Create less than.

mkLe :: Context -> AST -> AST -> IO AST Source #

Create less than or equal to.

mkGt :: Context -> AST -> AST -> IO AST Source #

Create greater than.

mkGe :: Context -> AST -> AST -> IO AST Source #

Create greater than or equal to.

mkInt2Real :: Context -> AST -> IO AST Source #

Coerce an integer to a real.

mkReal2Int :: Context -> AST -> IO AST Source #

Coerce a real to an integer.

mkIsInt :: Context -> AST -> IO AST Source #

Check if a real number is an integer.

Bit-vectors

mkBvnot :: Context -> AST -> IO AST Source #

Bitwise negation.

mkBvredand :: Context -> AST -> IO AST Source #

Take conjunction of bits in vector, return vector of length 1.

mkBvredor :: Context -> AST -> IO AST Source #

Take disjunction of bits in vector, return vector of length 1.

mkBvand :: Context -> AST -> AST -> IO AST Source #

Bitwise and.

mkBvor :: Context -> AST -> AST -> IO AST Source #

Bitwise or.

mkBvxor :: Context -> AST -> AST -> IO AST Source #

Bitwise exclusive-or.

mkBvnand :: Context -> AST -> AST -> IO AST Source #

Bitwise nand.

mkBvnor :: Context -> AST -> AST -> IO AST Source #

Bitwise nor.

mkBvxnor :: Context -> AST -> AST -> IO AST Source #

Bitwise xnor.

mkBvneg :: Context -> AST -> IO AST Source #

Standard two's complement unary minus.

mkBvadd :: Context -> AST -> AST -> IO AST Source #

Standard two's complement addition.

mkBvsub :: Context -> AST -> AST -> IO AST Source #

Standard two's complement subtraction.

mkBvmul :: Context -> AST -> AST -> IO AST Source #

Standard two's complement multiplication.

mkBvudiv :: Context -> AST -> AST -> IO AST Source #

Unsigned division.

mkBvsdiv :: Context -> AST -> AST -> IO AST Source #

Two's complement signed division.

mkBvurem :: Context -> AST -> AST -> IO AST Source #

Unsigned remainder.

mkBvsrem :: Context -> AST -> AST -> IO AST Source #

Two's complement signed remainder (sign follows dividend).

mkBvsmod :: Context -> AST -> AST -> IO AST Source #

Two's complement signed remainder (sign follows divisor).

mkBvult :: Context -> AST -> AST -> IO AST Source #

Unsigned less than.

mkBvslt :: Context -> AST -> AST -> IO AST Source #

Two's complement signed less than.

mkBvule :: Context -> AST -> AST -> IO AST Source #

Unsigned less than or equal to.

mkBvsle :: Context -> AST -> AST -> IO AST Source #

Two's complement signed less than or equal to.

mkBvuge :: Context -> AST -> AST -> IO AST Source #

Unsigned greater than or equal to.

mkBvsge :: Context -> AST -> AST -> IO AST Source #

Two's complement signed greater than or equal to.

mkBvugt :: Context -> AST -> AST -> IO AST Source #

Unsigned greater than.

mkBvsgt :: Context -> AST -> AST -> IO AST Source #

Two's complement signed greater than.

mkConcat :: Context -> AST -> AST -> IO AST Source #

Concatenate the given bit-vectors.

mkExtract :: Context -> Int -> Int -> AST -> IO AST Source #

Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.

mkSignExt :: Context -> Int -> AST -> IO AST Source #

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

mkZeroExt :: Context -> Int -> AST -> IO AST Source #

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

mkRepeat :: Context -> Int -> AST -> IO AST Source #

Repeat the given bit-vector up length i.

mkBvshl :: Context -> AST -> AST -> IO AST Source #

Shift left.

mkBvlshr :: Context -> AST -> AST -> IO AST Source #

Logical shift right.

mkBvashr :: Context -> AST -> AST -> IO AST Source #

Arithmetic shift right.

mkRotateLeft :: Context -> Int -> AST -> IO AST Source #

Rotate bits of t1 to the left i times.

mkRotateRight :: Context -> Int -> AST -> IO AST Source #

Rotate bits of t1 to the right i times.

mkExtRotateLeft :: Context -> AST -> AST -> IO AST Source #

Rotate bits of t1 to the left t2 times.

mkExtRotateRight :: Context -> AST -> AST -> IO AST Source #

Rotate bits of t1 to the right t2 times.

mkInt2bv :: Context -> Int -> AST -> IO AST Source #

Create an n bit bit-vector from the integer argument t1.

mkBv2int :: Context -> AST -> Bool -> IO AST Source #

Create an integer from the bit-vector argument t1.

If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.

mkBvnegNoOverflow :: Context -> AST -> IO AST Source #

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source #

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source #

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST Source #

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Arrays

mkSelect Source #

Arguments

:: Context
-> AST	Array.
-> AST	Index of the array to read.
-> IO AST

Array read. The argument a is the array and i is the index of the array that gets read.

mkStore Source #

Arguments

:: Context
-> AST	Array.
-> AST	Index i of the array.
-> AST	New value for i.
-> IO AST

Array update.

The result of this function is an array that is equal to the input array (with respect to select) on all indices except for i, where it maps to v.

The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details.

mkConstArray Source #

Arguments

:: Context
-> Sort	Domain sort of the array.
-> AST	Value v that the array maps to.
-> IO AST

Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

mkMap Source #

Arguments

:: Context
-> FuncDecl	Function f.
-> [AST]	List of arrays.
-> IO AST

Map a function f on the the argument arrays.

The n nodes args must be of array sorts [domain -> range_i]. The function declaration f must have type range_1 .. range_n -> range. The sort of the result is [domain -> range].

mkArrayDefault Source #

Arguments

:: Context
-> AST	Array.
-> IO AST

Access the array default value.

Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Sets

mkEmptySet Source #

Arguments

:: Context
-> Sort	Domain sort of the set.
-> IO AST

Create the empty set.

mkFullSet Source #

Arguments

:: Context
-> Sort	Domain sort of the set.
-> IO AST

Create the full set.

mkSetAdd Source #

Arguments

:: Context
-> AST	Set.
-> AST	Element.
-> IO AST

Add an element to a set.

mkSetDel Source #

Arguments

:: Context
-> AST	Set.
-> AST	Element.
-> IO AST

Remove an element from a set.

mkSetUnion :: Context -> [AST] -> IO AST Source #

Take the union of a list of sets.

mkSetIntersect :: Context -> [AST] -> IO AST Source #

Take the intersection of a list of sets.

mkSetDifference Source #

Arguments

:: Context
-> AST	First set.
-> AST	Second set.
-> IO AST

Take the set difference between two sets.

mkSetComplement Source #

Arguments

:: Context
-> AST	Set.
-> IO AST

Take the complement of a set.

mkSetMember Source #

Arguments

:: Context
-> AST	Element.
-> AST	Set.
-> IO AST

Check for set membership.

mkSetSubset Source #

Arguments

:: Context
-> AST	First set.
-> AST	Second set.
-> IO AST

Check if the first set is a subset of the second set.

Numerals

mkNumeral :: Context -> String -> Sort -> IO AST Source #

Create a numeral of a given sort.

mkReal Source #

Arguments

:: Context
-> Int	numerator
-> Int	denominator (/= 0)
-> IO AST

Create a real from a fraction.

mkInt :: Context -> Int -> Sort -> IO AST Source #