#include <expr_value.h>
Definition at line 534 of file expr_value.h.
CVC3::ExprApplyTmp::ExprApplyTmp | ( | ExprManager * | em, | |
const Op & | op, | |||
const std::vector< Expr > & | kids | |||
) | [inline] |
Definition at line 550 of file expr_value.h.
References CVC3::APPLY, CVC3::ExprValue::d_kind, DebugAssert, CVC3::Op::getExpr(), and CVC3::Expr::isNull().
virtual CVC3::ExprApplyTmp::~ExprApplyTmp | ( | ) | [inline, virtual] |
Definition at line 555 of file expr_value.h.
size_t CVC3::ExprApplyTmp::getMMIndex | ( | ) | const [inline, protected, virtual] |
Tell ExprManager who we are.
Reimplemented from CVC3::ExprNodeTmp.
Definition at line 540 of file expr_value.h.
References CVC3::EXPR_APPLY.
Referenced by copy(), and operator==().
size_t CVC3::ExprApplyTmp::computeHash | ( | ) | const [inline, protected, virtual] |
Use our static hash() for the member method.
Reimplemented from CVC3::ExprNodeTmp.
Definition at line 541 of file expr_value.h.
References d_opExpr, CVC3::Expr::hash(), and PRIME.
Op CVC3::ExprApplyTmp::getOp | ( | ) | const [inline, protected, virtual] |
Get the Op from an Apply Expr.
Reimplemented from CVC3::ExprValue.
Definition at line 544 of file expr_value.h.
References d_opExpr.
Referenced by operator==().
bool CVC3::ExprApplyTmp::isApply | ( | ) | const [inline, protected, virtual] |
Application of another expression.
Reimplemented from CVC3::ExprValue.
Definition at line 545 of file expr_value.h.
ExprValue * CVC3::ExprApplyTmp::copy | ( | ExprManager * | em, | |
ExprIndex | idx = 0 | |||
) | const [protected, virtual] |
Make a clean copy of itself using the given memory manager.
Reimplemented from CVC3::ExprNodeTmp.
Definition at line 254 of file expr_value.cpp.
References CVC3::ExprNodeTmp::d_children, CVC3::ExprValue::d_em, d_opExpr, CVC3::ExprValue::ExprApply, CVC3::ExprManager::getMM(), getMMIndex(), and CVC3::ExprValue::rebuild().
bool CVC3::ExprApplyTmp::operator== | ( | const ExprValue & | ev2 | ) | const [virtual] |
Compare with another ExprValue.
Reimplemented from CVC3::ExprNodeTmp.
Definition at line 246 of file expr_value.cpp.
References CVC3::ExprValue::getKids(), CVC3::ExprNodeTmp::getKids(), CVC3::ExprValue::getMMIndex(), getMMIndex(), CVC3::ExprValue::getOp(), and getOp().
friend class Expr [friend] |
friend class ExprManager [friend] |
Expr CVC3::ExprApplyTmp::d_opExpr [private] |