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 }
com.microsoft.z3.Native.getSortKind
static int getSortKind(long a0, long a1)
Definition: Native.java:2695
com.microsoft.z3.Sort.equals
boolean equals(Object o)
Definition: Sort.java:32
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Sort.getSortKind
Z3_sort_kind getSortKind()
Definition: Sort.java:63
Z3_BV_SORT
@ Z3_BV_SORT
Definition: z3_api.h:153
z3py.RealSort
def RealSort(ctx=None)
Definition: z3py.py:2944
Z3_FINITE_DOMAIN_SORT
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:157
com.microsoft.z3.Sort
Definition: Sort.java:26
com.microsoft
z3py.FiniteDomainSort
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7244
com.microsoft.z3.Sort.getName
Symbol getName()
Definition: Sort.java:72
Z3_RELATION_SORT
@ Z3_RELATION_SORT
Definition: z3_api.h:156
Z3_ARRAY_SORT
@ Z3_ARRAY_SORT
Definition: z3_api.h:154
com.microsoft.z3.Native.getSortName
static long getSortName(long a0, long a1)
Definition: Native.java:2659
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Sort.hashCode
int hashCode()
Definition: Sort.java:47
Z3_UNINTERPRETED_SORT
@ Z3_UNINTERPRETED_SORT
Definition: z3_api.h:149
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:147
Z3_REAL_SORT
@ Z3_REAL_SORT
Definition: z3_api.h:152
com.microsoft.z3.Native
Definition: Native.java:4
Z3_FLOATING_POINT_SORT
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:158
Z3_INT_SORT
@ Z3_INT_SORT
Definition: z3_api.h:151
z3py.FPSort
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9206
com.microsoft.z3
Definition: AlgebraicNum.java:18
Z3_RE_SORT
@ Z3_RE_SORT
Definition: z3_api.h:161
com.microsoft.z3.enumerations.Z3_ast_kind
Definition: Z3_ast_kind.java:13
com.microsoft.z3.enumerations.Z3_sort_kind.fromInt
static final Z3_sort_kind fromInt(int v)
Definition: Z3_sort_kind.java:45
z3py.ArraySort
def ArraySort(*sig)
Definition: z3py.py:4394
z3py.BitVecSort
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3763
com.microsoft.z3.AST
Definition: AST.java:25
Z3_BOOL_SORT
@ Z3_BOOL_SORT
Definition: z3_api.h:150
com.microsoft.z3.Sort.toString
String toString()
Definition: Sort.java:82
com
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:2928
com.microsoft.z3.enumerations.Z3_sort_kind
Definition: Z3_sort_kind.java:13
com.microsoft.z3.Context
Definition: Context.java:35
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:177
com.microsoft.z3.Sort.getId
int getId()
Definition: Sort.java:55
Z3_SEQ_SORT
@ Z3_SEQ_SORT
Definition: z3_api.h:160
com.microsoft.z3.Sort.translate
Sort translate(Context ctx)
Definition: Sort.java:94
com.microsoft.z3.Native.sortToString
static String sortToString(long a0, long a1)
Definition: Native.java:3840
com.microsoft.z3.Native.getSortId
static int getSortId(long a0, long a1)
Definition: Native.java:2668
z3py.SeqSort
def SeqSort(s)
Definition: z3py.py:10003
Z3_DATATYPE_SORT
@ Z3_DATATYPE_SORT
Definition: z3_api.h:155
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1553
z3py.ReSort
def ReSort(s)
Definition: z3py.py:10320
com.microsoft.z3.Native.isEqSort
static boolean isEqSort(long a0, long a1, long a2)
Definition: Native.java:2686
Z3_ROUNDING_MODE_SORT
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:159
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111