IntNum.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.math.BigInteger;
 
public class IntNum extends IntExpr
{
 
    IntNum(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    public int getInt()
    {
        Native.IntPtr res = new Native.IntPtr();
        if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Numeral is not an int");
        return res.value;
    }
 
    public long getInt64()
    {
        Native.LongPtr res = new Native.LongPtr();
        if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Numeral is not an int64");
        return res.value;
    }
 
    public int getUint()
    {
        Native.IntPtr res = new Native.IntPtr();
        if (!Native.getNumeralUint(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Numeral is not a uint");
        return res.value;
    }
 
    public long getUint64()
    {
        Native.LongPtr res = new Native.LongPtr();
        if (!Native.getNumeralUint64(getContext().nCtx(), getNativeObject(), res))
            throw new Z3Exception("Numeral is not a uint64");
        return res.value;
    }
 
    public BigInteger getBigInteger()
    {
        return new BigInteger(this.toString());
    }
 
    public String toString() {
        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
    }
}