Add new interfaces to term formula removal and theory preprocess (#5717)
[cvc5.git] / src / theory / interrupted.h
1 /********************* */
2 /*! \file interrupted.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Mathias Preiner, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief An exception signaling that a Theory should immediately
13 ** stop performing processing
14 **
15 ** An exception signaling that a Theory should immediately stop
16 ** performing processing and relinquish control to its caller (e.g.,
17 ** in a parallel environment). A Theory might be interrupted if it
18 ** calls into its CVC4::theory::OutputChannel, and it should only
19 ** catch this exception to perform emergency repair of any invariants
20 ** it must re-establish. Further, if this exception is caught by a
21 ** Theory, the Theory should rethrow the same exception (via "throw;"
22 ** in the exception block) rather than return, as the Interrupted
23 ** instance might contain additional information needed for the
24 ** proper management of CVC4 components.
25 **/
26
27 #include "cvc4_private.h"
28
29 #ifndef CVC4__THEORY__INTERRUPTED_H
30 #define CVC4__THEORY__INTERRUPTED_H
31
32 #include "base/exception.h"
33
34 namespace CVC4 {
35 namespace theory {
36
37 class Interrupted : public CVC4::Exception {
38 };/* class Interrupted */
39
40 }/* CVC4::theory namespace */
41 }/* CVC4 namespace */
42
43 #endif /* CVC4__THEORY__INTERRUPTED_H */