blob: bcdaefd9f0b95695b463bcd43c1e99c210f562f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
#include "smt/smt_engine.h"
#include "util/tls.h"
#include "util/Assert.h"
#include "expr/node_manager.h"
#include "util/output.h"
#pragma once
namespace CVC4 {
namespace smt {
extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
inline SmtEngine* currentSmtEngine() {
Assert(s_smtEngine_current != NULL);
return s_smtEngine_current;
}
class SmtScope : public NodeManagerScope {
/** The old NodeManager, to be restored on destruction. */
SmtEngine* d_oldSmtEngine;
public:
SmtScope(const SmtEngine* smt) :
NodeManagerScope(smt->d_nodeManager),
d_oldSmtEngine(s_smtEngine_current) {
Assert(smt != NULL);
s_smtEngine_current = const_cast<SmtEngine*>(smt);
Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
}
~SmtScope() {
s_smtEngine_current = d_oldSmtEngine;
Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
}
};/* class SmtScope */
}
}
|