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()
49  {
50  IntNum n = getNumerator();
51  return new BigInteger(n.toString());
52  }
53 
57  public BigInteger getBigIntDenominator()
58  {
59  IntNum n = getDenominator();
60  return new BigInteger(n.toString());
61  }
62 
68  public String toDecimalString(int precision)
69  {
70  return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
71  precision);
72  }
73 
77  public String toString()
78  {
79  try
80  {
81  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
82  } catch (Z3Exception e)
83  {
84  return "Z3Exception: " + e.getMessage();
85  }
86  }
87 
88  RatNum(Context ctx, long obj)
89  {
90  super(ctx, obj);
91  }
92 }
BigInteger getBigIntNumerator()
Definition: RatNum.java:48
static long getDenominator(long a0, long a1)
Definition: Native.java:2576
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition: Native.java:2558
static String getNumeralString(long a0, long a1)
Definition: Native.java:2549
IntNum getDenominator()
Definition: RatNum.java:39
static long getNumerator(long a0, long a1)
Definition: Native.java:2567
String toDecimalString(int precision)
Definition: RatNum.java:68
BigInteger getBigIntDenominator()
Definition: RatNum.java:57