llvm::SMTSort Class Reference

Generic base class for SMT sorts. More...

#include "llvm/Support/SMTAPI.h"

Public Member Functions
	SMTSort ()=default
virtual	~SMTSort ()=default
virtual bool	isBitvectorSort () const
	Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
virtual bool	isFloatSort () const
	Returns true if the sort is a floating-point, calls isFloatSortImpl().
virtual bool	isBooleanSort () const
	Returns true if the sort is a boolean, calls isBooleanSortImpl().
virtual unsigned	getBitvectorSortSize () const
	Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
virtual unsigned	getFloatSortSize () const
	Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl().
virtual void	Profile (llvm::FoldingSetNodeID &ID) const =0
bool	operator< (const SMTSort &Other) const
virtual void	print (raw_ostream &OS) const =0
LLVM_DUMP_METHOD void	dump () const

Protected Member Functions
virtual bool	equal_to (SMTSort const &other) const =0
	Query the SMT solver and returns true if two sorts are equal (same kind and bit width).
virtual bool	isBitvectorSortImpl () const =0
	Query the SMT solver and checks if a sort is bitvector.
virtual bool	isFloatSortImpl () const =0
	Query the SMT solver and checks if a sort is floating-point.
virtual bool	isBooleanSortImpl () const =0
	Query the SMT solver and checks if a sort is boolean.
virtual unsigned	getBitvectorSortSizeImpl () const =0
	Query the SMT solver and returns the sort bit width.
virtual unsigned	getFloatSortSizeImpl () const =0
	Query the SMT solver and returns the sort bit width.

Friends
bool	operator== (SMTSort const &LHS, SMTSort const &RHS)

Detailed Description

Generic base class for SMT sorts.

Definition at line 26 of file SMTAPI.h.

Constructor & Destructor Documentation

SMTSort()

llvm::SMTSort::SMTSort ( )

default

~SMTSort()

virtual llvm::SMTSort::~SMTSort ( )

virtualdefault

Member Function Documentation

dump()

LLVM_DUMP_METHOD void SMTSort::dump

(

)

const

Definition at line 992 of file Z3Solver.cpp.

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

equal_to()

virtual bool llvm::SMTSort::equal_to ( SMTSort const &  other ) const

protectedpure virtual

Query the SMT solver and returns true if two sorts are equal (same kind and bit width).

This does not check if the two sorts are the same objects.

getBitvectorSortSize()

virtual unsigned llvm::SMTSort::getBitvectorSortSize ( ) const

inlinevirtual

Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().

Definition at line 42 of file SMTAPI.h.

References assert(), getBitvectorSortSizeImpl(), isBitvectorSort(), and Size.

getBitvectorSortSizeImpl()

virtual unsigned llvm::SMTSort::getBitvectorSortSizeImpl ( ) const

protectedpure virtual

Query the SMT solver and returns the sort bit width.

Referenced by getBitvectorSortSize().

getFloatSortSize()

virtual unsigned llvm::SMTSort::getFloatSortSize ( ) const

inlinevirtual

Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl().

Definition at line 51 of file SMTAPI.h.

References assert(), getFloatSortSizeImpl(), isFloatSort(), and Size.

getFloatSortSizeImpl()

virtual unsigned llvm::SMTSort::getFloatSortSizeImpl ( ) const

protectedpure virtual

Query the SMT solver and returns the sort bit width.

Referenced by getFloatSortSize().

isBitvectorSort()

virtual bool llvm::SMTSort::isBitvectorSort ( ) const

inlinevirtual

Returns true if the sort is a bitvector, calls isBitvectorSortImpl().

Definition at line 32 of file SMTAPI.h.

References isBitvectorSortImpl().

Referenced by getBitvectorSortSize().

isBitvectorSortImpl()

virtual bool llvm::SMTSort::isBitvectorSortImpl ( ) const

protectedpure virtual

Query the SMT solver and checks if a sort is bitvector.

Referenced by isBitvectorSort().

isBooleanSort()

virtual bool llvm::SMTSort::isBooleanSort ( ) const

inlinevirtual

Returns true if the sort is a boolean, calls isBooleanSortImpl().

Definition at line 38 of file SMTAPI.h.

References isBooleanSortImpl().

isBooleanSortImpl()

virtual bool llvm::SMTSort::isBooleanSortImpl ( ) const

protectedpure virtual

Query the SMT solver and checks if a sort is boolean.

Referenced by isBooleanSort().

isFloatSort()

virtual bool llvm::SMTSort::isFloatSort ( ) const

inlinevirtual

Returns true if the sort is a floating-point, calls isFloatSortImpl().

Definition at line 35 of file SMTAPI.h.

References isFloatSortImpl().

Referenced by getFloatSortSize().

isFloatSortImpl()

virtual bool llvm::SMTSort::isFloatSortImpl ( ) const

protectedpure virtual

Query the SMT solver and checks if a sort is floating-point.

Referenced by isFloatSort().

operator<()

bool llvm::SMTSort::operator< ( const SMTSort &  Other ) const

inline

Definition at line 60 of file SMTAPI.h.

References llvm::Other, and Profile.

print()

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

pure virtual

Referenced by dump().

Profile()

virtual void llvm::SMTSort::Profile ( llvm::FoldingSetNodeID &  ID ) const

pure virtual

Friends And Related Function Documentation

operator==

bool operator== ( SMTSort const &  LHS, SMTSort const &  RHS  )

friend

Definition at line 67 of file SMTAPI.h.

---

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

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