74   Z3_sort Sort;  member in __anon13641eda0111::Z3Sort
78   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {  in Z3Sort()
79     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in Z3Sort()
83   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {  in Z3Sort()
84     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in Z3Sort()
90     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));  in operator =()
91     Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in operator =()
92     Sort = Other.Sort;  in operator =()
100     if (Sort)  in ~Z3Sort()
101       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in ~Z3Sort()
106         Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));  in Profile()
110     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);  in isBitvectorSortImpl()
114     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);  in isFloatSortImpl()
118     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);  in isBooleanSortImpl()
122     return Z3_get_bv_sort_size(Context.Context, Sort);  in getBitvectorSortSizeImpl()
126     return Z3_fpa_get_ebits(Context.Context, Sort) +  in getFloatSortSizeImpl()
127            Z3_fpa_get_sbits(Context.Context, Sort);  in getFloatSortSizeImpl()
131     return Z3_is_eq_sort(Context.Context, Sort,  in equal_to()
132                          static_cast<const Z3Sort &>(Other).Sort);  in equal_to()
136     OS << Z3_sort_to_string(Context.Context, Sort);  in print()
294   SMTSortRef newSortRef(const SMTSort &Sort) {  in newSortRef()  argument
295     auto It = CachedSorts.insert(toZ3Sort(Sort));  in newSortRef()
690                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkFPtoFP()
698                                toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkSBVtoFP()
706                                  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkUBVtoFP()
729     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;  in mkBitvector()
751     SMTSortRef Sort =  in mkFloat()  local
758                                     toZ3Sort(*Sort).Sort)));  in mkFloat()
761   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {  in mkSymbol()  argument
765                                     toZ3Sort(*Sort).Sort)));  in mkSymbol()
786   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPFloat()  argument
788     assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");  in toAPFloat()
790     llvm::APSInt Int(Sort->getFloatSortSize(), true);  in toAPFloat()
792         getFloatSemantics(Sort->getFloatSortSize());  in toAPFloat()
793     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());  in toAPFloat()
807   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPSInt()  argument
809     if (Sort->isBitvectorSort()) {  in toAPSInt()
810       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {  in toAPSInt()
821       if (Sort->getBitvectorSortSize() <= 64 ||  in toAPSInt()
822           Sort->getBitvectorSortSize() == 128) {  in toAPSInt()
831     if (Sort->isBooleanSort()) {  in toAPSInt()
855     SMTSortRef Sort = getSort(Assign);  in getInterpretation()  local
856     return toAPSInt(Sort, Assign, Int, true);  in getInterpretation()
869     SMTSortRef Sort = getSort(Assign);  in getInterpretation()  local
870     return toAPFloat(Sort, Assign, Float, true);  in getInterpretation()