From 7b8531e83dd4c95a5b0eaa4927da5228c6942b7c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 14 Aug 2017 15:32:23 -0700 Subject: [PATCH] Move function defns from smt_engine_scope.h to cpp (#216) Additionally, this commit removes unnecessary includes, adds includes to smt_engine.h in files that require it and removes s_smtEngine_current from smt_engine_scope.h. --- src/smt/model.cpp | 1 + src/smt/smt_engine_scope.cpp | 44 ++++++++++++- src/smt/smt_engine_scope.h | 65 +++++-------------- src/theory/quantifiers/macros.cpp | 1 + .../quantifiers/term_database_sygus.cpp | 3 +- 5 files changed, 63 insertions(+), 51 deletions(-) diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 7bfe307c3..892e8d888 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -21,6 +21,7 @@ #include "printer/printer.h" #include "smt/command.h" #include "smt/command_list.h" +#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" using namespace std; diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 87823775a..6c360cdc9 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -15,13 +15,55 @@ ** \todo document this file **/ -#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "base/configuration_private.h" +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "base/tls.h" +#include "proof/proof.h" +#include "smt/smt_engine.h" + namespace CVC4 { namespace smt { CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL; +SmtEngine* currentSmtEngine() { + Assert(s_smtEngine_current != NULL); + return s_smtEngine_current; +} + +bool smtEngineInScope() { return s_smtEngine_current != NULL; } + +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 */ +} + +SmtScope::SmtScope(const SmtEngine* smt) + : NodeManagerScope(smt->d_nodeManager), + d_oldSmtEngine(s_smtEngine_current) { + Assert(smt != NULL); + s_smtEngine_current = const_cast(smt); + Debug("current") << "smt scope: " << s_smtEngine_current << std::endl; +} + +SmtScope::~SmtScope() { + s_smtEngine_current = d_oldSmtEngine; + Debug("current") << "smt scope: returning to " << s_smtEngine_current + << std::endl; +} + +StatisticsRegistry* SmtScope::currentStatisticsRegistry() { + Assert(smtEngineInScope()); + return s_smtEngine_current->d_statisticsRegistry; +} + }/* CVC4::smt namespace */ }/* CVC4 namespace */ 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(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 */ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 6b071f8f7..a9fad80ae 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -21,6 +21,7 @@ #include "options/quantifiers_modes.h" #include "options/quantifiers_options.h" #include "proof/proof_manager.h" +#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 62ba32d1e..0a48b8834 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -16,8 +16,9 @@ #include "expr/datatype.h" #include "options/base_options.h" -#include "options/quantifiers_options.h" #include "options/datatypes_options.h" +#include "options/quantifiers_options.h" +#include "smt/smt_engine.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" -- 2.30.2