Lines Matching refs:AST
149 Z3_ast AST; member in __anonae660b540111::Z3Expr
152 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) { in Z3Expr()
153 Z3_inc_ref(Context.Context, AST); in Z3Expr()
157 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) { in Z3Expr()
158 Z3_inc_ref(Context.Context, AST); in Z3Expr()
164 Z3_inc_ref(Context.Context, Other.AST); in operator =()
165 Z3_dec_ref(Context.Context, AST); in operator =()
166 AST = Other.AST; in operator =()
174 if (AST) in ~Z3Expr()
175 Z3_dec_ref(Context.Context, AST); in ~Z3Expr()
179 ID.AddInteger(Z3_get_ast_id(Context.Context, AST)); in Profile()
184 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST), in equal_to()
186 static_cast<const Z3Expr &>(Other).AST)) && in equal_to()
188 return Z3_is_eq_ast(Context.Context, AST, in equal_to()
189 static_cast<const Z3Expr &>(Other).AST); in equal_to()
193 OS << Z3_ast_to_string(Context.Context, AST); in print()
289 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
317 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
338 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNeg()
343 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNot()
348 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); in mkNot()
353 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
354 toZ3Expr(*RHS).AST))); in mkBVAdd()
359 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
360 toZ3Expr(*RHS).AST))); in mkBVSub()
365 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, in mkBVMul()
366 toZ3Expr(*RHS).AST))); in mkBVMul()
371 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, in mkBVSRem()
372 toZ3Expr(*RHS).AST))); in mkBVSRem()
377 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, in mkBVURem()
378 toZ3Expr(*RHS).AST))); in mkBVURem()
383 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDiv()
384 toZ3Expr(*RHS).AST))); in mkBVSDiv()
389 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVUDiv()
390 toZ3Expr(*RHS).AST))); in mkBVUDiv()
395 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, in mkBVShl()
396 toZ3Expr(*RHS).AST))); in mkBVShl()
401 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, in mkBVAshr()
402 toZ3Expr(*RHS).AST))); in mkBVAshr()
407 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, in mkBVLshr()
408 toZ3Expr(*RHS).AST))); in mkBVLshr()
413 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, in mkBVXor()
414 toZ3Expr(*RHS).AST))); in mkBVXor()
419 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, in mkBVOr()
420 toZ3Expr(*RHS).AST))); in mkBVOr()
425 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, in mkBVAnd()
426 toZ3Expr(*RHS).AST))); in mkBVAnd()
431 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, in mkBVUlt()
432 toZ3Expr(*RHS).AST))); in mkBVUlt()
437 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSlt()
438 toZ3Expr(*RHS).AST))); in mkBVSlt()
443 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, in mkBVUgt()
444 toZ3Expr(*RHS).AST))); in mkBVUgt()
449 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSgt()
450 toZ3Expr(*RHS).AST))); in mkBVSgt()
455 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, in mkBVUle()
456 toZ3Expr(*RHS).AST))); in mkBVUle()
461 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, in mkBVSle()
462 toZ3Expr(*RHS).AST))); in mkBVSle()
467 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, in mkBVUge()
468 toZ3Expr(*RHS).AST))); in mkBVUge()
473 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, in mkBVSge()
474 toZ3Expr(*RHS).AST))); in mkBVSge()
478 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkAnd()
483 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkOr()
489 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, in mkEqual()
490 toZ3Expr(*RHS).AST))); in mkEqual()
495 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST))); in mkFPNeg()
500 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsInfinite()
505 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsNaN()
510 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsNormal()
515 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsZero()
522 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPMul()
523 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPMul()
530 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPDiv()
531 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPDiv()
536 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, in mkFPRem()
537 toZ3Expr(*RHS).AST))); in mkFPRem()
544 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPAdd()
545 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPAdd()
552 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPSub()
553 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPSub()
558 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, in mkFPLt()
559 toZ3Expr(*RHS).AST))); in mkFPLt()
564 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, in mkFPGt()
565 toZ3Expr(*RHS).AST))); in mkFPGt()
570 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, in mkFPLe()
571 toZ3Expr(*RHS).AST))); in mkFPLe()
576 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, in mkFPGe()
577 toZ3Expr(*RHS).AST))); in mkFPGe()
582 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, in mkFPEqual()
583 toZ3Expr(*RHS).AST))); in mkFPEqual()
589 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST, in mkIte()
590 toZ3Expr(*T).AST, toZ3Expr(*F).AST))); in mkIte()
595 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST))); in mkBVSignExt()
600 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST))); in mkBVZeroExt()
606 toZ3Expr(*Exp).AST))); in mkBVExtract()
614 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoOverflow()
615 toZ3Expr(*RHS).AST, isSigned))); in mkBVAddNoOverflow()
623 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoUnderflow()
624 toZ3Expr(*RHS).AST))); in mkBVAddNoUnderflow()
632 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoOverflow()
633 toZ3Expr(*RHS).AST))); in mkBVSubNoOverflow()
641 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoUnderflow()
642 toZ3Expr(*RHS).AST, isSigned))); in mkBVSubNoUnderflow()
650 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDivNoOverflow()
651 toZ3Expr(*RHS).AST))); in mkBVSDivNoOverflow()
658 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNegNoOverflow()
666 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoOverflow()
667 toZ3Expr(*RHS).AST, isSigned))); in mkBVMulNoOverflow()
675 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoUnderflow()
676 toZ3Expr(*RHS).AST))); in mkBVMulNoUnderflow()
681 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, in mkBVConcat()
682 toZ3Expr(*RHS).AST))); in mkBVConcat()
689 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoFP()
690 toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); in mkFPtoFP()
697 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST, in mkSBVtoFP()
698 toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); in mkSBVtoFP()
705 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST, in mkUBVtoFP()
706 toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); in mkUBVtoFP()
712 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoSBV()
713 toZ3Expr(*From).AST, ToWidth))); in mkFPtoSBV()
719 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoUBV()
720 toZ3Expr(*From).AST, ToWidth))); in mkFPtoUBV()
757 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, in mkFloat()
772 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), in getBitvector()
778 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE; in getBoolean()
786 bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST, in toAPFloat() argument
794 if (!toAPSInt(BVSort, AST, Int, true)) { in toAPFloat()
807 bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST, in toAPSInt() argument
823 Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned()); in toAPSInt()
837 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)), in toAPSInt()
848 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); in getInterpretation()
862 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); in getInterpretation()