From c90b1b66e6c8e3b77f2b73b73208f120445e5f91 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 31 Jul 2012 21:44:22 +0000 Subject: fixes for portfolio --- src/theory/rewriter.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'src/theory/rewriter.cpp') 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 d_rewriteStack; +#ifdef CVC4_ASSERTIONS +static CVC4_THREADLOCAL(std::hash_set*) 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(); + } #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) { -- cgit v1.2.3