CVC3::ContextManager Class Reference
[Context Management]

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

#include <context.h>

Collaboration diagram for CVC3::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)
• unsigned long getMemory ()

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 389 of file context.h.

---

Constructor & Destructor Documentation

ContextManager::ContextManager

(

)

Definition at line 314 of file context.cpp.

References createContext(), and d_curContext.

ContextManager::~ContextManager

(

)

Definition at line 320 of file context.cpp.

References d_contexts.

---

Member Function Documentation

void CVC3::ContextManager::push

(

)

[inline]

Definition at line 397 of file context.h.

References d_curContext, and CVC3::Context::push().

Referenced by CVC3::CoreSatAPI_implBase::check(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::VCL::poptoScope(), CVC3::SearchSatTheoryAPI::push(), CVC3::SearchImplBase::push(), CVC3::DecisionEngine::pushDecision(), and CVC3::VCL::pushScope().

void CVC3::ContextManager::pop

(

)

[inline]

Definition at line 398 of file context.h.

References d_curContext, and CVC3::Context::pop().

Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSatTheoryAPI::pop(), CVC3::SearchImplBase::pop(), CVC3::DecisionEngine::popDecision(), and CVC3::VCL::popScope().

void CVC3::ContextManager::popto

(

int

toLevel

)

[inline]

Definition at line 399 of file context.h.

References d_curContext, and CVC3::Context::popto().

Referenced by CVC3::CoreSatAPI_implBase::check(), CVC3::SearchEngineFast::checkValidMain(), CVC3::DecisionEngine::popTo(), CVC3::VCL::poptoScope(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), and CVC3::VCL::~VCL().

int CVC3::ContextManager::scopeLevel

(

)

[inline]

Definition at line 400 of file context.h.

References d_curContext, and CVC3::Context::level().

Referenced by CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), CVC3::CoreSatAPI_implBase::check(), CVC3::TheoryCore::enqueueFact(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::DecisionEngineMBTF::goalSatisfied(), CVC3::DecisionEngineCaching::goalSatisfied(), CVC3::RWTheoremValue::init(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::popTo(), CVC3::SearchSat::recordNewRootLit(), CVC3::RegTheoremValue::RegTheoremValue(), CVC3::SearchSat::restorePre(), CVC3::VCL::scopeLevel(), and CVC3::SearchImplBase::scopeLevel().

Context * ContextManager::createContext

(

const std::string &

name = ""

)

Definition at line 329 of file context.cpp.

References d_contexts.

Referenced by ContextManager().

Context* CVC3::ContextManager::getCurrentContext

(

)

[inline]

Definition at line 402 of file context.h.

References d_curContext.

Referenced by CVC3::TheoryQuant::add_parent(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryUF::assertFact(), SAT::DPLLTBasic::checkSat(), CVC3::TheoryQuant::combineOldNewTrigs(), SAT::DPLLTBasic::DPLLTBasic(), CVC3::ExprManager::ExprManager(), CVC3::VCL::getCurrentContext(), CVC3::TheoryQuant::hasGoodSynMultiInst(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::recursiveMap(), CVC3::VariableValue::setAssumpThm(), CVC3::VariableValue::setValue(), CVC3::TheoryQuant::synNewInst(), and CVC3::VariableManager::VariableManager().

Context * ContextManager::switchContext

(

Context *

context

)

Definition at line 336 of file context.cpp.

References d_contexts, d_curContext, DebugAssert, FatalAssert, and CVC3::Context::id().

unsigned long ContextManager::getMemory

(

)

Definition at line 348 of file context.cpp.

References d_curContext, and CVC3::Context::getMemory().

Referenced by CVC3::VCL::printMemory().

---

Member Data Documentation

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

Definition at line 390 of file context.h.

Referenced by ContextManager(), getCurrentContext(), getMemory(), pop(), popto(), push(), scopeLevel(), and switchContext().

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

Definition at line 391 of file context.h.

Referenced by createContext(), switchContext(), and ~ContextManager().

---

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

• context.h
• context.cpp

---