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 {
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 
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);
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 }
String toString()
Definition: Sort.java:82
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:147
def SeqSort(s)
Definition: z3py.py:9980
def ReSort(s)
Definition: z3py.py:10294
def RealSort(ctx=None)
Definition: z3py.py:2923
static int getSortKind(long a0, long a1)
Definition: Native.java:2693
static final Z3_sort_kind fromInt(int v)
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7221
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:177
static long getSortName(long a0, long a1)
Definition: Native.java:2657
boolean equals(Object o)
Definition: Sort.java:32
Sort translate(Context ctx)
Definition: Sort.java:94
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9183
Z3_sort_kind getSortKind()
Definition: Sort.java:63
def IntSort(ctx=None)
Definition: z3py.py:2907
Symbol getName()
Definition: Sort.java:72
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2684
def ArraySort(*sig)
Definition: z3py.py:4371
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740
static int getSortId(long a0, long a1)
Definition: Native.java:2666
static String sortToString(long a0, long a1)
Definition: Native.java:3838
def BoolSort(ctx=None)
Definition: z3py.py:1533
def String(name, ctx=None)
Definition: z3py.py:10085