CVCL::ContextManager Class Reference
[Context Management]

Manager for multiple contexts. Also holds current context. More...

#include <context.h>

Collaboration diagram for CVCL::ContextManager:

[legend]List of all members.

Public Member Functions

• ContextManager ()
• ~ContextManager ()
• void push ()
• void pop ()
• void popto (int toLevel)
• int scopeLevel ()
• Context * createContext (const std::string &name="")
• Context * getCurrentContext ()
• Context * switchContext (Context *context)

Private Attributes

• Context * d_curContext
• std::vector< Context * > d_contexts

---

Detailed Description

Manager for multiple contexts. Also holds current context.

Author: Clark Barrett

Created: Thu Feb 13 00:26:29 2003

Definition at line 292 of file context.h.

---

Constructor & Destructor Documentation

ContextManager::ContextManager (   )

Definition at line 363 of file context.cpp. References createContext(), and d_curContext.

ContextManager::~ContextManager (   )

Definition at line 369 of file context.cpp. References d_contexts.

---

Member Function Documentation

void CVCL::ContextManager::push (   )  [inline]

Definition at line 300 of file context.h. References d_curContext, and CVCL::Context::push(). Referenced by CVCL::VCL::assertFormula(), CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngine::getConcreteModel(), CVCL::VCL::poptoScope(), CVCL::VCL::push(), CVCL::SearchSatTheoryAPI::push(), CVCL::DecisionEngine::pushDecision(), CVCL::VCL::pushScope(), CVCL::VCL::query(), CVCL::VCL::simplifyThm(), and CVCL::VCL::subtypeType().

void CVCL::ContextManager::pop (   )  [inline]

Definition at line 301 of file context.h. References d_curContext, and CVCL::Context::pop(). Referenced by CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchSatTheoryAPI::pop(), CVCL::DecisionEngine::popDecision(), CVCL::VCL::popScope(), and CVCL::SearchSat::returnFromCheck().

void CVCL::ContextManager::popto (  int  toLevel  )  [inline]

Definition at line 302 of file context.h. References d_curContext, and CVCL::Context::popto(). Referenced by CVCL::VCL::assertFormula(), CVCL::SearchSat::check(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngine::getConcreteModel(), CVCL::VCL::pop(), CVCL::VCL::popto(), CVCL::DecisionEngine::popTo(), CVCL::VCL::poptoScope(), CVCL::VCL::query(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::SearchSat::returnFromCheck(), CVCL::VCL::simplifyThm(), and CVCL::VCL::subtypeType().

int CVCL::ContextManager::scopeLevel (   )  [inline]

Definition at line 303 of file context.h. References d_curContext, and CVCL::Context::level(). Referenced by CVCL::SearchSat::check(), TheoryCore::enqueueEquality(), TheoryCore::enqueueFact(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::SearchEngine::getConcreteModel(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::SearchSat::newUserAssumption(), CVCL::VCL::scopeLevel(), CVCL::SearchImplBase::scopeLevel(), CVCL::ExprManager::scopelevel(), CVCL::TheoryQuant::semCheckSat(), CVCL::TheoryQuant::synCheckSat(), and CVCL::TheoremValue::TheoremValue().

Context* CVCL::ContextManager::createContext (  const std::string &  name = ""  )

Referenced by ContextManager().

Context* CVCL::ContextManager::getCurrentContext (   )  [inline]

Definition at line 305 of file context.h. References d_curContext. Referenced by CVCL::SearchSat::addLemma(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryUF::assertFact(), CVCL::SearchSat::check(), CVCL::ExprManager::ExprManager(), CVCL::VCL::getCurrentContext(), CVCL::ExprManager::getCurrentContext(), CVCL::TheoryQuant::mapTermsByType(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryQuant::recursiveMap(), CVCL::VariableValue::setAssumpThm(), and CVCL::VariableValue::setValue().

Context * ContextManager::switchContext (  Context *  context  )

Definition at line 385 of file context.cpp. References d_contexts, d_curContext, and CVCL::Context::id().

---

Member Data Documentation

Context* CVCL::ContextManager::d_curContext [private]

Definition at line 293 of file context.h. Referenced by ContextManager(), getCurrentContext(), pop(), popto(), push(), scopeLevel(), and switchContext().

std::vector<Context*> CVCL::ContextManager::d_contexts [private]

Definition at line 294 of file context.h. Referenced by switchContext(), and ~ContextManager().

---

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

• context.h
• context.cpp

---