diff options
author | Tim King <taking@google.com> | 2016-11-18 15:17:31 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-11-18 15:28:24 -0800 |
commit | 044e20567fa7252be33aa0108b2f795b8181fb04 (patch) | |
tree | 1577f0cf1ad50aafc748628f681fc3acf7c6b4e3 /src/theory/output_channel.h | |
parent | c1f42884d4a277c2dadb876c967d0d7097b7b5f0 (diff) |
Removing some throw specifiers from OutputChannel. Fixes bug 716.
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 639793c7f..4ca113eed 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -101,7 +101,7 @@ public: * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. * @param pf - a proof of the conflict. This is only non-null if proofs - * are enabled. + * are enabled. */ virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0; @@ -128,17 +128,15 @@ public: virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, bool preprocess = false, - bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + bool sendAtoms = false) = 0; /** * Variant of the lemma function that does not require providing a proof rule. */ - virtual LemmaStatus lemma(TNode n, + virtual LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false, - bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + bool sendAtoms = false) { return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); } @@ -153,8 +151,7 @@ public: return splitLemma(n.orNode(n.notNode())); } - virtual LemmaStatus splitLemma(TNode n, bool removable = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0; /** * If a decision is made on n, it must be in the phase specified. |