diff options
author | Tim King <taking@cs.nyu.edu> | 2017-10-25 17:07:01 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-25 17:07:01 -0700 |
commit | 13c8e4a7b8575142ce9b70747969b71039389dfa (patch) | |
tree | b132e1b95223b2e9aa525388788912037037799a /src/theory/theory_engine.cpp | |
parent | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (diff) |
Removing throw specifiers from OutputChannel and subclasses. (#1209)
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); } |