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
75 public String toBinaryString()
76 {
77 return Native.getNumeralBinaryString(getContext().nCtx(), getNativeObject());
78 }
79
80 BitVecNum(Context ctx, long obj)
81 {
82 super(ctx, obj);
83 }
84}
com.microsoft.z3.BitVecExpr
Definition: BitVecExpr.java:24
com.microsoft.z3.BitVecNum
Definition: BitVecNum.java:26
com.microsoft.z3.BitVecNum.getLong
long getLong()
Definition: BitVecNum.java:46
com.microsoft.z3.BitVecNum.toBinaryString
String toBinaryString()
Definition: BitVecNum.java:75
com.microsoft.z3.BitVecNum.getInt
int getInt()
Definition: BitVecNum.java:32
com.microsoft.z3.BitVecNum.getBigInteger
BigInteger getBigInteger()
Definition: BitVecNum.java:58
com.microsoft.z3.BitVecNum.toString
String toString()
Definition: BitVecNum.java:67
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693