Lines Matching defs:Z3Sort

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