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, 4 insertions, 0 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index aef98d75b..4df9054a7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -76,6 +76,7 @@ namespace smt {
   class DefinedFunction;
 
   class SmtEnginePrivate;
+  class SmtScope;
 }/* CVC4::smt namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -248,6 +249,9 @@ class CVC4_PUBLIC SmtEngine {
   void setLogicInternal() throw(AssertionException);
 
   friend class ::CVC4::smt::SmtEnginePrivate;
+  friend class ::CVC4::smt::SmtScope;
+
+  StatisticsRegistry* d_statisticsRegistry;
 
   // === STATISTICS ===
   /** time spent in definition-expansion */