Z3
RatNum.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import java.math.BigInteger;
21
25public 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 {
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 getBigIntDenominator()
Definition: RatNum.java:57
IntNum getDenominator()
Definition: RatNum.java:39
BigInteger getBigIntNumerator()
Definition: RatNum.java:48
String toDecimalString(int precision)
Definition: RatNum.java:68
def String(name, ctx=None)
Definition: z3py.py:10693