Z3 |

Public Member Functions
FPSort Class Reference
Inheritance diagram for FPSort:

## Public Member Functions
| FPSort (Context ctx, long obj)
| FPSort (Context ctx, int ebits, int sbits)
int | getEBits ()
int | getSBits ()
Public Member Functions inherited from Sort
boolean | equals (Object o)
int | hashCode ()
int | getId ()
Z3_sort_kind | getSortKind ()
Symbol | getName ()
String | toString ()
Sort | translate (Context ctx)
Public Member Functions inherited from AST
boolean | equals (Object o)
int | compareTo (AST other)
int | hashCode ()
int | getId ()
AST | translate (Context ctx)
Z3_ast_kind | getASTKind ()
boolean | isExpr ()
boolean | isApp ()
boolean | isVar ()
boolean | isQuantifier ()
boolean | isSort ()
boolean | isFuncDecl ()
String | toString ()
String | getSExpr ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

A FloatingPoint sort

Definition at line 22 of file FPSort.java.

## Constructor & Destructor Documentation

## ◆ FPSort() [1/2]

FPSort | ( | Context | ctx,
|  | long | obj
| ) |  |
| inline

Definition at line 25 of file FPSort.java.

26 {
27 super(ctx, obj);
28 }

## ◆ FPSort() [2/2]

FPSort | ( | Context | ctx,
|  | int | ebits,
|  | int | sbits
| ) |  |
| inline

Definition at line 30 of file FPSort.java.

31 {
32 super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));
33 }

## Member Function Documentation

## ◆ getEBits()

int getEBits | ( |  | ) |
| inline

The number of exponent bits.

Definition at line 38 of file FPSort.java.

38 {
39 return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());
40 }

## ◆ getSBits()

int getSBits | ( |  | ) |
| inline

The number of significand bits.

Definition at line 45 of file FPSort.java.

45 {
46 return Native.fpaGetSbits(getContext().nCtx(), getNativeObject());
47 }