LLVM  10.0.0svn
Public Member Functions | Protected Member Functions | Friends | List of all members
llvm::SMTExpr Class Referenceabstract

Generic base class for SMT exprs. More...

#include "llvm/Support/SMTAPI.h"

Public Member Functions

 SMTExpr ()=default
 
virtual ~SMTExpr ()=default
 
bool operator< (const SMTExpr &Other) const
 
virtual void Profile (llvm::FoldingSetNodeID &ID) const =0
 
virtual void print (raw_ostream &OS) const =0
 
LLVM_DUMP_METHOD void dump () const
 

Protected Member Functions

virtual bool equal_to (SMTExpr const &other) const =0
 Query the SMT solver and returns true if two sorts are equal (same kind and bit width). More...
 

Friends

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

Detailed Description

Generic base class for SMT exprs.

Definition at line 100 of file SMTAPI.h.

Constructor & Destructor Documentation

◆ SMTExpr()

llvm::SMTExpr::SMTExpr ( )
default

◆ ~SMTExpr()

virtual llvm::SMTExpr::~SMTExpr ( )
virtualdefault

Member Function Documentation

◆ dump()

LLVM_DUMP_METHOD void SMTExpr::dump ( ) const

Definition at line 899 of file Z3Solver.cpp.

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

◆ equal_to()

virtual bool llvm::SMTExpr::equal_to ( SMTExpr 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.

◆ operator<()

bool llvm::SMTExpr::operator< ( const SMTExpr Other) const
inline

Definition at line 105 of file SMTAPI.h.

References llvm::SMTSort::Profile(), and Profile().

◆ print()

virtual void llvm::SMTExpr::print ( raw_ostream OS) const
pure virtual

◆ Profile()

virtual void llvm::SMTExpr::Profile ( llvm::FoldingSetNodeID ID) const
pure virtual

Referenced by operator<().

Friends And Related Function Documentation

◆ operator==

bool operator== ( SMTExpr const LHS,
SMTExpr const RHS 
)
friend

Definition at line 114 of file SMTAPI.h.


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