CVCL::Op Class Reference

#include <expr_op.h>

Collaboration diagram for CVCL::Op:

[legend]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)
• 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 ::CInterface
• std::ostream & operator<< (std::ostream &os, const Op &op)
• bool operator== (const Op &op1, const Op &op2)

---

Detailed Description

Definition at line 56 of file expr_op.h.

---

Constructor & Destructor Documentation

CVCL::Op::Op (  const Expr &  e  )  [inline, private]

Constructor for operators. Definition at line 66 of file expr_op.h.

CVCL::Op::Op (   )  [inline]

Definition at line 73 of file expr_op.h.

CVCL::Op::Op (  int  kind  )  [inline]

Definition at line 75 of file expr_op.h. References CVCL::APPLY.

CVCL::Op::Op (  const Op &  op  )  [inline]

Definition at line 78 of file expr_op.h.

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

Definition at line 35 of file expr_op.cpp. References d_expr, CVCL::Expr::isNull(), and CVCL::ExprManager::rebuild().

CVCL::Op::~Op (   )  [inline]

Definition at line 82 of file expr_op.h.

---

Member Function Documentation

Op & CVCL::Op::operator= (  const Op &  op  )

Definition at line 39 of file expr_op.cpp. References d_expr, and d_kind.

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

Definition at line 87 of file expr_op.h. References d_kind. Referenced by CVCL::Expr::Expr(), and CVCL::ExprManager::newLeafExpr().

const Expr& CVCL::Op::getExpr (   )  const [inline]

Definition at line 89 of file expr_op.h. References d_expr. Referenced by CVCL::TheoryUF::checkSat(), CVCL::TheoryDatatype::computeType(), CVCL::Expr::Expr(), CVCL::ExprApply::ExprApply(), CVCL::TheoryQuant::getHead(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::ExprManager::newLeafExpr(), CVCL::TheoryUF::print(), CVCL::TheoryBitvector::print(), CVCL::Expr::printAST(), and CVCL::UFTheoremProducer::relToClosure().

string CVCL::Op::toString (   )  const

Definition at line 46 of file expr_op.cpp.

---

Friends And Related Function Documentation

friend class Expr [friend]

Definition at line 57 of file expr_op.h.

friend class ExprApply [friend]

Definition at line 58 of file expr_op.h.

friend class ::CInterface [friend]

Definition at line 59 of file expr_op.h.

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

Definition at line 94 of file expr_op.h.

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

Definition at line 97 of file expr_op.h.

---

Member Data Documentation

int CVCL::Op::d_kind [private]

Definition at line 61 of file expr_op.h. Referenced by getKind(), and operator=().

Expr CVCL::Op::d_expr [private]

Definition at line 62 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

---