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 | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/output_channel.h | 23 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 29 | ||||
-rw-r--r-- | src/theory/rewriter.h | 11 | ||||
-rw-r--r-- | src/theory/rewriter_tables_template.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 34 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 24 |
17 files changed, 121 insertions, 55 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 0ff12da95..e13587323 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -28,6 +28,7 @@ #include "prop/sat_solver.h" #include "theory/valuation.h" #include "theory/theory_registrar.h" +#include "util/resource_manager.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -134,6 +135,7 @@ class TLazyBitblaster : public TBitblaster<Node> { {} bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); + void spendResource(); void safePoint(); }; @@ -228,7 +230,8 @@ private: Statistics(const std::string& name); ~Statistics(); }; - std::string d_name; + std::string d_name; +public: Statistics d_statistics; }; @@ -237,6 +240,9 @@ public: MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) { return true; } void notify(prop::SatClause& clause) { } + void spendResource() { + NodeManager::currentResourceManager()->spendResource(); + } void safePoint() {} }; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index f9f8ff581..57a635c20 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -67,6 +67,7 @@ bool EagerBitblastSolver::isInitialized() { } void EagerBitblastSolver::assertFormula(TNode formula) { + d_bv->spendResource(); Assert (isInitialized()); Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; d_assertionSet.insert(formula); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e8acf268f..5b139e327 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -557,6 +557,7 @@ bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) { void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) { bool changed = true; while(changed) { + // d_bv->spendResource(); changed = false; for (unsigned i = 0; i < worklist.size(); ++i) { // apply current substitutions diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index d0b99f869..c86572ead 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -103,8 +103,11 @@ void BitblastSolver::bitblastQueue() { // don't bit-blast lemma atoms continue; } - Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; - d_bitblaster->bbAtom(atom); + Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; + { + TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer); + d_bitblaster->bbAtom(atom); + } } } @@ -149,6 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) { // We need to ensure we are fully propagated, so propagate now if (d_useSatPropagation) { + d_bv->spendResource(); bool ok = d_bitblaster->propagate(); if (!ok) { std::vector<TNode> conflictAtoms; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index d2c79fec2..938a93b85 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -166,6 +166,9 @@ bool CoreSolver::decomposeFact(TNode fact) { bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; + + d_bv->spendResource(); + d_checkCalled = true; Assert (!d_bv->inConflict()); ++(d_statistics.d_numCallstoCheck); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 917b10c33..660551fe2 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -29,6 +29,7 @@ using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; ++(d_statistics.d_numCallstoCheck); + d_bv->spendResource(); bool ok = true; while (!done() && ok) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 877baec4e..065d5d5ef 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -103,6 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) { return; } + d_bv->spendResource(); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; d_termBBStrategies[node.getKind()] (node, bits, this); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index b74506e4d..e5b5ed664 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -170,6 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { return; } + d_bv->spendResource(); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; @@ -355,6 +356,10 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } +void TLazyBitblaster::MinisatNotify::spendResource() { + d_bv->spendResource(); +} + void TLazyBitblaster::MinisatNotify::safePoint() { d_bv->d_out->safePoint(); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 99bc764dd..eddd5017c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -107,6 +107,10 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } +void TheoryBV::spendResource() throw(UnsafeInterruptException) { + getOutputChannel().spendResource(); +} + TheoryBV::Statistics::Statistics(): d_avgConflictSize("theory::bv::AvgBVConflictSize"), d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), @@ -362,6 +366,7 @@ void TheoryBV::check(Effort e) return; } Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); // if we are using the eager solver diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a37a4019e..11d8cb895 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -103,6 +103,7 @@ private: Statistics d_statistics; + void spendResource() throw(UnsafeInterruptException); /** * Return the uninterpreted function symbol corresponding to division-by-zero @@ -218,6 +219,7 @@ private: friend class CoreSolver; friend class InequalitySolver; friend class AlgebraicSolver; + friend class EagerBitblastSolver; };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 40eba6ff5..fdf253d3f 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -21,6 +21,7 @@ #include "util/cvc4_assert.h" #include "theory/interrupted.h" +#include "util/resource_manager.h" namespace CVC4 { namespace theory { @@ -84,7 +85,7 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted, AssertionException) { + virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) { } /** @@ -97,7 +98,7 @@ public: * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. */ - virtual void conflict(TNode n) throw(AssertionException) = 0; + virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; /** * Propagate a theory literal. @@ -105,7 +106,7 @@ public: * @param n - a theory consequence at the current decision level * @return false if an immediate conflict was encountered */ - virtual bool propagate(TNode n) throw(AssertionException) = 0; + virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -119,7 +120,7 @@ public: */ virtual LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false) - throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Request a split on a new theory atom. This is equivalent to @@ -128,12 +129,12 @@ public: * @param n - a theory atom; must be of Boolean type */ LemmaStatus split(TNode n) - throw(TypeCheckingExceptionPrivate, AssertionException) { + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { return splitLemma(n.orNode(n.notNode())); } virtual LemmaStatus splitLemma(TNode n, bool removable = false) - throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * If a decision is made on n, it must be in the phase specified. @@ -148,7 +149,7 @@ public: * @param phase - the phase to decide on n */ virtual void requirePhase(TNode n, bool phase) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Flips the most recent unflipped decision to the other phase and @@ -191,14 +192,14 @@ public: * could be flipped, or if the root decision was re-flipped */ virtual bool flipDecision() - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Notification from a theory that it realizes it is incomplete at * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. */ - virtual void setIncomplete() throw(AssertionException) = 0; + virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0; /** * "Spend" a "resource." The meaning is specific to the context in @@ -211,7 +212,7 @@ public: * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource() throw() {} + virtual void spendResource() throw(UnsafeInterruptException) {} /** * Handle user attribute. @@ -226,7 +227,7 @@ public: * Using this leads to non-termination issues. * It is appropriate for prototyping for theories. */ - virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {} + virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {} };/* class OutputChannel */ 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 */ diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index b150b186a..44035e7d9 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,6 +19,8 @@ #pragma once #include "expr/node.h" +#include "util/unsafe_interrupt_exception.h" + //#include "expr/attribute.h" namespace CVC4 { @@ -56,7 +58,7 @@ class RewriterInitializer; class Rewriter { friend class RewriterInitializer; - + static unsigned long d_iterationCount; /** Returns the appropriate cache for a node */ static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node); @@ -100,20 +102,19 @@ class Rewriter { * Should be called to clean up any state. */ static void shutdown(); - + static void clearCachesInternal(); public: /** * Rewrites the node using theoryOf() to determine which rewriter to * use on the node. */ - static Node rewrite(TNode node); + static Node rewrite(TNode node) throw (UnsafeInterruptException); /** * Garbage collects the rewrite caches. */ - static void garbageCollect(); - + static void clearCaches(); };/* class Rewriter */ }/* CVC4::theory namespace */ diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 9b51d2b32..d79f464b5 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -85,7 +85,7 @@ void Rewriter::shutdown() { ${rewrite_shutdown} } -void Rewriter::garbageCollect() { +void Rewriter::clearCachesInternal() { typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId; std::vector<AttributeUniqueId> preids; ${pre_rewrite_attribute_ids} 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(); +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 136c0409f..6360ea5fb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -39,6 +39,7 @@ #include "util/statistics_registry.h" #include "util/cvc4_assert.h" #include "util/sort_inference.h" +#include "util/unsafe_interrupt_exception.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/uf/equality_engine.h" #include "theory/bv/bv_to_bool.h" @@ -46,6 +47,8 @@ namespace CVC4 { +class ResourceManager; + /** * A pair of a theory and a node. This is used to mark the flow of * propagations between theories. @@ -279,42 +282,42 @@ class TheoryEngine { { } - void safePoint() throw(theory::Interrupted, AssertionException) { + void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { spendResource(); if (d_engine->d_interrupted) { throw theory::Interrupted(); } } - void conflict(TNode conflictNode) throw(AssertionException) { + void conflict(TNode conflictNode) throw(AssertionException, UnsafeInterruptException) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; ++ d_statistics.conflicts; d_engine->d_outputChannelUsed = true; d_engine->conflict(conflictNode, d_theory); } - bool propagate(TNode literal) throw(AssertionException) { + bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) { Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; ++ d_statistics.propagations; d_engine->d_outputChannelUsed = true; return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST); } - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; return d_engine->lemma(lemma, false, removable, false, d_theory); } - void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) { + void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); Node restartVar = curr->mkSkolem("restartVar", curr->booleanType(), @@ -325,7 +328,7 @@ class TheoryEngine { } void requirePhase(TNode n, bool phase) - throw(theory::Interrupted, AssertionException) { + throw(theory::Interrupted, AssertionException, UnsafeInterruptException) { Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase << ")" << std::endl; ++ d_statistics.requirePhase; @@ -333,18 +336,18 @@ class TheoryEngine { } bool flipDecision() - throw(theory::Interrupted, AssertionException) { + throw(theory::Interrupted, AssertionException, UnsafeInterruptException) { Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl; ++ d_statistics.flipDecision; return d_engine->d_propEngine->flipDecision(); } - void setIncomplete() throw(AssertionException) { + void setIncomplete() throw(AssertionException, UnsafeInterruptException) { Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl; d_engine->setIncomplete(d_theory); } - void spendResource() throw() { + void spendResource() throw(UnsafeInterruptException) { d_engine->spendResource(); } @@ -387,12 +390,6 @@ class TheoryEngine { d_incomplete = true; } - /** - * "Spend" a resource during a search or preprocessing. - */ - void spendResource() throw() { - d_propEngine->spendResource(); - } /** * Mapping of propagations from recievers to senders. @@ -477,6 +474,7 @@ class TheoryEngine { /** Whether we were just interrupted (or not) */ bool d_interrupted; + ResourceManager* d_resourceManager; public: @@ -487,6 +485,10 @@ public: ~TheoryEngine(); void interrupt() throw(ModalException); + /** + * "Spend" a resource during a search or preprocessing. + */ + void spendResource(); /** * Adds a theory. Only one theory per TheoryId can be present, so if diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 6d1275c20..46a717cc5 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -23,13 +23,13 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/interrupted.h" +#include "util/unsafe_interrupt_exception.h" #include <vector> #include <utility> #include <iostream> namespace CVC4 { - namespace theory { /** @@ -72,42 +72,44 @@ public: void safePoint() throw(Interrupted, AssertionException) {} void conflict(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(CONFLICT, n); } bool propagate(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(PROPAGATE, n); return true; } void propagateAsDecision(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - void requirePhase(TNode, bool) throw(Interrupted, AssertionException) { + void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) { } - bool flipDecision() throw(Interrupted, AssertionException) { + bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) { return true; } - void setIncomplete() throw(AssertionException) {} + void setIncomplete() throw(AssertionException, UnsafeInterruptException) { + } - void handleUserAttribute( const char* attr, theory::Theory* t ){} + void handleUserAttribute( const char* attr, theory::Theory* t ) { + } void clear() { d_callHistory.clear(); } - LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){ + LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } @@ -125,7 +127,7 @@ public: return d_callHistory.size(); } - void printIth(std::ostream& os, int i){ + void printIth(std::ostream& os, int i) { os << "[TestOutputChannel " << i; os << " " << getIthCallType(i); os << " " << getIthNode(i) << "]"; |