1 /********************* */
2 /*! \file smt_engine_scope.h
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
20 #include "smt/smt_engine.h"
22 #include "util/cvc4_assert.h"
23 #include "expr/node_manager.h"
24 #include "util/output.h"
25 #include "proof/proof.h"
35 extern CVC4_THREADLOCAL(SmtEngine
*) s_smtEngine_current
;
37 inline SmtEngine
* currentSmtEngine() {
38 Assert(s_smtEngine_current
!= NULL
);
39 return s_smtEngine_current
;
42 inline ProofManager
* currentProofManager() {
44 Assert(options::proof() || options::unsatCores());
45 Assert(s_smtEngine_current
!= NULL
);
46 return s_smtEngine_current
->d_proofManager
;
47 #else /* CVC4_PROOF */
48 InternalError("proofs/unsat cores are not on, but ProofManager requested");
50 #endif /* CVC4_PROOF */
53 class SmtScope
: public NodeManagerScope
{
54 /** The old NodeManager, to be restored on destruction. */
55 SmtEngine
* d_oldSmtEngine
;
59 SmtScope(const SmtEngine
* smt
) :
60 NodeManagerScope(smt
->d_nodeManager
),
61 d_oldSmtEngine(s_smtEngine_current
) {
63 s_smtEngine_current
= const_cast<SmtEngine
*>(smt
);
64 Debug("current") << "smt scope: " << s_smtEngine_current
<< std::endl
;
68 s_smtEngine_current
= d_oldSmtEngine
;
69 Debug("current") << "smt scope: returning to " << s_smtEngine_current
<< std::endl
;
71 };/* class SmtScope */
73 }/* CVC4::smt namespace */