Z3
src/api/java/RatNum.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines