diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 892b331ea..402ba61ff 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -193,19 +193,21 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma( return result; } -bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) - throw(AssertionException, UnsafeInterruptException) { - Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; - ++ d_statistics.propagations; +bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) { + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory + << ">::propagate(" << literal << ")" << std::endl; + ++d_statistics.propagations; d_engine->d_outputChannelUsed = true; return d_engine->propagate(literal, d_theory); } -void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) - throw(AssertionException, UnsafeInterruptException) { - Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; - Assert (pf == NULL); // Theory shouldn't be producing proofs yet - ++ d_statistics.conflicts; +void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, + Proof* proof) { + Trace("theory::conflict") + << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode + << ")" << std::endl; + Assert(!proof); // Theory shouldn't be producing proofs yet + ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; d_engine->conflict(conflictNode, d_theory); } |