Lines Matching defs:Sort

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