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 
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 
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 }
boolean isSubnormal()
Definition: FPNum.java:155
static String fpaGetNumeralExponentString(long a0, long a1, boolean a2)
Definition: Native.java:6568
boolean isPositive()
Definition: FPNum.java:165
static boolean fpaIsNumeralNan(long a0, long a1)
Definition: Native.java:6460
static boolean fpaIsNumeralZero(long a0, long a1)
Definition: Native.java:6478
static boolean fpaIsNumeralPositive(long a0, long a1)
Definition: Native.java:6505
String getSignificand()
Definition: FPNum.java:51
boolean isNormal()
Definition: FPNum.java:145
boolean getSign()
Definition: FPNum.java:29
static long fpaGetNumeralExponentBv(long a0, long a1, boolean a2)
Definition: Native.java:6586
static boolean fpaIsNumeralNormal(long a0, long a1)
Definition: Native.java:6487
static boolean fpaIsNumeralNegative(long a0, long a1)
Definition: Native.java:6514
static long fpaGetNumeralSignificandBv(long a0, long a1)
Definition: Native.java:6532
BitVecExpr getSignBV()
Definition: FPNum.java:41
static long fpaGetNumeralSignBv(long a0, long a1)
Definition: Native.java:6523
static String getNumeralString(long a0, long a1)
Definition: Native.java:3168
static boolean fpaIsNumeralSubnormal(long a0, long a1)
Definition: Native.java:6496
String getExponent(boolean biased)
Definition: FPNum.java:84
static boolean fpaIsNumeralInf(long a0, long a1)
Definition: Native.java:6469
static String fpaGetNumeralSignificandString(long a0, long a1)
Definition: Native.java:6550
BitVecExpr getExponentBV(boolean biased)
Definition: FPNum.java:105
long getExponentInt64(boolean biased)
Definition: FPNum.java:93
boolean isNegative()
Definition: FPNum.java:175
long getSignificandUInt64()
Definition: FPNum.java:62
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2, boolean a3)
Definition: Native.java:6577
FPNum(Context ctx, long obj)
Definition: FPNum.java:181
static boolean fpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
Definition: Native.java:6559
BitVecExpr getSignificandBV()
Definition: FPNum.java:75
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
Definition: Native.java:6541
def String(name, ctx=None)
Definition: z3py.py:10087