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()
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()
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  Sort(Context ctx, long obj)
102  {
103  super(ctx, obj);
104  }
105 
106  void checkNativeObject(long obj)
107  {
108  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
109  .toInt())
110  throw new Z3Exception("Underlying object is not a sort");
111  super.checkNativeObject(obj);
112  }
113 
114  static Sort create(Context ctx, long obj)
115  {
116  Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
117  switch (sk)
118  {
119  case Z3_ARRAY_SORT:
120  return new ArraySort(ctx, obj);
121  case Z3_BOOL_SORT:
122  return new BoolSort(ctx, obj);
123  case Z3_BV_SORT:
124  return new BitVecSort(ctx, obj);
125  case Z3_DATATYPE_SORT:
126  return new DatatypeSort(ctx, obj);
127  case Z3_INT_SORT:
128  return new IntSort(ctx, obj);
129  case Z3_REAL_SORT:
130  return new RealSort(ctx, obj);
132  return new UninterpretedSort(ctx, obj);
134  return new FiniteDomainSort(ctx, obj);
135  case Z3_RELATION_SORT:
136  return new RelationSort(ctx, obj);
138  return new FPSort(ctx, obj);
140  return new FPRMSort(ctx, obj);
141  default:
142  throw new Z3Exception("Unknown sort kind");
143  }
144  }
145 }
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:2641
def IntSort
Definition: z3py.py:2625
def BoolSort
Definition: z3py.py:1336
def BitVecSort
Definition: z3py.py:3446
static int getSortKind(long a0, long a1)
Definition: Native.java:2063
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:214
static long getSortName(long a0, long a1)
Definition: Native.java:2027
boolean equals(Object o)
Definition: Sort.java:35
Z3_sort_kind getSortKind()
Definition: Sort.java:69
def ArraySort(d, r)
Definition: z3py.py:3978
Symbol getName()
Definition: Sort.java:78
static int getSortId(long a0, long a1)
Definition: Native.java:2036
static String sortToString(long a0, long a1)
Definition: Native.java:3076
def FPSort
Definition: z3py.py:7920