CVCL::ExprSkolem Class Reference

#include <expr_value.h>

Inheritance diagram for CVCL::ExprSkolem:

[legend]Collaboration diagram for CVCL::ExprSkolem:

[legend]List of all members.

Public Member Functions

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

  Overload operator new.
  

• 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 569 of file expr_value.h.

---

Constructor & Destructor Documentation

CVCL::ExprSkolem::ExprSkolem (  ExprManager *  em, int  index, const Expr &  exist, unsigned  idx = 0 )  [inline]

Definition at line 596 of file expr_value.h. Referenced by copy().

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

Definition at line 599 of file expr_value.h.

---

Member Function Documentation

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

Reimplemented from CVCL::ExprValue. Definition at line 575 of file expr_value.h. Referenced by copy(), and operator==().

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

Reimplemented from CVCL::ExprValue. Definition at line 576 of file expr_value.h. Referenced by copy(), and operator==().

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

Get unique memory manager ID. Reimplemented from CVCL::ExprValue. Definition at line 579 of file expr_value.h. References CVCL::EXPR_SKOLEM. Referenced by copy(), and operator==().

size_t CVCL::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 CVCL::ExprValue. Definition at line 582 of file expr_value.h.

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

Equality between any two ExprValue objects (including subclasses). Reimplemented from CVCL::ExprValue. Definition at line 138 of file expr_value.cpp. References CVCL::ExprValue::getBoundIndex(), getBoundIndex(), CVCL::ExprValue::getExistential(), getExistential(), CVCL::ExprValue::getMMIndex(), and getMMIndex().

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

Make a clean copy of itself using the given memory manager. Reimplemented from CVCL::ExprValue. Definition at line 146 of file expr_value.cpp. References CVCL::ExprValue::d_em, ExprSkolem(), getBoundIndex(), getExistential(), CVCL::ExprManager::getMM(), getMMIndex(), and CVCL::ExprValue::rebuild().

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

Uninterpreted constants. Reimplemented from CVCL::ExprValue. Definition at line 592 of file expr_value.h.

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

Overload operator new. Reimplemented from CVCL::ExprValue. Definition at line 601 of file expr_value.h. References CVCL::MemoryManager::newData().

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

Overload operator delete. Reimplemented from CVCL::ExprValue. Definition at line 604 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVCL::ExprValue. Definition at line 570 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVCL::ExprValue. Definition at line 571 of file expr_value.h.

---

Member Data Documentation

Expr CVCL::ExprSkolem::d_quant [private]

The quantified expression to skolemize. Definition at line 573 of file expr_value.h.

int CVCL::ExprSkolem::d_idx [private]

Variable index in the quantified expression. Definition at line 574 of file expr_value.h.

---

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

• expr_value.h
• expr_value.cpp

---