Z3 |

FPNum.java
Go to the documentation of this file.
1/*++
2 Copyright (c) 2013 Microsoft Corporation
3
4 Module Name:
5
6 FPNum.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
22 public 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
41 public BitVecExpr getSignBV() {
42 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
43 }
44
51 public String getSignificand() {
52 return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
53 }
54
62 public long getSignificandUInt64()
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
75 public BitVecExpr getSignificandBV() {
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
189 public String toString()
190 {
191 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
192 }
193}
com.microsoft.z3.BitVecExpr
Definition: BitVecExpr.java:24
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.FPExpr
Definition: FPExpr.java:23
com.microsoft.z3.FPNum
Definition: FPNum.java:23
com.microsoft.z3.FPNum.isInf
boolean isInf()
Definition: FPNum.java:125
com.microsoft.z3.FPNum.isNaN
boolean isNaN()
Definition: FPNum.java:115
com.microsoft.z3.FPNum.isZero
boolean isZero()
Definition: FPNum.java:135
com.microsoft.z3.FPNum.getExponentBV
BitVecExpr getExponentBV(boolean biased)
Definition: FPNum.java:105
com.microsoft.z3.FPNum.getSign
boolean getSign()
Definition: FPNum.java:29
com.microsoft.z3.FPNum.isPositive
boolean isPositive()
Definition: FPNum.java:165
com.microsoft.z3.FPNum.isSubnormal
boolean isSubnormal()
Definition: FPNum.java:155
com.microsoft.z3.FPNum.isNormal
boolean isNormal()
Definition: FPNum.java:145
com.microsoft.z3.FPNum.getExponent
String getExponent(boolean biased)
Definition: FPNum.java:84
com.microsoft.z3.FPNum.getSignificand
String getSignificand()
Definition: FPNum.java:51
com.microsoft.z3.FPNum.getExponentInt64
long getExponentInt64(boolean biased)
Definition: FPNum.java:93
com.microsoft.z3.FPNum.getSignificandBV
BitVecExpr getSignificandBV()
Definition: FPNum.java:75
com.microsoft.z3.FPNum.FPNum
FPNum(Context ctx, long obj)
Definition: FPNum.java:181
com.microsoft.z3.FPNum.toString
String toString()
Definition: FPNum.java:189
com.microsoft.z3.FPNum.getSignBV
BitVecExpr getSignBV()
Definition: FPNum.java:41
com.microsoft.z3.FPNum.isNegative
boolean isNegative()
Definition: FPNum.java:175
com.microsoft.z3.FPNum.getSignificandUInt64
long getSignificandUInt64()
Definition: FPNum.java:62
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693