12 files changed, 201 insertions, 199 deletions
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 4a8e7e1bc..868b7f97d 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Mathias Preiner, Aina Niemetz, Gereon Kremer
-## 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.
+###############################################################################
+# Top contributors (to current version):
+#   Mathias Preiner, Gereon Kremer, Aina Niemetz
+#
+# 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 build system configuration.
 ##
-#-----------------------------------------------------------------------------#
-# libmain source files
 
+# libmain source files
 set(libmain_src_files
   command_executor.cpp
   interactive_shell.cpp
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 75d116f33..c1cf3ed70 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file command_executor.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Kshitij Bansal, Andrew Reynolds, 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 additional layer between commands and invoking them.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Kshitij Bansal, Andrew Reynolds, 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 additional layer between commands and invoking them.
+ */
 
 #include "main/command_executor.h"
 
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 5a848bad0..bf34df579 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file command_executor.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Kshitij Bansal, 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 An additional layer between commands and invoking them.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Kshitij Bansal, Gereon Kremer
+ *
+ * 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 additional layer between commands and invoking them.
+ */
 
 #ifndef CVC5__MAIN__COMMAND_EXECUTOR_H
 #define CVC5__MAIN__COMMAND_EXECUTOR_H
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9488b5c6d..c5d89300c 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file driver_unified.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Liana Hadarean, Tim King
- ** 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 Driver for CVC4 executable (cvc4)
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Liana Hadarean, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Driver for CVC4 executable (cvc4).
+ */
 
 #include <stdio.h>
 #include <unistd.h>
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index e6ae7ad5d..904cba276 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file interactive_shell.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Andrew V. Jones
- ** 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 Interactive shell for CVC4
- **
- ** This file is the implementation for the CVC4 interactive shell.
- ** The shell supports the editline library.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Christopher L. Conway, Andrew V. Jones
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Interactive shell for cvc5.
+ *
+ * This file is the implementation for the cvc5 interactive shell.
+ * The shell supports the editline library.
+ */
 #include "main/interactive_shell.h"
 
 #include <algorithm>
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 5ae3b40ef..cf5f22b51 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file interactive_shell.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, 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 Interactive shell for CVC4
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Christopher L. Conway, Mathias Preiner
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Interactive shell for cvc5.
+ */
 
 #ifndef CVC5__INTERACTIVE_SHELL_H
 #define CVC5__INTERACTIVE_SHELL_H
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 37c122732..8532f9504 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file main.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Christopher L. Conway
- ** 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 Main driver for CVC4 executable
- **
- ** Main driver for CVC4 executable.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Aina Niemetz, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Main driver for cvc5 executable.
+ */
 #include "main/main.h"
 
 #include <cstdlib>
diff --git a/src/main/main.h b/src/main/main.h
index c263e9d7a..121f9d951 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file main.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Mathias Preiner
- ** 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 Header for main CVC4 driver
- **
- ** Header for main CVC4 driver.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Gereon Kremer, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Header for main cvc5 driver.
+ */
 
 #include <chrono>
 #include <exception>
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index a29872c95..1be6a7f35 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -1,22 +1,21 @@
-/*********************                                                        */
-/*! \file signal_handlers.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Gereon Kremer, 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 Implementation of signal handlers.
- **
- ** Implementation of signal handlers.
- **
- ** It is important to only call async-signal-safe functions from signal
- ** handlers. See: http://man7.org/linux/man-pages/man7/signal-safety.7.html for
- ** a list of async-signal-safe POSIX.1 functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * Implementation of signal handlers.
+ *
+ * It is important to only call async-signal-safe functions from signal
+ * handlers. See: http://man7.org/linux/man-pages/man7/signal-safety.7.html for
+ * a list of async-signal-safe POSIX.1 functions.
+ */
 
 #include <string.h>
 
diff --git a/src/main/signal_handlers.h b/src/main/signal_handlers.h
index c7506de4f..b849198c7 100644
--- a/src/main/signal_handlers.h
+++ b/src/main/signal_handlers.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file signal_handlers.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Gereon Kremer, Mathias Preiner
- ** 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 Implementation of signal handlers.
- **
- ** Implementation of signal handlers.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer, Mathias Preiner
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of signal handlers.
+ */
 
 #ifndef CVC5__MAIN__SIGNAL_HANDLERS_H
 #define CVC5__MAIN__SIGNAL_HANDLERS_H
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index e3a95d640..bd41ed7ed 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -1,44 +1,43 @@
-/*********************                                                        */
-/*! \file time_limit.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Gereon Kremer
- ** 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 Implementation of time limits.
- **
- ** Implementation of time limits that are imposed by the --tlimit option.
- **
- ** There are various strategies to implement time limits, with different
- ** advantages and disadvantages:
- **
- ** std::thread: we can spawn a new thread which waits for the time limit.
- ** Unless we use std::jthread (from C++20), std::thread is not interruptible
- ** and thus we need a synchronization mechanism so that the main thread can
- ** communicate to the timer thread that it wants to finish. Apparently, this
- ** is the only platform independent way.
- **
- ** POSIX setitimer: a very simple way that instructs the kernel to send a
- ** signal after some time. If available, this is what we want!
- **
- ** Win32 CreateWaitableTimer: unfortunately, this mechanism only calls the
- ** completion routine (the callback) when the main thread "enters an
- ** alertable wait state", i.e. it sleeps. We don't want our main thread to
- ** sleep, thus this approach is not appropriate.
- **
- ** Win32 SetTimer: while we can specify a callback function, we still need
- ** to process the windows event queue for the callback to be called. (see
- ** https://stackoverflow.com/a/15406527/2375725). We don't want our main
- ** thread to continuously monitor the event queue.
- **
- **
- ** We thus use the setitimer variant whenever possible, and the std::thread
- ** variant otherwise.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of time limits that are imposed by the --tlimit option.
+ *
+ * There are various strategies to implement time limits, with different
+ * advantages and disadvantages:
+ *
+ * std::thread: we can spawn a new thread which waits for the time limit.
+ * Unless we use std::jthread (from C++20), std::thread is not interruptible
+ * and thus we need a synchronization mechanism so that the main thread can
+ * communicate to the timer thread that it wants to finish. Apparently, this
+ * is the only platform independent way.
+ *
+ * POSIX setitimer: a very simple way that instructs the kernel to send a
+ * signal after some time. If available, this is what we want!
+ *
+ * Win32 CreateWaitableTimer: unfortunately, this mechanism only calls the
+ * completion routine (the callback) when the main thread "enters an
+ * alertable wait state", i.e. it sleeps. We don't want our main thread to
+ * sleep, thus this approach is not appropriate.
+ *
+ * Win32 SetTimer: while we can specify a callback function, we still need
+ * to process the windows event queue for the callback to be called. (see
+ * https://stackoverflow.com/a/15406527/2375725). We don't want our main
+ * thread to continuously monitor the event queue.
+ *
+ *
+ * We thus use the setitimer variant whenever possible, and the std::thread
+ * variant otherwise.
+ */
 
 #include "time_limit.h"
 
diff --git a/src/main/time_limit.h b/src/main/time_limit.h
index 1e87a21bc..c84e22b4b 100644
--- a/src/main/time_limit.h
+++ b/src/main/time_limit.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file time_limit.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Gereon Kremer
- ** 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 Implementation of time limits.
- **
- ** Implementation of time limits that are imposed by the --tlimit option.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of time limits that are imposed by the --tlimit option.
+ */
 
 #ifndef CVC5__MAIN__TIME_LIMIT_H
 #define CVC5__MAIN__TIME_LIMIT_H