diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-07-31 21:44:22 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-07-31 21:44:22 +0000 |
| commit | c90b1b66e6c8e3b77f2b73b73208f120445e5f91 (patch) | |
| tree | cc409476d04f4c0bfe1b889bf291b87f729ab78a /src/theory/rewriter.cpp | |
| parent | b88133bc679c541798c2063fec2bc441e744328a (diff) | |
fixes for portfolio
Diffstat (limited to 'src/theory/rewriter.cpp')
| -rw-r--r-- | src/theory/rewriter.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index a91243343..988b2b327 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -30,7 +30,9 @@ static TheoryId theoryOf(TNode node) { return Theory::theoryOf(THEORY_OF_TYPE_BASED, node); } -std::hash_set<Node, NodeHashFunction> d_rewriteStack; +#ifdef CVC4_ASSERTIONS +static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; +#endif /* CVC4_ASSERTIONS */ /** * TheoryEngine::rewrite() keeps a stack of things that are being pre- @@ -72,6 +74,10 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { #ifdef CVC4_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL; + + if(s_rewriteStack == NULL) { + s_rewriteStack = new std::hash_set<Node, NodeHashFunction>(); + } #endif Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl; @@ -171,12 +177,12 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Assert(response.node != rewriteStackTop.node); //TODO: this is not thread-safe - should make this assertion dependent on sequential build #ifdef CVC4_ASSERTIONS - Assert(d_rewriteStack.find(response.node) == d_rewriteStack.end()); - d_rewriteStack.insert(response.node); + Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end()); + s_rewriteStack->insert(response.node); #endif rewriteStackTop.node = rewriteTo(newTheoryId, response.node); #ifdef CVC4_ASSERTIONS - d_rewriteStack.erase(response.node); + s_rewriteStack->erase(response.node); #endif break; } else if (response.status == REWRITE_DONE) { |