/*********************                                                        */
/*! \file tableau.cpp
 ** \verbatim
 ** Original author: taking
 ** Major contributors: none
 ** Minor contributors (to current version): none
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** 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
 **/


#include "theory/arith/tableau.h"

using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::arith;

void Tableau::addRow(ArithVar basicVar,
                     const std::vector<Rational>& coeffs,
                     const std::vector<ArithVar>& variables){

  Assert(coeffs.size() == variables.size());
  Assert(d_basicManager.isMember(basicVar));

  //The new basic variable cannot already be a basic variable
  Assert(!d_activeBasicVars.isMember(basicVar));
  d_activeBasicVars.add(basicVar);
  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
  d_rowsTable[basicVar] = row_current;

  //A variable in the row may have been made non-basic already.
  //If this is the case we fake pivoting this variable
  vector<ArithVar>::const_iterator varsIter = variables.begin();
  vector<ArithVar>::const_iterator varsEnd = variables.end();

  for( ; varsIter != varsEnd; ++varsIter){
    ArithVar var = *varsIter;

    if(d_basicManager.isMember(var)){
      Assert(d_activeBasicVars.isMember(var));

      ReducedRowVector& row_var = lookup(var);
      row_current->substitute(row_var);
    }
  }
}

ReducedRowVector* Tableau::removeRow(ArithVar basic){
  Assert(d_basicManager.isMember(basic));
  Assert(d_activeBasicVars.isMember(basic));

  ReducedRowVector* row = d_rowsTable[basic];

  d_activeBasicVars.remove(basic);
  d_rowsTable[basic] = NULL;

  return row;
}

void Tableau::pivot(ArithVar x_r, ArithVar x_s){
  Assert(d_basicManager.isMember(x_r));
  Assert(!d_basicManager.isMember(x_s));

  Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;

  ReducedRowVector* row_s = d_rowsTable[x_r];
  Assert(row_s != NULL);
  Assert(row_s->has(x_s));

  //Swap x_r and x_s in d_activeRows
  d_rowsTable[x_s] = row_s;
  d_rowsTable[x_r] = NULL;

  d_activeBasicVars.remove(x_r);
  d_basicManager.remove(x_r);

  d_activeBasicVars.add(x_s);
  d_basicManager.add(x_s);

  row_s->pivot(x_s);

  for(ArithVarSet::iterator basicIter = begin(), endIter = end();
      basicIter != endIter; ++basicIter){
    ArithVar basic = *basicIter;
    if(basic == x_s) continue;

    ReducedRowVector& row_k = lookup(basic);
    if(row_k.has(x_s)){
      row_k.substitute(*row_s);
    }
  }
}
void Tableau::printTableau(){
  Debug("tableau") << "Tableau::d_activeRows"  << endl;

  typedef RowsTable::iterator table_iter;
  for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
      rowIter != end; ++rowIter){
    ReducedRowVector* row_k = *rowIter;
    if(row_k != NULL){
      row_k->printRow();
    }
  }
}