* 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, 16 insertions, 5 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 */