Private methods
[Expression Package]

Collaboration diagram for Private methods:

Functions

• size_t CVCL::ExprManager::HashString::operator() (const std::string &s) const
• CVCL::ExprManager::HashEV::HashEV (ExprManager *em)
• size_t CVCL::ExprManager::HashEV::operator() (ExprValue *ev) const
• virtual CVCL::ExprManager::TypeComputer::~TypeComputer ()
• virtual void CVCL::ExprManager::TypeComputer::computeType (const Expr &e)=0

  Compute the type of e.
  

• virtual void CVCL::ExprManager::TypeComputer::checkType (const Expr &e)=0

  Check that e is a valid Type expr.
  

• Expr CVCL::ExprManager::rebuildRec (const Expr &e)

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

• ExprValue * CVCL::ExprManager::newExprValue (ExprValue *ev)

  Return either an existing or a new ExprValue matching ev.
  

• unsigned CVCL::ExprManager::getFlag ()

  Return the current Expr flag counter.
  

• unsigned CVCL::ExprManager::nextFlag ()

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

• void CVCL::ExprManager::computeType (const Expr &e)

  Compute the type of the Expr.
  

• void CVCL::ExprManager::checkType (const Expr &e)

  Check well-formedness of a type Expr.
  

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

  Constructor.
  

• CVCL::ExprManager::~ExprManager ()

  Destructor.
  

• void CVCL::ExprManager::clear ()

  Free up all memory and delete all the expressions.
  

• bool CVCL::ExprManager::isActive ()

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

• void CVCL::ExprManager::gc (ExprValue *ev)

  Garbage collect the ExprValue pointer.
  

• void CVCL::ExprManager::postponeGC ()

  Postpone deletion of garbage-collected expressions.
  

• void CVCL::ExprManager::resumeGC ()

  Resume deletion of garbage-collected expressions.
  

• Expr CVCL::ExprManager::rebuild (const Expr &e)

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

• ExprIndex CVCL::ExprManager::nextIndex ()

  Return the next Expr index.
  

• ExprIndex CVCL::ExprManager::lastIndex ()
• void CVCL::ExprManager::clearFlags ()

  Clears the generic Expr flag in all Exprs.
  

• const Expr & CVCL::ExprManager::boolExpr ()

  BOOLEAN Expr.
  

• const Expr & CVCL::ExprManager::falseExpr ()

  FALSE Expr.
  

• const Expr & CVCL::ExprManager::trueExpr ()

  TRUE Expr.
  

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

  References to empty objects (used in ExprValue).
  

• const Expr & CVCL::ExprManager::getNullExpr ()

  References to empty objects (used in ExprValue).
  

• Expr CVCL::ExprManager::newExpr (ExprValue *ev)

  Return either an existing or a new Expr matching ev.
  

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

  Hash function for a single Expr.
  

• ContextManager * CVCL::ExprManager::getCM () const

  Fetch our ContextManager.
  

• Context * CVCL::ExprManager::getCurrentContext () const

  Get the current context from our ContextManager.
  

• int CVCL::ExprManager::scopelevel ()

  Get current scope level.
  

• MemoryManager * CVCL::ExprManager::getMM (size_t MMIndex)

  Return a MemoryManager for the given ExprValue type.
  

• unsigned CVCL::ExprManager::getSimpCacheTag () const

  Get the simplifier's cache tag.
  

• void CVCL::ExprManager::invalidateSimpCache ()

  Invalidate the simplifier's cache tag.
  

• void CVCL::ExprManager::registerTypeComputer (TypeComputer *typeComputer)

  Register type computer.
  

• int CVCL::ExprManager::printDepth () const

  Get printing depth.
  

• bool CVCL::ExprManager::withIndentation () const

  Whether to print with indentation.
  

• int CVCL::ExprManager::lineWidth () const

  Suggested line width for printing with indentation.
  

• int CVCL::ExprManager::indent () const

  Get initial indentation.
  

• int CVCL::ExprManager::indent (int n, bool permanent=false)

  Set initial indentation. Returns the previous permanent value.
  

• int CVCL::ExprManager::incIndent (int n, bool permanent=false)

  Increment the current transient indentation by n.
  

• void CVCL::ExprManager::restoreIndent ()

  Set transient indentation to permanent.
  

• InputLanguage CVCL::ExprManager::getInputLang () const

  Get the input language for printing.
  

• InputLanguage CVCL::ExprManager::getOutputLang () const

  Get the output language for printing.
  

• bool CVCL::ExprManager::dagPrinting () const

  Whether to print Expr's as DAGs.
  

• PrettyPrinter * CVCL::ExprManager::getPrinter () const

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

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

  Register a new kind.
  

• void CVCL::ExprManager::registerPrettyPrinter (PrettyPrinter &printer)

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

• void CVCL::ExprManager::unregisterPrettyPrinter ()

  Tell ExprManager that the printer is no longer valid.
  

• bool CVCL::ExprManager::isKindRegistered (int kind)

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

• bool CVCL::ExprManager::isTypeKind (int kind)

  Check if a kind represents a type.
  

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

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

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

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

• size_t CVCL::ExprManager::registerSubclass (size_t sizeOfSubclass)

  Register a new subclass of ExprValue.
  

• CVCL::ExprManagerNotifyObj::ExprManagerNotifyObj (ExprManager *em, Context *cxt)

  Constructor.
  

• void CVCL::ExprManagerNotifyObj::notifyPre (void)
• void CVCL::ExprManagerNotifyObj::notify (void)
• size_t CVCL::ExprManager::hash (const ExprValue *ev) const
• bool CVCL::ExprManager::EqEV::operator() (const ExprValue *ev1, const ExprValue *ev2) const

---

Function Documentation

size_t CVCL::ExprManager::HashString::operator() (  const std::string &  s  )  const [inline, inherited]

Definition at line 83 of file expr_manager.h. References CVCL::ExprManager::HashString::h.

CVCL::ExprManager::HashEV::HashEV (  ExprManager *  em  )  [inline, inherited]

Definition at line 123 of file expr_manager.h.

size_t CVCL::ExprManager::HashEV::operator() (  ExprValue *  ev  )  const [inline, inherited]

Definition at line 124 of file expr_manager.h. References CVCL::ExprManager::HashEV::d_em, and CVCL::ExprManager::hash().

virtual CVCL::ExprManager::TypeComputer::~TypeComputer (   )  [inline, virtual, inherited]

Definition at line 184 of file expr_manager.h.

virtual void CVCL::ExprManager::TypeComputer::computeType (  const Expr &  e  )  [pure virtual, inherited]

Compute the type of e. Implemented in CVCL::TypeComputerCore. Referenced by CVCL::ExprManager::computeType().

virtual void CVCL::ExprManager::TypeComputer::checkType (  const Expr &  e  )  [pure virtual, inherited]

Check that e is a valid Type expr. Implemented in CVCL::TypeComputerCore. Referenced by CVCL::ExprManager::checkType().

Expr ExprManager::rebuildRec (  const Expr &  e  )  [private, inherited]

Cached recursive descent. Must be called only during rebuild(). Definition at line 215 of file expr_manager.cpp. References CVCL::Expr::d_expr, CVCL::ExprManager::d_exprSet, CVCL::ExprManager::d_rebuildCache, CVCL::ExprValue::d_type, CVCL::MemoryManager::deleteData(), CVCL::ExprHashMap< Data >::end(), CVCL::ExprHashMap< Data >::find(), CVCL::Type::getExpr(), CVCL::ExprManager::getMM(), CVCL::ExprManager::installExprValue(), CVCL::Type::isNull(), CVCL::ExprManager::nextIndex(), CVCL::ExprValue::rebuild(), CVCL::Expr::toString(), and CVCL::ExprManager::Type. Referenced by CVCL::ExprValue::rebuild(), and CVCL::ExprManager::rebuild().

ExprValue * ExprManager::newExprValue (  ExprValue *  ev  )  [private, inherited]

Return either an existing or a new ExprValue matching ev. Definition at line 253 of file expr_manager.cpp. References CVCL::ExprValue::copy(), CVCL::ExprManager::d_exprSet, CVCL::ExprManager::installExprValue(), CVCL::ExprManager::isActive(), and CVCL::ExprManager::nextIndex(). Referenced by CVCL::Expr::Expr(), and CVCL::ExprManager::newExpr().

unsigned CVCL::ExprManager::getFlag (   )  [inline, private, inherited]

Return the current Expr flag counter. Definition at line 208 of file expr_manager.h. References CVCL::ExprManager::d_flagCounter. Referenced by CVCL::Expr::setFlag().

unsigned CVCL::ExprManager::nextFlag (   )  [inline, private, inherited]

Increment and return the Expr flag counter (this clears all the flags). Definition at line 210 of file expr_manager.h. References CVCL::ExprManager::d_flagCounter. Referenced by CVCL::ExprManager::clearFlags().

void ExprManager::computeType (  const Expr &  e  )  [private, inherited]

Compute the type of the Expr. Definition at line 436 of file expr_manager.cpp. References CVCL::ExprManager::TypeComputer::computeType(), CVCL::ExprManager::d_typeComputer, CVCL::Type::getExpr(), CVCL::Expr::getType(), and CVCL::Expr::isNull(). Referenced by CVCL::Expr::getType().

void ExprManager::checkType (  const Expr &  e  )  [private, inherited]

Check well-formedness of a type Expr. Definition at line 443 of file expr_manager.cpp. References CVCL::ExprManager::TypeComputer::checkType(), CVCL::ExprManager::d_typeComputer, and CVCL::Expr::isValidType(). Referenced by CVCL::Type::Type().

ExprManager::ExprManager (  ContextManager *  cm, const CLFlags &  flags )  [inherited]

Constructor. Definition at line 45 of file expr_manager.cpp. References CVCL::BOOLEAN, CVCL::ExprManager::d_bool, CVCL::ExprManager::d_cm, CVCL::ExprManager::d_false, CVCL::ExprManager::d_mm, CVCL::ExprManager::d_mmFlag, CVCL::ExprManager::d_notifyObj, CVCL::ExprManager::d_true, CVCL::EXPR_APPLY, CVCL::EXPR_BOUND_VAR, CVCL::EXPR_CLOSURE, CVCL::EXPR_NODE, CVCL::EXPR_RATIONAL, CVCL::EXPR_SKOLEM, CVCL::EXPR_STRING, CVCL::EXPR_SYMBOL, CVCL::EXPR_UCONST, CVCL::EXPR_VALUE, CVCL::FALSE, CVCL::ContextManager::getCurrentContext(), CVCL::ExprManager::IF_DEBUG(), CVCL::ExprManager::newLeafExpr(), registerKinds(), CVCL::Expr::setType(), CVCL::TRUE, and CVCL::Type::typeBool().

ExprManager::~ExprManager (   )  [inherited]

Destructor. Definition at line 100 of file expr_manager.cpp. References CVCL::ExprManager::clear(), CVCL::ExprManager::d_disableGC, CVCL::ExprManager::d_emptyVec, CVCL::ExprManager::d_mm, and CVCL::ExprManager::d_notifyObj.

void ExprManager::clear (   )  [inherited]

Free up all memory and delete all the expressions. No more expressions can be created after this point, only destructors ~Expr() can be called. This method is needed to dis-entangle the mutual dependency of ExprManager and ContextManager, when destructors of ExprValue (sub)classes need to delete backtracking objects, and deleting the ContextManager requires destruction of some remaining Exprs. Definition at line 116 of file expr_manager.cpp. References CVCL::ExprManager::d_bool, CVCL::ExprManager::d_disableGC, CVCL::ExprManager::d_exprSet, CVCL::ExprManager::d_false, CVCL::ExprManager::d_mm, CVCL::ExprManager::d_nullExpr, CVCL::ExprManager::d_true, CVCL::ExprManager::Expr, CVCL::ExprValue::getMMIndex(), CVCL::ExprManager::IF_DEBUG(), CVCL::ExprManager::isActive(), CVCL::Expr::isNull(), and CVCL::TRACE. Referenced by CVCL::ExprManager::~ExprManager().

bool ExprManager::isActive (   )  [inherited]

Check if the ExprManager is still active (clear() was not called). Definition at line 159 of file expr_manager.cpp. References CVCL::ExprManager::d_disableGC. Referenced by CVCL::ExprManager::clear(), CVCL::ExprManager::installExprValue(), CVCL::ExprManager::newExprValue(), and CVCL::ExprManager::rebuild().

void ExprManager::gc (  ExprValue *  ev  )  [inherited]

Garbage collect the ExprValue pointer. Definition at line 163 of file expr_manager.cpp. References CVCL::ExprManager::d_disableGC, CVCL::ExprManager::d_exprSet, CVCL::ExprManager::d_mm, CVCL::ExprManager::d_postponed, CVCL::ExprManager::d_postponeGC, and CVCL::ExprValue::getMMIndex(). Referenced by CVCL::ExprValue::decRefcount().

void CVCL::ExprManager::postponeGC (   )  [inline, inherited]

Postpone deletion of garbage-collected expressions. See also: resumeGC() Definition at line 241 of file expr_manager.h. References CVCL::ExprManager::d_postponeGC. Referenced by CVCL::ExprManagerNotifyObj::notifyPre().

void ExprManager::resumeGC (   )  [inherited]

Resume deletion of garbage-collected expressions. See also: postponeGC() Definition at line 176 of file expr_manager.cpp. References CVCL::ExprManager::d_mm, CVCL::ExprManager::d_postponed, CVCL::ExprManager::d_postponeGC, and CVCL::ExprValue::getMMIndex(). Referenced by CVCL::ExprManagerNotifyObj::notify().

Expr ExprManager::rebuild (  const Expr &  e  )  [inherited]

Rebuild the Expr with this ExprManager if it belongs to another ExprManager. Definition at line 190 of file expr_manager.cpp. References CVCL::ExprHashMap< Data >::clear(), CVCL::ExprManager::d_rebuildCache, CVCL::Expr::getEM(), CVCL::ExprManager::IF_DEBUG(), CVCL::ExprManager::isActive(), CVCL::Expr::isNull(), CVCL::ExprManager::rebuildRec(), CVCL::ExprHashMap< Data >::size(), and CVCL::TRACE. Referenced by CVCL::VCL::importExpr(), CVCL::VCL::importType(), CVCL::Op::Op(), and CVCL::Expr::rebuild().

ExprIndex CVCL::ExprManager::nextIndex (   )  [inline, inherited]

Return the next Expr index. It should be used only by ExprValue() constructor Definition at line 252 of file expr_manager.h. References CVCL::ExprManager::d_index. Referenced by CVCL::ExprManager::newExprValue(), and CVCL::ExprManager::rebuildRec().

ExprIndex CVCL::ExprManager::lastIndex (   )  [inline, inherited]

Definition at line 253 of file expr_manager.h. References CVCL::ExprManager::d_index. Referenced by CVCL::Expr::hasLastIndex().

void CVCL::ExprManager::clearFlags (   )  [inline, inherited]

Clears the generic Expr flag in all Exprs. Definition at line 256 of file expr_manager.h. References CVCL::ExprManager::nextFlag(). Referenced by CVCL::Expr::clearFlags().

const Expr& CVCL::ExprManager::boolExpr (   )  [inline, inherited]

BOOLEAN Expr. Definition at line 260 of file expr_manager.h. References CVCL::ExprManager::d_bool. Referenced by TheoryCore::parseExprOp(), and CVCL::Type::typeBool().

const Expr& CVCL::ExprManager::falseExpr (   )  [inline, inherited]

FALSE Expr. Definition at line 262 of file expr_manager.h. References CVCL::ExprManager::d_false. Referenced by CVCL::CoreTheoremProducer::AndToIte(), CVCL::TheorySimulate::computeTCC(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::VCL::falseExpr(), CVCL::Theory::falseExpr(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CommonTheoremProducer::iffNotFalse(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::CommonTheoremProducer::notToIff(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::CoreTheoremProducer::OrToIte(), TheoryCore::parseExprOp(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CommonTheoremProducer::rewriteIff(), CVCL::CoreTheoremProducer::rewriteIteCond(), CVCL::CommonTheoremProducer::rewriteNotTrue(), CVCL::CommonTheoremProducer::rewriteOr(), and CVCL::CoreTheoremProducer::rewriteOrSubterms().

const Expr& CVCL::ExprManager::trueExpr (   )  [inline, inherited]

TRUE Expr. Definition at line 264 of file expr_manager.h. References CVCL::ExprManager::d_true. Referenced by CVCL::CoreTheoremProducer::AndToIte(), TheoryCore::computeModelBasic(), CVCL::TheorySimulate::computeTCC(), TheoryCore::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::Theory::computeTypePred(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CommonTheoremProducer::iffTrue(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::CoreTheoremProducer::OrToIte(), TheoryCore::parseExprOp(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), CVCL::CoreTheoremProducer::rewriteIteCond(), CVCL::CommonTheoremProducer::rewriteNotFalse(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::CommonTheoremProducer::rewriteReflexivity(), CVCL::VCL::trueExpr(), CVCL::Theory::trueExpr(), and CVCL::CommonTheoremProducer::trueTheorem().

const std::vector<Expr>& CVCL::ExprManager::getEmptyVector (   )  [inline, inherited]

References to empty objects (used in ExprValue). Definition at line 266 of file expr_manager.h. References CVCL::ExprManager::d_emptyVec. Referenced by CVCL::ExprValue::getKids(), and CVCL::Expr::getKids().

const Expr& CVCL::ExprManager::getNullExpr (   )  [inline, inherited]

References to empty objects (used in ExprValue). Definition at line 268 of file expr_manager.h. References CVCL::ExprManager::d_nullExpr.

Expr CVCL::ExprManager::newExpr (  ExprValue *  ev  )  [inline, inherited]

Return either an existing or a new Expr matching ev. Definition at line 273 of file expr_manager.h. References CVCL::ExprManager::Expr, and CVCL::ExprManager::newExprValue(). Referenced by CVCL::ExprManager::newBoundVarExpr(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::ExprManager::newClosureExpr(), CVCL::ExprManager::newLeafExpr(), CVCL::ExprManager::newRatExpr(), CVCL::ExprManager::newSkolemExpr(), CVCL::ExprManager::newStringExpr(), CVCL::ExprManager::newSymbolExpr(), and CVCL::ExprManager::newVarExpr().

Expr CVCL::ExprManager::newLeafExpr (  const Op &  op  )  [inline, inherited]

Definition at line 417 of file expr_manager.h. References CVCL::Expr::getEM(), CVCL::Op::getExpr(), CVCL::Op::getKind(), CVCL::Expr::isNull(), and CVCL::ExprManager::newExpr(). Referenced by CVCL::ExprStream::addLetHeader(), CVCL::VCL::checkContinue(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::ExprManager::ExprManager(), CVCL::VCL::getClosure(), CVCL::VCL::getConcreteModel(), CVCL::VCL::getProof(), CVCL::VCL::getProofClosure(), CVCL::VCL::getProofTCC(), CVCL::VCL::getTCC(), TheoryCore::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::VCL::pop(), CVCL::VCL::popScope(), CVCL::VCL::push(), CVCL::VCL::pushScope(), and CVCL::TheoremProducer::TheoremProducer().

Expr CVCL::ExprManager::newStringExpr (  const std::string &  s  )  [inline, inherited]

Definition at line 431 of file expr_manager.h. References CVCL::ExprManager::newExpr().

Expr CVCL::ExprManager::newRatExpr (  const Rational &  r  )  [inline, inherited]

Definition at line 434 of file expr_manager.h. References CVCL::ExprManager::newExpr(). Referenced by CVCL::CommonTheoremProducer::andElim(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::TheoryBitvector::rat(), CVCL::TheoryArith::rat(), CVCL::BitvectorTheoremProducer::rat(), CVCL::ArithTheoremProducer::rat(), CVCL::VCL::ratExpr(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), and CVCL::CoreTheoremProducer::rewriteOrSubterms().

Expr CVCL::ExprManager::newSkolemExpr (  const Expr &  e, int  i )  [inline, inherited]

Definition at line 437 of file expr_manager.h. References CVCL::Expr::getEM(), and CVCL::ExprManager::newExpr(). Referenced by CVCL::Expr::skolemExpr().

Expr CVCL::ExprManager::newVarExpr (  const std::string &  s  )  [inline, inherited]

Definition at line 441 of file expr_manager.h. References CVCL::ExprManager::newExpr(). Referenced by CVCL::ExprStream::addLetHeader().

Expr CVCL::ExprManager::newSymbolExpr (  const std::string &  s, int  kind )  [inline, inherited]

Definition at line 444 of file expr_manager.h. References CVCL::ExprManager::newExpr().

Expr CVCL::ExprManager::newBoundVarExpr (  const std::string &  name, const std::string &  uid )  [inline, inherited]

Definition at line 447 of file expr_manager.h. References CVCL::ExprManager::newExpr(). Referenced by CVCL::TheoryUF::computeModel(), CVCL::ExprManager::newBoundVarExpr(), CVCL::TheoremProducer::newLabel(), and CVCL::CommonTheoremProducer::varIntroRule().

Expr CVCL::ExprManager::newBoundVarExpr (  const std::string &  name, const std::string &  uid, const Type &  type )  [inline, inherited]

Definition at line 451 of file expr_manager.h. References CVCL::ARROW, CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::Type::isNull(), CVCL::Expr::lookupType(), CVCL::ExprManager::newBoundVarExpr(), and CVCL::Expr::setType().

Expr CVCL::ExprManager::newBoundVarExpr (  const Type &  type  )  [inline, inherited]

Definition at line 462 of file expr_manager.h. References CVCL::int2string(), and CVCL::ExprManager::newBoundVarExpr().

Expr CVCL::ExprManager::newClosureExpr (  int  kind, const std::vector< Expr > &  vars, const Expr &  body )  [inline, inherited]

Definition at line 469 of file expr_manager.h. References CVCL::ExprManager::newExpr(). Referenced by CVCL::arrayLiteral(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::TheoryQuant::computeTCC(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::TheoremProducer::newPf(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::Expr::recursiveSubst(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::QuantTheoremProducer::rewriteNotForall(), CVCL::CommonTheoremProducer::rewriteNotForall(), and CVCL::CommonTheoremProducer::varIntroRule().

Expr CVCL::ExprManager::andExpr (  const std::vector< Expr > &  children  )  [inline, inherited]

Definition at line 289 of file expr_manager.h. References CVCL::AND, and CVCL::ExprManager::Expr.

Expr CVCL::ExprManager::orExpr (  const std::vector< Expr > &  children  )  [inline, inherited]

Definition at line 291 of file expr_manager.h. References CVCL::ExprManager::Expr, and CVCL::OR.

size_t CVCL::ExprManager::hash (  const Expr &  e  )  const [inline, inherited]

Hash function for a single Expr. Definition at line 484 of file expr_manager.h. References CVCL::Expr::d_expr, CVCL::ExprValue::hash(), and CVCL::Expr::isNull().

ContextManager* CVCL::ExprManager::getCM (   )  const [inline, inherited]

Fetch our ContextManager. Definition at line 299 of file expr_manager.h. References CVCL::ExprManager::d_cm.

Context* CVCL::ExprManager::getCurrentContext (   )  const [inline, inherited]

Get the current context from our ContextManager. Definition at line 301 of file expr_manager.h. References CVCL::ExprManager::d_cm, and CVCL::ContextManager::getCurrentContext(). Referenced by CVCL::Expr::setFind(), CVCL::Expr::setRep(), and CVCL::Expr::setSig().

int CVCL::ExprManager::scopelevel (   )  [inline, inherited]

Get current scope level. Definition at line 303 of file expr_manager.h. References CVCL::ExprManager::d_cm, and CVCL::ContextManager::scopeLevel().

MemoryManager* CVCL::ExprManager::getMM (  size_t  MMIndex  )  [inline, inherited]

Return a MemoryManager for the given ExprValue type. Definition at line 306 of file expr_manager.h. References CVCL::ExprManager::d_mm. Referenced by CVCL::ExprClosure::copy(), CVCL::ExprApply::copy(), CVCL::ExprBoundVar::copy(), CVCL::ExprSymbol::copy(), CVCL::ExprVar::copy(), CVCL::ExprRational::copy(), CVCL::ExprSkolem::copy(), CVCL::ExprString::copy(), CVCL::ExprNode::copy(), CVCL::ExprValue::copy(), CVCL::BVConstExpr::copy(), CVCL::ExprValue::getMM(), and CVCL::ExprManager::rebuildRec().

unsigned CVCL::ExprManager::getSimpCacheTag (   )  const [inline, inherited]

Get the simplifier's cache tag. Definition at line 311 of file expr_manager.h. References CVCL::ExprManager::d_simpCacheTagCurrent. Referenced by CVCL::Expr::setSimpCache(), and CVCL::Expr::validSimpCache().

void CVCL::ExprManager::invalidateSimpCache (   )  [inline, inherited]

Invalidate the simplifier's cache tag. Definition at line 313 of file expr_manager.h. References CVCL::ExprManager::d_simpCacheTagCurrent. Referenced by TheoryCore::assertEqualities(), TheoryCore::assertFormula(), CVCL::TheoryCore::CoreNotifyObj::notify(), and TheoryCore::simplify().

void CVCL::ExprManager::registerTypeComputer (  TypeComputer *  typeComputer  )  [inline, inherited]

Register type computer. Definition at line 316 of file expr_manager.h. References CVCL::ExprManager::d_typeComputer.

int CVCL::ExprManager::printDepth (   )  const [inline, inherited]

Get printing depth. Definition at line 320 of file expr_manager.h. References CVCL::ExprManager::d_printDepth.

bool CVCL::ExprManager::withIndentation (   )  const [inline, inherited]

Whether to print with indentation. Definition at line 322 of file expr_manager.h. References CVCL::ExprManager::d_withIndentation.

int CVCL::ExprManager::lineWidth (   )  const [inline, inherited]

Suggested line width for printing with indentation. Definition at line 324 of file expr_manager.h. References CVCL::ExprManager::d_lineWidth.

int CVCL::ExprManager::indent (   )  const [inline, inherited]

Get initial indentation. Definition at line 326 of file expr_manager.h. References CVCL::ExprManager::d_indentTransient. Referenced by CVCL::ExprStream::ExprStream(), and CVCL::Expr::indent().

int ExprManager::indent (  int  n, bool  permanent = false )  [inherited]

Set initial indentation. Returns the previous permanent value. Definition at line 331 of file expr_manager.cpp. References CVCL::ExprManager::d_indent, and CVCL::ExprManager::d_indentTransient.

int ExprManager::incIndent (  int  n, bool  permanent = false )  [inherited]

Increment the current transient indentation by n. If the second argument is true, sets the result as permanent. Returns: previous permanent value. Definition at line 342 of file expr_manager.cpp. References CVCL::ExprManager::d_indent, and CVCL::ExprManager::d_indentTransient.

void CVCL::ExprManager::restoreIndent (   )  [inline, inherited]

Set transient indentation to permanent. Definition at line 334 of file expr_manager.h. References CVCL::ExprManager::d_indent, and CVCL::ExprManager::d_indentTransient. Referenced by CVCL::operator<<().

InputLanguage ExprManager::getInputLang (   )  const [inherited]

Get the input language for printing. Definition at line 351 of file expr_manager.cpp. References CVCL::ExprManager::d_inputLang, and CVCL::getLanguage(). Referenced by main().

InputLanguage ExprManager::getOutputLang (   )  const [inherited]

Get the output language for printing. Definition at line 359 of file expr_manager.cpp. References CVCL::ExprManager::d_inputLang, CVCL::ExprManager::d_outputLang, and CVCL::getLanguage(). Referenced by CVCL::VCL::assertFormula(), main(), and CVCL::VCL::query().

bool CVCL::ExprManager::dagPrinting (   )  const [inline, inherited]

Whether to print Expr's as DAGs. Definition at line 340 of file expr_manager.h. References CVCL::ExprManager::d_dagPrinting.

PrettyPrinter* CVCL::ExprManager::getPrinter (   )  const [inline, inherited]

Return the pretty-printer if there is one; otherwise return NULL. Definition at line 343 of file expr_manager.h. References CVCL::ExprManager::d_prettyPrinter. Referenced by CVCL::operator<<().

void CVCL::ExprManager::newKind (  int  kind, const std::string &  name, bool  isType = false )  [inherited]

Register a new kind. The kind may already be regestered under the same name, but if the name is different, it's an error. If the new kind is supposed to represent a type, set isType to true. Referenced by CVCL::TheoremManager::TheoremManager(), CVCL::TheoryArith::TheoryArith(), CVCL::TheoryArray::TheoryArray(), CVCL::TheoryBitvector::TheoryBitvector(), CVCL::TheoryDatatype::TheoryDatatype(), CVCL::TheoryRecords::TheoryRecords(), and CVCL::TheoryUF::TheoryUF().

void ExprManager::registerPrettyPrinter (  PrettyPrinter &  printer  )  [inherited]

Register the pretty-printer (can only do it if none registered). The pointer is NOT owned by ExprManager. Delete it yourself. Definition at line 394 of file expr_manager.cpp. References CVCL::ExprManager::d_prettyPrinter.

void ExprManager::unregisterPrettyPrinter (   )  [inherited]

Tell ExprManager that the printer is no longer valid. Definition at line 401 of file expr_manager.cpp. References CVCL::ExprManager::d_prettyPrinter. Referenced by TheoryCore::~TheoryCore().

bool CVCL::ExprManager::isKindRegistered (  int  kind  )  [inline, inherited]

Returns true if kind is built into CVC or has been registered via newKind. Definition at line 364 of file expr_manager.h. References CVCL::ExprManager::d_kindMap. Referenced by CVCL::ExprValue::ExprValue().

bool CVCL::ExprManager::isTypeKind (  int  kind  )  [inline, inherited]

Check if a kind represents a type. Definition at line 366 of file expr_manager.h. References CVCL::ExprManager::d_typeKinds. Referenced by CVCL::Expr::isType().

const string & ExprManager::getKindName (  int  kind  )  [inherited]

Return the name associated with a kind. The kind must already be registered. Definition at line 408 of file expr_manager.cpp. References CVCL::ExprManager::d_kindMap, and CVCL::int2string(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::TypeComputerCore::computeType(), CVCL::Expr::print(), CVCL::Expr::printAST(), and CVCL::Theory::theoryOf().

int CVCL::ExprManager::getKind (  const std::string &  name  )  [inherited]

Return a kind associated with a name. Returns NULL_KIND if not found. Referenced by TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryDatatype::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), and CVCL::TheoryArith::parseExprOp().

size_t ExprManager::registerSubclass (  size_t  sizeOfSubclass  )  [inherited]

Register a new subclass of ExprValue. Takes the size (in bytes) of the new subclass and returns the unique index of that subclass. Subsequent calls to the subclass's getMMIndex() must return that index. Definition at line 424 of file expr_manager.cpp. References CVCL::ExprManager::d_mm, and CVCL::ExprManager::d_mmFlag. Referenced by CVCL::TheoryBitvector::TheoryBitvector().

CVCL::ExprManagerNotifyObj::ExprManagerNotifyObj (  ExprManager *  em, Context *  cxt )  [inline, inherited]

Constructor. Definition at line 402 of file expr_manager.h.

void ExprManagerNotifyObj::notifyPre (  void   )  [virtual, inherited]

Reimplemented from CVCL::ContextNotifyObj. Definition at line 614 of file expr_manager.cpp. References CVCL::ExprManagerNotifyObj::d_em, and CVCL::ExprManager::postponeGC().

void ExprManagerNotifyObj::notify (  void   )  [virtual, inherited]

Reimplemented from CVCL::ContextNotifyObj. Definition at line 619 of file expr_manager.cpp. References CVCL::ExprManagerNotifyObj::d_em, and CVCL::ExprManager::resumeGC().

size_t CVCL::ExprManager::hash (  const ExprValue *  ev  )  const [inline, private, inherited]

Definition at line 474 of file expr_manager.h. References CVCL::ExprValue::hash(). Referenced by CVCL::Expr::hash(), hf(), and CVCL::ExprManager::HashEV::operator()().

bool CVCL::ExprManager::EqEV::operator() (  const ExprValue *  ev1, const ExprValue *  ev2 )  const [inline, inherited]

Definition at line 479 of file expr_manager.h.

---