149 class Z3Expr : public SMTExpr {  class
157   Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {  in Z3Expr()  function in __anona2cc94240111::Z3Expr
162   Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {  in Z3Expr()  function in __anona2cc94240111::Z3Expr
168   Z3Expr &operator=(const Z3Expr &Other) {  in operator =()
175   Z3Expr(Z3Expr &&Other) = delete;
176   Z3Expr &operator=(Z3Expr &&Other) = delete;
178   ~Z3Expr() {  in ~Z3Expr()
191                                      static_cast<const Z3Expr &>(Other).AST)) &&  in equal_to()
194                         static_cast<const Z3Expr &>(Other).AST);  in equal_to()
202 static const Z3Expr &toZ3Expr(const SMTExpr &E) {  in toZ3Expr()
203   return static_cast<const Z3Expr &>(E);  in toZ3Expr()
286   std::set<Z3Expr> CachedExprs;
350         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNeg()
355         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNot()
360         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));  in mkNot()
365         Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAdd()
371         Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSub()
377         Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,  in mkBVMul()
383         Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSRem()
389         Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,  in mkBVURem()
395         Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSDiv()
401         Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUDiv()
407         Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,  in mkBVShl()
413         Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAshr()
419         Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,  in mkBVLshr()
425         Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,  in mkBVXor()
431         Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,  in mkBVOr()
437         Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAnd()
443         Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUlt()
449         Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSlt()
455         Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUgt()
461         Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSgt()
467         Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUle()
473         Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSle()
479         Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUge()
485         Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSge()
491     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));  in mkAnd()
496     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));  in mkOr()
501         Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,  in mkEqual()
507         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPNeg()
511     return newExprRef(Z3Expr(  in mkFPIsInfinite()
517         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNaN()
521     return newExprRef(Z3Expr(  in mkFPIsNormal()
526     return newExprRef(Z3Expr(  in mkFPIsZero()
533         Z3Expr(Context,  in mkFPMul()
541         Z3Expr(Context,  in mkFPDiv()
548         Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,  in mkFPRem()
555         Z3Expr(Context,  in mkFPAdd()
563         Z3Expr(Context,  in mkFPSub()
570         Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,  in mkFPLt()
576         Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,  in mkFPGt()
582         Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPLe()
588         Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPGe()
594         Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPEqual()
601         Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,  in mkIte()
606     return newExprRef(Z3Expr(  in mkBVSignExt()
611     return newExprRef(Z3Expr(  in mkBVZeroExt()
617     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,  in mkBVExtract()
625     return newExprRef(Z3Expr(  in mkBVAddNoOverflow()
634     return newExprRef(Z3Expr(  in mkBVAddNoUnderflow()
643     return newExprRef(Z3Expr(  in mkBVSubNoOverflow()
652     return newExprRef(Z3Expr(  in mkBVSubNoUnderflow()
661     return newExprRef(Z3Expr(  in mkBVSDivNoOverflow()
669     return newExprRef(Z3Expr(  in mkBVNegNoOverflow()
677     return newExprRef(Z3Expr(  in mkBVMulNoOverflow()
686     return newExprRef(Z3Expr(  in mkBVMulNoUnderflow()
693         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,  in mkBVConcat()
699     return newExprRef(Z3Expr(  in mkFPtoFP()
707     return newExprRef(Z3Expr(  in mkSBVtoFP()
715     return newExprRef(Z3Expr(  in mkUBVtoFP()
723     return newExprRef(Z3Expr(  in mkFPtoSBV()
730     return newExprRef(Z3Expr(  in mkFPtoUBV()
736     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)  in mkBoolean()
747       return newExprRef(Z3Expr(  in mkBitvector()
759     return newExprRef(Z3Expr(Context, Literal));  in mkBitvector()
768     return newExprRef(Z3Expr(  in mkFloat()
775         Z3Expr(Context, Z3_mk_const(Context.Context,  in mkSymbol()
795     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));  in getFloatRoundingMode()
865         Z3Expr(Context,  in getInterpretation()
879         Z3Expr(Context,  in getInterpretation()