Z3
Public Member Functions
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 ()
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object 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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

The FloatingPoint RoundingMode sort

Definition at line 22 of file FPRMSort.java.

Constructor & Destructor Documentation

FPRMSort ( Context  ctx)
inline

Definition at line 25 of file FPRMSort.java.

26  {
27  super(ctx, Native.mkFpaRoundingModeSort(ctx.nCtx()));
28  }
FPRMSort ( Context  ctx,
long  obj 
)
inline

Definition at line 30 of file FPRMSort.java.

31  {
32  super(ctx, obj);
33  }