LLVM 19.0.0git
Public Member Functions | Protected Member Functions | Friends | List of all members
llvm::SMTSort Class Referenceabstract

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