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 
20 
24 public class FPRMNum extends FPRMExpr {
25 
31 
37 
43 
49 
55 
61 
67 
72  public boolean isRTN() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
73 
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.FPRMNum.isRNE
boolean isRNE()
Definition: FPRMNum.java:36
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.FPRMNum.isRoundNearestTiesToAway
boolean isRoundNearestTiesToAway()
Definition: FPRMNum.java:42
com.microsoft.z3.FPRMNum
Definition: FPRMNum.java:24
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO
Z3_OP_FPA_RM_TOWARD_ZERO
Definition: Z3_decl_kind.java:225
com.microsoft
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition: Z3_decl_kind.java:221
com.microsoft.z3.FPRMNum.isRoundNearestTiesToEven
boolean isRoundNearestTiesToEven()
Definition: FPRMNum.java:30
com.microsoft.z3.enumerations.Z3_decl_kind
Definition: Z3_decl_kind.java:13
com.microsoft.z3.FPRMNum.isRTP
boolean isRTP()
Definition: FPRMNum.java:60
com.microsoft.z3.FPRMNum.isRoundTowardNegative
boolean isRoundTowardNegative()
Definition: FPRMNum.java:66
com.microsoft.z3.FPRMNum.isRoundTowardZero
boolean isRoundTowardZero()
Definition: FPRMNum.java:78
com.microsoft.z3.FPRMNum.isRNA
boolean isRNA()
Definition: FPRMNum.java:48
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.FPRMNum.isRTN
boolean isRTN()
Definition: FPRMNum.java:72
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition: Z3_decl_kind.java:222
com.microsoft.z3.FPRMNum.FPRMNum
FPRMNum(Context ctx, long obj)
Definition: FPRMNum.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE
Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition: Z3_decl_kind.java:223
com
com.microsoft.z3.Expr.getFuncDecl
FuncDecl getFuncDecl()
Definition: Expr.java:72
com.microsoft.z3.FuncDecl.getDeclKind
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:119
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.FPRMNum.isRTZ
boolean isRTZ()
Definition: FPRMNum.java:84
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE
Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition: Z3_decl_kind.java:224
com.microsoft.z3.AST.isApp
boolean isApp()
Definition: AST.java:131
com.microsoft.z3.FPRMNum.isRoundTowardPositive
boolean isRoundTowardPositive()
Definition: FPRMNum.java:54
com.microsoft.z3.FPRMExpr
Definition: FPRMExpr.java:23