RatNum.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.math.BigInteger;
 
public class RatNum extends RealExpr
{
    public IntNum getNumerator()
    {
        return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(),
                getNativeObject()));
    }
 
    public IntNum getDenominator()
    {
        return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(),
                getNativeObject()));
    }
 
    public BigInteger getBigIntNumerator()
    {
        IntNum n = getNumerator();
        return new BigInteger(n.toString());
    }
 
    public BigInteger getBigIntDenominator()
    {
        IntNum n = getDenominator();
        return new BigInteger(n.toString());
    }
 
    public String toDecimalString(int precision)
    {
        return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
                precision);
    }
 
    @Override
    public String toString() {
        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
    }
 
    RatNum(Context ctx, long obj)
    {
        super(ctx, obj);
    }
}