CVC3::ExprSkolem Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprSkolem:

[legend]Collaboration diagram for CVC3::ExprSkolem:

[legend]List of all members.

Public Member Functions

• ExprSkolem (ExprManager *em, int index, const Expr &exist, ExprIndex idx=0)
• virtual ~ExprSkolem ()
• void * operator new (size_t size, MemoryManager *mm)

  Overload operator new.
  

• void operator delete (void *pMem, MemoryManager *mm)
• void operator delete (void *)

  Overload operator delete.
  

Protected Member Functions

• size_t computeHash () const

  Non-caching hash function which actually computes the hash.
  

• bool operator== (const ExprValue &ev2) const

  Equality between any two ExprValue objects (including subclasses).
  

• ExprValue * copy (ExprManager *em, ExprIndex idx=0) const

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

• bool isVar () const

  Uninterpreted constants.
  

Private Member Functions

• const Expr & getExistential () const
• int getBoundIndex () const
• size_t getMMIndex () const

  Get unique memory manager ID.
  

Private Attributes

• Expr d_quant

  The quantified expression to skolemize.
  

• int d_idx

  Variable index in the quantified expression.
  

Friends

• class Expr
• class ExprManager

---

Detailed Description

Definition at line 663 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 690 of file expr_value.h.

Referenced by copy().

virtual CVC3::ExprSkolem::~ExprSkolem

(

)

[inline, virtual]

Definition at line 693 of file expr_value.h.

---

Member Function Documentation

const Expr& CVC3::ExprSkolem::getExistential

(

)

const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 669 of file expr_value.h.

References d_quant.

Referenced by computeHash(), copy(), and operator==().

int CVC3::ExprSkolem::getBoundIndex

(

)

const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 670 of file expr_value.h.

References d_idx.

Referenced by computeHash(), copy(), and operator==().

size_t CVC3::ExprSkolem::getMMIndex

(

)

const [inline, private, virtual]

Get unique memory manager ID.

Reimplemented from CVC3::ExprValue.

Definition at line 673 of file expr_value.h.

References CVC3::EXPR_SKOLEM.

Referenced by copy(), and operator==().

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 676 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 150 of file expr_value.cpp.

References CVC3::ExprValue::getBoundIndex(), getBoundIndex(), CVC3::ExprValue::getExistential(), getExistential(), CVC3::ExprValue::getMMIndex(), and 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 158 of file expr_value.cpp.

References CVC3::ExprValue::d_em, ExprSkolem(), getBoundIndex(), getExistential(), CVC3::ExprManager::getMM(), getMMIndex(), and CVC3::ExprValue::rebuild().

bool CVC3::ExprSkolem::isVar

(

)

const [inline, protected, virtual]

Uninterpreted constants.

Reimplemented from CVC3::ExprValue.

Definition at line 686 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 695 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 698 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 701 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 664 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 665 of file expr_value.h.

---

Member Data Documentation

Expr CVC3::ExprSkolem::d_quant [private]

The quantified expression to skolemize.

Definition at line 667 of file expr_value.h.

Referenced by getExistential().

int CVC3::ExprSkolem::d_idx [private]

Variable index in the quantified expression.

Definition at line 668 of file expr_value.h.

Referenced by getBoundIndex().

---

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

• expr_value.h
• expr_value.cpp

---