CVC3::Op Class Reference

#include <expr_op.h>

Collaboration diagram for CVC3::Op:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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 CVC3::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.

int CVC3::Op::getKind (  )  const [inline]

Definition at line 80 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 82 of file expr_op.h.

References d_expr.

Referenced by CVC3::TheoryDatatype::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::Expr::Expr(), CVC3::ExprApply::ExprApply(), CVC3::ExprApplyTmp::ExprApplyTmp(), getHeadExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoryUF::print(), CVC3::TheoryBitvector::print(), CVC3::Expr::printAST(), and CVC3::UFTheoremProducer::relToClosure().

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 87 of file expr_op.h.

bool operator== ( const Op op1,
const Op op2 
) [friend]

Definition at line 90 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 getKind(), 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:
Generated on Tue Jul 3 14:36:21 2007 for CVC3 by  doxygen 1.5.1