Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00020 import com.microsoft.z3.enumerations.Z3_ast_kind;
00021 import com.microsoft.z3.enumerations.Z3_sort_kind;
00022
00026 public class Sort extends AST
00027 {
00028
00029
00035 public boolean equals(Object o)
00036 {
00037 Sort casted = null;
00038
00039 try {
00040 casted = Sort.class.cast(o);
00041 } catch (ClassCastException e) {
00042 return false;
00043 }
00044
00045 return this.getNativeObject() == casted.getNativeObject();
00046 }
00047
00053 public int hashCode()
00054 {
00055 return super.hashCode();
00056 }
00057
00061 public int getId() throws Z3Exception
00062 {
00063 return Native.getSortId(getContext().nCtx(), getNativeObject());
00064 }
00065
00069 public Z3_sort_kind getSortKind() throws Z3Exception
00070 {
00071 return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
00072 getNativeObject()));
00073 }
00074
00078 public Symbol getName() throws Z3Exception
00079 {
00080 return Symbol.create(getContext(),
00081 Native.getSortName(getContext().nCtx(), getNativeObject()));
00082 }
00083
00087 public String toString()
00088 {
00089 try
00090 {
00091 return Native.sortToString(getContext().nCtx(), getNativeObject());
00092 } catch (Z3Exception e)
00093 {
00094 return "Z3Exception: " + e.getMessage();
00095 }
00096 }
00097
00101 protected Sort(Context ctx) throws Z3Exception
00102 {
00103 super(ctx);
00104 {
00105 }
00106 }
00107
00108 Sort(Context ctx, long obj) throws Z3Exception
00109 {
00110 super(ctx, obj);
00111 {
00112 }
00113 }
00114
00115 void checkNativeObject(long obj) throws Z3Exception
00116 {
00117 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
00118 .toInt())
00119 throw new Z3Exception("Underlying object is not a sort");
00120 super.checkNativeObject(obj);
00121 }
00122
00123 static Sort create(Context ctx, long obj) throws Z3Exception
00124 {
00125 Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
00126 switch (sk)
00127 {
00128 case Z3_ARRAY_SORT:
00129 return new ArraySort(ctx, obj);
00130 case Z3_BOOL_SORT:
00131 return new BoolSort(ctx, obj);
00132 case Z3_BV_SORT:
00133 return new BitVecSort(ctx, obj);
00134 case Z3_DATATYPE_SORT:
00135 return new DatatypeSort(ctx, obj);
00136 case Z3_INT_SORT:
00137 return new IntSort(ctx, obj);
00138 case Z3_REAL_SORT:
00139 return new RealSort(ctx, obj);
00140 case Z3_UNINTERPRETED_SORT:
00141 return new UninterpretedSort(ctx, obj);
00142 case Z3_FINITE_DOMAIN_SORT:
00143 return new FiniteDomainSort(ctx, obj);
00144 case Z3_RELATION_SORT:
00145 return new RelationSort(ctx, obj);
00146 default:
00147 throw new Z3Exception("Unknown sort kind");
00148 }
00149 }
00150 }