72   Z3_sort Sort;  member in __anonca7d1dd80111::Z3Sort
76   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {  in Z3Sort()
77     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in Z3Sort()
81   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {  in Z3Sort()
82     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in Z3Sort()
88     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));  in operator =()
89     Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in operator =()
90     Sort = Other.Sort;  in operator =()
98     if (Sort)  in ~Z3Sort()
99       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in ~Z3Sort()
104         Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));  in Profile()
108     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);  in isBitvectorSortImpl()
112     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);  in isFloatSortImpl()
116     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);  in isBooleanSortImpl()
120     return Z3_get_bv_sort_size(Context.Context, Sort);  in getBitvectorSortSizeImpl()
124     return Z3_fpa_get_ebits(Context.Context, Sort) +  in getFloatSortSizeImpl()
125            Z3_fpa_get_sbits(Context.Context, Sort);  in getFloatSortSizeImpl()
129     return Z3_is_eq_sort(Context.Context, Sort,  in equal_to()
130                          static_cast<const Z3Sort &>(Other).Sort);  in equal_to()
134     OS << Z3_sort_to_string(Context.Context, Sort);  in print()
292   SMTSortRef newSortRef(const SMTSort &Sort) {  in newSortRef()  argument
293     auto It = CachedSorts.insert(toZ3Sort(Sort));  in newSortRef()
688                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkFPtoFP()
696                                toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkSBVtoFP()
704                                  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkUBVtoFP()
727     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;  in mkBitvector()
749     SMTSortRef Sort =  in mkFloat()  local
756                                     toZ3Sort(*Sort).Sort)));  in mkFloat()
759   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {  in mkSymbol()  argument
763                                     toZ3Sort(*Sort).Sort)));  in mkSymbol()
784   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPFloat()  argument
786     assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");  in toAPFloat()
788     llvm::APSInt Int(Sort->getFloatSortSize(), true);  in toAPFloat()
790         getFloatSemantics(Sort->getFloatSortSize());  in toAPFloat()
791     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());  in toAPFloat()
805   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPSInt()  argument
807     if (Sort->isBitvectorSort()) {  in toAPSInt()
808       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {  in toAPSInt()
819       if (Sort->getBitvectorSortSize() <= 64 ||  in toAPSInt()
820           Sort->getBitvectorSortSize() == 128) {  in toAPSInt()
829     if (Sort->isBooleanSort()) {  in toAPSInt()
853     SMTSortRef Sort = getSort(Assign);  in getInterpretation()  local
854     return toAPSInt(Sort, Assign, Int, true);  in getInterpretation()
867     SMTSortRef Sort = getSort(Assign);  in getInterpretation()  local
868     return toAPFloat(Sort, Assign, Float, true);  in getInterpretation()