CVC3::Op Class Reference

#include <expr_op.h>

Collaboration diagram for CVC3::Op:

Public Member Functions
	Op ()
	Op (int kind)
	Op (const Op &op)
	Op (ExprManager *em, const Op &op)
	~Op ()
Op &	operator= (const Op &op)
bool	isNull () const
int	getKind () const
const Expr &	getExpr () const
std::string	toString () const

Private Member Functions
	Op (const Expr &e)
	Constructor for operators.

Private Attributes
int	d_kind
Expr	d_expr

Friends
class	Expr
class	ExprApply
class	ExprApplyTmp
class	::CInterface
std::ostream &	operator<< (std::ostream &os, const Op &op)
bool	operator== (const Op &op1, const Op &op2)

Detailed Description

Definition at line 48 of file expr_op.h.

Constructor & Destructor Documentation

CVC3::Op::Op ( const Expr &  e )

inlineprivate

Constructor for operators.

Definition at line 59 of file expr_op.h.

CVC3::Op::Op ( )

inline

Definition at line 66 of file expr_op.h.

CVC3::Op::Op ( int  kind )

inline

Definition at line 68 of file expr_op.h.

References APPLY, and DebugAssert.

CVC3::Op::Op ( const Op &  op )

inline

Definition at line 71 of file expr_op.h.

CVC3::Op::Op	(	ExprManager *	em,
		const Op &	op
	)

Definition at line 27 of file expr_op.cpp.

References d_expr, CVC3::Expr::isNull(), and CVC3::ExprManager::rebuild().

CVC3::Op::~Op ( )

inline

Definition at line 75 of file expr_op.h.

Member Function Documentation

Op & CVC3::Op::operator=

(

const Op &

op

)

Definition at line 31 of file expr_op.cpp.

References d_expr, and d_kind.

bool CVC3::Op::isNull ( ) const

inline

Definition at line 80 of file expr_op.h.

References d_kind, and NULL_KIND.

int CVC3::Op::getKind ( ) const

inline

Definition at line 82 of file expr_op.h.

References d_kind.

Referenced by CVC3::Expr::Expr(), and CVC3::ExprManager::newLeafExpr().

const Expr& CVC3::Op::getExpr ( ) const

inline

Definition at line 84 of file expr_op.h.

References APPLY, d_expr, d_kind, and DebugAssert.

Referenced by CVC3::TheoryUF::checkSat(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::Expr::Expr(), CVC3::ExprApply::ExprApply(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::TheoryQuant::getHeadExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoryUF::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryBitvector::printSmtLibShared(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::UFTheoremProducer::relToClosure(), CVC3::CompleteInstPreProcessor::substMacro(), and CVC3::VCL::transClosure().

string CVC3::Op::toString

(

)

const

Definition at line 38 of file expr_op.cpp.

Referenced by CVC3::CommonTheoremProducer::substitutivityRule().

Friends And Related Function Documentation

friend class Expr

friend

Definition at line 49 of file expr_op.h.

friend class ExprApply

friend

Definition at line 50 of file expr_op.h.

friend class ExprApplyTmp

friend

Definition at line 51 of file expr_op.h.

friend class ::CInterface

friend

Definition at line 52 of file expr_op.h.

std::ostream& operator<< ( std::ostream &  os, const Op &  op  )

friend

Definition at line 90 of file expr_op.h.

bool operator== ( const Op &  op1, const Op &  op2  )

friend

Definition at line 93 of file expr_op.h.

Member Data Documentation

int CVC3::Op::d_kind

private

Definition at line 54 of file expr_op.h.

Referenced by getExpr(), getKind(), isNull(), and operator=().

Expr CVC3::Op::d_expr

private

Definition at line 55 of file expr_op.h.

Referenced by getExpr(), Op(), and operator=().

---

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

• expr_op.h
• expr_op.cpp