CVC3::Op Class Reference

#include <expr_op.h>

Collaboration diagram for CVC3::Op:

List of all members.

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

)

[inline, private]

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