diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 02:49:35 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 02:49:35 +0000 |
| commit | 9b4696559cd2c74afb825d793614eb4cd6ee817e (patch) | |
| tree | a83bd5b4aac7fe1aa8160f9de7721e85a218b3ef /src/theory/rewriter.cpp | |
| parent | 134c6dc95199bc57013d07e0992f89254f49038b (diff) | |
Fixes lots of problems in bv rewrite rules and adds lots of assertions
to catch any that I may have missed
Diffstat (limited to 'src/theory/rewriter.cpp')
| -rw-r--r-- | src/theory/rewriter.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 2e8acfa89..e0b1458fb 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -26,6 +26,8 @@ using namespace std; namespace CVC4 { namespace theory { +std::hash_set<Node, NodeHashFunction> d_rewriteStack; + /** * TheoryEngine::rewrite() keeps a stack of things that are being pre- * and post-rewritten. Each element of the stack is a @@ -172,7 +174,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite 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); +#endif rewriteStackTop.node = rewriteTo(newTheoryId, response.node); +#ifdef CVC4_ASSERTIONS + d_rewriteStack.erase(response.node); +#endif break; } else if (response.status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS |