diff options
Diffstat (limited to 'src/theory/interrupted.h')
| -rw-r--r-- | src/theory/interrupted.h | 51 |
1 files changed, 26 insertions, 25 deletions
diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index 9b885ee46..618d5ac38 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -1,28 +1,29 @@ -/********************* */ -/*! \file interrupted.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 - ** - ** \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 cvc5::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. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Aina Niemetz, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * 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 cvc5::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. + */ #include "cvc4_private.h" |