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 
43  return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
44  }
45 
53  public long getSignificandUInt64()
54  {
55  Native.LongPtr res = new Native.LongPtr();
56  if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res))
57  throw new Z3Exception("Significand is not a 64 bit unsigned integer");
58  return res.value;
59  }
60 
65  public String getExponent() {
66  return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
67  }
68 
73  public long getExponentInt64() {
74  Native.LongPtr res = new Native.LongPtr();
75  if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res))
76  throw new Z3Exception("Exponent is not a 64 bit integer");
77  return res.value;
78  }
79 
80  public FPNum(Context ctx, long obj)
81  {
82  super(ctx, obj);
83  }
84 
88  public String toString()
89  {
90  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
91  }
92 
93 }
String getSignificand()
Definition: FPNum.java:42
long getExponentInt64()
Definition: FPNum.java:73
boolean getSign()
Definition: FPNum.java:29
static String fpaGetNumeralExponentString(long a0, long a1)
Definition: Native.java:6110
String getExponent()
Definition: FPNum.java:65
static String getNumeralString(long a0, long a1)
Definition: Native.java:2816
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2)
Definition: Native.java:6119
static String fpaGetNumeralSignificandString(long a0, long a1)
Definition: Native.java:6092
long getSignificandUInt64()
Definition: FPNum.java:53
FPNum(Context ctx, long obj)
Definition: FPNum.java:80
static boolean fpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
Definition: Native.java:6101
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
Definition: Native.java:6083
def String(name, ctx=None)
Definition: z3py.py:9443