Z3
src/api/java/Sort.java
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     /* Overloaded operators are not translated. */
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines