67 class Z3Sort : public SMTSort {  class
76   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {  in Z3Sort()  function in __anonca7d1dd80111::Z3Sort
81   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {  in Z3Sort()  function in __anonca7d1dd80111::Z3Sort
87   Z3Sort &operator=(const Z3Sort &Other) {  in operator =()
94   Z3Sort(Z3Sort &&Other) = delete;
95   Z3Sort &operator=(Z3Sort &&Other) = delete;
97   ~Z3Sort() {  in ~Z3Sort()
130                          static_cast<const Z3Sort &>(Other).Sort);  in equal_to()
138 static const Z3Sort &toZ3Sort(const SMTSort &S) {  in toZ3Sort()
139   return static_cast<const Z3Sort &>(S);  in toZ3Sort()
266   std::set<Z3Sort> CachedSorts;
305     return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));  in getBoolSort()
310         Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));  in getBitvectorSort()
315         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));  in getSort()
319     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));  in getFloat16Sort()
323     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));  in getFloat32Sort()
327     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));  in getFloat64Sort()
331     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));  in getFloat128Sort()
727     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;  in mkBitvector()  local
734           Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));  in mkBitvector()
743             ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)  in mkBitvector()
744             : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);  in mkBitvector()