1 /********************* */ 2 /*! \file smt_engine_scope.cpp 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Andres Noetzli, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief [[ Add one-line brief description here ]] 13 ** 14 ** [[ Add lengthier description here ]] 15 ** \todo document this file 16 **/ 17 18 #include "smt/smt_engine_scope.h" 19 20 #include "base/configuration_private.h" 21 #include "base/cvc4_assert.h" 22 #include "base/output.h" 23 #include "proof/proof.h" 24 #include "smt/smt_engine.h" 25 26 namespace CVC4 { 27 namespace smt { 28 29 thread_local SmtEngine* s_smtEngine_current = NULL; 30 currentSmtEngine()31SmtEngine* currentSmtEngine() { 32 Assert(s_smtEngine_current != NULL); 33 return s_smtEngine_current; 34 } 35 smtEngineInScope()36bool smtEngineInScope() { return s_smtEngine_current != NULL; } 37 currentProofManager()38ProofManager* currentProofManager() { 39 #if IS_PROOFS_BUILD 40 Assert(s_smtEngine_current != NULL); 41 return s_smtEngine_current->d_proofManager; 42 #else /* IS_PROOFS_BUILD */ 43 InternalError("proofs/unsat cores are not on, but ProofManager requested"); 44 return NULL; 45 #endif /* IS_PROOFS_BUILD */ 46 } 47 SmtScope(const SmtEngine * smt)48SmtScope::SmtScope(const SmtEngine* smt) 49 : NodeManagerScope(smt->d_nodeManager), 50 d_oldSmtEngine(s_smtEngine_current) { 51 Assert(smt != NULL); 52 s_smtEngine_current = const_cast<SmtEngine*>(smt); 53 Debug("current") << "smt scope: " << s_smtEngine_current << std::endl; 54 } 55 ~SmtScope()56SmtScope::~SmtScope() { 57 s_smtEngine_current = d_oldSmtEngine; 58 Debug("current") << "smt scope: returning to " << s_smtEngine_current 59 << std::endl; 60 } 61 currentStatisticsRegistry()62StatisticsRegistry* SmtScope::currentStatisticsRegistry() { 63 Assert(smtEngineInScope()); 64 return s_smtEngine_current->d_statisticsRegistry; 65 } 66 67 }/* CVC4::smt namespace */ 68 }/* CVC4 namespace */ 69