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()) &&
40  getContext().nCtx(),
41  getNativeObject(),
42  other.getNativeObject()
43  ));
44  }
45 
51  public int hashCode()
52  {
53  return super.hashCode();
54  }
55 
59  public int getId()
60  {
61  return Native.getSortId(getContext().nCtx(), getNativeObject());
62  }
63 
68  {
69  return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
70  getNativeObject()));
71  }
72 
76  public Symbol getName()
77  {
78  return Symbol.create(getContext(),
79  Native.getSortName(getContext().nCtx(), getNativeObject()));
80  }
81 
85  @Override
86  public String toString() {
87  return Native.sortToString(getContext().nCtx(), getNativeObject());
88  }
89 
93  Sort(Context ctx, long obj)
94  {
95  super(ctx, obj);
96  }
97 
98  @Override
99  void checkNativeObject(long obj)
100  {
101  if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
102  .toInt())
103  throw new Z3Exception("Underlying object is not a sort");
104  super.checkNativeObject(obj);
105  }
106 
107  static Sort create(Context ctx, long obj)
108  {
109  Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
110  switch (sk)
111  {
112  case Z3_ARRAY_SORT:
113  return new ArraySort(ctx, obj);
114  case Z3_BOOL_SORT:
115  return new BoolSort(ctx, obj);
116  case Z3_BV_SORT:
117  return new BitVecSort(ctx, obj);
118  case Z3_DATATYPE_SORT:
119  return new DatatypeSort(ctx, obj);
120  case Z3_INT_SORT:
121  return new IntSort(ctx, obj);
122  case Z3_REAL_SORT:
123  return new RealSort(ctx, obj);
125  return new UninterpretedSort(ctx, obj);
127  return new FiniteDomainSort(ctx, obj);
128  case Z3_RELATION_SORT:
129  return new RelationSort(ctx, obj);
131  return new FPSort(ctx, obj);
133  return new FPRMSort(ctx, obj);
134  case Z3_SEQ_SORT:
135  return new SeqSort(ctx, obj);
136  case Z3_RE_SORT:
137  return new ReSort(ctx, obj);
138  default:
139  throw new Z3Exception("Unknown sort kind");
140  }
141  }
142 }
String toString()
Definition: Sort.java:86
def SeqSort(s)
Definition: z3py.py:9357
def ReSort(s)
Definition: z3py.py:9584
def RealSort(ctx=None)
Definition: z3py.py:2721
static int getSortKind(long a0, long a1)
Definition: Native.java:2348
static final Z3_sort_kind fromInt(int v)
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563
static long getSortName(long a0, long a1)
Definition: Native.java:2312
boolean equals(Object o)
Definition: Sort.java:32
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556
Z3_sort_kind getSortKind()
Definition: Sort.java:67
def ArraySort(d, r)
Definition: z3py.py:4110
def IntSort(ctx=None)
Definition: z3py.py:2705
Symbol getName()
Definition: Sort.java:76
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2339
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3530
static int getAstKind(long a0, long a1)
Definition: Native.java:2762
static int getSortId(long a0, long a1)
Definition: Native.java:2321
static String sortToString(long a0, long a1)
Definition: Native.java:3397
def BoolSort(ctx=None)
Definition: z3py.py:1407
def String(name, ctx=None)
Definition: z3py.py:9443