CVC3
|
#include <expr_op.h>
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) |
|
inlineprivate |
|
inline |
Definition at line 68 of file expr_op.h.
References APPLY, and DebugAssert.
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().
Definition at line 31 of file expr_op.cpp.
|
inline |
|
inline |
Definition at line 82 of file expr_op.h.
References d_kind.
Referenced by CVC3::Expr::Expr(), and CVC3::ExprManager::newLeafExpr().
|
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().
|
friend |
|
friend |
|
private |
|
private |
Definition at line 55 of file expr_op.h.
Referenced by getExpr(), Op(), and operator=().