Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)

[cvc5.git] / src / theory / arith / tableau.cpp

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 080104118d4160631292098c4a7c7c1f1652887f..6f3ddd5eb99e34a38187780439e7dfc73988646f 100644 (file)
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -1,25 +1,26 @@
-/*********************                                                        */
-/*! \file tableau.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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):
+ *   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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "base/output.h"
 #include "theory/arith/tableau.h"
 
 using namespace std;
-namespace CVC4 {
+namespace cvc5 {
 namespace theory {
 namespace arith {
 
@@ -102,7 +103,7 @@ void Tableau::addRow(ArithVar basic,
 {
   Assert(basic < getNumColumns());
   Assert(debugIsASet(variables));
-  Assert(coefficients.size() == variables.size() );
+  Assert(coefficients.size() == variables.size());
   Assert(!isBasic(basic));
 
   RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
@@ -190,6 +191,6 @@ void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
   printRow(basicToRowIndex(basic), out);
 }
 
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5