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

Definition at line 157 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.

◆ 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

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

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

◆ setBoolParam()

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

pure virtual

Sets the requested option.

◆ setUnsignedParam()

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

pure virtual

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

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

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ SMTSolver()

◆ ~SMTSolver()

Member Function Documentation

◆ addConstraint()

◆ check()

◆ dump()

◆ getBitvector()

◆ getBitvectorSort()

◆ getBoolean()

◆ getBoolSort()

◆ getFloat128Sort()

◆ getFloat16Sort()

◆ getFloat32Sort()

◆ getFloat64Sort()

◆ getFloatRoundingMode()

◆ getFloatSort()

◆ getInterpretation() [1/2]

◆ getInterpretation() [2/2]

◆ getSort()

◆ getStatistics()

◆ isFPSupported()

◆ mkAnd()

◆ mkBitvector()

◆ mkBoolean()

◆ mkBVAdd()

◆ mkBVAddNoOverflow()

◆ mkBVAddNoUnderflow()

◆ mkBVAnd()

◆ mkBVAshr()

◆ mkBVConcat()

◆ mkBVExtract()

◆ mkBVLshr()

◆ mkBVMul()

◆ mkBVMulNoOverflow()

◆ mkBVMulNoUnderflow()

◆ mkBVNeg()

◆ mkBVNegNoOverflow()

◆ mkBVNot()

◆ mkBVOr()

◆ mkBVSDiv()

◆ mkBVSDivNoOverflow()

◆ mkBVSge()

◆ mkBVSgt()

◆ mkBVShl()

◆ mkBVSignExt()

◆ mkBVSle()

◆ mkBVSlt()

◆ mkBVSRem()

◆ mkBVSub()

◆ mkBVSubNoOverflow()

◆ mkBVSubNoUnderflow()

◆ mkBVUDiv()

◆ mkBVUge()

◆ mkBVUgt()

◆ mkBVUle()

◆ mkBVUlt()

◆ mkBVURem()

◆ mkBVXor()

◆ mkBVZeroExt()

◆ mkEqual()

◆ mkFloat()

◆ mkFPAdd()

◆ mkFPDiv()

◆ mkFPEqual()

◆ mkFPGe()

◆ mkFPGt()

◆ mkFPIsInfinite()

◆ mkFPIsNaN()

◆ mkFPIsNormal()

◆ mkFPIsZero()

◆ mkFPLe()

◆ mkFPLt()

◆ mkFPMul()

◆ mkFPNeg()

◆ mkFPRem()

◆ mkFPSub()

◆ mkFPtoFP()