diff options
Diffstat (limited to 'src/smt/smt_engine_scope.h')
-rw-r--r-- | src/smt/smt_engine_scope.h | 65 |
1 files changed, 16 insertions, 49 deletions
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index a3f716238..fda4d5e10 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -17,76 +17,43 @@ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__SMT__SMT_ENGINE_SCOPE_H +#define __CVC4__SMT__SMT_ENGINE_SCOPE_H -#include "base/configuration_private.h" -#include "base/cvc4_assert.h" -#include "base/output.h" -#include "base/tls.h" #include "expr/node_manager.h" -#include "proof/proof.h" -#include "proof/proof_manager.h" -#include "options/smt_options.h" -#include "smt/smt_engine.h" - namespace CVC4 { class ProofManager; +class SmtEngine; +class StatisticsRegistry; namespace smt { -extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; - -inline SmtEngine* currentSmtEngine() { - Assert(s_smtEngine_current != NULL); - return s_smtEngine_current; -} -inline bool smtEngineInScope() { - return s_smtEngine_current != NULL; -} +SmtEngine* currentSmtEngine(); +bool smtEngineInScope(); // FIXME: Maybe move into SmtScope? -inline ProofManager* currentProofManager() { -#if IS_PROOFS_BUILD - Assert(s_smtEngine_current != NULL); - return s_smtEngine_current->d_proofManager; -#else /* IS_PROOFS_BUILD */ - InternalError("proofs/unsat cores are not on, but ProofManager requested"); - return NULL; -#endif /* IS_PROOFS_BUILD */ -} +ProofManager* currentProofManager(); class SmtScope : public NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ SmtEngine* d_oldSmtEngine; public: + SmtScope(const SmtEngine* smt); + ~SmtScope(); - SmtScope(const SmtEngine* smt) : - NodeManagerScope(smt->d_nodeManager), - d_oldSmtEngine(s_smtEngine_current) { - Assert(smt != NULL); - s_smtEngine_current = const_cast<SmtEngine*>(smt); - Debug("current") << "smt scope: " << s_smtEngine_current << std::endl; - } - - ~SmtScope() { - s_smtEngine_current = d_oldSmtEngine; - Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl; - } - - /** - * This returns the StatisticsRegistry attached to the currently in scope - * SmtEngine. - */ - static StatisticsRegistry* currentStatisticsRegistry() { - Assert(smtEngineInScope()); - return s_smtEngine_current->d_statisticsRegistry; - } + /** + * This returns the StatisticsRegistry attached to the currently in scope + * SmtEngine. + */ + static StatisticsRegistry* currentStatisticsRegistry(); };/* class SmtScope */ }/* CVC4::smt namespace */ }/* CVC4 namespace */ + +#endif /* __CVC4__SMT__SMT_ENGINE_SCOPE_H */ |