69 class Z3Sort : public SMTSort {  class
78   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {  in Z3Sort()  function in __anon13641eda0111::Z3Sort
83   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {  in Z3Sort()  function in __anon13641eda0111::Z3Sort
89   Z3Sort &operator=(const Z3Sort &Other) {  in operator =()
96   Z3Sort(Z3Sort &&Other) = delete;
97   Z3Sort &operator=(Z3Sort &&Other) = delete;
99   ~Z3Sort() {  in ~Z3Sort()
132                          static_cast<const Z3Sort &>(Other).Sort);  in equal_to()
140 static const Z3Sort &toZ3Sort(const SMTSort &S) {  in toZ3Sort()
141   return static_cast<const Z3Sort &>(S);  in toZ3Sort()
268   std::set<Z3Sort> CachedSorts;
307     return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));  in getBoolSort()
312         Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));  in getBitvectorSort()
317         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));  in getSort()
321     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));  in getFloat16Sort()
325     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));  in getFloat32Sort()
329     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));  in getFloat64Sort()
333     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));  in getFloat128Sort()
729     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;  in mkBitvector()  local
736           Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));  in mkBitvector()
745             ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)  in mkBitvector()
746             : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);  in mkBitvector()