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 }
com.microsoft.z3.FPNum.isNaN
boolean isNaN()
Definition: FPNum.java:115
com.microsoft.z3.Native.fpaIsNumeralNormal
static boolean fpaIsNumeralNormal(long a0, long a1)
Definition: Native.java:6526
com.microsoft.z3.Native.fpaGetNumeralSignificandBv
static long fpaGetNumeralSignificandBv(long a0, long a1)
Definition: Native.java:6571
com.microsoft.z3.FPNum.getExponentInt64
long getExponentInt64(boolean biased)
Definition: FPNum.java:93
com.microsoft.z3.Native.IntPtr
Definition: Native.java:5
com.microsoft.z3.FPNum.FPNum
FPNum(Context ctx, long obj)
Definition: FPNum.java:181
com.microsoft.z3.Native.fpaGetNumeralSign
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
Definition: Native.java:6580
com.microsoft.z3.Native.fpaIsNumeralNegative
static boolean fpaIsNumeralNegative(long a0, long a1)
Definition: Native.java:6553
com.microsoft.z3.Native.fpaGetNumeralExponentInt64
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2, boolean a3)
Definition: Native.java:6616
com.microsoft.z3.FPNum.getSignBV
BitVecExpr getSignBV()
Definition: FPNum.java:41
com.microsoft.z3.Native.fpaGetNumeralExponentString
static String fpaGetNumeralExponentString(long a0, long a1, boolean a2)
Definition: Native.java:6607
com.microsoft.z3.FPNum.isSubnormal
boolean isSubnormal()
Definition: FPNum.java:155
com.microsoft.z3.FPNum.getExponentBV
BitVecExpr getExponentBV(boolean biased)
Definition: FPNum.java:105
com.microsoft.z3.FPNum.getSignificandBV
BitVecExpr getSignificandBV()
Definition: FPNum.java:75
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.BitVecExpr
Definition: BitVecExpr.java:24
com.microsoft.z3.Native.fpaIsNumeralSubnormal
static boolean fpaIsNumeralSubnormal(long a0, long a1)
Definition: Native.java:6535
com.microsoft.z3.Native.fpaGetNumeralExponentBv
static long fpaGetNumeralExponentBv(long a0, long a1, boolean a2)
Definition: Native.java:6625
com.microsoft.z3.FPExpr
Definition: FPExpr.java:23
com.microsoft.z3.Native.LongPtr
Definition: Native.java:6
com.microsoft.z3.FPNum.toString
String toString()
Definition: FPNum.java:189
com.microsoft.z3.Native.fpaIsNumeralInf
static boolean fpaIsNumeralInf(long a0, long a1)
Definition: Native.java:6508
com.microsoft.z3.FPNum.isNegative
boolean isNegative()
Definition: FPNum.java:175
com.microsoft.z3.FPNum.isInf
boolean isInf()
Definition: FPNum.java:125
com.microsoft.z3.Native.fpaGetNumeralSignificandString
static String fpaGetNumeralSignificandString(long a0, long a1)
Definition: Native.java:6589
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.fpaIsNumeralPositive
static boolean fpaIsNumeralPositive(long a0, long a1)
Definition: Native.java:6544
com.microsoft.z3.FPNum.getSignificand
String getSignificand()
Definition: FPNum.java:51
com.microsoft.z3.Native.getNumeralString
static String getNumeralString(long a0, long a1)
Definition: Native.java:3181
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Native.fpaIsNumeralZero
static boolean fpaIsNumeralZero(long a0, long a1)
Definition: Native.java:6517
com.microsoft.z3.FPNum
Definition: FPNum.java:23
com.microsoft.z3.FPNum.isZero
boolean isZero()
Definition: FPNum.java:135
com.microsoft.z3.FPNum.getSign
boolean getSign()
Definition: FPNum.java:29
com.microsoft.z3.Native.fpaIsNumeralNan
static boolean fpaIsNumeralNan(long a0, long a1)
Definition: Native.java:6499
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Native.fpaGetNumeralSignificandUint64
static boolean fpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
Definition: Native.java:6598
com.microsoft.z3.Native.fpaGetNumeralSignBv
static long fpaGetNumeralSignBv(long a0, long a1)
Definition: Native.java:6562
com.microsoft.z3.FPNum.isPositive
boolean isPositive()
Definition: FPNum.java:165
com.microsoft.z3.FPNum.getSignificandUInt64
long getSignificandUInt64()
Definition: FPNum.java:62
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111