144 class Z3Expr : public SMTExpr {  class
152   Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {  in Z3Expr()  function in __anon13641eda0111::Z3Expr
157   Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {  in Z3Expr()  function in __anon13641eda0111::Z3Expr
163   Z3Expr &operator=(const Z3Expr &Other) {  in operator =()
170   Z3Expr(Z3Expr &&Other) = delete;
171   Z3Expr &operator=(Z3Expr &&Other) = delete;
173   ~Z3Expr() {  in ~Z3Expr()
186                                      static_cast<const Z3Expr &>(Other).AST)) &&  in equal_to()
189                         static_cast<const Z3Expr &>(Other).AST);  in equal_to()
197 static const Z3Expr &toZ3Expr(const SMTExpr &E) {  in toZ3Expr()
198   return static_cast<const Z3Expr &>(E);  in toZ3Expr()
271   std::set<Z3Expr> CachedExprs;
338         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNeg()
343         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNot()
348         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));  in mkNot()
353         Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAdd()
359         Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSub()
365         Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,  in mkBVMul()
371         Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSRem()
377         Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,  in mkBVURem()
383         Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSDiv()
389         Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUDiv()
395         Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,  in mkBVShl()
401         Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAshr()
407         Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,  in mkBVLshr()
413         Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,  in mkBVXor()
419         Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,  in mkBVOr()
425         Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,  in mkBVAnd()
431         Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUlt()
437         Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSlt()
443         Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUgt()
449         Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSgt()
455         Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUle()
461         Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSle()
467         Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,  in mkBVUge()
473         Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,  in mkBVSge()
479     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));  in mkAnd()
484     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));  in mkOr()
489         Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,  in mkEqual()
495         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPNeg()
499     return newExprRef(Z3Expr(  in mkFPIsInfinite()
505         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNaN()
509     return newExprRef(Z3Expr(  in mkFPIsNormal()
514     return newExprRef(Z3Expr(  in mkFPIsZero()
521         Z3Expr(Context,  in mkFPMul()
529         Z3Expr(Context,  in mkFPDiv()
536         Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,  in mkFPRem()
543         Z3Expr(Context,  in mkFPAdd()
551         Z3Expr(Context,  in mkFPSub()
558         Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,  in mkFPLt()
564         Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,  in mkFPGt()
570         Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPLe()
576         Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPGe()
582         Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,  in mkFPEqual()
589         Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,  in mkIte()
594     return newExprRef(Z3Expr(  in mkBVSignExt()
599     return newExprRef(Z3Expr(  in mkBVZeroExt()
605     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,  in mkBVExtract()
613     return newExprRef(Z3Expr(  in mkBVAddNoOverflow()
622     return newExprRef(Z3Expr(  in mkBVAddNoUnderflow()
631     return newExprRef(Z3Expr(  in mkBVSubNoOverflow()
640     return newExprRef(Z3Expr(  in mkBVSubNoUnderflow()
649     return newExprRef(Z3Expr(  in mkBVSDivNoOverflow()
657     return newExprRef(Z3Expr(  in mkBVNegNoOverflow()
665     return newExprRef(Z3Expr(  in mkBVMulNoOverflow()
674     return newExprRef(Z3Expr(  in mkBVMulNoUnderflow()
681         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,  in mkBVConcat()
687     return newExprRef(Z3Expr(  in mkFPtoFP()
695     return newExprRef(Z3Expr(  in mkSBVtoFP()
703     return newExprRef(Z3Expr(  in mkUBVtoFP()
711     return newExprRef(Z3Expr(  in mkFPtoSBV()
718     return newExprRef(Z3Expr(  in mkFPtoUBV()
724     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)  in mkBoolean()
735       return newExprRef(Z3Expr(  in mkBitvector()
747     return newExprRef(Z3Expr(Context, Literal));  in mkBitvector()
756     return newExprRef(Z3Expr(  in mkFloat()
763         Z3Expr(Context, Z3_mk_const(Context.Context,  in mkSymbol()
783     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));  in getFloatRoundingMode()
853         Z3Expr(Context,  in getInterpretation()
867         Z3Expr(Context,  in getInterpretation()