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) ^ true)
32  throw new Z3Exception("Sign is not a Boolean value");
33  return res.value != 0;
34  }
35 
42  public String getSignificand() {
43  return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
44  }
45 
50  public String getExponent() {
51  return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
52  }
53 
58  public long getExponentInt64() {
59  Native.LongPtr res = new Native.LongPtr();
60  if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
61  throw new Z3Exception("Exponent is not a 64 bit integer");
62  return res.value;
63  }
64 
65  public FPNum(Context ctx, long obj)
66  {
67  super(ctx, obj);
68  }
69 
73  public String toString()
74  {
75  try
76  {
77  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
78  } catch (Z3Exception e)
79  {
80  return "Z3Exception: " + e.getMessage();
81  }
82  }
83 
84 }
String getSignificand()
Definition: FPNum.java:42
long getExponentInt64()
Definition: FPNum.java:58
boolean getSign()
Definition: FPNum.java:29
static String fpaGetNumeralExponentString(long a0, long a1)
Definition: Native.java:5899
String getExponent()
Definition: FPNum.java:50
static String getNumeralString(long a0, long a1)
Definition: Native.java:2495
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2)
Definition: Native.java:5908
static String fpaGetNumeralSignificandString(long a0, long a1)
Definition: Native.java:5890
FPNum(Context ctx, long obj)
Definition: FPNum.java:65
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
Definition: Native.java:5881