Refactor and update copyright headers. (#6316)

11 files changed, 163 insertions, 163 deletions

diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h
index e5a63fa4f..20b74b1a7 100644
--- a/src/proof/clause_id.h
+++ b/src/proof/clause_id.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file clause_id.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Paul Meng, Mathias Preiner, Liana Hadarean
- ** 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 Definition of ClauseId
- **
- ** A ClauseId is a shared identifier between the proofs module and the sat
- ** solver for a clause.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Paul Meng, Mathias Preiner, Liana Hadarean
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Definition of ClauseId.
+ *
+ * A ClauseId is a shared identifier between the proofs module and the sat
+ * solver for a clause.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index fbe87c267..867977a29 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file cnf_proof.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Andres Noetzli, Haniel Barbosa
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Liana Hadarean, Andres Noetzli, Haniel Barbosa
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "proof/cnf_proof.h"
 
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 9fa491c3d..19cd37679 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -1,20 +1,17 @@
-/*********************                                                        */
-/*! \file cnf_proof.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Haniel Barbosa, 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 A manager for CnfProofs.
- **
- ** A manager for CnfProofs.
- **
- **
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Liana Hadarean, Haniel Barbosa, 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.
+ * ****************************************************************************
+ *
+ * A manager for CnfProofs.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index c2e8bd863..9763bcda3 100644
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file dot_printer.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Diego Camargos
- ** 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 Implemantation of the module for printing dot proofs
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Diego Della Rocca de Camargos
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implemantation of the module for printing dot proofs.
+ */
 
 #include "proof/dot/dot_printer.h"
 
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index a56eab50d..9aefcffff 100644
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file dot_printer.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Diego Camargos
- ** 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 module for printing dot proofs
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Diego Della Rocca de Camargos
+ *
+ * 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 module for printing dot proofs.
+ */
 
 #include "cvc4_private.h"
 
@@ -71,4 +72,4 @@ class DotPrinter
 }  // namespace proof
 }  // namespace cvc5
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d9fd9c37a..9b6a6c658 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -1,19 +1,19 @@
-/*********************                                                        */
-/*! \file proof_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Morgan Deters, 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
- **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Liana Hadarean, Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ */
 
 #include "proof/proof_manager.h"
 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 28be23e54..22c84db83 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file proof_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Haniel Barbosa, Andrew Reynolds
- ** 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 A manager for Proofs
- **
- ** A manager for Proofs.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Liana Hadarean, Haniel Barbosa, 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.
+ * ****************************************************************************
+ *
+ * A manager for Proofs.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index fcd1199e4..e5a76eee1 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file sat_proof.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, 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 Resolution proof
- **
- ** Resolution proof
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Liana Hadarean, Tim King, 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.
+ * ****************************************************************************
+ *
+ * Resolution proof.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 9a7263af6..40ff7755d 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file sat_proof_implementation.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Guy Katz
- ** 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 Resolution proof
- **
- ** Resolution proof
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Liana Hadarean, Tim King, Guy Katz
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Resolution proof.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index e13db65d0..f7e600fe8 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file unsat_core.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Clark Barrett
- ** 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 Representation of unsat cores
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Andrew Reynolds, Clark Barrett
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Representation of unsat cores.
+ */
 
 #include "proof/unsat_core.h"
 
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 81ccb55b0..739a3d209 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file unsat_core.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, 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 Representation of unsat cores.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Representation of unsat cores.
+ */
 
 #include "cvc4_private.h"