CVCL::ExprManager Class Reference

#include <expr_manager.h>

Collaboration diagram for CVCL::ExprManager:

[legend]List of all members.

Public Member Functions

• ExprManager (ContextManager *cm, const CLFlags &flags)

  Constructor.
  

• ~ExprManager ()

  Destructor.
  

• void clear ()

  Free up all memory and delete all the expressions.
  

• bool isActive ()

  Check if the ExprManager is still active (clear() was not called).
  

• void gc (ExprValue *ev)

  Garbage collect the ExprValue pointer.
  

• void postponeGC ()

  Postpone deletion of garbage-collected expressions.
  

• void resumeGC ()

  Resume deletion of garbage-collected expressions.
  

• Expr rebuild (const Expr &e)

  Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
  

• ExprIndex nextIndex ()

  Return the next Expr index.
  

• ExprIndex lastIndex ()
• void clearFlags ()

  Clears the generic Expr flag in all Exprs.
  

• const Expr & boolExpr ()

  BOOLEAN Expr.
  

• const Expr & falseExpr ()

  FALSE Expr.
  

• const Expr & trueExpr ()

  TRUE Expr.
  

• const std::vector< Expr > & getEmptyVector ()

  References to empty objects (used in ExprValue).
  

• const Expr & getNullExpr ()

  References to empty objects (used in ExprValue).
  

• Expr newExpr (ExprValue *ev)

  Return either an existing or a new Expr matching ev.
  

• Expr newLeafExpr (const Op &op)
• Expr newStringExpr (const std::string &s)
• Expr newRatExpr (const Rational &r)
• Expr newSkolemExpr (const Expr &e, int i)
• Expr newVarExpr (const std::string &s)
• Expr newSymbolExpr (const std::string &s, int kind)
• Expr newBoundVarExpr (const std::string &name, const std::string &uid)
• Expr newBoundVarExpr (const std::string &name, const std::string &uid, const Type &type)
• Expr newBoundVarExpr (const Type &type)
• Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body)
• Expr andExpr (const std::vector< Expr > &children)
• Expr orExpr (const std::vector< Expr > &children)
• size_t hash (const Expr &e) const

  Hash function for a single Expr.
  

• ContextManager * getCM () const

  Fetch our ContextManager.
  

• Context * getCurrentContext () const

  Get the current context from our ContextManager.
  

• int scopelevel ()

  Get current scope level.
  

• MemoryManager * getMM (size_t MMIndex)

  Return a MemoryManager for the given ExprValue type.
  

• unsigned getSimpCacheTag () const

  Get the simplifier's cache tag.
  

• void invalidateSimpCache ()

  Invalidate the simplifier's cache tag.
  

• void registerTypeComputer (TypeComputer *typeComputer)

  Register type computer.
  

• int printDepth () const

  Get printing depth.
  

• bool withIndentation () const

  Whether to print with indentation.
  

• int lineWidth () const

  Suggested line width for printing with indentation.
  

• int indent () const

  Get initial indentation.
  

• int indent (int n, bool permanent=false)

  Set initial indentation. Returns the previous permanent value.
  

• int incIndent (int n, bool permanent=false)

  Increment the current transient indentation by n.
  

• void restoreIndent ()

  Set transient indentation to permanent.
  

• InputLanguage getInputLang () const

  Get the input language for printing.
  

• InputLanguage getOutputLang () const

  Get the output language for printing.
  

• bool dagPrinting () const

  Whether to print Expr's as DAGs.
  

• PrettyPrinter * getPrinter () const

  Return the pretty-printer if there is one; otherwise return NULL.
  

• void newKind (int kind, const std::string &name, bool isType=false)

  Register a new kind.
  

• void registerPrettyPrinter (PrettyPrinter &printer)

  Register the pretty-printer (can only do it if none registered).
  

• void unregisterPrettyPrinter ()

  Tell ExprManager that the printer is no longer valid.
  

• bool isKindRegistered (int kind)

  Returns true if kind is built into CVC or has been registered via newKind.
  

• bool isTypeKind (int kind)

  Check if a kind represents a type.
  

• const std::string & getKindName (int kind)

  Return the name associated with a kind. The kind must already be registered.
  

• int getKind (const std::string &name)

  Return a kind associated with a name. Returns NULL_KIND if not found.
  

• size_t registerSubclass (size_t sizeOfSubclass)

  Register a new subclass of ExprValue.
  

Private Types

• typedef std::hash_set< ExprValue *,
  HashEV, EqEV > ExprValueSet

  Hash set type for uniquifying expressions.
  

Private Member Functions

• size_t hash (const ExprValue *ev) const
• void installExprValue (ExprValue *ev)
• IF_DEBUG (bool d_inRebuild)
• Expr rebuildRec (const Expr &e)

  Cached recursive descent. Must be called only during rebuild().
  

• ExprValue * newExprValue (ExprValue *ev)

  Return either an existing or a new ExprValue matching ev.
  

• unsigned getFlag ()

  Return the current Expr flag counter.
  

• unsigned nextFlag ()

  Increment and return the Expr flag counter (this clears all the flags).
  

• void computeType (const Expr &e)

  Compute the type of the Expr.
  

• void checkType (const Expr &e)

  Check well-formedness of a type Expr.
  

Private Attributes

• ContextManager * d_cm

  For backtracking attributes.
  

• ExprManagerNotifyObj * d_notifyObj

  Notification on pop().
  

• ExprIndex d_index

  Index counter for Expr compare().
  

• unsigned d_flagCounter

  Counter for a generic Expr flag.
  

• std::hash_map< int, std::string > d_kindMap

  The database of registered kinds.
  

• std::hash_set< int > d_typeKinds

  The set of kinds representing a type.
  

• std::hash_map< std::string,
  int, HashString > d_kindMapByName

  The reverse map of names to kinds.
  

• PrettyPrinter * d_prettyPrinter

  The registered pretty-printer, a connector to theory-specific pretty-printers.
  

• const int * d_printDepth

  Print upto the given depth, replace the rest with "...". -1==unlimited depth.
  

• const bool * d_withIndentation

  Whether to print with indentation.
  

• int d_indent

  Permanent indentation.
  

• int d_indentTransient

  Transient indentation.
  

• const int * d_lineWidth

  Suggested line width for printing with indentation.
  

• const std::string * d_inputLang

  Input language (printing).
  

• const std::string * d_outputLang

  Output language (printing).
  

• const bool * d_dagPrinting

  Whether to print Expr's as DAGs.
  

• const std::string d_mmFlag

  Which memory manager to use (copy the flag value and keep it the same).
  

• ExprValueSet d_exprSet

  Hash set for uniquifying expressions.
  

• std::vector< MemoryManager * > d_mm

  Array of memory managers for subclasses of ExprValue.
  

• std::hash< void * > d_pointerHash

  A hash function for hashing pointers.
  

• Expr d_bool

  Expr constants cached for fast access.
  

• Expr d_false
• Expr d_true
• std::vector< Expr > d_emptyVec

  Empty vector of Expr to return by reference as empty vector of children.
  

• Expr d_nullExpr

  Null Expr to return by reference, for efficiency.
  

• unsigned d_simpCacheTagCurrent

  Current value of the simplifier cache tag.
  

• bool d_disableGC

  Disable garbage collection.
  

• bool d_postponeGC

  Postpone deleting garbage-collected expressions.
  

• std::vector< ExprValue * > d_postponed

  Vector of postponed garbage-collected expressions.
  

• ExprHashMap< Expr > d_rebuildCache

  Rebuild cache.
  

• TypeComputer * d_typeComputer

  Instance of TypeComputer: must be registered.
  

Friends

• class Expr
• class ExprValue
• class Op
• class HashEV
• class Type

Classes

• class EqEV

  Private class for d_exprSet. More...
  

• class HashEV

  Private classe for d_exprSet. More...
  

• class HashString

  Private class for hashing strings. More...
  

• class TypeComputer

  Abstract class for computing expr type. More...
  

---

Detailed Description

Class: ExprManager

Author: Sergey Berezin

Created: Wed Dec 4 14:26:35 2002

Description: Global state of the Expr package for a particular instance of CVC Lite. Each instance of the CVC Lite library has its own expression manager, for thread-safety.

Definition at line 63 of file expr_manager.h.

---

Member Typedef Documentation

typedef std::hash_set<ExprValue*, HashEV, EqEV> CVCL::ExprManager::ExprValueSet [private]

Hash set type for uniquifying expressions. Definition at line 133 of file expr_manager.h.

---

Member Function Documentation

void ExprManager::installExprValue (  ExprValue *  ev  )  [private]

Definition at line 297 of file expr_manager.cpp. References CVCL::AND, CVCL::ExprValue::arity(), d_exprSet, CVCL::ExprValue::d_height, CVCL::ExprValue::d_highestKid, CVCL::ExprValue::d_kind, CVCL::ExprValue::getKids(), CVCL::IFF, CVCL::IMPLIES, isActive(), CVCL::ITE, CVCL::NOT, and CVCL::OR. Referenced by newExprValue(), and rebuildRec().

CVCL::ExprManager::IF_DEBUG (  bool  d_inRebuild  )  [private]

Referenced by clear(), ExprManager(), and rebuild().

---

Friends And Related Function Documentation

friend class Expr [friend]

Definition at line 64 of file expr_manager.h. Referenced by andExpr(), clear(), newExpr(), and orExpr().

friend class ExprValue [friend]

Definition at line 65 of file expr_manager.h.

friend class Op [friend]

Definition at line 66 of file expr_manager.h.

friend class HashEV [friend]

Definition at line 67 of file expr_manager.h.

friend class Type [friend]

Definition at line 68 of file expr_manager.h. Referenced by rebuildRec().

---

Member Data Documentation

ContextManager* CVCL::ExprManager::d_cm [private]

For backtracking attributes. Definition at line 70 of file expr_manager.h. Referenced by ExprManager(), getCM(), getCurrentContext(), and scopelevel().

ExprManagerNotifyObj* CVCL::ExprManager::d_notifyObj [private]

Notification on pop(). Definition at line 71 of file expr_manager.h. Referenced by ExprManager(), and ~ExprManager().

ExprIndex CVCL::ExprManager::d_index [private]

Index counter for Expr compare(). Definition at line 72 of file expr_manager.h. Referenced by lastIndex(), and nextIndex().

unsigned CVCL::ExprManager::d_flagCounter [private]

Counter for a generic Expr flag. Definition at line 73 of file expr_manager.h. Referenced by getFlag(), and nextFlag().

std::hash_map<int, std::string> CVCL::ExprManager::d_kindMap [private]

The database of registered kinds. Definition at line 76 of file expr_manager.h. Referenced by getKindName(), and isKindRegistered().

std::hash_set<int> CVCL::ExprManager::d_typeKinds [private]

The set of kinds representing a type. Definition at line 78 of file expr_manager.h. Referenced by isTypeKind().

std::hash_map<std::string, int, HashString> CVCL::ExprManager::d_kindMapByName [private]

The reverse map of names to kinds. Definition at line 88 of file expr_manager.h.

PrettyPrinter* CVCL::ExprManager::d_prettyPrinter [private]

The registered pretty-printer, a connector to theory-specific pretty-printers. Definition at line 91 of file expr_manager.h. Referenced by getPrinter(), registerPrettyPrinter(), and unregisterPrettyPrinter().

const int* CVCL::ExprManager::d_printDepth [private]

Print upto the given depth, replace the rest with "...". -1==unlimited depth. Definition at line 99 of file expr_manager.h. Referenced by printDepth().

const bool* CVCL::ExprManager::d_withIndentation [private]

Whether to print with indentation. Definition at line 101 of file expr_manager.h. Referenced by withIndentation().

int CVCL::ExprManager::d_indent [private]

Permanent indentation. Definition at line 103 of file expr_manager.h. Referenced by incIndent(), indent(), and restoreIndent().

int CVCL::ExprManager::d_indentTransient [private]

Transient indentation. Normally is the same as d_indent, but may temporarily be different for printing one single Expr Definition at line 107 of file expr_manager.h. Referenced by incIndent(), indent(), and restoreIndent().

const int* CVCL::ExprManager::d_lineWidth [private]

Suggested line width for printing with indentation. Definition at line 109 of file expr_manager.h. Referenced by lineWidth().

const std::string* CVCL::ExprManager::d_inputLang [private]

Input language (printing). Definition at line 111 of file expr_manager.h. Referenced by getInputLang(), and getOutputLang().

const std::string* CVCL::ExprManager::d_outputLang [private]

Output language (printing). Definition at line 113 of file expr_manager.h. Referenced by getOutputLang().

const bool* CVCL::ExprManager::d_dagPrinting [private]

Whether to print Expr's as DAGs. Definition at line 115 of file expr_manager.h. Referenced by dagPrinting().

const std::string CVCL::ExprManager::d_mmFlag [private]

Which memory manager to use (copy the flag value and keep it the same). Definition at line 117 of file expr_manager.h. Referenced by ExprManager(), and registerSubclass().

ExprValueSet CVCL::ExprManager::d_exprSet [private]

Hash set for uniquifying expressions. Definition at line 135 of file expr_manager.h. Referenced by clear(), gc(), installExprValue(), newExprValue(), and rebuildRec().

std::vector<MemoryManager*> CVCL::ExprManager::d_mm [private]

Array of memory managers for subclasses of ExprValue. Definition at line 137 of file expr_manager.h. Referenced by clear(), ExprManager(), gc(), getMM(), registerSubclass(), resumeGC(), and ~ExprManager().

std::hash<void*> CVCL::ExprManager::d_pointerHash [private]

A hash function for hashing pointers. Definition at line 140 of file expr_manager.h.

Expr CVCL::ExprManager::d_bool [private]

Expr constants cached for fast access. Definition at line 143 of file expr_manager.h. Referenced by boolExpr(), clear(), and ExprManager().

Expr CVCL::ExprManager::d_false [private]

Definition at line 144 of file expr_manager.h. Referenced by clear(), ExprManager(), and falseExpr().

Expr CVCL::ExprManager::d_true [private]

Definition at line 145 of file expr_manager.h. Referenced by clear(), ExprManager(), and trueExpr().

std::vector<Expr> CVCL::ExprManager::d_emptyVec [private]

Empty vector of Expr to return by reference as empty vector of children. Definition at line 147 of file expr_manager.h. Referenced by getEmptyVector(), and ~ExprManager().

Expr CVCL::ExprManager::d_nullExpr [private]

Null Expr to return by reference, for efficiency. Definition at line 149 of file expr_manager.h. Referenced by clear(), and getNullExpr().

unsigned CVCL::ExprManager::d_simpCacheTagCurrent [private]

Current value of the simplifier cache tag. The cached values of calls to Simplify are valid as long as their cache tag matches this tag. Caches can then be invalidated by incrementing this tag. Definition at line 157 of file expr_manager.h. Referenced by getSimpCacheTag(), and invalidateSimpCache().

bool CVCL::ExprManager::d_disableGC [private]

Disable garbage collection. This flag disables the garbage collection. Normally, it's set in the destructor, so that we can delete all remaining expressions without GC getting in the way. Definition at line 163 of file expr_manager.h. Referenced by clear(), gc(), isActive(), CVCL::Expr::~Expr(), and ~ExprManager().

bool CVCL::ExprManager::d_postponeGC [private]

Postpone deleting garbage-collected expressions. Useful during manipulation of context, especially at the time of backtracking, since we may have objects with circular dependencies (like find pointers). The postponed expressions will be deleted the next time the garbage collector is called after this flag is cleared. Definition at line 172 of file expr_manager.h. Referenced by gc(), postponeGC(), and resumeGC().

std::vector<ExprValue*> CVCL::ExprManager::d_postponed [private]

Vector of postponed garbage-collected expressions. Definition at line 174 of file expr_manager.h. Referenced by gc(), and resumeGC().

ExprHashMap<Expr> CVCL::ExprManager::d_rebuildCache [private]

Rebuild cache. Definition at line 176 of file expr_manager.h. Referenced by rebuild(), and rebuildRec().

TypeComputer* CVCL::ExprManager::d_typeComputer [private]

Instance of TypeComputer: must be registered. Definition at line 192 of file expr_manager.h. Referenced by checkType(), computeType(), and registerTypeComputer().

---

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

• expr_manager.h
• expr_manager.cpp

---