BitVecNum.java

Go to the documentation of this file.

package com.microsoft.z3;

import java.math.BigInteger;

public class BitVecNum extends BitVecExpr
{
    public int getInt()
    {
        Native.IntPtr res = new Native.IntPtr();
        if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
            throw new Z3Exception("Numeral is not an int");
        return res.value;
    }

    public long getLong()
    {
        Native.LongPtr res = new Native.LongPtr();
        if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
            throw new Z3Exception("Numeral is not a long");
        return res.value;
    }

    public BigInteger getBigInteger()
    {
        return new BigInteger(this.toString());
    }

    public String toString()
    {
        try
        {
            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

    BitVecNum(Context ctx, long obj)
    {
        super(ctx, obj);
    }
}