LLVM 19.0.0git
Public Member Functions | List of all members
llvm::SMTSolver Class Referenceabstract

Generic base class for SMT Solvers. More...

#include "llvm/Support/SMTAPI.h"

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< boolcheck () 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
 

Detailed Description

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.

Constructor & Destructor Documentation

◆ SMTSolver()

llvm::SMTSolver::SMTSolver ( )
default

◆ ~SMTSolver()

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

Member Function Documentation

◆ 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()

LLVM_DUMP_METHOD void SMTSolver::dump ( ) const

Definition at line 918 of file Z3Solver.cpp.

References llvm::errs(), and print().

◆ getBitvector()

virtual llvm::APSInt llvm::SMTSolver::getBitvector ( const SMTExprRef Exp,
unsigned  BitWidth,
bool  isUnsigned 
)
pure virtual

◆ getBitvectorSort()

virtual SMTSortRef llvm::SMTSolver::getBitvectorSort ( const unsigned  BitWidth)
pure virtual

◆ getBoolean()

virtual bool llvm::SMTSolver::getBoolean ( const SMTExprRef Exp)
pure virtual

◆ getBoolSort()

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

◆ getFloat128Sort()

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

Referenced by getFloatSort().

◆ getFloat16Sort()

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

Referenced by getFloatSort().

◆ getFloat32Sort()

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

Referenced by getFloatSort().

◆ getFloat64Sort()

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

Referenced by getFloatSort().

◆ getFloatRoundingMode()

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

◆ getFloatSort()

SMTSortRef llvm::SMTSolver::getFloatSort ( unsigned  BitWidth)
inline

◆ getInterpretation() [1/2]

virtual bool llvm::SMTSolver::getInterpretation ( const SMTExprRef Exp,
llvm::APFloat Float 
)
pure virtual

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

◆ getInterpretation() [2/2]

virtual bool llvm::SMTSolver::getInterpretation ( const SMTExprRef Exp,
llvm::APSInt Int 
)
pure virtual

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

◆ getSort()

virtual SMTSortRef llvm::SMTSolver::getSort ( const SMTExprRef AST)
pure virtual

◆ isFPSupported()

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

Checks if the solver supports floating-points.

◆ mkAnd()

virtual SMTExprRef llvm::SMTSolver::mkAnd ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a boolean and operation.

◆ mkBitvector()

virtual SMTExprRef llvm::SMTSolver::mkBitvector ( const llvm::APSInt  Int,
unsigned  BitWidth 
)
pure virtual

Constructs an SMTExprRef from an APSInt and its bit width.

◆ mkBoolean()

virtual SMTExprRef llvm::SMTSolver::mkBoolean ( const bool  b)
pure virtual

Constructs an SMTExprRef from a boolean.

◆ mkBVAdd()

virtual SMTExprRef llvm::SMTSolver::mkBVAdd ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector addition operation.

◆ mkBVAddNoOverflow()

virtual SMTExprRef llvm::SMTSolver::mkBVAddNoOverflow ( const SMTExprRef LHS,
const SMTExprRef RHS,
bool  isSigned 
)
pure virtual

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

◆ mkBVAddNoUnderflow()

virtual SMTExprRef llvm::SMTSolver::mkBVAddNoUnderflow ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

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

◆ mkBVAnd()

virtual SMTExprRef llvm::SMTSolver::mkBVAnd ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector and operation.

◆ mkBVAshr()

virtual SMTExprRef llvm::SMTSolver::mkBVAshr ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector arithmetic shift right operation.

◆ mkBVConcat()

virtual SMTExprRef llvm::SMTSolver::mkBVConcat ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector concat operation.

◆ mkBVExtract()

virtual SMTExprRef llvm::SMTSolver::mkBVExtract ( unsigned  High,
unsigned  Low,
const SMTExprRef Exp 
)
pure virtual

Creates a bitvector extract operation.

◆ mkBVLshr()

virtual SMTExprRef llvm::SMTSolver::mkBVLshr ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector logical shift right operation.

◆ mkBVMul()

virtual SMTExprRef llvm::SMTSolver::mkBVMul ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector multiplication operation.

◆ mkBVMulNoOverflow()

virtual SMTExprRef llvm::SMTSolver::mkBVMulNoOverflow ( const SMTExprRef LHS,
const SMTExprRef RHS,
bool  isSigned 
)
pure virtual

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

◆ mkBVMulNoUnderflow()

virtual SMTExprRef llvm::SMTSolver::mkBVMulNoUnderflow ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

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

◆ mkBVNeg()

virtual SMTExprRef llvm::SMTSolver::mkBVNeg ( const SMTExprRef Exp)
pure virtual

Creates a bitvector negation operation.

◆ mkBVNegNoOverflow()

virtual SMTExprRef llvm::SMTSolver::mkBVNegNoOverflow ( const SMTExprRef Exp)
pure virtual

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

◆ mkBVNot()

virtual SMTExprRef llvm::SMTSolver::mkBVNot ( const SMTExprRef Exp)
pure virtual

Creates a bitvector not operation.

◆ mkBVOr()

virtual SMTExprRef llvm::SMTSolver::mkBVOr ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector or operation.

◆ mkBVSDiv()

virtual SMTExprRef llvm::SMTSolver::mkBVSDiv ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector signed division operation.

◆ mkBVSDivNoOverflow()

virtual SMTExprRef llvm::SMTSolver::mkBVSDivNoOverflow ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

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

◆ mkBVSge()

virtual SMTExprRef llvm::SMTSolver::mkBVSge ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector signed greater-equal-than operation.

◆ mkBVSgt()

virtual SMTExprRef llvm::SMTSolver::mkBVSgt ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector signed greater-than operation.

◆ mkBVShl()

virtual SMTExprRef llvm::SMTSolver::mkBVShl ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector logical shift left operation.

◆ mkBVSignExt()

virtual SMTExprRef llvm::SMTSolver::mkBVSignExt ( unsigned  i,
const SMTExprRef Exp 
)
pure virtual

Creates a bitvector sign extension operation.

◆ mkBVSle()

virtual SMTExprRef llvm::SMTSolver::mkBVSle ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector signed less-equal-than operation.

◆ mkBVSlt()

virtual SMTExprRef llvm::SMTSolver::mkBVSlt ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector signed less-than operation.

◆ mkBVSRem()

virtual SMTExprRef llvm::SMTSolver::mkBVSRem ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector signed modulus operation.

◆ mkBVSub()

virtual SMTExprRef llvm::SMTSolver::mkBVSub ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector subtraction operation.

◆ mkBVSubNoOverflow()

virtual SMTExprRef llvm::SMTSolver::mkBVSubNoOverflow ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

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

◆ mkBVSubNoUnderflow()

virtual SMTExprRef llvm::SMTSolver::mkBVSubNoUnderflow ( const SMTExprRef LHS,
const SMTExprRef RHS,
bool  isSigned 
)
pure virtual

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

◆ mkBVUDiv()

virtual SMTExprRef llvm::SMTSolver::mkBVUDiv ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector unsigned division operation.

◆ mkBVUge()

virtual SMTExprRef llvm::SMTSolver::mkBVUge ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector unsigned greater-equal-than operation.

◆ mkBVUgt()

virtual SMTExprRef llvm::SMTSolver::mkBVUgt ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector unsigned greater-than operation.

◆ mkBVUle()

virtual SMTExprRef llvm::SMTSolver::mkBVUle ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector unsigned less-equal-than operation.

◆ mkBVUlt()

virtual SMTExprRef llvm::SMTSolver::mkBVUlt ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector unsigned less-than operation.

◆ mkBVURem()

virtual SMTExprRef llvm::SMTSolver::mkBVURem ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector unsigned modulus operation.

◆ mkBVXor()

virtual SMTExprRef llvm::SMTSolver::mkBVXor ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a bitvector xor operation.

◆ mkBVZeroExt()

virtual SMTExprRef llvm::SMTSolver::mkBVZeroExt ( unsigned  i,
const SMTExprRef Exp 
)
pure virtual

Creates a bitvector zero extension operation.

◆ mkEqual()

virtual SMTExprRef llvm::SMTSolver::mkEqual ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a boolean equality operation.

◆ mkFloat()

virtual SMTExprRef llvm::SMTSolver::mkFloat ( const llvm::APFloat  Float)
pure virtual

Constructs an SMTExprRef from a finite APFloat.

◆ mkFPAdd()

virtual SMTExprRef llvm::SMTSolver::mkFPAdd ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point addition operation.

◆ mkFPDiv()

virtual SMTExprRef llvm::SMTSolver::mkFPDiv ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point division operation.

◆ mkFPEqual()

virtual SMTExprRef llvm::SMTSolver::mkFPEqual ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point equality operation.

◆ mkFPGe()

virtual SMTExprRef llvm::SMTSolver::mkFPGe ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

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

◆ mkFPGt()

virtual SMTExprRef llvm::SMTSolver::mkFPGt ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point greater-than operation.

◆ mkFPIsInfinite()

virtual SMTExprRef llvm::SMTSolver::mkFPIsInfinite ( const SMTExprRef Exp)
pure virtual

Creates a floating-point isInfinite operation.

◆ mkFPIsNaN()

virtual SMTExprRef llvm::SMTSolver::mkFPIsNaN ( const SMTExprRef Exp)
pure virtual

Creates a floating-point isNaN operation.

◆ mkFPIsNormal()

virtual SMTExprRef llvm::SMTSolver::mkFPIsNormal ( const SMTExprRef Exp)
pure virtual

Creates a floating-point isNormal operation.

◆ mkFPIsZero()

virtual SMTExprRef llvm::SMTSolver::mkFPIsZero ( const SMTExprRef Exp)
pure virtual

Creates a floating-point isZero operation.

◆ mkFPLe()

virtual SMTExprRef llvm::SMTSolver::mkFPLe ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

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

◆ mkFPLt()

virtual SMTExprRef llvm::SMTSolver::mkFPLt ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point less-than operation.

◆ mkFPMul()

virtual SMTExprRef llvm::SMTSolver::mkFPMul ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point multiplication operation.

◆ mkFPNeg()

virtual SMTExprRef llvm::SMTSolver::mkFPNeg ( const SMTExprRef Exp)
pure virtual

Creates a floating-point negation operation.

◆ mkFPRem()

virtual SMTExprRef llvm::SMTSolver::mkFPRem ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point remainder operation.

◆ mkFPSub()

virtual SMTExprRef llvm::SMTSolver::mkFPSub ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a floating-point subtraction operation.

◆ mkFPtoFP()

virtual SMTExprRef llvm::SMTSolver::mkFPtoFP ( const SMTExprRef From,
const SMTSortRef To 
)
pure virtual

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

◆ mkFPtoSBV()

virtual SMTExprRef llvm::SMTSolver::mkFPtoSBV ( const SMTExprRef From,
unsigned  ToWidth 
)
pure virtual

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

◆ mkFPtoUBV()

virtual SMTExprRef llvm::SMTSolver::mkFPtoUBV ( const SMTExprRef From,
unsigned  ToWidth 
)
pure virtual

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

◆ mkIte()

virtual SMTExprRef llvm::SMTSolver::mkIte ( const SMTExprRef Cond,
const SMTExprRef T,
const SMTExprRef F 
)
pure virtual

Creates a boolean ite operation.

◆ mkNot()

virtual SMTExprRef llvm::SMTSolver::mkNot ( const SMTExprRef Exp)
pure virtual

Creates a boolean not operation.

◆ mkOr()

virtual SMTExprRef llvm::SMTSolver::mkOr ( const SMTExprRef LHS,
const SMTExprRef RHS 
)
pure virtual

Creates a boolean or operation.

◆ mkSBVtoFP()

virtual SMTExprRef llvm::SMTSolver::mkSBVtoFP ( const SMTExprRef From,
const SMTSortRef To 
)
pure virtual

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

◆ mkSymbol()

virtual SMTExprRef llvm::SMTSolver::mkSymbol ( const char Name,
SMTSortRef  Sort 
)
pure virtual

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

◆ mkUBVtoFP()

virtual SMTExprRef llvm::SMTSolver::mkUBVtoFP ( const SMTExprRef From,
const SMTSortRef To 
)
pure virtual

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

Referenced by dump().

◆ 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.


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