Lines Matching refs:AST
147 Z3_ast AST; member in __anonca7d1dd80111::Z3Expr
150 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) { in Z3Expr()
151 Z3_inc_ref(Context.Context, AST); in Z3Expr()
155 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) { in Z3Expr()
156 Z3_inc_ref(Context.Context, AST); in Z3Expr()
162 Z3_inc_ref(Context.Context, Other.AST); in operator =()
163 Z3_dec_ref(Context.Context, AST); in operator =()
164 AST = Other.AST; in operator =()
172 if (AST) in ~Z3Expr()
173 Z3_dec_ref(Context.Context, AST); in ~Z3Expr()
177 ID.AddInteger(Z3_get_ast_id(Context.Context, AST)); in Profile()
182 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST), in equal_to()
184 static_cast<const Z3Expr &>(Other).AST)) && in equal_to()
186 return Z3_is_eq_ast(Context.Context, AST, in equal_to()
187 static_cast<const Z3Expr &>(Other).AST); in equal_to()
191 OS << Z3_ast_to_string(Context.Context, AST); in print()
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
315 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
336 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNeg()
341 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNot()
346 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); in mkNot()
351 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
352 toZ3Expr(*RHS).AST))); in mkBVAdd()
357 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
358 toZ3Expr(*RHS).AST))); in mkBVSub()
363 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, in mkBVMul()
364 toZ3Expr(*RHS).AST))); in mkBVMul()
369 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, in mkBVSRem()
370 toZ3Expr(*RHS).AST))); in mkBVSRem()
375 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, in mkBVURem()
376 toZ3Expr(*RHS).AST))); in mkBVURem()
381 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDiv()
382 toZ3Expr(*RHS).AST))); in mkBVSDiv()
387 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVUDiv()
388 toZ3Expr(*RHS).AST))); in mkBVUDiv()
393 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, in mkBVShl()
394 toZ3Expr(*RHS).AST))); in mkBVShl()
399 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, in mkBVAshr()
400 toZ3Expr(*RHS).AST))); in mkBVAshr()
405 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, in mkBVLshr()
406 toZ3Expr(*RHS).AST))); in mkBVLshr()
411 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, in mkBVXor()
412 toZ3Expr(*RHS).AST))); in mkBVXor()
417 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, in mkBVOr()
418 toZ3Expr(*RHS).AST))); in mkBVOr()
423 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, in mkBVAnd()
424 toZ3Expr(*RHS).AST))); in mkBVAnd()
429 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, in mkBVUlt()
430 toZ3Expr(*RHS).AST))); in mkBVUlt()
435 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSlt()
436 toZ3Expr(*RHS).AST))); in mkBVSlt()
441 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, in mkBVUgt()
442 toZ3Expr(*RHS).AST))); in mkBVUgt()
447 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSgt()
448 toZ3Expr(*RHS).AST))); in mkBVSgt()
453 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, in mkBVUle()
454 toZ3Expr(*RHS).AST))); in mkBVUle()
459 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, in mkBVSle()
460 toZ3Expr(*RHS).AST))); in mkBVSle()
465 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, in mkBVUge()
466 toZ3Expr(*RHS).AST))); in mkBVUge()
471 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, in mkBVSge()
472 toZ3Expr(*RHS).AST))); in mkBVSge()
476 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkAnd()
481 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkOr()
487 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, in mkEqual()
488 toZ3Expr(*RHS).AST))); in mkEqual()
493 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST))); in mkFPNeg()
498 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsInfinite()
503 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsNaN()
508 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsNormal()
513 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsZero()
520 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPMul()
521 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPMul()
528 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPDiv()
529 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPDiv()
534 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, in mkFPRem()
535 toZ3Expr(*RHS).AST))); in mkFPRem()
542 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPAdd()
543 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPAdd()
550 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPSub()
551 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPSub()
556 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, in mkFPLt()
557 toZ3Expr(*RHS).AST))); in mkFPLt()
562 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, in mkFPGt()
563 toZ3Expr(*RHS).AST))); in mkFPGt()
568 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, in mkFPLe()
569 toZ3Expr(*RHS).AST))); in mkFPLe()
574 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, in mkFPGe()
575 toZ3Expr(*RHS).AST))); in mkFPGe()
580 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, in mkFPEqual()
581 toZ3Expr(*RHS).AST))); in mkFPEqual()
587 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST, in mkIte()
588 toZ3Expr(*T).AST, toZ3Expr(*F).AST))); in mkIte()
593 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST))); in mkBVSignExt()
598 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST))); in mkBVZeroExt()
604 toZ3Expr(*Exp).AST))); in mkBVExtract()
612 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoOverflow()
613 toZ3Expr(*RHS).AST, isSigned))); in mkBVAddNoOverflow()
621 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoUnderflow()
622 toZ3Expr(*RHS).AST))); in mkBVAddNoUnderflow()
630 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoOverflow()
631 toZ3Expr(*RHS).AST))); in mkBVSubNoOverflow()
639 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoUnderflow()
640 toZ3Expr(*RHS).AST, isSigned))); in mkBVSubNoUnderflow()
648 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDivNoOverflow()
649 toZ3Expr(*RHS).AST))); in mkBVSDivNoOverflow()
656 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNegNoOverflow()
664 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoOverflow()
665 toZ3Expr(*RHS).AST, isSigned))); in mkBVMulNoOverflow()
673 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoUnderflow()
674 toZ3Expr(*RHS).AST))); in mkBVMulNoUnderflow()
679 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, in mkBVConcat()
680 toZ3Expr(*RHS).AST))); in mkBVConcat()
687 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoFP()
688 toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); in mkFPtoFP()
695 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST, in mkSBVtoFP()
696 toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); in mkSBVtoFP()
703 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST, in mkUBVtoFP()
704 toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); in mkUBVtoFP()
710 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoSBV()
711 toZ3Expr(*From).AST, ToWidth))); in mkFPtoSBV()
717 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoUBV()
718 toZ3Expr(*From).AST, ToWidth))); in mkFPtoUBV()
755 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, in mkFloat()
770 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), in getBitvector()
776 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE; in getBoolean()
784 bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST, in toAPFloat() argument
792 if (!toAPSInt(BVSort, AST, Int, true)) { in toAPFloat()
805 bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST, in toAPSInt() argument
821 Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned()); in toAPSInt()
835 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)), in toAPSInt()
846 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); in getInterpretation()
860 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); in getInterpretation()