CVC3::ContextManager Class Reference
[Context Management]
Manager for multiple contexts. Also holds current context.
More...
#include <context.h>
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 (int verbosity)
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 393 of file context.h.
Constructor & Destructor Documentation
| ContextManager::ContextManager | ( | ) |
| ContextManager::~ContextManager | ( | ) |
Member Function Documentation
| void CVC3::ContextManager::push | ( | ) | [inline] |
Definition at line 401 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::init(), CVC3::ExprTransform::newPPrec(), CVC3::VCL::poptoScope(), CVC3::SearchSatTheoryAPI::push(), CVC3::SearchImplBase::push(), CVC3::DecisionEngine::pushDecision(), and CVC3::VCL::pushScope().
| void CVC3::ContextManager::pop | ( | ) | [inline] |
Definition at line 402 of file context.h.
References d_curContext, and CVC3::Context::pop().
Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::ExprTransform::newPPrec(), CVC3::SearchSatTheoryAPI::pop(), CVC3::SearchImplBase::pop(), CVC3::DecisionEngine::popDecision(), and CVC3::VCL::popScope().
| void CVC3::ContextManager::popto | ( | int | toLevel | ) | [inline] |
Definition at line 403 of file context.h.
References d_curContext, and CVC3::Context::popto().
Referenced by CVC3::CoreSatAPI_implBase::check(), CVC3::SearchEngineFast::checkValidMain(), CVC3::VCL::destroy(), CVC3::DecisionEngine::popTo(), CVC3::VCL::poptoScope(), CVC3::SearchSimple::restartInternal(), and CVC3::SearchEngineFast::restartInternal().
| int CVC3::ContextManager::scopeLevel | ( | ) | [inline] |
Definition at line 404 of file context.h.
References d_curContext, and CVC3::Context::level().
Referenced by CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), CVC3::CoreSatAPI_implBase::check(), CVC3::RWTheoremValue::init(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::popTo(), CVC3::SearchSat::recordNewRootLit(), CVC3::RegTheoremValue::RegTheoremValue(), CVC3::SearchSat::restorePre(), CVC3::VCL::scopeLevel(), CVC3::SearchImplBase::scopeLevel(), and CVC3::VCL::tryModelGeneration().
| Context * ContextManager::createContext | ( | const std::string & | name = "" |
) |
| Context* CVC3::ContextManager::getCurrentContext | ( | ) | [inline] |
Definition at line 406 of file context.h.
References d_curContext.
Referenced by CVC3::TheoryQuant::add_parent(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryUF::assertFact(), CVC3::TheoryQuant::checkSat(), SAT::DPLLTBasic::checkSat(), CVC3::TheoryQuant::combineOldNewTrigs(), SAT::DPLLTBasic::DPLLTBasic(), CVC3::TheoryQuant::enqueueInst(), CVC3::ExprManager::ExprManager(), CVC3::VCL::getCurrentContext(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdge(), CVC3::VCL::init(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryQuant::pushBackList(), CVC3::TheoryQuant::pushForwList(), CVC3::TheoryQuant::recursiveMap(), CVC3::VariableValue::setAssumpThm(), CVC3::VariableValue::setValue(), CVC3::TheoryQuant::synCheckSat(), CVC3::TheoryQuant::synNewInst(), and CVC3::VariableManager::VariableManager().
Definition at line 352 of file context.cpp.
References d_contexts, d_curContext, DebugAssert, FatalAssert, and CVC3::Context::id().
| unsigned long ContextManager::getMemory | ( | int | verbosity | ) |
Definition at line 364 of file context.cpp.
References d_contexts, CVC3::ContextMemoryManager::getStaticMemory(), and CVC3::MemoryTracker::print().
Referenced by CVC3::VCL::getMemory().
Member Data Documentation
Context* CVC3::ContextManager::d_curContext [private] |
Definition at line 394 of file context.h.
Referenced by ContextManager(), getCurrentContext(), pop(), popto(), push(), scopeLevel(), and switchContext().
std::vector<Context*> CVC3::ContextManager::d_contexts [private] |
Definition at line 395 of file context.h.
Referenced by createContext(), getMemory(), switchContext(), and ~ContextManager().
The documentation for this class was generated from the following files:
