Z3 |

Sort.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
20 import com.microsoft.z3.enumerations.Z3_ast_kind;
21 import com.microsoft.z3.enumerations.Z3_sort_kind;
22
26 public 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
63 public Z3_sort_kind getSortKind()
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
94 public Sort translate(Context ctx)
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);
133 case Z3_UNINTERPRETED_SORT:
134 return new UninterpretedSort(ctx, obj);
135 case Z3_FINITE_DOMAIN_SORT:
136 return new FiniteDomainSort(ctx, obj);
137 case Z3_RELATION_SORT:
138 return new RelationSort(ctx, obj);
139 case Z3_FLOATING_POINT_SORT:
140 return new FPSort(ctx, obj);
141 case Z3_ROUNDING_MODE_SORT:
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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Sort.hashCode
int hashCode()
Definition: Sort.java:47
com.microsoft.z3.Sort.getSortKind
Z3_sort_kind getSortKind()
Definition: Sort.java:63
com.microsoft.z3.Sort.translate
Sort translate(Context ctx)
Definition: Sort.java:94
com.microsoft.z3.Sort.equals
boolean equals(Object o)
Definition: Sort.java:32
com.microsoft.z3.Sort.getId
int getId()
Definition: Sort.java:55
com.microsoft.z3.Sort.getName
Symbol getName()
Definition: Sort.java:72
com.microsoft.z3.Sort.toString
String toString()
Definition: Sort.java:82
com.microsoft.z3.Symbol
Definition: Symbol.java:25
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:3100
z3py.RealSort
def RealSort(ctx=None)
Definition: z3py.py:3117
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1655
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
z3py.FiniteDomainSort
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7590
z3py.FPSort
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727
z3py.BitVecSort
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150
Z3_RELATION_SORT
@ Z3_RELATION_SORT
Definition: z3_api.h:158
Z3_BOOL_SORT
@ Z3_BOOL_SORT
Definition: z3_api.h:152
Z3_ROUNDING_MODE_SORT
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:161
Z3_BV_SORT
@ Z3_BV_SORT
Definition: z3_api.h:155
Z3_DATATYPE_SORT
@ Z3_DATATYPE_SORT
Definition: z3_api.h:157
Z3_INT_SORT
@ Z3_INT_SORT
Definition: z3_api.h:153
Z3_FINITE_DOMAIN_SORT
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:159
Z3_RE_SORT
@ Z3_RE_SORT
Definition: z3_api.h:163
Z3_UNINTERPRETED_SORT
@ Z3_UNINTERPRETED_SORT
Definition: z3_api.h:151
Z3_FLOATING_POINT_SORT
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:160
Z3_ARRAY_SORT
@ Z3_ARRAY_SORT
Definition: z3_api.h:156
Z3_REAL_SORT
@ Z3_REAL_SORT
Definition: z3_api.h:154
Z3_SEQ_SORT
@ Z3_SEQ_SORT
Definition: z3_api.h:162