Type Aliases Reference


                    
                    
                    Z3Int

An integer AST type. Note that this is not the same as a machine integer.

Declaration

Swift

public typealias Z3Int = Z3Ast<IntSort>


                    
                    
                    Z3Real

A real number AST type. Note that this type is not a floating point number.

Declaration

Swift

public typealias Z3Real = Z3Ast<RealSort>


                    
                    
                    AnyZ3BitVector

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>


                    
                    
                    Z3BitVector

A specialized BitVector AST type.

Declaration

Swift

public typealias Z3BitVector<T> = Z3Ast<T> where T : BitVectorSort


                    
                    
                    Z3BitVector1

A typealias for a Z3BitVector with BitVectorSort1 sort.

Declaration

Swift

public typealias Z3BitVector1 = Z3BitVector<BitVectorSort1>


                    
                    
                    Z3BitVector128

A typealias for a Z3BitVector with BitVectorSort128 sort.

Declaration

Swift

public typealias Z3BitVector128 = Z3BitVector<BitVectorSort128>


                    
                    
                    Z3BitVector32

A typealias for a Z3BitVector with BitVectorSort32 sort.

Declaration

Swift

public typealias Z3BitVector32 = Z3BitVector<BitVectorSort32>


                    
                    
                    Z3BitVector64

A typealias for a Z3BitVector with BitVectorSort64 sort.

Declaration

Swift

public typealias Z3BitVector64 = Z3BitVector<BitVectorSort64>


                    
                    
                    Z3BitVectorU32

A typealias for a Z3BitVector with BitVectorSortUnsigned32 sort.

Declaration

Swift

public typealias Z3BitVectorU32 = Z3BitVector<BitVectorSortUnsigned32>


                    
                    
                    Z3BitVectorU64

A typealias for a Z3BitVector with BitVectorSortUnsigned64 sort.

Declaration

Swift

public typealias Z3BitVectorU64 = Z3BitVector<BitVectorSortUnsigned64>


                    
                    
                    AnyZ3FloatingPoint

Type alias for a generic Z3Ast floating-point instance that features an underlying AST that is a non-specific floating-point number.

Declaration

Swift

public typealias AnyZ3FloatingPoint = Z3Ast<AnyFPSort>


                    
                    
                    Z3Double

A 64-bit precision floating-point AST type.

Declaration

Swift

public typealias Z3Double = Z3FloatingPoint<Double>


                    
                    
                    Z3Float

A 32-bit precision floating-point AST type.

Declaration

Swift

public typealias Z3Float = Z3FloatingPoint<Float>


                    
                    
                    Z3FloatingPoint

A typealias for general Floating Point-sort ASTs

Declaration

Swift

public typealias Z3FloatingPoint<T> = Z3Ast<T> where T : FloatingSort


                    
                    
                    Z3RoundingMode

A typealias for a Z3Ast with a RoundingModeSort sort.

Declaration

Swift

public typealias Z3RoundingMode = Z3Ast<RoundingModeSort>


                    
                    
                    Z3Array

An Array AST type

Declaration

Swift

public typealias Z3Array<D, R> = Z3Ast<ArraySort<D, R>> where D : SortKind, R : SortKind


                    
                    
                    Z3Bool

A Boolean AST type.

Declaration

Swift

public typealias Z3Bool = Z3Ast<Bool>


                    
                    
                    Z3Char

A unicode character AST.

Declaration

Swift

public typealias Z3Char = Z3Ast<CharSort>


                    
                    
                    Z3Set

A Set AST type. Equivalent to an array of domain T and range Bool.

Declaration

Swift

public typealias Z3Set<T> = Z3Ast<SetSort<T>> where T : SortKind


                    
                    
                    Z3String

A String type AST. Equivalent to the sort of a sequence of char.

Declaration

Swift

public typealias Z3String = Z3Seq<CharSort>


                    
                    
                    Z3AstKind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Declaration

Swift

public typealias Z3AstKind = Z3_ast_kind


                    
                    
                    Z3AstPrintMode

Z3 pretty printing modes (See #Z3_set_ast_print_mode).

Declaration

Swift

public typealias Z3AstPrintMode = Z3_ast_print_mode


                    
                    
                    Z3DeclKind

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


                    
                    
                    Z3ErrorCode

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


                    
                    
                    Z3GoalPrec

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


                    
                    
                    Z3LBool

Lifted Boolean type: false, undefined, true.

Declaration

Swift

public typealias Z3LBool = Z3_lbool


                    
                    
                    Z3ParamKind

The different kinds of parameters that can be associated with parameter sets. (see #Z3_mk_params).

Declaration

Swift

public typealias Z3ParamKind = Z3_param_kind


                    
                    
                    Z3ParameterKind

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


                    
                    
                    Z3SortKind

The different kinds of Z3 types (See #Z3_get_sort_kind).

Declaration

Swift

public typealias Z3SortKind = Z3_sort_kind


                    
                    
                    Z3SymbolKind

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


                    
                    
                    BitVectorSort8

A bit vector of length 8

Declaration

Swift

public typealias BitVectorSort8 = BitVectorOfInt<Int8>


                    
                    
                    BitVectorSort16

A bit vector of length 16

Declaration

Swift

public typealias BitVectorSort16 = BitVectorOfInt<Int16>


                    
                    
                    BitVectorSort32

A bit vector of length 32

Declaration

Swift

public typealias BitVectorSort32 = BitVectorOfInt<Int32>


                    
                    
                    BitVectorSort64

A bit vector of length 64

Declaration

Swift

public typealias BitVectorSort64 = BitVectorOfInt<Int64>


                    
                    
                    BitVectorSortUnsigned8

A bit vector of length 8, unsigned.

Declaration

Swift

public typealias BitVectorSortUnsigned8 = BitVectorOfInt<UInt8>


                    
                    
                    BitVectorSortUnsigned16

A bit vector of length 16, unsigned.

Declaration

Swift

public typealias BitVectorSortUnsigned16 = BitVectorOfInt<UInt16>


                    
                    
                    BitVectorSortUnsigned32

A bit vector of length 32, unsigned.

Declaration

Swift

public typealias BitVectorSortUnsigned32 = BitVectorOfInt<UInt32>


                    
                    
                    BitVectorSortUnsigned64

A bit vector of length 64, unsigned.

Declaration

Swift

public typealias BitVectorSortUnsigned64 = BitVectorOfInt<UInt64>


                    
                    
                    SetSort

Represents a Set sort, specializing an Array sort with a range of Bool sort.

Declaration

Swift

public typealias SetSort<T> = ArraySort<T, Bool> where T : SortKind


                    
                    
                    Z3CString

Declaration

Swift

public typealias Z3CString = Z3_string