Support for having two SmtEngines with the same ExprManager.

Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine.  Otherwise, theories register the
same statistic twice.  This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed.  Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).

1 files changed, 40 insertions, 0 deletions

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
new file mode 100644
index 000000000..bcdaefd9f
--- /dev/null
+++ b/src/smt/smt_engine_scope.h
@@ -0,0 +1,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 */
+
+}
+}