Update copyright headers.

[cvc5.git] / src / theory / interrupted.h

diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h
index f7a269f0ba95bc146ef2b32f6be7660a3906903a..d336e93142a4098de4f9bb4326e6962ed7c54958 100644 (file)
--- a/src/theory/interrupted.h
+++ b/src/theory/interrupted.h
@@ -1,37 +1,43 @@
 /*********************                                                        */
-/** interrupted.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
+/*! \file interrupted.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
- ** The theory output channel interface.
+ ** \brief An exception signaling that a Theory should immediately
+ ** stop performing processing
+ **
+ ** An exception signaling that a Theory should immediately stop
+ ** performing processing and relinquish control to its caller (e.g.,
+ ** in a parallel environment).  A Theory might be interrupted if it
+ ** calls into its CVC4::theory::OutputChannel, and it should only
+ ** catch this exception to perform emergency repair of any invariants
+ ** it must re-establish.  Further, if this exception is caught by a
+ ** Theory, the Theory should rethrow the same exception (via "throw;"
+ ** in the exception block) rather than return, as the Interrupted
+ ** instance might contain additional information needed for the
+ ** proper management of CVC4 components.
  **/
 
-#ifndef __CVC4__THEORY__INTERRUPTED_H
-#define __CVC4__THEORY__INTERRUPTED_H
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__INTERRUPTED_H
+#define CVC4__THEORY__INTERRUPTED_H
 
-#include "util/exception.h"
+#include "base/exception.h"
 
 namespace CVC4 {
 namespace theory {
 
-class CVC4_PUBLIC Interrupted : public CVC4::Exception {
-public:
-
-  // Constructors
-  Interrupted() : CVC4::Exception("CVC4::Theory::Interrupted") {}
-  Interrupted(const std::string& msg) : CVC4::Exception(msg) {}
-  Interrupted(const char* msg) : CVC4::Exception(msg) {}
-
+class Interrupted : public CVC4::Exception {
 };/* class Interrupted */
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__INTERRUPTED_H */
+#endif /* CVC4__THEORY__INTERRUPTED_H */