* 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.)

1 files changed, 14 insertions, 12 deletions

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 */