Z3
FiniteDomainNum.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import java.math.BigInteger;
21 
25 public class FiniteDomainNum extends FiniteDomainExpr
26 {
27 
28  FiniteDomainNum(Context ctx, long obj)
29  {
30  super(ctx, obj);
31  }
32 
36  public int getInt()
37  {
38  Native.IntPtr res = new Native.IntPtr();
39  if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
40  throw new Z3Exception("Numeral is not an int");
41  }
42  return res.value;
43  }
44 
48  public long getInt64()
49  {
50  Native.LongPtr res = new Native.LongPtr();
51  if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
52  throw new Z3Exception("Numeral is not an int64");
53  }
54  return res.value;
55  }
56 
60  public BigInteger getBigInteger()
61  {
62  return new BigInteger(this.toString());
63  }
64 
68  @Override
69  public String toString()
70  {
71  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
72  }
73 }
com.microsoft.z3.FiniteDomainNum.getBigInteger
BigInteger getBigInteger()
Definition: FiniteDomainNum.java:60
com.microsoft.z3.Native.IntPtr
Definition: Native.java:5
com.microsoft.z3.FiniteDomainNum.getInt
int getInt()
Definition: FiniteDomainNum.java:36
com.microsoft.z3.FiniteDomainNum.getInt64
long getInt64()
Definition: FiniteDomainNum.java:48
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.FiniteDomainNum.toString
String toString()
Definition: FiniteDomainNum.java:69
com.microsoft.z3.FiniteDomainExpr
Definition: FiniteDomainExpr.java:23
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.FiniteDomainNum
Definition: FiniteDomainNum.java:25
com.microsoft.z3.Context
Definition: Context.java:35
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111