Lines Matching refs:Solver
27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
30 return Solver->getBoolSort();
33 return Solver->getFloatSort(BitWidth);
35 return Solver->getBitvectorSort(BitWidth);
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
44 return Solver->mkBVNeg(Exp);
47 return Solver->mkBVNot(Exp);
50 return Solver->mkNot(Exp);
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
63 return Solver->mkFPNeg(Exp);
66 return fromUnOp(Solver, Op, Exp);
75 fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op,
84 res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
85 : Solver->mkOr(res, ASTs[i]);
90 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,
95 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
101 return Solver->mkBVMul(LHS, RHS);
104 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
107 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
111 return Solver->mkBVAdd(LHS, RHS);
114 return Solver->mkBVSub(LHS, RHS);
118 return Solver->mkBVShl(LHS, RHS);
121 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
125 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
128 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
131 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
134 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
138 return Solver->mkEqual(LHS, RHS);
141 return fromUnOp(Solver, UO_LNot,
142 fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
146 return Solver->mkBVAnd(LHS, RHS);
149 return Solver->mkBVXor(LHS, RHS);
152 return Solver->mkBVOr(LHS, RHS);
156 return Solver->mkAnd(LHS, RHS);
159 return Solver->mkOr(LHS, RHS);
169 fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
177 return Solver->mkFPIsInfinite(LHS);
180 return Solver->mkFPIsNaN(LHS);
183 return Solver->mkFPIsNormal(LHS);
186 return Solver->mkFPIsZero(LHS);
191 return fromFloatUnOp(Solver, UO_LNot,
192 fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
201 static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,
205 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
211 return Solver->mkFPMul(LHS, RHS);
214 return Solver->mkFPDiv(LHS, RHS);
217 return Solver->mkFPRem(LHS, RHS);
221 return Solver->mkFPAdd(LHS, RHS);
224 return Solver->mkFPSub(LHS, RHS);
228 return Solver->mkFPLt(LHS, RHS);
231 return Solver->mkFPGt(LHS, RHS);
234 return Solver->mkFPLe(LHS, RHS);
237 return Solver->mkFPGe(LHS, RHS);
241 return Solver->mkFPEqual(LHS, RHS);
244 return fromFloatUnOp(Solver, UO_LNot,
245 fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
250 return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
260 static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,
273 return Solver->mkIte(
274 Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
275 Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
280 ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
281 : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
284 return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
298 llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
300 ? Solver->mkSBVtoFP(Exp, Sort)
301 : Solver->mkUBVtoFP(Exp, Sort);
306 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
307 : Solver->mkFPtoUBV(Exp, ToBitWidth);
313 static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
323 fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
331 return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
335 static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
339 return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
346 getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
352 doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
374 ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
375 : fromBinOp(Solver, NewLHS, Op, NewRHS,
381 static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
391 getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison);
395 Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
396 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
403 Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
405 getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
406 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
411 getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison);
413 getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
414 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
422 static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
430 return fromData(Solver, Ctx, SD);
439 getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
446 return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
455 getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
458 ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
459 : fromUnOp(Solver, USE->getOpcode(), OperandExp);
468 return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
475 getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
489 static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
497 return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
501 static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
508 return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
509 Solver->mkFloat(Zero));
518 return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
521 Solver, Exp, Assumption ? BO_EQ : BO_NE,
522 Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
532 getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
539 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
543 llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
547 return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
554 Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
559 getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
561 llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
565 return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
595 static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
606 Solver, Ctx, LHS, LTy, RHS, RTy);
612 Solver, Ctx, LHS, LTy, RHS, RTy);
632 LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
635 RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
670 template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
672 static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
684 LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
691 RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
708 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
711 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
718 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
721 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
729 RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
732 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
742 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
744 LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
752 template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
755 doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
762 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
767 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
780 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
783 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);