74 class Z3Sort : public SMTSort {  class
83   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {  in Z3Sort()  function in __anon1aad92b90111::Z3Sort
88   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {  in Z3Sort()  function in __anon1aad92b90111::Z3Sort
94   Z3Sort &operator=(const Z3Sort &Other) {  in operator =()
101   Z3Sort(Z3Sort &&Other) = delete;
102   Z3Sort &operator=(Z3Sort &&Other) = delete;
104   ~Z3Sort() {  in ~Z3Sort()
137                          static_cast<const Z3Sort &>(Other).Sort);  in equal_to()
145 static const Z3Sort &toZ3Sort(const SMTSort &S) {  in toZ3Sort()
146   return static_cast<const Z3Sort &>(S);  in toZ3Sort()
283   std::set<Z3Sort> CachedSorts;
319     return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));  in getBoolSort()
324         Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));  in getBitvectorSort()
329         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));  in getSort()
333     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));  in getFloat16Sort()
337     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));  in getFloat32Sort()
341     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));  in getFloat64Sort()
345     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));  in getFloat128Sort()
741     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;  in mkBitvector()  local
748           Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));  in mkBitvector()
757             ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)  in mkBitvector()
758             : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);  in mkBitvector()