79   Z3_sort Sort;  member in __anon1aad92b90111::Z3Sort
83   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {  in Z3Sort()
84     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in Z3Sort()
88   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {  in Z3Sort()
89     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in Z3Sort()
95     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));  in operator =()
96     Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in operator =()
97     Sort = Other.Sort;  in operator =()
105     if (Sort)  in ~Z3Sort()
106       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));  in ~Z3Sort()
111         Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));  in Profile()
115     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);  in isBitvectorSortImpl()
119     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);  in isFloatSortImpl()
123     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);  in isBooleanSortImpl()
127     return Z3_get_bv_sort_size(Context.Context, Sort);  in getBitvectorSortSizeImpl()
131     return Z3_fpa_get_ebits(Context.Context, Sort) +  in getFloatSortSizeImpl()
132            Z3_fpa_get_sbits(Context.Context, Sort);  in getFloatSortSizeImpl()
136     return Z3_is_eq_sort(Context.Context, Sort,  in equal_to()
137                          static_cast<const Z3Sort &>(Other).Sort);  in equal_to()
141     OS << Z3_sort_to_string(Context.Context, Sort);  in print()
306   SMTSortRef newSortRef(const SMTSort &Sort) {  in newSortRef()  argument
307     auto It = CachedSorts.insert(toZ3Sort(Sort));  in newSortRef()
702                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkFPtoFP()
710                                toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkSBVtoFP()
718                                  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));  in mkUBVtoFP()
741     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;  in mkBitvector()
763     SMTSortRef Sort =  in mkFloat()  local
770                                     toZ3Sort(*Sort).Sort)));  in mkFloat()
773   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {  in mkSymbol()  argument
777                                     toZ3Sort(*Sort).Sort)));  in mkSymbol()
798   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPFloat()  argument
800     assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");  in toAPFloat()
802     llvm::APSInt Int(Sort->getFloatSortSize(), true);  in toAPFloat()
804         getFloatSemantics(Sort->getFloatSortSize());  in toAPFloat()
805     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());  in toAPFloat()
819   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPSInt()  argument
821     if (Sort->isBitvectorSort()) {  in toAPSInt()
822       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {  in toAPSInt()
833       if (Sort->getBitvectorSortSize() <= 64 ||  in toAPSInt()
834           Sort->getBitvectorSortSize() == 128) {  in toAPSInt()
843     if (Sort->isBooleanSort()) {  in toAPSInt()
867     SMTSortRef Sort = getSort(Assign);  in getInterpretation()  local
868     return toAPSInt(Sort, Assign, Int, true);  in getInterpretation()
881     SMTSortRef Sort = getSort(Assign);  in getInterpretation()  local
882     return toAPFloat(Sort, Assign, Float, true);  in getInterpretation()