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.

    {
        super(ctx, obj);        
    }

FPSort() [2/2]

FPSort ( Context  ctx, int  ebits, int  sbits  )

inline

Definition at line 30 of file FPSort.java.

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

Member Function Documentation

getEBits()

int getEBits ( )

inline

The number of exponent bits.

Definition at line 38 of file FPSort.java.

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

getSBits()

int getSBits ( )

inline

The number of significand bits.

Definition at line 45 of file FPSort.java.

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