CVC3  2.4.1
Classes | Public Member Functions | Private Types | Private Member Functions | Private Attributes | Friends
CVC3::ExprManager Class Reference

#include <expr_manager.h>

List of all members.

Classes

class  EqEV
 Private class for d_exprSet. More...
class  HashEV
 Private class for d_exprSet. More...
class  HashString
 Private class for hashing strings. More...
class  TypeComputer
 Abstract class for computing expr type. More...

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 ExprboolExpr ()
 BOOLEAN Expr.
const ExprfalseExpr ()
 FALSE Expr.
const ExprtrueExpr ()
 TRUE Expr.
const std::vector< Expr > & getEmptyVector ()
 References to empty objects (used in ExprValue)
const ExprgetNullExpr ()
 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 Expr &var, const Expr &body)
Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body)
Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)
Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)
Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)
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.
ContextManagergetCM () const
 Fetch our ContextManager.
ContextgetCurrentContext () const
 Get the current context from our ContextManager.
int scopelevel ()
 Get current scope level.
void setTM (TheoremManager *tm)
 Set the TheoremManager.
TheoremManagergetTM () const
 Fetch the TheoremManager.
MemoryManagergetMM (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.
PrettyPrintergetPrinter () 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.
unsigned long getMemory (int verbosity)
 Calculate memory usage.

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)
Expr rebuildRec (const Expr &e)
 Cached recursive descent. Must be called only during rebuild()
ExprValuenewExprValue (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.
Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)
 Get information related to finiteness of a type.

Private Attributes

ContextManagerd_cm
 For backtracking attributes.
TheoremManagerd_tm
 Needed for Refl Theorems.
ExprManagerNotifyObjd_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.
PrettyPrinterd_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< Exprd_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.
bool d_inGC
 Flag for whether GC is already running.
std::deque< ExprValue * > d_pending
 Queue of pending exprs to GC.
ExprHashMap< Exprd_rebuildCache
 Rebuild cache.
TypeComputerd_typeComputer
 Instance of TypeComputer: must be registered.

Friends

class Expr
class ExprValue
class Op
class HashEV
class Type

Detailed Description

Expression Manager

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 CVC3. Each instance of the CVC3 library has its own expression manager, for thread-safety.

Definition at line 58 of file expr_manager.h.


Member Typedef Documentation

Hash set type for uniquifying expressions.

Definition at line 129 of file expr_manager.h.


Member Function Documentation

void ExprManager::installExprValue ( ExprValue ev)
private

Definition at line 36 of file expr_manager.cpp.

References DebugAssert.


Friends And Related Function Documentation

friend class Expr
friend

Definition at line 59 of file expr_manager.h.

Referenced by clear().

friend class ExprValue
friend

Definition at line 60 of file expr_manager.h.

friend class Op
friend

Definition at line 61 of file expr_manager.h.

friend class HashEV
friend

Definition at line 62 of file expr_manager.h.

friend class Type
friend

Definition at line 63 of file expr_manager.h.

Referenced by rebuildRec().


Member Data Documentation

ContextManager* CVC3::ExprManager::d_cm
private

For backtracking attributes.

Definition at line 65 of file expr_manager.h.

Referenced by ExprManager().

TheoremManager* CVC3::ExprManager::d_tm
private

Needed for Refl Theorems.

Definition at line 66 of file expr_manager.h.

ExprManagerNotifyObj* CVC3::ExprManager::d_notifyObj
private

Notification on pop()

Definition at line 67 of file expr_manager.h.

Referenced by ExprManager(), and ~ExprManager().

ExprIndex CVC3::ExprManager::d_index
private

Index counter for Expr compare()

Definition at line 68 of file expr_manager.h.

unsigned CVC3::ExprManager::d_flagCounter
private

Counter for a generic Expr flag.

Definition at line 69 of file expr_manager.h.

std::hash_map<int, std::string> CVC3::ExprManager::d_kindMap
private

The database of registered kinds.

Definition at line 72 of file expr_manager.h.

Referenced by getKindName(), and newKind().

std::hash_set<int> CVC3::ExprManager::d_typeKinds
private

The set of kinds representing a type.

Definition at line 74 of file expr_manager.h.

Referenced by newKind().

std::hash_map<std::string, int, HashString> CVC3::ExprManager::d_kindMapByName
private

The reverse map of names to kinds.

Definition at line 84 of file expr_manager.h.

Referenced by getKind(), and newKind().

PrettyPrinter* CVC3::ExprManager::d_prettyPrinter
private

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

Definition at line 87 of file expr_manager.h.

Referenced by registerPrettyPrinter(), and unregisterPrettyPrinter().

const int* CVC3::ExprManager::d_printDepth
private

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

Definition at line 95 of file expr_manager.h.

const bool* CVC3::ExprManager::d_withIndentation
private

Whether to print with indentation.

Definition at line 97 of file expr_manager.h.

int CVC3::ExprManager::d_indent
private

Permanent indentation.

Definition at line 99 of file expr_manager.h.

Referenced by incIndent(), and indent().

int CVC3::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 103 of file expr_manager.h.

Referenced by incIndent(), and indent().

const int* CVC3::ExprManager::d_lineWidth
private

Suggested line width for printing with indentation.

Definition at line 105 of file expr_manager.h.

const std::string* CVC3::ExprManager::d_inputLang
private

Input language (printing)

Definition at line 107 of file expr_manager.h.

Referenced by getInputLang(), and getOutputLang().

const std::string* CVC3::ExprManager::d_outputLang
private

Output language (printing)

Definition at line 109 of file expr_manager.h.

Referenced by getOutputLang().

const bool* CVC3::ExprManager::d_dagPrinting
private

Whether to print Expr's as DAGs.

Definition at line 111 of file expr_manager.h.

const std::string CVC3::ExprManager::d_mmFlag
private

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

Definition at line 113 of file expr_manager.h.

Referenced by ExprManager(), getMemory(), and registerSubclass().

ExprValueSet CVC3::ExprManager::d_exprSet
private

Hash set for uniquifying expressions.

Definition at line 131 of file expr_manager.h.

Referenced by clear(), gc(), newExprValue(), and rebuildRec().

std::vector<MemoryManager*> CVC3::ExprManager::d_mm
private

Array of memory managers for subclasses of ExprValue.

Definition at line 133 of file expr_manager.h.

Referenced by clear(), ExprManager(), gc(), registerSubclass(), resumeGC(), and ~ExprManager().

std::hash<void*> CVC3::ExprManager::d_pointerHash
private

A hash function for hashing pointers.

Definition at line 136 of file expr_manager.h.

Expr CVC3::ExprManager::d_bool
private

Expr constants cached for fast access.

Definition at line 139 of file expr_manager.h.

Referenced by clear(), and ExprManager().

Expr CVC3::ExprManager::d_false
private

Definition at line 140 of file expr_manager.h.

Referenced by clear(), and ExprManager().

Expr CVC3::ExprManager::d_true
private

Definition at line 141 of file expr_manager.h.

Referenced by clear(), and ExprManager().

std::vector<Expr> CVC3::ExprManager::d_emptyVec
private

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

Definition at line 143 of file expr_manager.h.

Referenced by ~ExprManager().

Expr CVC3::ExprManager::d_nullExpr
private

Null Expr to return by reference, for efficiency.

Definition at line 145 of file expr_manager.h.

Referenced by clear().

unsigned CVC3::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 153 of file expr_manager.h.

bool CVC3::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 159 of file expr_manager.h.

Referenced by clear(), gc(), isActive(), and ~ExprManager().

bool CVC3::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 168 of file expr_manager.h.

Referenced by gc(), and resumeGC().

std::vector<ExprValue*> CVC3::ExprManager::d_postponed
private

Vector of postponed garbage-collected expressions.

Definition at line 170 of file expr_manager.h.

Referenced by gc(), and resumeGC().

bool CVC3::ExprManager::d_inGC
private

Flag for whether GC is already running.

Definition at line 173 of file expr_manager.h.

Referenced by gc().

std::deque<ExprValue*> CVC3::ExprManager::d_pending
private

Queue of pending exprs to GC.

Definition at line 175 of file expr_manager.h.

Referenced by gc().

ExprHashMap<Expr> CVC3::ExprManager::d_rebuildCache
private

Rebuild cache.

Definition at line 178 of file expr_manager.h.

Referenced by rebuild(), and rebuildRec().

TypeComputer* CVC3::ExprManager::d_typeComputer
private

Instance of TypeComputer: must be registered.

Definition at line 197 of file expr_manager.h.

Referenced by checkType(), computeType(), and finiteTypeInfo().


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