+/******************************************************************************
+ * 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 {
d_basic2RowIndex.set(basicNew, rid);
d_rowIndex2basic.set(rid, basicNew);
- cb.swap(basicOld, basicNew, a_rs_sgn);
+ 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);
printRow(basicToRowIndex(basic), out);
}
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace arith
+} // namespace theory
+} // namespace cvc5