4 files changed, 71 insertions, 69 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 29093235d..47b376151 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1,35 +1,34 @@
-/*********************                                                        */
-/*! \file cvc5.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Andres Noetzli
- ** 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 The CVC4 C++ API.
- **
- ** The CVC4 C++ API.
- **
- ** A brief note on how to guard API functions:
- **
- ** In general, we think of API guards as a fence -- they are supposed to make
- ** sure that no invalid arguments get passed into internal realms of CVC4.
- ** Thus we always want to catch such cases on the API level (and can then
- ** assert internally that no invalid argument is passed in).
- **
- ** The only special case is when we use 3rd party back-ends we have no control
- ** over, and which throw (invalid_argument) exceptions anyways. In this case,
- ** we do not replicate argument checks but delegate them to the back-end,
- ** catch thrown exceptions, and raise a CVC4ApiException.
- **
- ** Our Integer implementation, e.g., is such a special case since we support
- ** two different back end implementations (GMP, CLN). Be aware that they do
- ** not fully agree on what is (in)valid input, which requires extra checks for
- ** consistent behavior (see Solver::mkRealFromStrHelper for an example).
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * The cvc5 C++ API.
+ *
+ * A brief note on how to guard API functions:
+ *
+ * In general, we think of API guards as a fence -- they are supposed to make
+ * sure that no invalid arguments get passed into internal realms of cvc5.
+ * Thus we always want to catch such cases on the API level (and can then
+ * assert internally that no invalid argument is passed in).
+ *
+ * The only special case is when we use 3rd party back-ends we have no control
+ * over, and which throw (invalid_argument) exceptions anyways. In this case,
+ * we do not replicate argument checks but delegate them to the back-end,
+ * catch thrown exceptions, and raise a CVC4ApiException.
+ *
+ * Our Integer implementation, e.g., is such a special case since we support
+ * two different back end implementations (GMP, CLN). Be aware that they do
+ * not fully agree on what is (in)valid input, which requires extra checks for
+ * consistent behavior (see Solver::mkRealFromStrHelper for an example).
+ */
 
 #include "api/cpp/cvc5.h"
 
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 56b23bf89..4876caf80 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1,14 +1,15 @@
-/***
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
- ** 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.
- */
-
-/**
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
  * The cvc5 C++ API.
  */
 
diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h
index f210dddf6..83290088c 100644
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -1,18 +1,19 @@
-/*********************                                                        */
-/*! \file checks.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** 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 Check macros for the cvc5 C++ API.
- **
- ** These macros implement guards for the cvc5 C++ API functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Abdalrhman Mohamed, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Check macros for the cvc5 C++ API.
+ *
+ * These macros implement guards for the cvc5 C++ API functions.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index e149770fa..eaa4e6079 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1,14 +1,15 @@
-/***
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Makai Mann
- ** 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.
- */
-
-/**
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Makai Mann
+ *
+ * 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.
+ * ****************************************************************************
+ *
  * The term kinds of the cvc5 C++ API.
  */