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 {
28  /* Overloaded operators are not translated. */
29 
35  public boolean equals(Object o)
36  {
37  Sort casted = null;
38 
39  try {
40  casted = Sort.class.cast(o);
41  } catch (ClassCastException e) {
42  return false;
43  }
44 
45  return this.getNativeObject() == casted.getNativeObject();
46  }
47 
53  public int hashCode()
54  {
55  return super.hashCode();
56  }
57 
61  public int getId() throws Z3Exception
62  {
63  return Native.getSortId(getContext().nCtx(), getNativeObject());
64  }
65 
70  {
71  return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
72  getNativeObject()));
73  }
74 
78  public Symbol getName() throws Z3Exception
79  {
80  return Symbol.create(getContext(),
81  Native.getSortName(getContext().nCtx(), getNativeObject()));
82  }
83 
87  public String toString()
88  {
89  try
90  {
91  return Native.sortToString(getContext().nCtx(), getNativeObject());
92  } catch (Z3Exception e)
93  {
94  return "Z3Exception: " + e.getMessage();
95  }
96  }
97 
101  protected Sort(Context ctx) throws Z3Exception
102  {
103  super(ctx);
104  {
105  }
106  }
107 
108  Sort(Context ctx, long obj) throws Z3Exception
109  {
110  super(ctx, obj);
111  {
112  }
113  }
114 
115  void checkNativeObject(long obj) throws Z3Exception
116  {
117  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
118  .toInt())
119  throw new Z3Exception("Underlying object is not a sort");
120  super.checkNativeObject(obj);
121  }
122 
123  static Sort create(Context ctx, long obj) throws Z3Exception
124  {
125  Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
126  switch (sk)
127  {
128  case Z3_ARRAY_SORT:
129  return new ArraySort(ctx, obj);
130  case Z3_BOOL_SORT:
131  return new BoolSort(ctx, obj);
132  case Z3_BV_SORT:
133  return new BitVecSort(ctx, obj);
134  case Z3_DATATYPE_SORT:
135  return new DatatypeSort(ctx, obj);
136  case Z3_INT_SORT:
137  return new IntSort(ctx, obj);
138  case Z3_REAL_SORT:
139  return new RealSort(ctx, obj);
141  return new UninterpretedSort(ctx, obj);
143  return new FiniteDomainSort(ctx, obj);
144  case Z3_RELATION_SORT:
145  return new RelationSort(ctx, obj);
146  default:
147  throw new Z3Exception("Unknown sort kind");
148  }
149  }
150 }
String toString()
Definition: Sort.java:87
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
def RealSort
Definition: z3py.py:2630
def IntSort
Definition: z3py.py:2614
def BoolSort
Definition: z3py.py:1325
def BitVecSort
Definition: z3py.py:3435
Sort(Context ctx)
Definition: Sort.java:101
static int getSortKind(long a0, long a1)
Definition: Native.java:1994
static final Z3_sort_kind fromInt(int v)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
static long getSortName(long a0, long a1)
Definition: Native.java:1958
boolean equals(Object o)
Definition: Sort.java:35
Z3_sort_kind getSortKind()
Definition: Sort.java:69
def ArraySort(d, r)
Definition: z3py.py:3955
Symbol getName()
Definition: Sort.java:78
static int getSortId(long a0, long a1)
Definition: Native.java:1967
static String sortToString(long a0, long a1)
Definition: Native.java:3007