FPNum.java

Go to the documentation of this file.

/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    FPNum.java

Abstract:

Author:

    Christoph Wintersteiger (cwinter) 2013-06-10

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

public class FPNum extends FPExpr
{
    public boolean getSign() {
        Native.IntPtr res = new Native.IntPtr();
        if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true)                
            throw new Z3Exception("Sign is not a Boolean value");
        return res.value != 0;
    }

    public String getSignificand() {
        return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
    }

    public long getSignificandUInt64()
    {
        Native.LongPtr res = new Native.LongPtr();
        if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true)
            throw new Z3Exception("Significand is not a 64 bit unsigned integer");
        return res.value;
    }
    
    public String getExponent() {
        return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
    }

    public long getExponentInt64()  {
        Native.LongPtr res = new Native.LongPtr();
        if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
            throw new Z3Exception("Exponent is not a 64 bit integer");
        return res.value;
    }
    
    public FPNum(Context ctx, long obj)
    {
        super(ctx, obj);
    }
    
    public String toString()
    {
        try
        {
            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

}