/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    FPNum.java

Abstract:

Author:

    Christoph Wintersteiger (cwinter) 2013-06-10

Notes:
    
--*/
package com.microsoft.z3;

/**
 * FloatingPoint Numerals
 */
public class FPNum extends FPExpr
{    
    /**
     * Retrieves the sign of a floating-point literal     
     * Remarks: returns true if the numeral is negative 
     * @throws Z3Exception 
     */
    public boolean getSign() {
        Native.IntPtr res = new Native.IntPtr();
        if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Sign is not a Boolean value");
        return res.value != 0;
    }

    /**
     * The sign of a floating-point numeral as a bit-vector expression
     * Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments.
     * @throws Z3Exception 
     */
    public BitVecExpr getSignBV() {
        return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
    }

    /**
     * The significand value of a floating-point numeral as a string
     * Remarks: The significand s is always 0 < s < 2.0; the resulting string is long
     * enough to represent the real significand precisely.
     * @throws Z3Exception 
     **/
    public String getSignificand() {
        return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
    }

    /**
     * The significand value of a floating-point numeral as a UInt64
     * Remarks: This function extracts the significand bits, without the 
     * hidden bit or normalization. Throws an exception if the
     * significand does not fit into a UInt64.
     * @throws Z3Exception
     **/
    public long getSignificandUInt64()
    {
        Native.LongPtr res = new Native.LongPtr();
        if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Significand is not a 64 bit unsigned integer");
        return res.value;
    }

    /**
     * The significand of a floating-point numeral as a bit-vector expression
     * Remarks: NaN is an invalid argument.
     * @throws Z3Exception 
     */
    public BitVecExpr getSignificandBV() {
        return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
    }
    
    /**
     * Return the exponent value of a floating-point numeral as a string
     * Remarks: NaN is an invalid argument.
     * @throws Z3Exception 
     */
    public String getExponent(boolean biased) {
        return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
    }

    /**
     * Return the exponent value of a floating-point numeral as a signed 64-bit integer
     * Remarks: NaN is an invalid argument.
     * @throws Z3Exception 
     */
    public long getExponentInt64(boolean biased)  {
        Native.LongPtr res = new Native.LongPtr();
        if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased))
            throw new Z3Exception("Exponent is not a 64 bit integer");
        return res.value;
    }

    /**
     * The exponent of a floating-point numeral as a bit-vector expression
     * Remarks: NaN is an invalid argument.
     * @throws Z3Exception 
     */
    public BitVecExpr getExponentBV(boolean biased) {
        return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
    }

    
    /**
     * Indicates whether the numeral is a NaN.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isNaN()
    {
        return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
    }    

    /**
     * Indicates whether the numeral is a +oo or -oo.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isInf()
    {
        return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
    }
    
    /**
     * Indicates whether the numeral is +zero or -zero.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isZero()
    {
        return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
    }

    /**
     * Indicates whether the numeral is normal.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isNormal()
    {
        return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
    }
    
    /**
     * Indicates whether the numeral is subnormal.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isSubnormal()
    {
        return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
    }

    /**
     * Indicates whether the numeral is positive.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isPositive()
    {
        return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
    }

    /**
     * Indicates whether the numeral is negative.
     * @throws Z3Exception on error
     * @return a boolean
     **/
    public boolean isNegative()
    {
        return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
    }

    
    public FPNum(Context ctx, long obj)
    {
        super(ctx, obj);
    }
    
    /**
     * Returns a string representation of the numeral.
     */           
    public String toString()
    {
        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
    }    
}