Z3
Sort.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
22 
26 public class Sort extends AST
27 {
33  public boolean equals(Object o)
34  {
35  Sort casted = null;
36 
37  try {
38  casted = Sort.class.cast(o);
39  } catch (ClassCastException e) {
40  return false;
41  }
42 
43  return
44  (this == casted) ||
45  (this != null) &&
46  (casted != null) &&
47  (getContext().nCtx() == casted.getContext().nCtx()) &&
48  (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
49  }
50 
56  public int hashCode()
57  {
58  return super.hashCode();
59  }
60 
64  public int getId()
65  {
66  return Native.getSortId(getContext().nCtx(), getNativeObject());
67  }
68 
73  {
74  return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
75  getNativeObject()));
76  }
77 
81  public Symbol getName()
82  {
83  return Symbol.create(getContext(),
84  Native.getSortName(getContext().nCtx(), getNativeObject()));
85  }
86 
90  public String toString()
91  {
92  try
93  {
94  return Native.sortToString(getContext().nCtx(), getNativeObject());
95  } catch (Z3Exception e)
96  {
97  return "Z3Exception: " + e.getMessage();
98  }
99  }
100 
104  Sort(Context ctx, long obj)
105  {
106  super(ctx, obj);
107  }
108 
109  void checkNativeObject(long obj)
110  {
111  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
112  .toInt())
113  throw new Z3Exception("Underlying object is not a sort");
114  super.checkNativeObject(obj);
115  }
116 
117  static Sort create(Context ctx, long obj)
118  {
119  Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
120  switch (sk)
121  {
122  case Z3_ARRAY_SORT:
123  return new ArraySort(ctx, obj);
124  case Z3_BOOL_SORT:
125  return new BoolSort(ctx, obj);
126  case Z3_BV_SORT:
127  return new BitVecSort(ctx, obj);
128  case Z3_DATATYPE_SORT:
129  return new DatatypeSort(ctx, obj);
130  case Z3_INT_SORT:
131  return new IntSort(ctx, obj);
132  case Z3_REAL_SORT:
133  return new RealSort(ctx, obj);
135  return new UninterpretedSort(ctx, obj);
137  return new FiniteDomainSort(ctx, obj);
138  case Z3_RELATION_SORT:
139  return new RelationSort(ctx, obj);
141  return new FPSort(ctx, obj);
143  return new FPRMSort(ctx, obj);
144  default:
145  throw new Z3Exception("Unknown sort kind");
146  }
147  }
148 }
String toString()
Definition: Sort.java:90
def RealSort(ctx=None)
Definition: z3py.py:2655
static int getSortKind(long a0, long a1)
Definition: Native.java:2090
static final Z3_sort_kind fromInt(int v)
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
static long getSortName(long a0, long a1)
Definition: Native.java:2054
boolean equals(Object o)
Definition: Sort.java:33
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
Z3_sort_kind getSortKind()
Definition: Sort.java:72
def ArraySort(d, r)
Definition: z3py.py:4004
def IntSort(ctx=None)
Definition: z3py.py:2639
Symbol getName()
Definition: Sort.java:81
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2081
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3460
static int getAstKind(long a0, long a1)
Definition: Native.java:2495
static int getSortId(long a0, long a1)
Definition: Native.java:2063
static String sortToString(long a0, long a1)
Definition: Native.java:3130
def BoolSort(ctx=None)
Definition: z3py.py:1346