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 (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 ()
 

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.

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

§ FPRMSort() [2/2]

FPRMSort ( Context  ctx,
long  obj 
)
inline

Definition at line 30 of file FPRMSort.java.

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