CVC3
|
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 |
Manager for multiple contexts. Also holds current context.
Author: Clark Barrett
Created: Thu Feb 13 00:26:29 2003
ContextManager::ContextManager | ( | ) |
Definition at line 330 of file context.cpp.
ContextManager::~ContextManager | ( | ) |
Definition at line 336 of file context.cpp.
|
inline |
Definition at line 401 of file context.h.
Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::ExprTransform::newPPrec(), CVC3::SearchImplBase::push(), and CVC3::DecisionEngine::pushDecision().
|
inline |
Definition at line 402 of file context.h.
Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::ExprTransform::newPPrec(), CVC3::SearchImplBase::pop(), and CVC3::DecisionEngine::popDecision().
|
inline |
Definition at line 403 of file context.h.
Referenced by CVC3::SearchEngineFast::checkValidMain(), CVC3::DecisionEngine::popTo(), CVC3::SearchSimple::restartInternal(), and CVC3::SearchEngineFast::restartInternal().
|
inline |
Definition at line 404 of file context.h.
Referenced by CVC3::RWTheoremValue::init(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::popTo(), CVC3::RegTheoremValue::RegTheoremValue(), and CVC3::SearchImplBase::scopeLevel().
Context * ContextManager::createContext | ( | const std::string & | name = "" | ) |
Definition at line 345 of file context.cpp.
References CVC3::Context::Context().
|
inline |
Definition at line 406 of file context.h.
Referenced by CVC3::TheoryQuant::add_parent(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryUF::assertFact(), SAT::DPLLTBasic::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::combineOldNewTrigs(), SAT::DPLLTBasic::DPLLTBasic(), CVC3::TheoryQuant::enqueueInst(), CVC3::ExprManager::ExprManager(), CVC3::TheoryQuant::mapTermsByType(), 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 DebugAssert, FatalAssert, and CVC3::Context::id().
unsigned long ContextManager::getMemory | ( | int | verbosity | ) |
Definition at line 364 of file context.cpp.
References CVC3::ContextMemoryManager::getStaticMemory(), and CVC3::MemoryTracker::print().
|
private |