Lines Matching refs:Exp
41 const llvm::SMTExprRef &Exp) {
44 return Solver->mkBVNeg(Exp);
47 return Solver->mkBVNot(Exp);
50 return Solver->mkNot(Exp);
60 const llvm::SMTExprRef &Exp) {
63 return Solver->mkFPNeg(Exp);
66 return fromUnOp(Solver, Op, Exp);
261 const llvm::SMTExprRef &Exp,
274 Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
280 ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
281 : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
284 return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
287 return Exp;
292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
294 return Exp;
300 ? Solver->mkSBVtoFP(Exp, Sort)
301 : Solver->mkUBVtoFP(Exp, Sort);
306 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
307 : Solver->mkFPtoUBV(Exp, ToBitWidth);
332 const llvm::SMTExprRef &Exp,
334 return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
434 llvm::SMTExprRef Exp =
442 return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
446 llvm::SMTExprRef Exp =
451 return Exp;
475 const llvm::SMTExprRef &Exp,
480 return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
490 return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
493 Solver, Exp, Assumption ? BO_EQ : BO_NE,
515 llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
519 return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
531 getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
533 llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,