Z3
FPNum.java
Go to the documentation of this file.
1/*++
2Copyright (c) 2013 Microsoft Corporation
3
4Module Name:
5
6 FPNum.java
7
8Abstract:
9
10Author:
11
12 Christoph Wintersteiger (cwinter) 2013-06-10
13
14Notes:
15
16--*/
17package com.microsoft.z3;
18
22public class FPNum extends FPExpr
23{
29 public boolean getSign() {
30 Native.IntPtr res = new Native.IntPtr();
31 if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res))
32 throw new Z3Exception("Sign is not a Boolean value");
33 return res.value != 0;
34 }
35
42 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
43 }
44
52 return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
53 }
54
63 {
64 Native.LongPtr res = new Native.LongPtr();
65 if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res))
66 throw new Z3Exception("Significand is not a 64 bit unsigned integer");
67 return res.value;
68 }
69
76 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
77 }
78
84 public String getExponent(boolean biased) {
85 return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
86 }
87
93 public long getExponentInt64(boolean biased) {
94 Native.LongPtr res = new Native.LongPtr();
95 if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased))
96 throw new Z3Exception("Exponent is not a 64 bit integer");
97 return res.value;
98 }
99
105 public BitVecExpr getExponentBV(boolean biased) {
106 return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
107 }
108
109
115 public boolean isNaN()
116 {
117 return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
118 }
119
125 public boolean isInf()
126 {
127 return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
128 }
129
135 public boolean isZero()
136 {
137 return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
138 }
139
145 public boolean isNormal()
146 {
147 return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
148 }
149
155 public boolean isSubnormal()
156 {
157 return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
158 }
159
165 public boolean isPositive()
166 {
167 return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
168 }
169
175 public boolean isNegative()
176 {
177 return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
178 }
179
180
181 public FPNum(Context ctx, long obj)
182 {
183 super(ctx, obj);
184 }
185
190 {
191 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
192 }
193}
BitVecExpr getExponentBV(boolean biased)
Definition: FPNum.java:105
boolean getSign()
Definition: FPNum.java:29
boolean isPositive()
Definition: FPNum.java:165
boolean isSubnormal()
Definition: FPNum.java:155
boolean isNormal()
Definition: FPNum.java:145
String getExponent(boolean biased)
Definition: FPNum.java:84
String getSignificand()
Definition: FPNum.java:51
long getExponentInt64(boolean biased)
Definition: FPNum.java:93
BitVecExpr getSignificandBV()
Definition: FPNum.java:75
FPNum(Context ctx, long obj)
Definition: FPNum.java:181
BitVecExpr getSignBV()
Definition: FPNum.java:41
boolean isNegative()
Definition: FPNum.java:175
long getSignificandUInt64()
Definition: FPNum.java:62
static boolean fpaIsNumeralZero(long a0, long a1)
Definition: Native.java:6497
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
Definition: Native.java:6560
static String fpaGetNumeralSignificandString(long a0, long a1)
Definition: Native.java:6569
static long fpaGetNumeralSignificandBv(long a0, long a1)
Definition: Native.java:6551
static boolean fpaIsNumeralNan(long a0, long a1)
Definition: Native.java:6479
static boolean fpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
Definition: Native.java:6578
static boolean fpaIsNumeralSubnormal(long a0, long a1)
Definition: Native.java:6515
static boolean fpaIsNumeralNormal(long a0, long a1)
Definition: Native.java:6506
static long fpaGetNumeralSignBv(long a0, long a1)
Definition: Native.java:6542
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2, boolean a3)
Definition: Native.java:6596
static String getNumeralString(long a0, long a1)
Definition: Native.java:3179
static boolean fpaIsNumeralPositive(long a0, long a1)
Definition: Native.java:6524
static boolean fpaIsNumeralNegative(long a0, long a1)
Definition: Native.java:6533
static boolean fpaIsNumeralInf(long a0, long a1)
Definition: Native.java:6488
static String fpaGetNumeralExponentString(long a0, long a1, boolean a2)
Definition: Native.java:6587
static long fpaGetNumeralExponentBv(long a0, long a1, boolean a2)
Definition: Native.java:6605
def String(name, ctx=None)
Definition: z3py.py:10085