llvm::SMTSolver Class Reference

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

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 156 of file SMTAPI.h.

Constructor & Destructor Documentation

SMTSolver()

llvm::SMTSolver::SMTSolver ( )

default

~SMTSolver()

virtual llvm::SMTSolver::~SMTSolver ( )

virtualdefault

References LLVM_DUMP_METHOD.

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 996 of file Z3Solver.cpp.

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

getBitvector()

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

pure virtual

References llvm::BitWidth.

getBitvectorSort()

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

pure virtual

References llvm::BitWidth.

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

Definition at line 166 of file SMTAPI.h.

References llvm::BitWidth, getFloat128Sort(), getFloat16Sort(), getFloat32Sort(), getFloat64Sort(), and llvm_unreachable.

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.

References Float.

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.

References Int.

getSort()

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

pure virtual

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

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

pure virtual

Creates a boolean and operation.

References LHS, and RHS.

mkBitvector()

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

pure virtual

Constructs an SMTExprRef from an APSInt and its bit width.

References llvm::BitWidth, and Int.

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.

References LHS, and RHS.

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.

References isSigned(), LHS, and RHS.

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.

References LHS, and RHS.

mkBVAnd()

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

pure virtual

Creates a bitvector and operation.

References LHS, and RHS.

mkBVAshr()

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

pure virtual

Creates a bitvector arithmetic shift right operation.

References LHS, and RHS.

mkBVConcat()

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

pure virtual

Creates a bitvector concat operation.

References LHS, and RHS.

mkBVExtract()

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

pure virtual

Creates a bitvector extract operation.

References High, and llvm::Low.

mkBVLshr()

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

pure virtual

Creates a bitvector logical shift right operation.

References LHS, and RHS.

mkBVMul()

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

pure virtual

Creates a bitvector multiplication operation.

References LHS, and RHS.

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.

References isSigned(), LHS, and RHS.

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.

References LHS, and RHS.

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.

References LHS, and RHS.

mkBVSDiv()

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

pure virtual

Creates a bitvector signed division operation.

References LHS, and RHS.

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.

References LHS, and RHS.

mkBVSge()

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

pure virtual

Creates a bitvector signed greater-equal-than operation.

References LHS, and RHS.

mkBVSgt()

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

pure virtual

Creates a bitvector signed greater-than operation.

References LHS, and RHS.

mkBVShl()

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

pure virtual

Creates a bitvector logical shift left operation.

References LHS, and RHS.

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.

References LHS, and RHS.

mkBVSlt()

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

pure virtual

Creates a bitvector signed less-than operation.

References LHS, and RHS.

mkBVSRem()

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

pure virtual

Creates a bitvector signed modulus operation.

References LHS, and RHS.

mkBVSub()

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

pure virtual

Creates a bitvector subtraction operation.

References LHS, and RHS.

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.

References LHS, and RHS.

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.

References isSigned(), LHS, and RHS.

mkBVUDiv()

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

pure virtual

Creates a bitvector unsigned division operation.

References LHS, and RHS.

mkBVUge()

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

pure virtual

Creates a bitvector unsigned greater-equal-than operation.

References LHS, and RHS.

mkBVUgt()

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

pure virtual

Creates a bitvector unsigned greater-than operation.

References LHS, and RHS.

mkBVUle()

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

pure virtual

Creates a bitvector unsigned less-equal-than operation.

References LHS, and RHS.

mkBVUlt()

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

pure virtual

Creates a bitvector unsigned less-than operation.

References LHS, and RHS.

mkBVURem()

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

pure virtual

Creates a bitvector unsigned modulus operation.

References LHS, and RHS.

mkBVXor()

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

pure virtual

Creates a bitvector xor operation.

References LHS, and RHS.

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.

References LHS, and RHS.

mkFloat()

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

pure virtual

Constructs an SMTExprRef from a finite APFloat.

References Float.

mkFPAdd()

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

pure virtual

Creates a floating-point addition operation.

References LHS, and RHS.

mkFPDiv()

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

pure virtual

Creates a floating-point division operation.

References LHS, and RHS.

mkFPEqual()

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

pure virtual

Creates a floating-point equality operation.

References LHS, and RHS.

mkFPGe()

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

pure virtual

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

References LHS, and RHS.

mkFPGt()

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

pure virtual

Creates a floating-point greater-than operation.

References LHS, and RHS.

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.

References LHS, and RHS.

mkFPLt()

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

pure virtual

Creates a floating-point less-than operation.

References LHS, and RHS.

mkFPMul()

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

pure virtual

Creates a floating-point multiplication operation.

References LHS, and RHS.

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.

References LHS, and RHS.

mkFPSub()

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

pure virtual

Creates a floating-point subtraction operation.

References LHS, and RHS.

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.

References Cond, F, and T.

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.

References LHS, and RHS.

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.

setBoolParam()

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

pure virtual

Sets the requested option.

References llvm::InnerAnalysisManagerProxy< AnalysisManagerT, IRUnitT, ExtraArgTs... >::Key.

setUnsignedParam()

virtual void llvm::SMTSolver::setUnsignedParam ( StringRef Key, unsigned Value )

pure virtual

References llvm::InnerAnalysisManagerProxy< AnalysisManagerT, IRUnitT, ExtraArgTs... >::Key.

---

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

• include/llvm/Support/SMTAPI.h
• lib/Support/Z3Solver.cpp