class SMTSolver

Declaration

class SMTSolver { /* full declaration omitted */ };

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.

Declared at: llvm/include/llvm/Support/SMTAPI.h:136

Method Overview

• public SMTSolver()
• public virtual void addConstraint(const llvm::SMTExprRef & Exp) const
• public virtual Optional<bool> check() const
• public void dump() const
• public virtual llvm::APSInt getBitvector(const llvm::SMTExprRef & Exp, unsigned int BitWidth, bool isUnsigned)
• public virtual llvm::SMTSortRef getBitvectorSort(const unsigned int BitWidth)
• public virtual llvm::SMTSortRef getBoolSort()
• public virtual bool getBoolean(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTSortRef getFloat128Sort()
• public virtual llvm::SMTSortRef getFloat16Sort()
• public virtual llvm::SMTSortRef getFloat32Sort()
• public virtual llvm::SMTSortRef getFloat64Sort()
• public virtual llvm::SMTExprRef getFloatRoundingMode()
• public llvm::SMTSortRef getFloatSort(unsigned int BitWidth)
• public virtual bool getInterpretation(const llvm::SMTExprRef & Exp, llvm::APFloat & Float)
• public virtual bool getInterpretation(const llvm::SMTExprRef & Exp, llvm::APSInt & Int)
• public virtual llvm::SMTSortRef getSort(const llvm::SMTExprRef & AST)
• public virtual bool isFPSupported()
• public virtual llvm::SMTExprRef mkAnd(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVAdd(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVAddNoOverflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS, bool isSigned)
• public virtual llvm::SMTExprRef mkBVAddNoUnderflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVAnd(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVAshr(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVConcat(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVExtract(unsigned int High, unsigned int Low, const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkBVLshr(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVMul(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVMulNoOverflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS, bool isSigned)
• public virtual llvm::SMTExprRef mkBVMulNoUnderflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVNeg(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkBVNegNoOverflow(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkBVNot(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkBVOr(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSDiv(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSDivNoOverflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSRem(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSge(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSgt(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVShl(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSignExt(unsigned int i, const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkBVSle(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSlt(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSub(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSubNoOverflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVSubNoUnderflow(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS, bool isSigned)
• public virtual llvm::SMTExprRef mkBVUDiv(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVURem(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVUge(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVUgt(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVUle(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVUlt(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVXor(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkBVZeroExt(unsigned int i, const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned int BitWidth)
• public virtual llvm::SMTExprRef mkBoolean(const bool b)
• public virtual llvm::SMTExprRef mkEqual(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPAdd(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPDiv(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPEqual(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPGe(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPGt(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPIsInfinite(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkFPIsNaN(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkFPIsNormal(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkFPIsZero(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkFPLe(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPLt(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPMul(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPNeg(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkFPRem(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPSub(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkFPtoFP(const llvm::SMTExprRef & From, const llvm::SMTSortRef & To)
• public virtual llvm::SMTExprRef mkFPtoSBV(const llvm::SMTExprRef & From, unsigned int ToWidth)
• public virtual llvm::SMTExprRef mkFPtoUBV(const llvm::SMTExprRef & From, unsigned int ToWidth)
• public virtual llvm::SMTExprRef mkFloat(const llvm::APFloat Float)
• public virtual llvm::SMTExprRef mkIte(const llvm::SMTExprRef & Cond, const llvm::SMTExprRef & T, const llvm::SMTExprRef & F)
• public virtual llvm::SMTExprRef mkNot(const llvm::SMTExprRef & Exp)
• public virtual llvm::SMTExprRef mkOr(const llvm::SMTExprRef & LHS, const llvm::SMTExprRef & RHS)
• public virtual llvm::SMTExprRef mkSBVtoFP(const llvm::SMTExprRef & From, const llvm::SMTSortRef & To)
• public virtual llvm::SMTExprRef mkSymbol(const char * Name, llvm::SMTSortRef Sort)
• public virtual llvm::SMTExprRef mkUBVtoFP(const llvm::SMTExprRef & From, const llvm::SMTSortRef & To)
• public virtual void pop(unsigned int NumStates = 1)
• public virtual void print(llvm::raw_ostream & OS) const
• public virtual void push()
• public virtual void reset()
• public virtual ~SMTSolver()

Methods

¶SMTSolver()

Declared at: llvm/include/llvm/Support/SMTAPI.h:138

¶virtual void addConstraint(
    const llvm::SMTExprRef& Exp) const

Description

Given a constraint, adds it to the solver

Declared at: llvm/include/llvm/Support/SMTAPI.h:181

Parameters

const llvm::SMTExprRef& Exp

¶virtual Optional<bool> check() const

Description

Check if the constraints are satisfiable

Declared at: llvm/include/llvm/Support/SMTAPI.h:422

¶void dump() const

Declared at: llvm/include/llvm/Support/SMTAPI.h:141

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:399

Parameters

const llvm::SMTExprRef& Exp

unsigned int BitWidth

bool isUnsigned

¶virtual llvm::SMTSortRef getBitvectorSort(
    const unsigned int BitWidth)

Declared at: llvm/include/llvm/Support/SMTAPI.h:163

Parameters

const unsigned int BitWidth

¶virtual llvm::SMTSortRef getBoolSort()

Declared at: llvm/include/llvm/Support/SMTAPI.h:160

¶virtual bool getBoolean(
    const llvm::SMTExprRef& Exp)

Declared at: llvm/include/llvm/Support/SMTAPI.h:403

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTSortRef getFloat128Sort()

Declared at: llvm/include/llvm/Support/SMTAPI.h:175

¶virtual llvm::SMTSortRef getFloat16Sort()

Declared at: llvm/include/llvm/Support/SMTAPI.h:166

¶virtual llvm::SMTSortRef getFloat32Sort()

Declared at: llvm/include/llvm/Support/SMTAPI.h:169

¶virtual llvm::SMTSortRef getFloat64Sort()

Declared at: llvm/include/llvm/Support/SMTAPI.h:172

¶virtual llvm::SMTExprRef getFloatRoundingMode()

Declared at: llvm/include/llvm/Support/SMTAPI.h:396

¶llvm::SMTSortRef getFloatSort(
    unsigned int BitWidth)

Declared at: llvm/include/llvm/Support/SMTAPI.h:144

Parameters

unsigned int BitWidth

¶virtual bool getInterpretation(
    const llvm::SMTExprRef& Exp,
    llvm::APFloat& Float)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:418

Parameters

const llvm::SMTExprRef& Exp

llvm::APFloat& Float

¶virtual bool getInterpretation(
    const llvm::SMTExprRef& Exp,
    llvm::APSInt& Int)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:415

Parameters

const llvm::SMTExprRef& Exp

llvm::APSInt& Int

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:178

Parameters

const llvm::SMTExprRef& AST

¶virtual bool isFPSupported()

Description

Checks if the solver supports floating-points.

Declared at: llvm/include/llvm/Support/SMTAPI.h:434

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

Description

Creates a boolean and operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:259

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVAdd(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

Creates a bitvector addition operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:184

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVAddNoOverflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS,
    bool isSigned)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:284

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

bool isSigned

¶virtual llvm::SMTExprRef mkBVAddNoUnderflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:290

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector and operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:226

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector arithmetic shift right operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:208

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector concat operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:279

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector extract operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:275

Parameters

unsigned int High

unsigned int Low

const llvm::SMTExprRef& Exp

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

Description

Creates a bitvector logical shift right operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:211

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector multiplication operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:190

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVMulNoOverflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS,
    bool isSigned)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:315

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

bool isSigned

¶virtual llvm::SMTExprRef mkBVMulNoUnderflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:321

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVNeg(
    const llvm::SMTExprRef& Exp)

Description

Creates a bitvector negation operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:214

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkBVNegNoOverflow(
    const llvm::SMTExprRef& Exp)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:311

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkBVNot(
    const llvm::SMTExprRef& Exp)

Description

Creates a bitvector not operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:217

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkBVOr(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

Creates a bitvector or operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:223

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector signed division operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:199

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVSDivNoOverflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:306

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector signed modulus operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:193

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector signed greater-equal-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:250

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector signed greater-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:238

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector logical shift left operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:205

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVSignExt(
    unsigned int i,
    const llvm::SMTExprRef& Exp)

Description

Creates a bitvector sign extension operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:269

Parameters

unsigned int i

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkBVSle(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

Creates a bitvector signed less-equal-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:244

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector signed less-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:232

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector subtraction operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:187

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVSubNoOverflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:295

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVSubNoUnderflow(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS,
    bool isSigned)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:300

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

bool isSigned

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

Description

Creates a bitvector unsigned division operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:202

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector unsigned modulus operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:196

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector unsigned greater-equal-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:247

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector unsigned greater-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:235

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector unsigned less-equal-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:241

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector unsigned less-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:229

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a bitvector xor operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:220

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkBVZeroExt(
    unsigned int i,
    const llvm::SMTExprRef& Exp)

Description

Creates a bitvector zero extension operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:272

Parameters

unsigned int i

const llvm::SMTExprRef& Exp

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

Description

Constructs an SMTExprRef from an APSInt and its bit width

Declared at: llvm/include/llvm/Support/SMTAPI.h:412

Parameters

const llvm::APSInt Int

unsigned int BitWidth

¶virtual llvm::SMTExprRef mkBoolean(const bool b)

Description

Constructs an SMTExprRef from a boolean.

Declared at: llvm/include/llvm/Support/SMTAPI.h:406

Parameters

const bool b

¶virtual llvm::SMTExprRef mkEqual(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

Creates a boolean equality operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:256

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point addition operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:349

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point division operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:343

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point equality operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:367

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:364

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point greater-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:358

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkFPIsInfinite(
    const llvm::SMTExprRef& Exp)

Description

Creates a floating-point isInfinite operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:328

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkFPIsNaN(
    const llvm::SMTExprRef& Exp)

Description

Creates a floating-point isNaN operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:331

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkFPIsNormal(
    const llvm::SMTExprRef& Exp)

Description

Creates a floating-point isNormal operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:334

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkFPIsZero(
    const llvm::SMTExprRef& Exp)

Description

Creates a floating-point isZero operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:337

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkFPLe(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:361

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point less-than operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:355

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point multiplication operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:340

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkFPNeg(
    const llvm::SMTExprRef& Exp)

Description

Creates a floating-point negation operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:325

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkFPRem(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

Creates a floating-point remainder operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:346

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

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

Description

Creates a floating-point subtraction operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:352

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkFPtoFP(
    const llvm::SMTExprRef& From,
    const llvm::SMTSortRef& To)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:372

Parameters

const llvm::SMTExprRef& From

const llvm::SMTSortRef& To

¶virtual llvm::SMTExprRef mkFPtoSBV(
    const llvm::SMTExprRef& From,
    unsigned int ToWidth)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:386

Parameters

const llvm::SMTExprRef& From

unsigned int ToWidth

¶virtual llvm::SMTExprRef mkFPtoUBV(
    const llvm::SMTExprRef& From,
    unsigned int ToWidth)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:390

Parameters

const llvm::SMTExprRef& From

unsigned int ToWidth

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

Description

Constructs an SMTExprRef from a finite APFloat.

Declared at: llvm/include/llvm/Support/SMTAPI.h:409

Parameters

const llvm::APFloat Float

¶virtual llvm::SMTExprRef mkIte(
    const llvm::SMTExprRef& Cond,
    const llvm::SMTExprRef& T,
    const llvm::SMTExprRef& F)

Description

Creates a boolean ite operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:265

Parameters

const llvm::SMTExprRef& Cond

const llvm::SMTExprRef& T

const llvm::SMTExprRef& F

¶virtual llvm::SMTExprRef mkNot(
    const llvm::SMTExprRef& Exp)

Description

Creates a boolean not operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:253

Parameters

const llvm::SMTExprRef& Exp

¶virtual llvm::SMTExprRef mkOr(
    const llvm::SMTExprRef& LHS,
    const llvm::SMTExprRef& RHS)

Description

Creates a boolean or operation

Declared at: llvm/include/llvm/Support/SMTAPI.h:262

Parameters

const llvm::SMTExprRef& LHS

const llvm::SMTExprRef& RHS

¶virtual llvm::SMTExprRef mkSBVtoFP(
    const llvm::SMTExprRef& From,
    const llvm::SMTSortRef& To)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:376

Parameters

const llvm::SMTExprRef& From

const llvm::SMTSortRef& To

¶virtual llvm::SMTExprRef mkSymbol(
    const char* Name,
    llvm::SMTSortRef Sort)

Description

Creates a new symbol, given a name and a sort

Declared at: llvm/include/llvm/Support/SMTAPI.h:393

Parameters

const char* Name

llvm::SMTSortRef Sort

¶virtual llvm::SMTExprRef mkUBVtoFP(
    const llvm::SMTExprRef& From,
    const llvm::SMTSortRef& To)

Description

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

Declared at: llvm/include/llvm/Support/SMTAPI.h:381

Parameters

const llvm::SMTExprRef& From

const llvm::SMTSortRef& To

¶virtual void pop(unsigned int NumStates = 1)

Description

Pop the previous solver state

Declared at: llvm/include/llvm/Support/SMTAPI.h:428

Parameters

unsigned int NumStates = 1

¶virtual void print(llvm::raw_ostream& OS) const

Declared at: llvm/include/llvm/Support/SMTAPI.h:436

Parameters

llvm::raw_ostream& OS

¶virtual void push()

Description

Push the current solver state

Declared at: llvm/include/llvm/Support/SMTAPI.h:425

¶virtual void reset()

Description

Reset the solver and remove all constraints.

Declared at: llvm/include/llvm/Support/SMTAPI.h:431

¶virtual ~SMTSolver()

Declared at: llvm/include/llvm/Support/SMTAPI.h:139