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{
30 public IntNum getNumerator()
31 {
32 return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(),
33 getNativeObject()));
34 }
35
39 public IntNum getDenominator()
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}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.IntNum
Definition: IntNum.java:26
com.microsoft.z3.IntNum.toString
String toString()
Definition: IntNum.java:66
com.microsoft.z3.RatNum
Definition: RatNum.java:26
com.microsoft.z3.RatNum.getBigIntDenominator
BigInteger getBigIntDenominator()
Definition: RatNum.java:57
com.microsoft.z3.RatNum.getDenominator
IntNum getDenominator()
Definition: RatNum.java:39
com.microsoft.z3.RatNum.getBigIntNumerator
BigInteger getBigIntNumerator()
Definition: RatNum.java:48
com.microsoft.z3.RatNum.toDecimalString
String toDecimalString(int precision)
Definition: RatNum.java:68
com.microsoft.z3.RatNum.toString
String toString()
Definition: RatNum.java:78
com.microsoft.z3.RatNum.getNumerator
IntNum getNumerator()
Definition: RatNum.java:30
com.microsoft.z3.RealExpr
Definition: RealExpr.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693