From 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 6 Oct 2012 04:05:19 +0000 Subject: * 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.) --- src/theory/rewriter.cpp | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'src/theory/rewriter.cpp') 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*) 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 */ -- cgit v1.2.3