Lines Matching refs:toZ3Expr
195 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
300 auto It = CachedExprs.insert(toZ3Expr(Exp));
315 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
336 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
341 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
346 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
351 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
352 toZ3Expr(*RHS).AST)));
357 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
358 toZ3Expr(*RHS).AST)));
363 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
364 toZ3Expr(*RHS).AST)));
369 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
370 toZ3Expr(*RHS).AST)));
375 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
376 toZ3Expr(*RHS).AST)));
381 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
382 toZ3Expr(*RHS).AST)));
387 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
388 toZ3Expr(*RHS).AST)));
393 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
394 toZ3Expr(*RHS).AST)));
399 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
400 toZ3Expr(*RHS).AST)));
405 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
406 toZ3Expr(*RHS).AST)));
411 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
412 toZ3Expr(*RHS).AST)));
417 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
418 toZ3Expr(*RHS).AST)));
423 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
424 toZ3Expr(*RHS).AST)));
429 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
430 toZ3Expr(*RHS).AST)));
435 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
436 toZ3Expr(*RHS).AST)));
441 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
442 toZ3Expr(*RHS).AST)));
447 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
448 toZ3Expr(*RHS).AST)));
453 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
454 toZ3Expr(*RHS).AST)));
459 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
460 toZ3Expr(*RHS).AST)));
465 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
466 toZ3Expr(*RHS).AST)));
471 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
472 toZ3Expr(*RHS).AST)));
476 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
481 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
487 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
488 toZ3Expr(*RHS).AST)));
493 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
498 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
503 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
508 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
513 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
520 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
521 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
528 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
529 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
534 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
535 toZ3Expr(*RHS).AST)));
542 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
543 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
550 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
551 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
556 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
557 toZ3Expr(*RHS).AST)));
562 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
563 toZ3Expr(*RHS).AST)));
568 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
569 toZ3Expr(*RHS).AST)));
574 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
575 toZ3Expr(*RHS).AST)));
580 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
581 toZ3Expr(*RHS).AST)));
587 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
588 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
593 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
598 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
604 toZ3Expr(*Exp).AST)));
612 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
613 toZ3Expr(*RHS).AST, isSigned)));
621 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
622 toZ3Expr(*RHS).AST)));
630 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
631 toZ3Expr(*RHS).AST)));
639 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
640 toZ3Expr(*RHS).AST, isSigned)));
648 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
649 toZ3Expr(*RHS).AST)));
656 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
664 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
665 toZ3Expr(*RHS).AST, isSigned)));
673 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
674 toZ3Expr(*RHS).AST)));
679 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
680 toZ3Expr(*RHS).AST)));
687 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
688 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
695 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
696 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
703 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
704 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
710 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
711 toZ3Expr(*From).AST, ToWidth)));
717 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
718 toZ3Expr(*From).AST, ToWidth)));
755 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
770 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
776 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
846 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
860 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));