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 103 of file SMTAPI.h.

Constructor & Destructor Documentation

◆ SMTExpr()

llvm::SMTExpr::SMTExpr ( )

default

Referenced by equal_to(), operator<(), and operator==.

◆ ~SMTExpr()

virtual llvm::SMTExpr::~SMTExpr ( )

virtualdefault

Member Function Documentation

◆ dump()

LLVM_DUMP_METHOD void SMTExpr::dump ( ) const

Definition at line 995 of file Z3Solver.cpp.

References llvm::errs(), LLVM_DUMP_METHOD, 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.

References SMTExpr().

◆ operator<()

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

inline

Definition at line 108 of file SMTAPI.h.

References llvm::Other, Profile, and SMTExpr().

◆ print()

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

pure virtual

References LLVM_DUMP_METHOD.

Referenced by dump().

◆ Profile()

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

pure virtual

◆ operator==

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

friend

Definition at line 117 of file SMTAPI.h.

References LHS, RHS, and SMTExpr().

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

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

Public Member Functions

Protected Member Functions

Friends