Lines Matching defs:AST
154 Z3_ast AST;
157 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
158 Z3_inc_ref(Context.Context, AST);
162 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
163 Z3_inc_ref(Context.Context, AST);
169 Z3_inc_ref(Context.Context, Other.AST);
170 Z3_dec_ref(Context.Context, AST);
171 AST = Other.AST;
179 if (AST)
180 Z3_dec_ref(Context.Context, AST);
184 ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
187 /// Comparison of AST equality, not model equivalence.
189 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
191 static_cast<const Z3Expr &>(Other).AST)) &&
192 "AST's must have the same sort");
193 return Z3_is_eq_ast(Context.Context, AST,
194 static_cast<const Z3Expr &>(Other).AST);
198 OS << Z3_ast_to_string(Context.Context, AST);
301 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
329 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
350 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
355 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
360 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
365 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
366 toZ3Expr(*RHS).AST)));
371 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
372 toZ3Expr(*RHS).AST)));
377 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
378 toZ3Expr(*RHS).AST)));
383 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
384 toZ3Expr(*RHS).AST)));
389 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
390 toZ3Expr(*RHS).AST)));
395 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
396 toZ3Expr(*RHS).AST)));
401 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
402 toZ3Expr(*RHS).AST)));
407 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
408 toZ3Expr(*RHS).AST)));
413 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
414 toZ3Expr(*RHS).AST)));
419 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
420 toZ3Expr(*RHS).AST)));
425 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
426 toZ3Expr(*RHS).AST)));
431 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
432 toZ3Expr(*RHS).AST)));
437 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
438 toZ3Expr(*RHS).AST)));
443 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
444 toZ3Expr(*RHS).AST)));
449 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
450 toZ3Expr(*RHS).AST)));
455 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
456 toZ3Expr(*RHS).AST)));
461 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
462 toZ3Expr(*RHS).AST)));
467 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
468 toZ3Expr(*RHS).AST)));
473 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
474 toZ3Expr(*RHS).AST)));
479 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
480 toZ3Expr(*RHS).AST)));
485 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
486 toZ3Expr(*RHS).AST)));
490 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
495 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
501 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
502 toZ3Expr(*RHS).AST)));
507 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
512 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
517 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
522 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
527 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
534 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
535 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
542 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
543 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
548 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
549 toZ3Expr(*RHS).AST)));
556 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
557 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
564 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
565 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
570 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
571 toZ3Expr(*RHS).AST)));
576 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
577 toZ3Expr(*RHS).AST)));
582 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
583 toZ3Expr(*RHS).AST)));
588 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
589 toZ3Expr(*RHS).AST)));
594 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
595 toZ3Expr(*RHS).AST)));
601 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
602 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
607 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
612 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
618 toZ3Expr(*Exp).AST)));
626 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
627 toZ3Expr(*RHS).AST, isSigned)));
635 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
636 toZ3Expr(*RHS).AST)));
644 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
645 toZ3Expr(*RHS).AST)));
653 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
654 toZ3Expr(*RHS).AST, isSigned)));
662 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
663 toZ3Expr(*RHS).AST)));
670 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
678 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
679 toZ3Expr(*RHS).AST, isSigned)));
687 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
688 toZ3Expr(*RHS).AST)));
693 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
694 toZ3Expr(*RHS).AST)));
701 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
702 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
709 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
710 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
717 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
718 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
724 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
725 toZ3Expr(*From).AST, ToWidth)));
731 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
732 toZ3Expr(*From).AST, ToWidth)));
769 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
784 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
790 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
798 bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
806 if (!toAPSInt(BVSort, AST, Int, true)) {
819 bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
835 Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
849 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
860 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
874 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));