diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/theory/theory_engine.cpp | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 12a169e09..d83626a6b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,6 +26,7 @@ #include "expr/node_builder.h" #include "options/options.h" #include "util/lemma_output_channel.h" +#include "util/resource_manager.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -142,6 +143,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true(), d_false(), d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -334,8 +336,7 @@ void TheoryEngine::dumpAssertions(const char* tag) { * @param effort the effort level to use */ void TheoryEngine::check(Theory::Effort effort) { - - d_propEngine->checkTime(); + // spendResource(); // Reset the interrupt flag d_interrupted = false; @@ -846,6 +847,7 @@ struct preprocess_stack_element { Node TheoryEngine::preprocess(TNode assertion) { Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl; + // spendResource(); // Do a topological sort of the subexpressions and substitute them vector<preprocess_stack_element> toVisit; @@ -1082,7 +1084,7 @@ void TheoryEngine::assertFact(TNode literal) { Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl; - d_propEngine->checkTime(); + // spendResource(); // If we're in conflict, nothing to do if (d_inConflict) { @@ -1145,7 +1147,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl; - d_propEngine->checkTime(); + // spendResource(); if(Dump.isOn("t-propagations")) { Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") @@ -1368,7 +1370,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). - spendResource(); + // spendResource(); // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { @@ -1553,7 +1555,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){ Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl; d_iteUtilities->clear(); - Rewriter::garbageCollect(); + Rewriter::clearCaches(); d_iteRemover.garbageCollect(); nm->reclaimZombiesUntil(options::zombieHuntThreshold()); Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; @@ -1742,3 +1744,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T return th->entailmentCheck(lit, params, seffects); } + +void TheoryEngine::spendResource() { + d_resourceManager->spendResource(); +} |