Z3
BitVecNum.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import java.math.BigInteger;
21 
25 public class BitVecNum extends BitVecExpr
26 {
32  public int getInt()
33  {
34  Native.IntPtr res = new Native.IntPtr();
35  if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
36  throw new Z3Exception("Numeral is not an int");
37  }
38  return res.value;
39  }
40 
46  public long getLong()
47  {
48  Native.LongPtr res = new Native.LongPtr();
49  if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
50  throw new Z3Exception("Numeral is not a long");
51  }
52  return res.value;
53  }
54 
58  public BigInteger getBigInteger()
59  {
60  return new BigInteger(this.toString());
61  }
62 
66  @Override
67  public String toString()
68  {
69  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
70  }
71 
72  BitVecNum(Context ctx, long obj)
73  {
74  super(ctx, obj);
75  }
76 }
com.microsoft.z3.BitVecNum.getLong
long getLong()
Definition: BitVecNum.java:46
com.microsoft.z3.BitVecNum.toString
String toString()
Definition: BitVecNum.java:67
com.microsoft.z3.BitVecNum.getInt
int getInt()
Definition: BitVecNum.java:32
com.microsoft.z3.Native.IntPtr
Definition: Native.java:5
com.microsoft.z3.BitVecNum
Definition: BitVecNum.java:25
com.microsoft.z3.BitVecExpr
Definition: BitVecExpr.java:23
com.microsoft.z3.Native.getNumeralInt64
static boolean getNumeralInt64(long a0, long a1, LongPtr a2)
Definition: Native.java:3262
com.microsoft.z3.Native.LongPtr
Definition: Native.java:6
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.getNumeralString
static String getNumeralString(long a0, long a1)
Definition: Native.java:3181
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.Native.getNumeralInt
static boolean getNumeralInt(long a0, long a1, IntPtr a2)
Definition: Native.java:3235
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.BitVecNum.getBigInteger
BigInteger getBigInteger()
Definition: BitVecNum.java:58
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111