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()31 SmtEngine* currentSmtEngine() {
32   Assert(s_smtEngine_current != NULL);
33   return s_smtEngine_current;
34 }
35 
smtEngineInScope()36 bool smtEngineInScope() { return s_smtEngine_current != NULL; }
37 
currentProofManager()38 ProofManager* 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)48 SmtScope::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()56 SmtScope::~SmtScope() {
57   s_smtEngine_current = d_oldSmtEngine;
58   Debug("current") << "smt scope: returning to " << s_smtEngine_current
59                    << std::endl;
60 }
61 
currentStatisticsRegistry()62 StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
63   Assert(smtEngineInScope());
64   return s_smtEngine_current->d_statisticsRegistry;
65 }
66 
67 }/* CVC4::smt namespace */
68 }/* CVC4 namespace */
69