Z3
FPRMNum.java
Go to the documentation of this file.
1/*++
2Copyright (c) 2013 Microsoft Corporation
3
4Module Name:
5
6 FPRMNum.java
7
8Abstract:
9
10Author:
11
12 Christoph Wintersteiger (cwinter) 2013-06-10
13
14Notes:
15
16--*/
17package com.microsoft.z3;
18
19import com.microsoft.z3.enumerations.Z3_decl_kind;
20
24public class FPRMNum extends FPRMExpr {
25
30 public boolean isRoundNearestTiesToEven() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
31
36 public boolean isRNE() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
37
42 public boolean isRoundNearestTiesToAway() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
43
48 public boolean isRNA() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
49
54 public boolean isRoundTowardPositive() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
55
60 public boolean isRTP() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
61
66 public boolean isRoundTowardNegative() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
67
72 public boolean isRTN() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
73
78 public boolean isRoundTowardZero() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
79
84 public boolean isRTZ() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
85
86 public FPRMNum(Context ctx, long obj) {
87 super(ctx, obj);
88 }
89
90}
FuncDecl< R > getFuncDecl()
Definition: Expr.java:76
boolean isRoundTowardPositive()
Definition: FPRMNum.java:54
boolean isRoundTowardZero()
Definition: FPRMNum.java:78
boolean isRoundNearestTiesToEven()
Definition: FPRMNum.java:30
boolean isRoundTowardNegative()
Definition: FPRMNum.java:66
boolean isRoundNearestTiesToAway()
Definition: FPRMNum.java:42
FPRMNum(Context ctx, long obj)
Definition: FPRMNum.java:86
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000