LLVM: llvm::SMTSolver Class Reference (original) (raw)

Generic base class for SMT Solvers. More...

#include "[llvm/Support/SMTAPI.h](SMTAPI%5F8h%5Fsource.html)"

Public Member Functions
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.
virtual SMTExprRef mkBVAdd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector addition operation.
virtual SMTExprRef mkBVSub (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector subtraction operation.
virtual SMTExprRef mkBVMul (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector multiplication operation.
virtual SMTExprRef mkBVSRem (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed modulus operation.
virtual SMTExprRef mkBVURem (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned modulus operation.
virtual SMTExprRef mkBVSDiv (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed division operation.
virtual SMTExprRef mkBVUDiv (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned division operation.
virtual SMTExprRef mkBVShl (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift left operation.
virtual SMTExprRef mkBVAshr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector arithmetic shift right operation.
virtual SMTExprRef mkBVLshr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift right operation.
virtual SMTExprRef mkBVNeg (const SMTExprRef &Exp)=0
Creates a bitvector negation operation.
virtual SMTExprRef mkBVNot (const SMTExprRef &Exp)=0
Creates a bitvector not operation.
virtual SMTExprRef mkBVXor (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector xor operation.
virtual SMTExprRef mkBVOr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector or operation.
virtual SMTExprRef mkBVAnd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector and operation.
virtual SMTExprRef mkBVUlt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-than operation.
virtual SMTExprRef mkBVSlt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-than operation.
virtual SMTExprRef mkBVUgt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-than operation.
virtual SMTExprRef mkBVSgt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-than operation.
virtual SMTExprRef mkBVUle (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-equal-than operation.
virtual SMTExprRef mkBVSle (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-equal-than operation.
virtual SMTExprRef mkBVUge (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-equal-than operation.
virtual SMTExprRef mkBVSge (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-equal-than operation.
virtual SMTExprRef mkNot (const SMTExprRef &Exp)=0
Creates a boolean not operation.
virtual SMTExprRef mkEqual (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean equality operation.
virtual SMTExprRef mkAnd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean and operation.
virtual SMTExprRef mkOr (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean or operation.
virtual SMTExprRef mkIte (const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0
Creates a boolean ite operation.
virtual SMTExprRef mkBVSignExt (unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector sign extension operation.
virtual SMTExprRef mkBVZeroExt (unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector zero extension operation.
virtual SMTExprRef mkBVExtract (unsigned High, unsigned Low, const SMTExprRef &Exp)=0
Creates a bitvector extract operation.
virtual SMTExprRef mkBVConcat (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector concat operation.
virtual SMTExprRef mkBVAddNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector addition operation.
virtual SMTExprRef mkBVAddNoUnderflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector addition operation.
virtual SMTExprRef mkBVSubNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector subtraction operation.
virtual SMTExprRef mkBVSubNoUnderflow (const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for underflow in a bitvector subtraction operation.
virtual SMTExprRef mkBVSDivNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector division/modulus operation.
virtual SMTExprRef mkBVNegNoOverflow (const SMTExprRef &Exp)=0
Creates a predicate that checks for overflow in a bitvector negation operation.
virtual SMTExprRef mkBVMulNoOverflow (const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector multiplication operation.
virtual SMTExprRef mkBVMulNoUnderflow (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector multiplication operation.
virtual SMTExprRef mkFPNeg (const SMTExprRef &Exp)=0
Creates a floating-point negation operation.
virtual SMTExprRef mkFPIsInfinite (const SMTExprRef &Exp)=0
Creates a floating-point isInfinite operation.
virtual SMTExprRef mkFPIsNaN (const SMTExprRef &Exp)=0
Creates a floating-point isNaN operation.
virtual SMTExprRef mkFPIsNormal (const SMTExprRef &Exp)=0
Creates a floating-point isNormal operation.
virtual SMTExprRef mkFPIsZero (const SMTExprRef &Exp)=0
Creates a floating-point isZero operation.
virtual SMTExprRef mkFPMul (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point multiplication operation.
virtual SMTExprRef mkFPDiv (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point division operation.
virtual SMTExprRef mkFPRem (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point remainder operation.
virtual SMTExprRef mkFPAdd (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point addition operation.
virtual SMTExprRef mkFPSub (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point subtraction operation.
virtual SMTExprRef mkFPLt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than operation.
virtual SMTExprRef mkFPGt (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than operation.
virtual SMTExprRef mkFPLe (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than-or-equal operation.
virtual SMTExprRef mkFPGe (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than-or-equal operation.
virtual SMTExprRef mkFPEqual (const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point equality operation.
virtual SMTExprRef mkFPtoFP (const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from floatint-point to floating-point operation.
virtual SMTExprRef mkSBVtoFP (const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from signed bitvector to floatint-point operation.
virtual SMTExprRef mkUBVtoFP (const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from unsigned bitvector to floatint-point operation.
virtual SMTExprRef mkFPtoSBV (const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to signed bitvector operation.
virtual SMTExprRef mkFPtoUBV (const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to unsigned bitvector operation.
virtual SMTExprRef mkSymbol (const char *Name, SMTSortRef Sort)=0
Creates a new symbol, given a name and a sort.
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.
virtual SMTExprRef mkFloat (const llvm::APFloat Float)=0
Constructs an SMTExprRef from a finite APFloat.
virtual SMTExprRef mkBitvector (const llvm::APSInt Int, unsigned BitWidth)=0
Constructs an SMTExprRef from an APSInt and its bit width.
virtual bool getInterpretation (const SMTExprRef &Exp, llvm::APSInt &Int)=0
Given an expression, extract the value of this operand in the model.
virtual bool getInterpretation (const SMTExprRef &Exp, llvm::APFloat &Float)=0
Given an expression extract the value of this operand in the model.
virtual std::optional< bool > check () const =0
Check if the constraints are satisfiable.
virtual void push ()=0
Push the current solver state.
virtual void pop (unsigned NumStates=1)=0
Pop the previous solver state.
virtual void reset ()=0
Reset the solver and remove all constraints.
virtual bool isFPSupported ()=0
Checks if the solver supports floating-points.
virtual void print (raw_ostream &OS) const =0
virtual void setBoolParam (StringRef Key, bool Value)=0
Sets the requested option.
virtual void setUnsignedParam (StringRef Key, unsigned Value)=0
virtual std::unique_ptr< SMTSolverStatistics > getStatistics () 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 156 of file SMTAPI.h.

llvm::SMTSolver::SMTSolver ( ) default

◆ ~SMTSolver()

virtual llvm::SMTSolver::~SMTSolver ( ) virtualdefault

◆ addConstraint()

virtual void llvm::SMTSolver::addConstraint ( const SMTExprRef & Exp) const pure virtual

Given a constraint, adds it to the solver.

◆ check()

virtual std::optional< bool > llvm::SMTSolver::check ( ) const pure virtual

Check if the constraints are satisfiable.

◆ dump()

◆ getBitvector()

◆ getBitvectorSort()

◆ getBoolean()

◆ getBoolSort()

virtual SMTSortRef llvm::SMTSolver::getBoolSort ( ) pure virtual

◆ getFloat128Sort()

virtual SMTSortRef llvm::SMTSolver::getFloat128Sort ( ) pure virtual

◆ getFloat16Sort()

virtual SMTSortRef llvm::SMTSolver::getFloat16Sort ( ) pure virtual

◆ getFloat32Sort()

virtual SMTSortRef llvm::SMTSolver::getFloat32Sort ( ) pure virtual

◆ getFloat64Sort()

virtual SMTSortRef llvm::SMTSolver::getFloat64Sort ( ) pure virtual

◆ getFloatRoundingMode()

virtual SMTExprRef llvm::SMTSolver::getFloatRoundingMode ( ) pure virtual

◆ getFloatSort()

◆ getInterpretation() [1/2]

Given an expression extract the value of this operand in the model.

References Float.

◆ getInterpretation() [2/2]

Given an expression, extract the value of this operand in the model.

References Int.

◆ getSort()

◆ getStatistics()

virtual std::unique_ptr< SMTSolverStatistics > llvm::SMTSolver::getStatistics ( ) const pure virtual

◆ isFPSupported()

virtual bool llvm::SMTSolver::isFPSupported ( ) pure virtual

Checks if the solver supports floating-points.

◆ mkAnd()

Creates a boolean and operation.

References LHS, and RHS.

◆ mkBitvector()

◆ mkBoolean()

◆ mkBVAdd()

Creates a bitvector addition operation.

References LHS, and RHS.

◆ mkBVAddNoOverflow()

Creates a predicate that checks for overflow in a bitvector addition operation.

References isSigned(), LHS, and RHS.

◆ mkBVAddNoUnderflow()

Creates a predicate that checks for underflow in a signed bitvector addition operation.

References LHS, and RHS.

◆ mkBVAnd()

Creates a bitvector and operation.

References LHS, and RHS.

◆ mkBVAshr()

Creates a bitvector arithmetic shift right operation.

References LHS, and RHS.

◆ mkBVConcat()

Creates a bitvector concat operation.

References LHS, and RHS.

◆ mkBVExtract()

Creates a bitvector extract operation.

References High, and llvm::Low.

◆ mkBVLshr()

Creates a bitvector logical shift right operation.

References LHS, and RHS.

◆ mkBVMul()

Creates a bitvector multiplication operation.

References LHS, and RHS.

◆ mkBVMulNoOverflow()

Creates a predicate that checks for overflow in a bitvector multiplication operation.

References isSigned(), LHS, and RHS.

◆ mkBVMulNoUnderflow()

Creates a predicate that checks for underflow in a signed bitvector multiplication operation.

References LHS, and RHS.

◆ mkBVNeg()

Creates a bitvector negation operation.

◆ mkBVNegNoOverflow()

Creates a predicate that checks for overflow in a bitvector negation operation.

◆ mkBVNot()

Creates a bitvector not operation.

◆ mkBVOr()

Creates a bitvector or operation.

References LHS, and RHS.

◆ mkBVSDiv()

Creates a bitvector signed division operation.

References LHS, and RHS.

◆ mkBVSDivNoOverflow()

Creates a predicate that checks for overflow in a signed bitvector division/modulus operation.

References LHS, and RHS.

◆ mkBVSge()

Creates a bitvector signed greater-equal-than operation.

References LHS, and RHS.

◆ mkBVSgt()

Creates a bitvector signed greater-than operation.

References LHS, and RHS.

◆ mkBVShl()

Creates a bitvector logical shift left operation.

References LHS, and RHS.

◆ mkBVSignExt()

Creates a bitvector sign extension operation.

◆ mkBVSle()

Creates a bitvector signed less-equal-than operation.

References LHS, and RHS.

◆ mkBVSlt()

Creates a bitvector signed less-than operation.

References LHS, and RHS.

◆ mkBVSRem()

Creates a bitvector signed modulus operation.

References LHS, and RHS.

◆ mkBVSub()

Creates a bitvector subtraction operation.

References LHS, and RHS.

◆ mkBVSubNoOverflow()

Creates a predicate that checks for overflow in a signed bitvector subtraction operation.

References LHS, and RHS.

◆ mkBVSubNoUnderflow()

Creates a predicate that checks for underflow in a bitvector subtraction operation.

References isSigned(), LHS, and RHS.

◆ mkBVUDiv()

Creates a bitvector unsigned division operation.

References LHS, and RHS.

◆ mkBVUge()

Creates a bitvector unsigned greater-equal-than operation.

References LHS, and RHS.

◆ mkBVUgt()

Creates a bitvector unsigned greater-than operation.

References LHS, and RHS.

◆ mkBVUle()

Creates a bitvector unsigned less-equal-than operation.

References LHS, and RHS.

◆ mkBVUlt()

Creates a bitvector unsigned less-than operation.

References LHS, and RHS.

◆ mkBVURem()

Creates a bitvector unsigned modulus operation.

References LHS, and RHS.

◆ mkBVXor()

Creates a bitvector xor operation.

References LHS, and RHS.

◆ mkBVZeroExt()

Creates a bitvector zero extension operation.

◆ mkEqual()

Creates a boolean equality operation.

References LHS, and RHS.

◆ mkFloat()

◆ mkFPAdd()

Creates a floating-point addition operation.

References LHS, and RHS.

◆ mkFPDiv()

Creates a floating-point division operation.

References LHS, and RHS.

◆ mkFPEqual()

Creates a floating-point equality operation.

References LHS, and RHS.

◆ mkFPGe()

Creates a floating-point greater-than-or-equal operation.

References LHS, and RHS.

◆ mkFPGt()

Creates a floating-point greater-than operation.

References LHS, and RHS.

◆ mkFPIsInfinite()

Creates a floating-point isInfinite operation.

◆ mkFPIsNaN()

Creates a floating-point isNaN operation.

◆ mkFPIsNormal()

Creates a floating-point isNormal operation.

◆ mkFPIsZero()

Creates a floating-point isZero operation.

◆ mkFPLe()

Creates a floating-point less-than-or-equal operation.

References LHS, and RHS.

◆ mkFPLt()

Creates a floating-point less-than operation.

References LHS, and RHS.

◆ mkFPMul()

Creates a floating-point multiplication operation.

References LHS, and RHS.

◆ mkFPNeg()

Creates a floating-point negation operation.

◆ mkFPRem()

Creates a floating-point remainder operation.

References LHS, and RHS.

◆ mkFPSub()

Creates a floating-point subtraction operation.

References LHS, and RHS.

◆ mkFPtoFP()

Creates a floating-point conversion from floatint-point to floating-point operation.

◆ mkFPtoSBV()

Creates a floating-point conversion from floatint-point to signed bitvector operation.

◆ mkFPtoUBV()

Creates a floating-point conversion from floatint-point to unsigned bitvector operation.

◆ mkIte()

Creates a boolean ite operation.

References Cond, F, and T.

◆ mkNot()

Creates a boolean not operation.

◆ mkOr()

Creates a boolean or operation.

References LHS, and RHS.

◆ mkSBVtoFP()

Creates a floating-point conversion from signed bitvector to floatint-point operation.

◆ mkSymbol()

Creates a new symbol, given a name and a sort.

◆ mkUBVtoFP()

Creates a floating-point conversion from unsigned bitvector to floatint-point operation.

◆ pop()

virtual void llvm::SMTSolver::pop ( unsigned NumStates = 1) pure virtual

Pop the previous solver state.

◆ print()

virtual void llvm::SMTSolver::print ( raw_ostream & OS) const pure virtual

◆ push()

virtual void llvm::SMTSolver::push ( ) pure virtual

Push the current solver state.

◆ reset()

virtual void llvm::SMTSolver::reset ( ) pure virtual

Reset the solver and remove all constraints.

◆ setBoolParam()

virtual void llvm::SMTSolver::setBoolParam ( StringRef Key, bool Value ) pure virtual

◆ setUnsignedParam()

The documentation for this class was generated from the following files: