diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/rewriter.cpp | 21 | ||||
-rw-r--r-- | src/theory/rewriter.h | 26 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
3 files changed, 31 insertions, 20 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 */ 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 */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4de6dc231..252109a26 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -5,7 +5,7 @@ ** Major contributors: barrett, dejan ** Minor contributors (to current version): cconway, taking ** 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 @@ -94,7 +94,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_curr_model = new theory::TheoryModel( context, "DefaultModel", true ); d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); - Rewriter::init(); StatisticsRegistry::registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -677,7 +676,6 @@ void TheoryEngine::shutdown() { } } - theory::Rewriter::shutdown(); d_ppCache.clear(); } |