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 "cvc4_private.h"
22 #include "smt/smt_engine.h"
24 #include "util/Assert.h"
25 #include "expr/node_manager.h"
26 #include "util/output.h"
33 extern CVC4_THREADLOCAL(SmtEngine
*) s_smtEngine_current
;
35 inline SmtEngine
* currentSmtEngine() {
36 Assert(s_smtEngine_current
!= NULL
);
37 return s_smtEngine_current
;
40 class SmtScope
: public NodeManagerScope
{
41 /** The old NodeManager, to be restored on destruction. */
42 SmtEngine
* d_oldSmtEngine
;
46 SmtScope(const SmtEngine
* smt
) :
47 NodeManagerScope(smt
->d_nodeManager
),
48 d_oldSmtEngine(s_smtEngine_current
) {
50 s_smtEngine_current
= const_cast<SmtEngine
*>(smt
);
51 Debug("current") << "smt scope: " << s_smtEngine_current
<< std::endl
;
55 s_smtEngine_current
= d_oldSmtEngine
;
56 Debug("current") << "smt scope: returning to " << s_smtEngine_current
<< std::endl
;
58 };/* class SmtScope */
60 }/* CVC4::smt namespace */