* Fix some regressions' expected outputs.

* Ensure Rewriter::init() is called before ::rewrite().
  The array type enumerator recently gave us an end-run around
  ::init().  TheoryEngine no longer calls these, they're done
  via static initialization.

* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).

(this commit was certified error- and warning-free by the test-and-commit script.)

3 files changed, 31 insertions, 20 deletions

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 988b2b327..5cdd507d2 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -34,6 +34,18 @@ static TheoryId theoryOf(TNode node) {
 static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
 #endif /* CVC4_ASSERTIONS */
 
+class RewriterInitializer {
+  static RewriterInitializer s_rewriterInitializer;
+  RewriterInitializer() { Rewriter::init(); }
+  ~RewriterInitializer() { Rewriter::shutdown(); }
+};/* class RewriterInitializer */
+
+/**
+ * This causes initialization of the rewriter before first use,
+ * and tear-down at exit time.
+ */
+RewriterInitializer RewriterInitializer::s_rewriterInitializer;
+
 /**
  * TheoryEngine::rewrite() keeps a stack of things that are being pre-
  * and post-rewritten.  Each element of the stack is a
@@ -220,8 +232,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
   Unreachable();
   return Node::null();
-}
-
+}/* Rewriter::rewriteTo() */
 
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index afca18b76..9a6618215 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -50,11 +50,15 @@ struct RewriteResponse {
     status(status), node(node) {}
 };/* struct RewriteResponse */
 
+class RewriterInitializer;
+
 /**
  * The main rewriter class.  All functionality is static.
  */
 class Rewriter {
 
+  friend class RewriterInitializer;
+
   /** Returns the appropriate cache for a node */
   static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
 
@@ -70,8 +74,8 @@ class Rewriter {
                                   TNode node, TNode cache);
 
   // disable construction of rewriters; all functionality is static
-  Rewriter() CVC4_UNUSED;
-  Rewriter(const Rewriter&) CVC4_UNUSED;
+  Rewriter() CVC4_UNDEFINED;
+  Rewriter(const Rewriter&) CVC4_UNDEFINED;
 
   /**
    * Rewrites the node using the given theory rewriter.
@@ -89,15 +93,6 @@ class Rewriter {
    */
   static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
 
-public:
-
-
-  /**
-   * Rewrites the node using theoryOf() to determine which rewriter to
-   * use on the node.
-   */
-  static Node rewrite(TNode node);
-
   /**
    * Should be called before the rewriter gets used for the first time.
    */
@@ -108,6 +103,13 @@ public:
    */
   static void shutdown();
 
+public:
+
+  /**
+   * Rewrites the node using theoryOf() to determine which rewriter to
+   * use on the node.
+   */
+  static Node rewrite(TNode node);
 
 };/* class Rewriter */
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4de6dc231..252109a26 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: barrett, dejan
  ** Minor contributors (to current version): cconway, taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -94,7 +94,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_curr_model = new theory::TheoryModel( context, "DefaultModel", true );
   d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
 
-  Rewriter::init();
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -677,7 +676,6 @@ void TheoryEngine::shutdown() {
     }
   }
 
-  theory::Rewriter::shutdown();
   d_ppCache.clear();
 }