diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 04:05:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 04:05:19 +0000 |
commit | 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 (patch) | |
tree | da76170cfa5311ce3b72b25e8e8179a4f1aa6f6c /src/theory/rewriter.cpp | |
parent | 04b89b1a5256a8a70df1615c9a7873a2d870fe82 (diff) |
* 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.)
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 21 |
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 */ |