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