f10f4e767819a8aff44e7761ccfabbc9243bf2e0
1 /********************* */
2 /*! \file smt_engine_scope.h
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "smt/smt_engine.h"
22 #include "util/Assert.h"
23 #include "expr/node_manager.h"
24 #include "util/output.h"
31 extern CVC4_THREADLOCAL(SmtEngine
*) s_smtEngine_current
;
33 inline SmtEngine
* currentSmtEngine() {
34 Assert(s_smtEngine_current
!= NULL
);
35 return s_smtEngine_current
;
38 class SmtScope
: public NodeManagerScope
{
39 /** The old NodeManager, to be restored on destruction. */
40 SmtEngine
* d_oldSmtEngine
;
44 SmtScope(const SmtEngine
* smt
) :
45 NodeManagerScope(smt
->d_nodeManager
),
46 d_oldSmtEngine(s_smtEngine_current
) {
48 s_smtEngine_current
= const_cast<SmtEngine
*>(smt
);
49 Debug("current") << "smt scope: " << s_smtEngine_current
<< std::endl
;
53 s_smtEngine_current
= d_oldSmtEngine
;
54 Debug("current") << "smt scope: returning to " << s_smtEngine_current
<< std::endl
;
56 };/* class SmtScope */
58 }/* CVC4::smt namespace */