142 class Z3Expr : public SMTExpr {  class
150   Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {  in Z3Expr()  function in __anonca7d1dd80111::Z3Expr
155   Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {  in Z3Expr()  function in __anonca7d1dd80111::Z3Expr
161   Z3Expr &operator=(const Z3Expr &Other) {  in operator =()
168   Z3Expr(Z3Expr &&Other) = delete;
169   Z3Expr &operator=(Z3Expr &&Other) = delete;
171   ~Z3Expr() {  in ~Z3Expr()
184                                      static_cast<const Z3Expr &>(Other).AST)) &&  in equal_to()
187                         static_cast<const Z3Expr &>(Other).AST);  in equal_to()
195 static const Z3Expr &toZ3Expr(const SMTExpr &E) {  in toZ3Expr()
196   return static_cast<const Z3Expr &>(E);  in toZ3Expr()
269   std::set<Z3Expr> CachedExprs;
336         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNeg()
341         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNot()
346         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));  in mkNot()
351         Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAdd()
357         Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSub()
363         Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,  in mkBVMul()
369         Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSRem()
375         Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,  in mkBVURem()
381         Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSDiv()
387         Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUDiv()
393         Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,  in mkBVShl()
399         Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAshr()
405         Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,  in mkBVLshr()
411         Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,  in mkBVXor()
417         Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,  in mkBVOr()
423         Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAnd()
429         Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUlt()
435         Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSlt()
441         Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUgt()
447         Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSgt()
453         Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUle()
459         Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSle()
465         Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUge()
471         Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSge()
477     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));  in mkAnd()
482     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));  in mkOr()
487         Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,  in mkEqual()
493         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPNeg()
497     return newExprRef(Z3Expr(  in mkFPIsInfinite()
503         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNaN()
507     return newExprRef(Z3Expr(  in mkFPIsNormal()
512     return newExprRef(Z3Expr(  in mkFPIsZero()
519         Z3Expr(Context,  in mkFPMul()
527         Z3Expr(Context,  in mkFPDiv()
534         Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,  in mkFPRem()
541         Z3Expr(Context,  in mkFPAdd()
549         Z3Expr(Context,  in mkFPSub()
556         Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,  in mkFPLt()
562         Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,  in mkFPGt()
568         Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPLe()
574         Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPGe()
580         Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPEqual()
587         Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,  in mkIte()
592     return newExprRef(Z3Expr(  in mkBVSignExt()
597     return newExprRef(Z3Expr(  in mkBVZeroExt()
603     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,  in mkBVExtract()
611     return newExprRef(Z3Expr(  in mkBVAddNoOverflow()
620     return newExprRef(Z3Expr(  in mkBVAddNoUnderflow()
629     return newExprRef(Z3Expr(  in mkBVSubNoOverflow()
638     return newExprRef(Z3Expr(  in mkBVSubNoUnderflow()
647     return newExprRef(Z3Expr(  in mkBVSDivNoOverflow()
655     return newExprRef(Z3Expr(  in mkBVNegNoOverflow()
663     return newExprRef(Z3Expr(  in mkBVMulNoOverflow()
672     return newExprRef(Z3Expr(  in mkBVMulNoUnderflow()
679         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,  in mkBVConcat()
685     return newExprRef(Z3Expr(  in mkFPtoFP()
693     return newExprRef(Z3Expr(  in mkSBVtoFP()
701     return newExprRef(Z3Expr(  in mkUBVtoFP()
709     return newExprRef(Z3Expr(  in mkFPtoSBV()
716     return newExprRef(Z3Expr(  in mkFPtoUBV()
722     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)  in mkBoolean()
733       return newExprRef(Z3Expr(  in mkBitvector()
745     return newExprRef(Z3Expr(Context, Literal));  in mkBitvector()
754     return newExprRef(Z3Expr(  in mkFloat()
761         Z3Expr(Context, Z3_mk_const(Context.Context,  in mkSymbol()
781     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));  in getFloatRoundingMode()
851         Z3Expr(Context,  in getInterpretation()
865         Z3Expr(Context,  in getInterpretation()