LLVM 19.0.0git
llvm::SMTSolver Member List

This is the complete list of members for llvm::SMTSolver, including all inherited members.

addConstraint(const SMTExprRef &Exp) const =0llvm::SMTSolverpure virtual
check() const =0llvm::SMTSolverpure virtual
dump() constllvm::SMTSolver
getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0llvm::SMTSolverpure virtual
getBitvectorSort(const unsigned BitWidth)=0llvm::SMTSolverpure virtual
getBoolean(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
getBoolSort()=0llvm::SMTSolverpure virtual
getFloat128Sort()=0llvm::SMTSolverpure virtual
getFloat16Sort()=0llvm::SMTSolverpure virtual
getFloat32Sort()=0llvm::SMTSolverpure virtual
getFloat64Sort()=0llvm::SMTSolverpure virtual
getFloatRoundingMode()=0llvm::SMTSolverpure virtual
getFloatSort(unsigned BitWidth)llvm::SMTSolverinline
getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0llvm::SMTSolverpure virtual
getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float)=0llvm::SMTSolverpure virtual
getSort(const SMTExprRef &AST)=0llvm::SMTSolverpure virtual
isFPSupported()=0llvm::SMTSolverpure virtual
mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0llvm::SMTSolverpure virtual
mkBoolean(const bool b)=0llvm::SMTSolverpure virtual
mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0llvm::SMTSolverpure virtual
mkBVAddNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0llvm::SMTSolverpure virtual
mkBVMulNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVNeg(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkBVNegNoOverflow(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkBVNot(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSDivNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSubNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0llvm::SMTSolverpure virtual
mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFloat(const llvm::APFloat Float)=0llvm::SMTSolverpure virtual
mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPIsInfinite(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkFPIsNaN(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkFPIsNormal(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkFPIsZero(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPNeg(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0llvm::SMTSolverpure virtual
mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0llvm::SMTSolverpure virtual
mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0llvm::SMTSolverpure virtual
mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0llvm::SMTSolverpure virtual
mkNot(const SMTExprRef &Exp)=0llvm::SMTSolverpure virtual
mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0llvm::SMTSolverpure virtual
mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0llvm::SMTSolverpure virtual
mkSymbol(const char *Name, SMTSortRef Sort)=0llvm::SMTSolverpure virtual
mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0llvm::SMTSolverpure virtual
pop(unsigned NumStates=1)=0llvm::SMTSolverpure virtual
print(raw_ostream &OS) const =0llvm::SMTSolverpure virtual
push()=0llvm::SMTSolverpure virtual
reset()=0llvm::SMTSolverpure virtual
SMTSolver()=defaultllvm::SMTSolver
~SMTSolver()=defaultllvm::SMTSolvervirtual