Lines Matching defs:Z3Expr
149 class Z3Expr : public SMTExpr {
157 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
162 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
168 Z3Expr &operator=(const Z3Expr &Other) {
175 Z3Expr(Z3Expr &&Other) = delete;
176 Z3Expr &operator=(Z3Expr &&Other) = delete;
178 ~Z3Expr() {
191 static_cast<const Z3Expr &>(Other).AST)) &&
194 static_cast<const Z3Expr &>(Other).AST);
200 }; // end class Z3Expr
202 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
203 return static_cast<const Z3Expr &>(E);
286 std::set<Z3Expr> CachedExprs;
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,
371 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
377 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
383 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
389 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
395 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
401 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
407 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
413 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
419 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
425 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
431 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
437 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
443 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
449 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
455 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
461 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
467 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
473 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
479 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
485 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
491 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
496 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
501 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
507 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
511 return newExprRef(Z3Expr(
517 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
521 return newExprRef(Z3Expr(
526 return newExprRef(Z3Expr(
533 Z3Expr(Context,
541 Z3Expr(Context,
548 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
555 Z3Expr(Context,
563 Z3Expr(Context,
570 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
576 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
582 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
588 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
594 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
601 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
606 return newExprRef(Z3Expr(
611 return newExprRef(Z3Expr(
617 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
625 return newExprRef(Z3Expr(
634 return newExprRef(Z3Expr(
643 return newExprRef(Z3Expr(
652 return newExprRef(Z3Expr(
661 return newExprRef(Z3Expr(
669 return newExprRef(Z3Expr(
677 return newExprRef(Z3Expr(
686 return newExprRef(Z3Expr(
693 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
699 return newExprRef(Z3Expr(
707 return newExprRef(Z3Expr(
715 return newExprRef(Z3Expr(
723 return newExprRef(Z3Expr(
730 return newExprRef(Z3Expr(
736 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
747 return newExprRef(Z3Expr(
759 return newExprRef(Z3Expr(Context, Literal));
768 return newExprRef(Z3Expr(
775 Z3Expr(Context, Z3_mk_const(Context.Context,
795 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
865 Z3Expr(Context,
879 Z3Expr(Context,