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  @Override
78  public String toString() {
79  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
80  }
81 
82  RatNum(Context ctx, long obj)
83  {
84  super(ctx, obj);
85  }
86 }
BigInteger getBigIntNumerator()
Definition: RatNum.java:48
static long getDenominator(long a0, long a1)
Definition: Native.java:2843
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition: Native.java:2825
static String getNumeralString(long a0, long a1)
Definition: Native.java:2816
IntNum getDenominator()
Definition: RatNum.java:39
static long getNumerator(long a0, long a1)
Definition: Native.java:2834
String toDecimalString(int precision)
Definition: RatNum.java:68
BigInteger getBigIntDenominator()
Definition: RatNum.java:57
def String(name, ctx=None)
Definition: z3py.py:9443