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);