llvm::SMTSolver Member List
This is the complete list of members for llvm::SMTSolver, including all inherited members.
| addConstraint(const SMTExprRef &Exp) const =0 | llvm::SMTSolver | pure virtual |
| check() const =0 | llvm::SMTSolver | pure virtual |
| dump() const | llvm::SMTSolver | |
| getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0 | llvm::SMTSolver | pure virtual |
| getBitvectorSort(const unsigned BitWidth)=0 | llvm::SMTSolver | pure virtual |
| getBoolean(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| getBoolSort()=0 | llvm::SMTSolver | pure virtual |
| getFloat128Sort()=0 | llvm::SMTSolver | pure virtual |
| getFloat16Sort()=0 | llvm::SMTSolver | pure virtual |
| getFloat32Sort()=0 | llvm::SMTSolver | pure virtual |
| getFloat64Sort()=0 | llvm::SMTSolver | pure virtual |
| getFloatRoundingMode()=0 | llvm::SMTSolver | pure virtual |
| getFloatSort(unsigned BitWidth) | llvm::SMTSolver | inline |
| getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0 | llvm::SMTSolver | pure virtual |
| getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float)=0 | llvm::SMTSolver | pure virtual |
| getSort(const SMTExprRef &AST)=0 | llvm::SMTSolver | pure virtual |
| getStatistics() const =0 | llvm::SMTSolver | pure virtual |
| isFPSupported()=0 | llvm::SMTSolver | pure virtual |
| mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0 | llvm::SMTSolver | pure virtual |
| mkBoolean(const bool b)=0 | llvm::SMTSolver | pure virtual |
| mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0 | llvm::SMTSolver | pure virtual |
| mkBVAddNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0 | llvm::SMTSolver | pure virtual |
| mkBVMulNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVNeg(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkBVNegNoOverflow(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkBVNot(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSDivNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSubNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0 | llvm::SMTSolver | pure virtual |
| mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFloat(const llvm::APFloat Float)=0 | llvm::SMTSolver | pure virtual |
| mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPIsInfinite(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkFPIsNaN(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkFPIsNormal(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkFPIsZero(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPNeg(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0 | llvm::SMTSolver | pure virtual |
| mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0 | llvm::SMTSolver | pure virtual |
| mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0 | llvm::SMTSolver | pure virtual |
| mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0 | llvm::SMTSolver | pure virtual |
| mkNot(const SMTExprRef &Exp)=0 | llvm::SMTSolver | pure virtual |
| mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0 | llvm::SMTSolver | pure virtual |
| mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0 | llvm::SMTSolver | pure virtual |
| mkSymbol(const char *Name, SMTSortRef Sort)=0 | llvm::SMTSolver | pure virtual |
| mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0 | llvm::SMTSolver | pure virtual |
| pop(unsigned NumStates=1)=0 | llvm::SMTSolver | pure virtual |
| print(raw_ostream &OS) const =0 | llvm::SMTSolver | pure virtual |
| push()=0 | llvm::SMTSolver | pure virtual |
| reset()=0 | llvm::SMTSolver | pure virtual |
| setBoolParam(StringRef Key, bool Value)=0 | llvm::SMTSolver | pure virtual |
| setUnsignedParam(StringRef Key, unsigned Value)=0 | llvm::SMTSolver | pure virtual |
| SMTSolver()=default | llvm::SMTSolver | |
| ~SMTSolver()=default | llvm::SMTSolver | virtual |
Generated on for LLVM by
1.14.0