FPRMSort Class Reference

Inheritance diagram for FPRMSort:

Public Member Functions
	FPRMSort (Context ctx)
	FPRMSort (Context ctx, long obj)
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

The FloatingPoint RoundingMode sort

Definition at line 22 of file FPRMSort.java.

Constructor & Destructor Documentation

FPRMSort() [1/2]

FPRMSort ( Context  ctx )

inline

Definition at line 25 of file FPRMSort.java.

    {        
        super(ctx, Native.mkFpaRoundingModeSort(ctx.nCtx()));
    }

FPRMSort() [2/2]

FPRMSort ( Context  ctx, long  obj  )

inline

Definition at line 30 of file FPRMSort.java.

    {
        super(ctx, obj); 
    }