00001 00018 package com.microsoft.z3; 00019 00020 import java.math.BigInteger; 00021 00025 public class RatNum extends RealExpr 00026 { 00030 public IntNum getNumerator() throws Z3Exception 00031 { 00032 return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(), 00033 getNativeObject())); 00034 } 00035 00039 public IntNum getDenominator() throws Z3Exception 00040 { 00041 return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(), 00042 getNativeObject())); 00043 } 00044 00048 public BigInteger getBigIntNumerator() throws Z3Exception 00049 { 00050 IntNum n = getNumerator(); 00051 return new BigInteger(n.toString()); 00052 } 00053 00057 public BigInteger getBigIntDenominator() throws Z3Exception 00058 { 00059 IntNum n = getDenominator(); 00060 return new BigInteger(n.toString()); 00061 } 00062 00067 public String toDecimalString(int precision) throws Z3Exception 00068 { 00069 return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(), 00070 precision); 00071 } 00072 00076 public String toString() 00077 { 00078 try 00079 { 00080 return Native.getNumeralString(getContext().nCtx(), getNativeObject()); 00081 } catch (Z3Exception e) 00082 { 00083 return "Z3Exception: " + e.getMessage(); 00084 } 00085 } 00086 00087 RatNum(Context ctx, long obj) throws Z3Exception 00088 { 00089 super(ctx, obj); 00090 } 00091 }