Z3 |

FPRMNum.java
Go to the documentation of this file.
1/*++
2 Copyright (c) 2013 Microsoft Corporation
3
4 Module Name:
5
6 FPRMNum.java
7
8 Abstract:
9
10 Author:
11
12 Christoph Wintersteiger (cwinter) 2013-06-10
13
14 Notes:
15
16--*/
17 package com.microsoft.z3;
18
19 import com.microsoft.z3.enumerations.Z3_decl_kind;
20
24 public 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}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Expr< FPRMSort >::getFuncDecl
FuncDecl< R > getFuncDecl()
Definition: Expr.java:76
com.microsoft.z3.FPRMExpr
Definition: FPRMExpr.java:23
com.microsoft.z3.FPRMNum
Definition: FPRMNum.java:24
com.microsoft.z3.FPRMNum.isRoundTowardPositive
boolean isRoundTowardPositive()
Definition: FPRMNum.java:54
com.microsoft.z3.FPRMNum.isRoundTowardZero
boolean isRoundTowardZero()
Definition: FPRMNum.java:78
com.microsoft.z3.FPRMNum.isRoundNearestTiesToEven
boolean isRoundNearestTiesToEven()
Definition: FPRMNum.java:30
com.microsoft.z3.FPRMNum.isRoundTowardNegative
boolean isRoundTowardNegative()
Definition: FPRMNum.java:66
com.microsoft.z3.FPRMNum.isRoundNearestTiesToAway
boolean isRoundNearestTiesToAway()
Definition: FPRMNum.java:42
com.microsoft.z3.FPRMNum.isRTN
boolean isRTN()
Definition: FPRMNum.java:72
com.microsoft.z3.FPRMNum.isRTP
boolean isRTP()
Definition: FPRMNum.java:60
com.microsoft.z3.FPRMNum.isRNA
boolean isRNA()
Definition: FPRMNum.java:48
com.microsoft.z3.FPRMNum.isRTZ
boolean isRTZ()
Definition: FPRMNum.java:84
com.microsoft.z3.FPRMNum.FPRMNum
FPRMNum(Context ctx, long obj)
Definition: FPRMNum.java:86
com.microsoft.z3.FPRMNum.isRNE
boolean isRNE()
Definition: FPRMNum.java:36
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000