Type Aliases
The following type aliases are available globally.
-
Type alias for a generic
Z3Ast
bit-vector instance that features an underlying AST that is a non-specific sized bit vector.Declaration
Swift
public typealias AnyZ3BitVector = Z3Ast<AnyBitVectorSort>
-
A specialized BitVector AST type.
Declaration
Swift
public typealias Z3BitVector<T> = Z3Ast<T> where T : BitVectorSort
-
A typealias for a
Z3BitVector
withBitVectorSort1
sort.Declaration
Swift
public typealias Z3BitVector1 = Z3BitVector<BitVectorSort1>
-
A typealias for a
Z3BitVector
withBitVectorSort128
sort.Declaration
Swift
public typealias Z3BitVector128 = Z3BitVector<BitVectorSort128>
-
A typealias for a
Z3BitVector
withBitVectorSort32
sort.Declaration
Swift
public typealias Z3BitVector32 = Z3BitVector<BitVectorSort32>
-
A typealias for a
Z3BitVector
withBitVectorSort64
sort.Declaration
Swift
public typealias Z3BitVector64 = Z3BitVector<BitVectorSort64>
-
A typealias for a
Z3BitVector
withBitVectorSortUnsigned32
sort.Declaration
Swift
public typealias Z3BitVectorU32 = Z3BitVector<BitVectorSortUnsigned32>
-
A typealias for a
Z3BitVector
withBitVectorSortUnsigned64
sort.Declaration
Swift
public typealias Z3BitVectorU64 = Z3BitVector<BitVectorSortUnsigned64>
-
A 64-bit precision floating-point AST type.
Declaration
Swift
public typealias Z3Double = Z3FloatingPoint<Double>
-
A 32-bit precision floating-point AST type.
Declaration
Swift
public typealias Z3Float = Z3FloatingPoint<Float>
-
A typealias for general Floating Point-sort ASTs
Declaration
Swift
public typealias Z3FloatingPoint<T> = Z3Ast<T> where T : FloatingSort
-
A typealias for a Z3Ast with a
RoundingModeSort
sort.Declaration
Swift
public typealias Z3RoundingMode = Z3Ast<RoundingModeSort>
-
A Boolean AST type.
Declaration
Swift
public typealias Z3Bool = Z3Ast<Bool>
-
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Declaration
Swift
public typealias Z3AstKind = Z3_ast_kind
-
Z3 pretty printing modes (See #Z3_set_ast_print_mode).
Declaration
Swift
public typealias Z3AstPrintMode = Z3_ast_print_mode
-
The different kinds of interpreted function kinds.
- Z3_OP_PR_CLAUSE_TRAIL, Clausal proof trail of additions and deletions
Declaration
Swift
public typealias Z3DeclKind = Z3_decl_kind
-
Z3 error codes (See #Z3_get_error_code).
- Z3_FILE_ACCESS_ERRROR: A file could not be accessed.
Declaration
Swift
public typealias Z3ErrorCode = Z3_error_code
-
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.
Declaration
Swift
public typealias Z3GoalPrec = Z3_goal_prec
-
Lifted Boolean type:
false
,undefined
,true
.Declaration
Swift
public typealias Z3LBool = Z3_lbool
-
The different kinds of parameters that can be associated with parameter sets. (see #Z3_mk_params).
Declaration
Swift
public typealias Z3ParamKind = Z3_param_kind
-
The different kinds of parameters that can be associated with function symbols. \sa Z3_get_decl_num_parameters \sa Z3_get_decl_parameter_kind
Declaration
Swift
public typealias Z3ParameterKind = Z3_parameter_kind
-
The different kinds of Z3 types (See #Z3_get_sort_kind).
Declaration
Swift
public typealias Z3SortKind = Z3_sort_kind
-
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3_get_symbol_kind).
\sa Z3_mk_int_symbol \sa Z3_mk_string_symbol
Declaration
Swift
public typealias Z3SymbolKind = Z3_symbol_kind
-
A bit vector of length 8
Declaration
Swift
public typealias BitVectorSort8 = BitVectorOfInt<Int8>
-
A bit vector of length 16
Declaration
Swift
public typealias BitVectorSort16 = BitVectorOfInt<Int16>
-
A bit vector of length 32
Declaration
Swift
public typealias BitVectorSort32 = BitVectorOfInt<Int32>
-
A bit vector of length 64
Declaration
Swift
public typealias BitVectorSort64 = BitVectorOfInt<Int64>
-
A bit vector of length 8, unsigned.
Declaration
Swift
public typealias BitVectorSortUnsigned8 = BitVectorOfInt<UInt8>
-
A bit vector of length 16, unsigned.
Declaration
Swift
public typealias BitVectorSortUnsigned16 = BitVectorOfInt<UInt16>
-
A bit vector of length 32, unsigned.
Declaration
Swift
public typealias BitVectorSortUnsigned32 = BitVectorOfInt<UInt32>
-
A bit vector of length 64, unsigned.
Declaration
Swift
public typealias BitVectorSortUnsigned64 = BitVectorOfInt<UInt64>
-
Declaration
Swift
public typealias Z3CString = Z3_string