Lines Matching refs:Z3Expr
142 class Z3Expr : public SMTExpr {
150 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
155 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
161 Z3Expr &operator=(const Z3Expr &Other) {
168 Z3Expr(Z3Expr &&Other) = delete;
169 Z3Expr &operator=(Z3Expr &&Other) = delete;
171 ~Z3Expr() {
184 static_cast<const Z3Expr &>(Other).AST)) &&
187 static_cast<const Z3Expr &>(Other).AST);
193 }; // end class Z3Expr
195 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
196 return static_cast<const Z3Expr &>(E);
269 std::set<Z3Expr> CachedExprs;
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,
357 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
363 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
369 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
375 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
381 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
387 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
393 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
399 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
405 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
411 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
417 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
423 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
429 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
435 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
441 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
447 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
453 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
459 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
465 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
471 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
477 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
482 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
487 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
493 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
497 return newExprRef(Z3Expr(
503 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
507 return newExprRef(Z3Expr(
512 return newExprRef(Z3Expr(
519 Z3Expr(Context,
527 Z3Expr(Context,
534 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
541 Z3Expr(Context,
549 Z3Expr(Context,
556 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
562 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
568 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
574 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
580 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
587 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
592 return newExprRef(Z3Expr(
597 return newExprRef(Z3Expr(
603 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
611 return newExprRef(Z3Expr(
620 return newExprRef(Z3Expr(
629 return newExprRef(Z3Expr(
638 return newExprRef(Z3Expr(
647 return newExprRef(Z3Expr(
655 return newExprRef(Z3Expr(
663 return newExprRef(Z3Expr(
672 return newExprRef(Z3Expr(
679 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
685 return newExprRef(Z3Expr(
693 return newExprRef(Z3Expr(
701 return newExprRef(Z3Expr(
709 return newExprRef(Z3Expr(
716 return newExprRef(Z3Expr(
722 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
733 return newExprRef(Z3Expr(
745 return newExprRef(Z3Expr(Context, Literal));
754 return newExprRef(Z3Expr(
761 Z3Expr(Context, Z3_mk_const(Context.Context,
781 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
851 Z3Expr(Context,
865 Z3Expr(Context,