Z3
Sort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_ast_kind;
21import com.microsoft.z3.enumerations.Z3_sort_kind;
22
26public class Sort extends AST
27{
31 @Override
32 public boolean equals(Object o)
33 {
34 if (o == this) return true;
35 if (!(o instanceof Sort)) return false;
36 Sort other = (Sort) o;
37
38 return (getContext().nCtx() == other.getContext().nCtx()) &&
39 (Native.isEqSort(getContext().nCtx(), getNativeObject(), other.getNativeObject()));
40 }
41
47 public int hashCode()
48 {
49 return super.hashCode();
50 }
51
55 public int getId()
56 {
57 return Native.getSortId(getContext().nCtx(), getNativeObject());
58 }
59
64 {
65 return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
66 getNativeObject()));
67 }
68
72 public Symbol getName()
73 {
74 return Symbol.create(getContext(),
75 Native.getSortName(getContext().nCtx(), getNativeObject()));
76 }
77
81 @Override
82 public String toString() {
83 return Native.sortToString(getContext().nCtx(), getNativeObject());
84 }
85
95 {
96 return (Sort) super.translate(ctx);
97 }
98
102 Sort(Context ctx, long obj)
103 {
104 super(ctx, obj);
105 }
106
107 @Override
108 void checkNativeObject(long obj)
109 {
110 if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
111 .toInt())
112 throw new Z3Exception("Underlying object is not a sort");
113 super.checkNativeObject(obj);
114 }
115
116 static Sort create(Context ctx, long obj)
117 {
118 Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
119 switch (sk)
120 {
121 case Z3_ARRAY_SORT:
122 return new ArraySort(ctx, obj);
123 case Z3_BOOL_SORT:
124 return new BoolSort(ctx, obj);
125 case Z3_BV_SORT:
126 return new BitVecSort(ctx, obj);
127 case Z3_DATATYPE_SORT:
128 return new DatatypeSort(ctx, obj);
129 case Z3_INT_SORT:
130 return new IntSort(ctx, obj);
131 case Z3_REAL_SORT:
132 return new RealSort(ctx, obj);
134 return new UninterpretedSort(ctx, obj);
136 return new FiniteDomainSort(ctx, obj);
137 case Z3_RELATION_SORT:
138 return new RelationSort(ctx, obj);
140 return new FPSort(ctx, obj);
142 return new FPRMSort(ctx, obj);
143 case Z3_SEQ_SORT:
144 return new SeqSort(ctx, obj);
145 case Z3_RE_SORT:
146 return new ReSort(ctx, obj);
147 default:
148 throw new Z3Exception("Unknown sort kind");
149 }
150 }
151}
static int getSortKind(long a0, long a1)
Definition: Native.java:2693
static String sortToString(long a0, long a1)
Definition: Native.java:3838
static long getSortName(long a0, long a1)
Definition: Native.java:2657
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2684
static int getSortId(long a0, long a1)
Definition: Native.java:2666
Z3_sort_kind getSortKind()
Definition: Sort.java:63
Sort translate(Context ctx)
Definition: Sort.java:94
boolean equals(Object o)
Definition: Sort.java:32
Symbol getName()
Definition: Sort.java:72
String toString()
Definition: Sort.java:82
static final Z3_sort_kind fromInt(int v)
def IntSort(ctx=None)
Definition: z3py.py:2907
def SeqSort(s)
Definition: z3py.py:9980
def RealSort(ctx=None)
Definition: z3py.py:2923
def ArraySort(*sig)
Definition: z3py.py:4371
def BoolSort(ctx=None)
Definition: z3py.py:1533
def ReSort(s)
Definition: z3py.py:10294
def String(name, ctx=None)
Definition: z3py.py:10085
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7221
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9183
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:178
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:148
@ Z3_RELATION_SORT
Definition: z3_api.h:156
@ Z3_BOOL_SORT
Definition: z3_api.h:150
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:159
@ Z3_BV_SORT
Definition: z3_api.h:153
@ Z3_DATATYPE_SORT
Definition: z3_api.h:155
@ Z3_INT_SORT
Definition: z3_api.h:151
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:157
@ Z3_RE_SORT
Definition: z3_api.h:161
@ Z3_UNINTERPRETED_SORT
Definition: z3_api.h:149
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:158
@ Z3_ARRAY_SORT
Definition: z3_api.h:154
@ Z3_REAL_SORT
Definition: z3_api.h:152
@ Z3_SEQ_SORT
Definition: z3_api.h:160