CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::Op Class Reference

#include <expr_op.h>

Public Member Functions

 Op ()
 
 Op (int kind)
 
 Op (const Op &op)
 
 Op (ExprManager *em, const Op &op)
 
 ~Op ()
 
Opoperator= (const Op &op)
 
bool isNull () const
 
int getKind () const
 
const ExprgetExpr () const
 
std::string toString () const
 

Private Member Functions

 Op (const Expr &e)
 Constructor for operators. More...
 

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