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.BoolPtr res = new Native.BoolPtr();
        if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Sign is not a Boolean value");
        return res.value;
    }
 
    public BitVecExpr getSignBV() {
        return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
    }
 
    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))
            throw new Z3Exception("Significand is not a 64 bit unsigned integer");
        return res.value;
    }
 
    public BitVecExpr getSignificandBV() {
        return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
    }
    
    public String getExponent(boolean biased) {
        return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
    }
 
    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;
    }
 
    public BitVecExpr getExponentBV(boolean biased) {
        return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
    }
 
    
    public boolean isNaN()
    {
        return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
    }    
 
    public boolean isInf()
    {
        return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
    }
    
    public boolean isZero()
    {
        return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isNormal()
    {
        return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
    }
    
    public boolean isSubnormal()
    {
        return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isPositive()
    {
        return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isNegative()
    {
        return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
    }
 
    
    public FPNum(Context ctx, long obj)
    {
        super(ctx, obj);
    }
    
    public String toString()
    {
        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
    }    
}