Lines Matching defs:Exp

300   void addConstraint(const SMTExprRef &Exp) const override {
301     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
313   SMTExprRef newExprRef(const SMTExpr &Exp) {
314     auto It = CachedExprs.insert(toZ3Expr(Exp));
327   SMTSortRef getSort(const SMTExprRef &Exp) override {
329         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
348   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
350         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
353   SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
355         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
358   SMTExprRef mkNot(const SMTExprRef &Exp) override {
360         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
505   SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
507         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
510   SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
512         Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
515   SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
517         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
520   SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
522         Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
525   SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
527         Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
605   SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
607         Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
610   SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
612         Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
616                          const SMTExprRef &Exp) override {
618                                                     toZ3Expr(*Exp).AST)));
668   SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override {
670         Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
780   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
784                     Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
789   bool getBoolean(const SMTExprRef &Exp) override {
790     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
857   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
860         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
871   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
874         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));