diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 29 |
1 files changed, 27 insertions, 2 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 960602846..a940bcc3d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -18,12 +18,16 @@ #include "theory/theory.h" #include "theory/rewriter.h" #include "theory/rewriter_tables.h" +#include "smt/smt_engine_scope.h" +#include "util/resource_manager.h" using namespace std; namespace CVC4 { namespace theory { +unsigned long Rewriter::d_iterationCount = 0; + static TheoryId theoryOf(TNode node) { return Theory::theoryOf(THEORY_OF_TYPE_BASED, node); } @@ -76,7 +80,7 @@ struct RewriteStackElement { } }; -Node Rewriter::rewrite(TNode node) { +Node Rewriter::rewrite(TNode node) throw (UnsafeInterruptException){ return rewriteTo(theoryOf(node), node); } @@ -102,9 +106,20 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { vector<RewriteStackElement> rewriteStack; rewriteStack.push_back(RewriteStackElement(node, theoryId)); + ResourceManager* rm = NULL; + bool hasSmtEngine = smt::smtEngineInScope(); + if (hasSmtEngine) { + rm = NodeManager::currentResourceManager(); + } // Rewrite until the stack is empty for (;;){ + if (hasSmtEngine && + d_iterationCount % ResourceManager::getFrequencyCount() == 0) { + rm->spendResource(); + d_iterationCount = 0; + } + // Get the top of the recursion stack RewriteStackElement& rewriteStackTop = rewriteStack.back(); @@ -139,7 +154,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { rewriteStackTop.theoryId = theoryOf(cached); } } - + rewriteStackTop.original =rewriteStackTop.node; // Now it's time to rewrite the children, check if this has already been done Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); @@ -233,5 +248,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { return Node::null(); }/* Rewriter::rewriteTo() */ +void Rewriter::clearCaches() { +#ifdef CVC4_ASSERTIONS + if(s_rewriteStack != NULL) { + delete s_rewriteStack; + s_rewriteStack = NULL; + } +#endif + Rewriter::clearCachesInternal(); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |