diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 34 |
1 files changed, 18 insertions, 16 deletions
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 |