CVC3
Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | Friends

CVC3::ExprSkolem Class Reference

#include <expr_value.h>

Inherits CVC3::ExprValue.

Collaboration diagram for CVC3::ExprSkolem:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Friends


Detailed Description

Definition at line 700 of file expr_value.h.


Constructor & Destructor Documentation

CVC3::ExprSkolem::ExprSkolem ( ExprManager em,
int  index,
const Expr exist,
ExprIndex  idx = 0 
) [inline]

Definition at line 727 of file expr_value.h.

virtual CVC3::ExprSkolem::~ExprSkolem ( ) [inline, virtual]

Definition at line 730 of file expr_value.h.


Member Function Documentation

const Expr& CVC3::ExprSkolem::getExistential ( ) const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 706 of file expr_value.h.

References d_quant.

Referenced by computeHash().

int CVC3::ExprSkolem::getBoundIndex ( ) const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 707 of file expr_value.h.

References d_idx.

Referenced by computeHash().

size_t CVC3::ExprSkolem::getMMIndex ( ) const [inline, private, virtual]

Get unique memory manager ID.

Reimplemented from CVC3::ExprValue.

Definition at line 710 of file expr_value.h.

References CVC3::EXPR_SKOLEM.

size_t CVC3::ExprSkolem::computeHash ( ) const [inline, protected, virtual]

Non-caching hash function which actually computes the hash.

This is the method that all subclasses should implement

Reimplemented from CVC3::ExprValue.

Definition at line 713 of file expr_value.h.

References CVC3::Expr::getBody(), getBoundIndex(), getExistential(), CVC3::Expr::hash(), and PRIME.

bool CVC3::ExprSkolem::operator== ( const ExprValue ev2) const [protected, virtual]

Equality between any two ExprValue objects (including subclasses)

Reimplemented from CVC3::ExprValue.

Definition at line 156 of file expr_value.cpp.

References CVC3::ExprValue::getBoundIndex(), CVC3::ExprValue::getExistential(), and CVC3::ExprValue::getMMIndex().

ExprValue * CVC3::ExprSkolem::copy ( ExprManager em,
ExprIndex  idx = 0 
) const [protected, virtual]

Make a clean copy of itself using the given memory manager.

Reimplemented from CVC3::ExprValue.

Definition at line 164 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

bool CVC3::ExprSkolem::isVar ( ) const [inline, protected, virtual]

Uninterpreted constants.

Reimplemented from CVC3::ExprValue.

Definition at line 723 of file expr_value.h.

void* CVC3::ExprSkolem::operator new ( size_t  size,
MemoryManager mm 
) [inline]

Overload operator new.

Reimplemented from CVC3::ExprValue.

Definition at line 732 of file expr_value.h.

References CVC3::MemoryManager::newData().

void CVC3::ExprSkolem::operator delete ( void *  pMem,
MemoryManager mm 
) [inline]

Reimplemented from CVC3::ExprValue.

Definition at line 735 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprSkolem::operator delete ( void *  ) [inline]

Overload operator delete.

Reimplemented from CVC3::ExprValue.

Definition at line 738 of file expr_value.h.


Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 701 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 702 of file expr_value.h.


Member Data Documentation

The quantified expression to skolemize.

Definition at line 704 of file expr_value.h.

Referenced by getExistential().

int CVC3::ExprSkolem::d_idx [private]

Variable index in the quantified expression.

Definition at line 705 of file expr_value.h.

Referenced by getBoundIndex().


The documentation for this class was generated from the following files: