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 9d06fadc4999492eb56188da7a31c5195df9c1ca..6f3ddd5eb99e34a38187780439e7dfc73988646f 100644 (file)
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -1,7 +1,26 @@
+/******************************************************************************
+ * 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 {
 
@@ -78,15 +97,13 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCa
   cb.multiplyRow(rid, -a_rs_sgn);
 }
 
-
-
 void Tableau::addRow(ArithVar basic,
                      const std::vector<Rational>& coefficients,
                      const std::vector<ArithVar>& variables)
 {
   Assert(basic < getNumColumns());
-
-  Assert(coefficients.size() == variables.size() );
+  Assert(debugIsASet(variables));
+  Assert(coefficients.size() == variables.size());
   Assert(!isBasic(basic));
 
   RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
@@ -174,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