|
| SMTSolver ()=default |
|
virtual | ~SMTSolver ()=default |
|
LLVM_DUMP_METHOD void | dump () const |
|
SMTSortRef | getFloatSort (unsigned BitWidth) |
|
virtual SMTSortRef | getBoolSort ()=0 |
|
virtual SMTSortRef | getBitvectorSort (const unsigned BitWidth)=0 |
|
virtual SMTSortRef | getFloat16Sort ()=0 |
|
virtual SMTSortRef | getFloat32Sort ()=0 |
|
virtual SMTSortRef | getFloat64Sort ()=0 |
|
virtual SMTSortRef | getFloat128Sort ()=0 |
|
virtual SMTSortRef | getSort (const SMTExprRef &AST)=0 |
|
virtual void | addConstraint (const SMTExprRef &Exp) const =0 |
| Given a constraint, adds it to the solver. More...
|
|
virtual SMTExprRef | mkBVAdd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector addition operation. More...
|
|
virtual SMTExprRef | mkBVSub (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector subtraction operation. More...
|
|
virtual SMTExprRef | mkBVMul (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector multiplication operation. More...
|
|
virtual SMTExprRef | mkBVSRem (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector signed modulus operation. More...
|
|
virtual SMTExprRef | mkBVURem (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector unsigned modulus operation. More...
|
|
virtual SMTExprRef | mkBVSDiv (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector signed division operation. More...
|
|
virtual SMTExprRef | mkBVUDiv (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector unsigned division operation. More...
|
|
virtual SMTExprRef | mkBVShl (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector logical shift left operation. More...
|
|
virtual SMTExprRef | mkBVAshr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector arithmetic shift right operation. More...
|
|
virtual SMTExprRef | mkBVLshr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector logical shift right operation. More...
|
|
virtual SMTExprRef | mkBVNeg (const SMTExprRef &Exp)=0 |
| Creates a bitvector negation operation. More...
|
|
virtual SMTExprRef | mkBVNot (const SMTExprRef &Exp)=0 |
| Creates a bitvector not operation. More...
|
|
virtual SMTExprRef | mkBVXor (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector xor operation. More...
|
|
virtual SMTExprRef | mkBVOr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector or operation. More...
|
|
virtual SMTExprRef | mkBVAnd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector and operation. More...
|
|
virtual SMTExprRef | mkBVUlt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector unsigned less-than operation. More...
|
|
virtual SMTExprRef | mkBVSlt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector signed less-than operation. More...
|
|
virtual SMTExprRef | mkBVUgt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector unsigned greater-than operation. More...
|
|
virtual SMTExprRef | mkBVSgt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector signed greater-than operation. More...
|
|
virtual SMTExprRef | mkBVUle (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector unsigned less-equal-than operation. More...
|
|
virtual SMTExprRef | mkBVSle (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector signed less-equal-than operation. More...
|
|
virtual SMTExprRef | mkBVUge (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector unsigned greater-equal-than operation. More...
|
|
virtual SMTExprRef | mkBVSge (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector signed greater-equal-than operation. More...
|
|
virtual SMTExprRef | mkNot (const SMTExprRef &Exp)=0 |
| Creates a boolean not operation. More...
|
|
virtual SMTExprRef | mkEqual (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a boolean equality operation. More...
|
|
virtual SMTExprRef | mkAnd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a boolean and operation. More...
|
|
virtual SMTExprRef | mkOr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a boolean or operation. More...
|
|
virtual SMTExprRef | mkIte (const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0 |
| Creates a boolean ite operation. More...
|
|
virtual SMTExprRef | mkBVSignExt (unsigned i, const SMTExprRef &Exp)=0 |
| Creates a bitvector sign extension operation. More...
|
|
virtual SMTExprRef | mkBVZeroExt (unsigned i, const SMTExprRef &Exp)=0 |
| Creates a bitvector zero extension operation. More...
|
|
virtual SMTExprRef | mkBVExtract (unsigned High, unsigned Low, const SMTExprRef &Exp)=0 |
| Creates a bitvector extract operation. More...
|
|
virtual SMTExprRef | mkBVConcat (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a bitvector concat operation. More...
|
|
virtual SMTExprRef | mkBVAddNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0 |
| Creates a predicate that checks for overflow in a bitvector addition operation. More...
|
|
virtual SMTExprRef | mkBVAddNoUnderflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a predicate that checks for underflow in a signed bitvector addition operation. More...
|
|
virtual SMTExprRef | mkBVSubNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a predicate that checks for overflow in a signed bitvector subtraction operation. More...
|
|
virtual SMTExprRef | mkBVSubNoUnderflow (const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0 |
| Creates a predicate that checks for underflow in a bitvector subtraction operation. More...
|
|
virtual SMTExprRef | mkBVSDivNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a predicate that checks for overflow in a signed bitvector division/modulus operation. More...
|
|
virtual SMTExprRef | mkBVNegNoOverflow (const SMTExprRef &Exp)=0 |
| Creates a predicate that checks for overflow in a bitvector negation operation. More...
|
|
virtual SMTExprRef | mkBVMulNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0 |
| Creates a predicate that checks for overflow in a bitvector multiplication operation. More...
|
|
virtual SMTExprRef | mkBVMulNoUnderflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a predicate that checks for underflow in a signed bitvector multiplication operation. More...
|
|
virtual SMTExprRef | mkFPNeg (const SMTExprRef &Exp)=0 |
| Creates a floating-point negation operation. More...
|
|
virtual SMTExprRef | mkFPIsInfinite (const SMTExprRef &Exp)=0 |
| Creates a floating-point isInfinite operation. More...
|
|
virtual SMTExprRef | mkFPIsNaN (const SMTExprRef &Exp)=0 |
| Creates a floating-point isNaN operation. More...
|
|
virtual SMTExprRef | mkFPIsNormal (const SMTExprRef &Exp)=0 |
| Creates a floating-point isNormal operation. More...
|
|
virtual SMTExprRef | mkFPIsZero (const SMTExprRef &Exp)=0 |
| Creates a floating-point isZero operation. More...
|
|
virtual SMTExprRef | mkFPMul (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point multiplication operation. More...
|
|
virtual SMTExprRef | mkFPDiv (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point division operation. More...
|
|
virtual SMTExprRef | mkFPRem (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point remainder operation. More...
|
|
virtual SMTExprRef | mkFPAdd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point addition operation. More...
|
|
virtual SMTExprRef | mkFPSub (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point subtraction operation. More...
|
|
virtual SMTExprRef | mkFPLt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point less-than operation. More...
|
|
virtual SMTExprRef | mkFPGt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point greater-than operation. More...
|
|
virtual SMTExprRef | mkFPLe (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point less-than-or-equal operation. More...
|
|
virtual SMTExprRef | mkFPGe (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point greater-than-or-equal operation. More...
|
|
virtual SMTExprRef | mkFPEqual (const SMTExprRef &LHS, const SMTExprRef &RHS)=0 |
| Creates a floating-point equality operation. More...
|
|
virtual SMTExprRef | mkFPtoFP (const SMTExprRef &From, const SMTSortRef &To)=0 |
| Creates a floating-point conversion from floatint-point to floating-point operation. More...
|
|
virtual SMTExprRef | mkSBVtoFP (const SMTExprRef &From, const SMTSortRef &To)=0 |
| Creates a floating-point conversion from signed bitvector to floatint-point operation. More...
|
|
virtual SMTExprRef | mkUBVtoFP (const SMTExprRef &From, const SMTSortRef &To)=0 |
| Creates a floating-point conversion from unsigned bitvector to floatint-point operation. More...
|
|
virtual SMTExprRef | mkFPtoSBV (const SMTExprRef &From, unsigned ToWidth)=0 |
| Creates a floating-point conversion from floatint-point to signed bitvector operation. More...
|
|
virtual SMTExprRef | mkFPtoUBV (const SMTExprRef &From, unsigned ToWidth)=0 |
| Creates a floating-point conversion from floatint-point to unsigned bitvector operation. More...
|
|
virtual SMTExprRef | mkSymbol (const char *Name, SMTSortRef Sort)=0 |
| Creates a new symbol, given a name and a sort. More...
|
|
virtual SMTExprRef | getFloatRoundingMode ()=0 |
|
virtual llvm::APSInt | getBitvector (const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0 |
|
virtual bool | getBoolean (const SMTExprRef &Exp)=0 |
|
virtual SMTExprRef | mkBoolean (const bool b)=0 |
| Constructs an SMTExprRef from a boolean. More...
|
|
virtual SMTExprRef | mkFloat (const llvm::APFloat Float)=0 |
| Constructs an SMTExprRef from a finite APFloat. More...
|
|
virtual SMTExprRef | mkBitvector (const llvm::APSInt Int, unsigned BitWidth)=0 |
| Constructs an SMTExprRef from an APSInt and its bit width. More...
|
|
virtual bool | getInterpretation (const SMTExprRef &Exp, llvm::APSInt &Int)=0 |
| Given an expression, extract the value of this operand in the model. More...
|
|
virtual bool | getInterpretation (const SMTExprRef &Exp, llvm::APFloat &Float)=0 |
| Given an expression extract the value of this operand in the model. More...
|
|
virtual Optional< bool > | check () const =0 |
| Check if the constraints are satisfiable. More...
|
|
virtual void | push ()=0 |
| Push the current solver state. More...
|
|
virtual void | pop (unsigned NumStates=1)=0 |
| Pop the previous solver state. More...
|
|
virtual void | reset ()=0 |
| Reset the solver and remove all constraints. More...
|
|
virtual bool | isFPSupported ()=0 |
| Checks if the solver supports floating-points. More...
|
|
virtual void | print (raw_ostream &OS) const =0 |
|
Generic base class for SMT Solvers.
This class is responsible for wrapping all sorts and expression generation, through the mk* methods. It also provides methods to create SMT expressions straight from clang's AST, through the from* methods.
Definition at line 136 of file SMTAPI.h.