Z3
RatNum.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import java.math.BigInteger;
21 
25 public class RatNum extends RealExpr
26 {
31  {
32  return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(),
33  getNativeObject()));
34  }
35 
40  {
41  return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(),
42  getNativeObject()));
43  }
44 
48  public BigInteger getBigIntNumerator() throws Z3Exception
49  {
50  IntNum n = getNumerator();
51  return new BigInteger(n.toString());
52  }
53 
57  public BigInteger getBigIntDenominator() throws Z3Exception
58  {
59  IntNum n = getDenominator();
60  return new BigInteger(n.toString());
61  }
62 
67  public String toDecimalString(int precision) throws Z3Exception
68  {
69  return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
70  precision);
71  }
72 
76  public String toString()
77  {
78  try
79  {
80  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
81  } catch (Z3Exception e)
82  {
83  return "Z3Exception: " + e.getMessage();
84  }
85  }
86 
87  RatNum(Context ctx, long obj) throws Z3Exception
88  {
89  super(ctx, obj);
90  }
91 }
BigInteger getBigIntNumerator()
Definition: RatNum.java:48
static long getDenominator(long a0, long a1)
Definition: Native.java:2453
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition: Native.java:2435
static String getNumeralString(long a0, long a1)
Definition: Native.java:2426
IntNum getDenominator()
Definition: RatNum.java:39
static long getNumerator(long a0, long a1)
Definition: Native.java:2444
String toDecimalString(int precision)
Definition: RatNum.java:67
BigInteger getBigIntDenominator()
Definition: RatNum.java:57