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