llvm::SMTExpr Class Reference

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

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 917 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::Other, and Profile.

print()

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

pure virtual

Referenced by dump().

Profile()

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

pure virtual

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:

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