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
int compareTo (AST other)
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
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  }