solverational.cpp

Go to the documentation of this file.

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/*                                                                           */
/*                  This file is part of the class library                   */
/*       SoPlex --- the Sequential object-oriented simPlex.                  */
/*                                                                           */
/*    Copyright (C) 1996-2019 Konrad-Zuse-Zentrum                            */
/*                            fuer Informationstechnik Berlin                */
/*                                                                           */
/*  SoPlex is distributed under the terms of the ZIB Academic Licence.       */
/*                                                                           */
/*  You should have received a copy of the ZIB Academic License              */
/*  along with SoPlex; see the file COPYING. If not email to soplex@zib.de.  */
/*                                                                           */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */

#include <iostream>
#include <assert.h>

#include "soplex.h"
#include "soplex/statistics.h"
#include "soplex/slufactor_rational.h"
#include "soplex/ratrecon.h"

namespace soplex
{
/// solves rational LP
void SoPlex::_optimizeRational()
{
   bool hasUnboundedRay = false;
   bool infeasibilityNotCertified = false;
   bool unboundednessNotCertified = false;

   // start timing
   _statistics->solvingTime->start();
   _statistics->preprocessingTime->start();

   // remember that last solve was rational
   _lastSolveMode = SOLVEMODE_RATIONAL;

   // ensure that the solver has the original problem
   if(!_isRealLPLoaded)
   {
      assert(_realLP != &_solver);

      _solver.loadLP(*_realLP);
      spx_free(_realLP);
      _realLP = &_solver;
      _isRealLPLoaded = true;
   }
   // during the rational solve, we always store basis information in the basis arrays
   else if(_hasBasis)
   {
      _basisStatusRows.reSize(numRowsReal());
      _basisStatusCols.reSize(numColsReal());
      _solver.getBasis(_basisStatusRows.get_ptr(), _basisStatusCols.get_ptr(), _basisStatusRows.size(),
                       _basisStatusCols.size());
   }

   // store objective, bounds, and sides of real LP in case they will be modified during iterative refinement
   _storeLPReal();

   // deactivate objective limit in floating-point solver
   if(realParam(SoPlex::OBJLIMIT_LOWER) > -realParam(SoPlex::INFTY)
         || realParam(SoPlex::OBJLIMIT_UPPER) < realParam(SoPlex::INFTY))
   {
      MSG_INFO2(spxout, spxout << "Deactivating objective limit.\n");
   }

   _solver.setTerminationValue(realParam(SoPlex::INFTY));

   _statistics->preprocessingTime->stop();

   // apply lifting to reduce range of nonzero matrix coefficients
   if(boolParam(SoPlex::LIFTING))
      _lift();

   // force column representation
   ///@todo implement row objectives with row representation
   int oldRepresentation = intParam(SoPlex::REPRESENTATION);
   setIntParam(SoPlex::REPRESENTATION, SoPlex::REPRESENTATION_COLUMN);

   // force ratio test (avoid bound flipping)
   int oldRatiotester = intParam(SoPlex::RATIOTESTER);
   setIntParam(SoPlex::RATIOTESTER, SoPlex::RATIOTESTER_FAST);

   ///@todo implement handling of row objectives in Cplex interface
#ifdef SOPLEX_WITH_CPX
   int oldEqtrans = boolParam(SoPlex::EQTRANS);
   setBoolParam(SoPlex::EQTRANS, true);
#endif

   // introduce slack variables to transform inequality constraints into equations
   if(boolParam(SoPlex::EQTRANS))
      _transformEquality();

   _storedBasis = false;

   bool stoppedTime;
   bool stoppedIter;

   do
   {
      bool primalFeasible = false;
      bool dualFeasible = false;
      bool infeasible = false;
      bool unbounded = false;
      bool error = false;
      stoppedTime = false;
      stoppedIter = false;

      // solve problem with iterative refinement and recovery mechanism
      _performOptIRStable(_solRational, !unboundednessNotCertified, !infeasibilityNotCertified, 0,
                          primalFeasible, dualFeasible, infeasible, unbounded, stoppedTime, stoppedIter, error);

      // case: an unrecoverable error occured
      if(error)
      {
         _status = SPxSolver::ERROR;
         break;
      }
      // case: stopped due to some limit
      else if(stoppedTime)
      {
         _status = SPxSolver::ABORT_TIME;
         break;
      }
      else if(stoppedIter)
      {
         _status = SPxSolver::ABORT_ITER;
         break;
      }
      // case: unboundedness detected for the first time
      else if(unbounded && !unboundednessNotCertified)
      {
         SolRational solUnbounded;

         _performUnboundedIRStable(solUnbounded, hasUnboundedRay, stoppedTime, stoppedIter, error);

         assert(!hasUnboundedRay || solUnbounded.hasPrimalRay());
         assert(!solUnbounded.hasPrimalRay() || hasUnboundedRay);

         if(error)
         {
            MSG_INFO1(spxout, spxout << "Error while testing for unboundedness.\n");
            _status = SPxSolver::ERROR;
            break;
         }

         if(hasUnboundedRay)
         {
            MSG_INFO1(spxout, spxout << "Dual infeasible.  Primal unbounded ray available.\n");
         }
         else
         {
            MSG_INFO1(spxout, spxout << "Dual feasible.  Rejecting primal unboundedness.\n");
         }

         unboundednessNotCertified = !hasUnboundedRay;

         if(stoppedTime)
         {
            _status = SPxSolver::ABORT_TIME;
            break;
         }
         else if(stoppedIter)
         {
            _status = SPxSolver::ABORT_ITER;
            break;
         }

         _performFeasIRStable(_solRational, infeasible, stoppedTime, stoppedIter, error);

         ///@todo this should be stored already earlier, possible switch use solRational above and solFeas here
         if(hasUnboundedRay)
         {
            _solRational._primalRay = solUnbounded._primalRay;
            _solRational._hasPrimalRay = true;
         }

         if(error)
         {
            MSG_INFO1(spxout, spxout << "Error while testing for feasibility.\n");
            _status = SPxSolver::ERROR;
            break;
         }
         else if(stoppedTime)
         {
            _status = SPxSolver::ABORT_TIME;
            break;
         }
         else if(stoppedIter)
         {
            _status = SPxSolver::ABORT_ITER;
            break;
         }
         else if(infeasible)
         {
            MSG_INFO1(spxout, spxout << "Primal infeasible.  Dual Farkas ray available.\n");
            _status = SPxSolver::INFEASIBLE;
            break;
         }
         else if(hasUnboundedRay)
         {
            MSG_INFO1(spxout, spxout << "Primal feasible and unbounded.\n");
            _status = SPxSolver::UNBOUNDED;
            break;
         }
         else
         {
            MSG_INFO1(spxout, spxout << "Primal feasible and bounded.\n");
            continue;
         }
      }
      // case: infeasibility detected
      else if(infeasible && !infeasibilityNotCertified)
      {
         _storeBasis();

         _performFeasIRStable(_solRational, infeasible, stoppedTime, stoppedIter, error);

         if(error)
         {
            MSG_INFO1(spxout, spxout << "Error while testing for infeasibility.\n");
            _status = SPxSolver::ERROR;
            _restoreBasis();
            break;
         }

         infeasibilityNotCertified = !infeasible;

         if(stoppedTime)
         {
            _status = SPxSolver::ABORT_TIME;
            _restoreBasis();
            break;
         }
         else if(stoppedIter)
         {
            _status = SPxSolver::ABORT_ITER;
            _restoreBasis();
            break;
         }

         if(infeasible && boolParam(SoPlex::TESTDUALINF))
         {
            SolRational solUnbounded;

            _performUnboundedIRStable(solUnbounded, hasUnboundedRay, stoppedTime, stoppedIter, error);

            assert(!hasUnboundedRay || solUnbounded.hasPrimalRay());
            assert(!solUnbounded.hasPrimalRay() || hasUnboundedRay);

            if(error)
            {
               MSG_INFO1(spxout, spxout << "Error while testing for dual infeasibility.\n");
               _status = SPxSolver::ERROR;
               _restoreBasis();
               break;
            }

            if(hasUnboundedRay)
            {
               MSG_INFO1(spxout, spxout << "Dual infeasible.  Primal unbounded ray available.\n");
               _solRational._primalRay = solUnbounded._primalRay;
               _solRational._hasPrimalRay = true;
            }
            else if(solUnbounded._isDualFeasible)
            {
               MSG_INFO1(spxout, spxout << "Dual feasible.  Storing dual multipliers.\n");
               _solRational._dual = solUnbounded._dual;
               _solRational._redCost = solUnbounded._redCost;
               _solRational._isDualFeasible = true;
            }
            else
            {
               assert(false);
               MSG_INFO1(spxout, spxout << "Not dual infeasible.\n");
            }
         }

         _restoreBasis();

         if(infeasible)
         {
            MSG_INFO1(spxout, spxout << "Primal infeasible.  Dual Farkas ray available.\n");
            _status = SPxSolver::INFEASIBLE;
            break;
         }
         else if(hasUnboundedRay)
         {
            MSG_INFO1(spxout, spxout << "Primal feasible and unbounded.\n");
            _status = SPxSolver::UNBOUNDED;
            break;
         }
         else
         {
            MSG_INFO1(spxout, spxout << "Primal feasible.  Optimizing again.\n");
            continue;
         }
      }
      else if(primalFeasible && dualFeasible)
      {
         MSG_INFO1(spxout, spxout << "Solved to optimality.\n");
         _status = SPxSolver::OPTIMAL;
         break;
      }
      else
      {
         MSG_INFO1(spxout, spxout << "Terminating without success.\n");
         break;
      }
   }
   while(!_isSolveStopped(stoppedTime, stoppedIter));

   ///@todo set status to ABORT_VALUE if optimal solution exceeds objective limit

   if(_status == SPxSolver::OPTIMAL || _status == SPxSolver::INFEASIBLE
         || _status == SPxSolver::UNBOUNDED)
      _hasSolRational = true;

   // restore original problem
   if(boolParam(SoPlex::EQTRANS))
      _untransformEquality(_solRational);

#ifdef SOPLEX_WITH_CPX
   setBoolParam(SoPlex::EQTRANS, oldEqtrans);
#endif

   // reset representation and ratio test
   setIntParam(SoPlex::REPRESENTATION, oldRepresentation);
   setIntParam(SoPlex::RATIOTESTER, oldRatiotester);

   // undo lifting
   if(boolParam(SoPlex::LIFTING))
      _project(_solRational);

   // restore objective, bounds, and sides of real LP in case they have been modified during iterative refinement
   _restoreLPReal();

   // since the real LP is loaded in the solver, we need to also pass the basis information to the solver if
   // available
   if(_hasBasis)
   {
      assert(_isRealLPLoaded);
      _solver.setBasis(_basisStatusRows.get_const_ptr(), _basisStatusCols.get_const_ptr());
      _hasBasis = (_solver.basis().status() > SPxBasis::NO_PROBLEM);
      // since setBasis always sets the basis status to regular, we need to set it manually here
      switch(_status)
      {
         case SPxSolver::OPTIMAL:
           _solver.setBasisStatus(SPxBasis::OPTIMAL);
           break;
         case SPxSolver::INFEASIBLE:
            _solver.setBasisStatus(SPxBasis::INFEASIBLE);
            break;
         case SPxSolver::UNBOUNDED:
            _solver.setBasisStatus(SPxBasis::UNBOUNDED);
            break;
         default:
            break;
      }
   }

   // stop timing
   _statistics->solvingTime->stop();
}



/// solves current problem with iterative refinement and recovery mechanism
void SoPlex::_performOptIRStable(
   SolRational& sol,
   bool acceptUnbounded,
   bool acceptInfeasible,
   int minRounds,
   bool& primalFeasible,
   bool& dualFeasible,
   bool& infeasible,
   bool& unbounded,
   bool& stoppedTime,
   bool& stoppedIter,
   bool& error)
{
   // start rational solving timing
   _statistics->rationalTime->start();

   primalFeasible = false;
   dualFeasible = false;
   infeasible = false;
   unbounded = false;
   stoppedTime = false;
   stoppedIter = false;
   error = false;

   // set working tolerances in floating-point solver
   _solver.setFeastol(realParam(SoPlex::FPFEASTOL));
   _solver.setOpttol(realParam(SoPlex::FPOPTTOL));

   // declare vectors and variables
   SPxSolver::Status result = SPxSolver::UNKNOWN;

   _modLower.reDim(numColsRational(), false);
   _modUpper.reDim(numColsRational(), false);
   _modLhs.reDim(numRowsRational(), false);
   _modRhs.reDim(numRowsRational(), false);
   _modObj.reDim(numColsRational(), false);

   DVectorReal primalReal(numColsRational());
   DVectorReal dualReal(numRowsRational());

   Rational boundsViolation;
   Rational sideViolation;
   Rational redCostViolation;
   Rational dualViolation;
   Rational primalScale;
   Rational dualScale;
   Rational maxScale;

   // solve original LP
   MSG_INFO1(spxout, spxout << "Initial floating-point solve . . .\n");

   if(_hasBasis)
   {
      assert(_basisStatusRows.size() == numRowsRational());
      assert(_basisStatusCols.size() == numColsRational());
      _solver.setBasis(_basisStatusRows.get_const_ptr(), _basisStatusCols.get_const_ptr());
      _hasBasis = (_solver.basis().status() > SPxBasis::NO_PROBLEM);
   }

   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      assert(_solver.maxRowObj(r) == 0.0);
   }

   _statistics->rationalTime->stop();
   result = _solveRealStable(acceptUnbounded, acceptInfeasible, primalReal, dualReal, _basisStatusRows,
                             _basisStatusCols, _hasBasis);

   // evaluate result
   switch(result)
   {
   case SPxSolver::OPTIMAL:
      MSG_INFO1(spxout, spxout << "Floating-point optimal.\n");
      break;

   case SPxSolver::INFEASIBLE:
      MSG_INFO1(spxout, spxout << "Floating-point infeasible.\n");

      // the floating-point solve returns a Farkas ray if and only if the simplifier was not used, which is exactly
      // the case when a basis could be returned
      if(_hasBasis)
      {
         sol._dualFarkas = dualReal;
         sol._hasDualFarkas = true;
      }
      else
         sol._hasDualFarkas = false;

      infeasible = true;
      return;

   case SPxSolver::UNBOUNDED:
      MSG_INFO1(spxout, spxout << "Floating-point unbounded.\n");
      unbounded = true;
      return;

   case SPxSolver::ABORT_TIME:
      stoppedTime = true;
      return;

   case SPxSolver::ABORT_ITER:
      stoppedIter = true;
      return;

   default:
      error = true;
      return;
   }

   _statistics->rationalTime->start();

   // store floating-point solution of original LP as current rational solution and ensure that solution vectors have
   // right dimension; ensure that solution is aligned with basis
   sol._primal.reDim(numColsRational(), false);
   sol._slacks.reDim(numRowsRational(), false);
   sol._dual.reDim(numRowsRational(), false);
   sol._redCost.reDim(numColsRational(), false);
   sol._isPrimalFeasible = true;
   sol._isDualFeasible = true;

   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      SPxSolver::VarStatus& basisStatusCol = _basisStatusCols[c];

      if(basisStatusCol == SPxSolver::ON_LOWER)
         sol._primal[c] = lowerRational(c);
      else if(basisStatusCol == SPxSolver::ON_UPPER)
         sol._primal[c] = upperRational(c);
      else if(basisStatusCol == SPxSolver::FIXED)
      {
         // it may happen that lower and upper are only equal in the real LP but different in the rational LP; we do
         // not check this to avoid rational comparisons, but simply switch the basis status to the lower bound; this
         // is necessary, because for fixed variables any reduced cost is feasible
         sol._primal[c] = lowerRational(c);
         basisStatusCol = SPxSolver::ON_LOWER;
      }
      else if(basisStatusCol == SPxSolver::ZERO)
         sol._primal[c] = 0;
      else
         sol._primal[c] = primalReal[c];
   }

   _rationalLP->computePrimalActivity(sol._primal, sol._slacks);

   int dualSize = 0;

   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      SPxSolver::VarStatus& basisStatusRow = _basisStatusRows[r];

      // it may happen that left-hand and right-hand side are different in the rational, but equal in the real LP,
      // leading to a fixed basis status; this is critical because rows with fixed basis status are ignored in the
      // computation of the dual violation; to avoid rational comparisons we do not check this but simply switch to
      // the left-hand side status
      if(basisStatusRow == SPxSolver::FIXED)
         basisStatusRow = SPxSolver::ON_LOWER;

      {
         sol._dual[r] = dualReal[r];

         if(dualReal[r] != 0.0)
            dualSize++;
      }
   }

   // we assume that the objective function vector has less nonzeros than the reduced cost vector, and so multiplying
   // with -1 first and subtracting the dual activity should be faster than adding the dual activity and negating
   // afterwards
   _rationalLP->getObj(sol._redCost);
   _rationalLP->subDualActivity(sol._dual, sol._redCost);

   // initial scaling factors are one
   primalScale = _rationalPosone;
   dualScale = _rationalPosone;

   // control progress
   Rational maxViolation;
   Rational bestViolation = _rationalPosInfty;
   const Rational violationImprovementFactor = 0.9;
   const Rational errorCorrectionFactor = 1.1;
   Rational errorCorrection = 2;
   int numFailedRefinements = 0;

   // store basis status in case solving modified problem failed
   DataArray< SPxSolver::VarStatus > basisStatusRowsFirst;
   DataArray< SPxSolver::VarStatus > basisStatusColsFirst;

   // refinement loop
   const bool maximizing = (intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MAXIMIZE);
   const int maxDimRational = numColsRational() > numRowsRational() ? numColsRational() :
                              numRowsRational();
   SolRational factorSol;
   bool factorSolNewBasis = true;
   int lastStallRefinements = 0;
   int nextRatrecRefinement = 0;

   do
   {
      // decrement minRounds counter
      minRounds--;

      MSG_DEBUG(std::cout << "Computing primal violations.\n");

      // compute violation of bounds
      boundsViolation = 0;

      for(int c = numColsRational() - 1; c >= 0; c--)
      {
         // lower bound
         assert((lowerRational(c) > _rationalNegInfty) == _lowerFinite(_colTypes[c]));

         if(_lowerFinite(_colTypes[c]))
         {
            if(lowerRational(c) == 0)
            {
               _modLower[c] = sol._primal[c];
               _modLower[c] *= -1;

               if(_modLower[c] > boundsViolation)
                  boundsViolation = _modLower[c];
            }
            else
            {
               _modLower[c] = lowerRational(c);
               _modLower[c] -= sol._primal[c];

               if(_modLower[c] > boundsViolation)
                  boundsViolation = _modLower[c];
            }
         }

         // upper bound
         assert((upperRational(c) < _rationalPosInfty) == _upperFinite(_colTypes[c]));

         if(_upperFinite(_colTypes[c]))
         {
            if(upperRational(c) == 0)
            {
               _modUpper[c] = sol._primal[c];
               _modUpper[c] *= -1;

               if(_modUpper[c] < -boundsViolation)
                  boundsViolation = -_modUpper[c];
            }
            else
            {
               _modUpper[c] = upperRational(c);
               _modUpper[c] -= sol._primal[c];

               if(_modUpper[c] < -boundsViolation)
                  boundsViolation = -_modUpper[c];
            }
         }
      }

      // compute violation of sides
      sideViolation = 0;

      for(int r = numRowsRational() - 1; r >= 0; r--)
      {
         const SPxSolver::VarStatus& basisStatusRow = _basisStatusRows[r];

         // left-hand side
         assert((lhsRational(r) > _rationalNegInfty) == _lowerFinite(_rowTypes[r]));

         if(_lowerFinite(_rowTypes[r]))
         {
            if(lhsRational(r) == 0)
            {
               _modLhs[r] = sol._slacks[r];
               _modLhs[r] *= -1;
            }
            else
            {
               _modLhs[r] = lhsRational(r);
               _modLhs[r] -= sol._slacks[r];
            }

            if(_modLhs[r] > sideViolation)
               sideViolation = _modLhs[r];
            // if the activity is feasible, but too far from the bound, this violates complementary slackness; we
            // count it as side violation here
            else if(basisStatusRow == SPxSolver::ON_LOWER && _modLhs[r] < -sideViolation)
               sideViolation = -_modLhs[r];
         }

         // right-hand side
         assert((rhsRational(r) < _rationalPosInfty) == _upperFinite(_rowTypes[r]));

         if(_upperFinite(_rowTypes[r]))
         {
            if(rhsRational(r) == 0)
            {
               _modRhs[r] = sol._slacks[r];
               _modRhs[r] *= -1;
            }
            else
            {
               _modRhs[r] = rhsRational(r);
               _modRhs[r] -= sol._slacks[r];
            }

            if(_modRhs[r] < -sideViolation)
               sideViolation = -_modRhs[r];
            // if the activity is feasible, but too far from the bound, this violates complementary slackness; we
            // count it as side violation here
            else if(basisStatusRow == SPxSolver::ON_UPPER && _modRhs[r] > sideViolation)
               sideViolation = _modRhs[r];
         }
      }

      MSG_DEBUG(std::cout << "Computing dual violations.\n");

      // compute reduced cost violation
      redCostViolation = 0;

      for(int c = numColsRational() - 1; c >= 0; c--)
      {
         if(_colTypes[c] == RANGETYPE_FIXED)
            continue;

         const SPxSolver::VarStatus& basisStatusCol = _basisStatusCols[c];
         assert(basisStatusCol != SPxSolver::FIXED);

         if(((maximizing && basisStatusCol != SPxSolver::ON_LOWER) || (!maximizing
               && basisStatusCol != SPxSolver::ON_UPPER))
               && sol._redCost[c] < -redCostViolation)
         {
            MSG_DEBUG(std::cout << "basisStatusCol = " << basisStatusCol
                      << ", lower tight = " << bool(sol._primal[c] <= lowerRational(c))
                      << ", upper tight = " << bool(sol._primal[c] >= upperRational(c))
                      << ", sol._redCost[c] = " << rationalToString(sol._redCost[c])
                      << "\n");
            redCostViolation = -sol._redCost[c];
         }

         if(((maximizing && basisStatusCol != SPxSolver::ON_UPPER) || (!maximizing
               && basisStatusCol != SPxSolver::ON_LOWER))
               && sol._redCost[c] > redCostViolation)
         {
            MSG_DEBUG(std::cout << "basisStatusCol = " << basisStatusCol
                      << ", lower tight = " << bool(sol._primal[c] <= lowerRational(c))
                      << ", upper tight = " << bool(sol._primal[c] >= upperRational(c))
                      << ", sol._redCost[c] = " << rationalToString(sol._redCost[c])
                      << "\n");
            redCostViolation = sol._redCost[c];
         }
      }

      // compute dual violation
      dualViolation = 0;

      for(int r = numRowsRational() - 1; r >= 0; r--)
      {
         if(_rowTypes[r] == RANGETYPE_FIXED)
            continue;

         const SPxSolver::VarStatus& basisStatusRow = _basisStatusRows[r];
         assert(basisStatusRow != SPxSolver::FIXED);

         if(((maximizing && basisStatusRow != SPxSolver::ON_LOWER) || (!maximizing
               && basisStatusRow != SPxSolver::ON_UPPER))
               && sol._dual[r] < -dualViolation)
         {
            MSG_DEBUG(std::cout << "basisStatusRow = " << basisStatusRow
                      << ", lower tight = " << bool(sol._slacks[r] <= lhsRational(r))
                      << ", upper tight = " << bool(sol._slacks[r] >= rhsRational(r))
                      << ", sol._dual[r] = " << rationalToString(sol._dual[r])
                      << "\n");
            dualViolation = -sol._dual[r];
         }

         if(((maximizing && basisStatusRow != SPxSolver::ON_UPPER) || (!maximizing
               && basisStatusRow != SPxSolver::ON_LOWER))
               && sol._dual[r] > dualViolation)
         {
            MSG_DEBUG(std::cout << "basisStatusRow = " << basisStatusRow
                      << ", lower tight = " << bool(sol._slacks[r] <= lhsRational(r))
                      << ", upper tight = " << bool(sol._slacks[r] >= rhsRational(r))
                      << ", sol._dual[r] = " << rationalToString(sol._dual[r])
                      << "\n");
            dualViolation = sol._dual[r];
         }
      }

      _modObj = sol._redCost;

      // output violations; the reduced cost violations for artificially introduced slack columns are actually violations of the dual multipliers
      MSG_INFO1(spxout, spxout
                << "Max. bound violation = " << rationalToString(boundsViolation) << "\n"
                << "Max. row violation = " << rationalToString(sideViolation) << "\n"
                << "Max. reduced cost violation = " << rationalToString(redCostViolation) << "\n"
                << "Max. dual violation = " << rationalToString(dualViolation) << "\n");

      MSG_DEBUG(spxout
                << std::fixed << std::setprecision(2) << std::setw(10)
                << "Progress table: "
                << std::setw(10) << _statistics->refinements << " & "
                << std::setw(10) << _statistics->iterations << " & "
                << std::setw(10) << _statistics->solvingTime->time() << " & "
                << std::setw(10) << _statistics->rationalTime->time() << " & "
                << std::setw(10) << rationalToString(boundsViolation > sideViolation ? boundsViolation :
                      sideViolation, 2) << " & "
                << std::setw(10) << rationalToString(redCostViolation > dualViolation ? redCostViolation :
                      dualViolation, 2) << "\n");

      // terminate if tolerances are satisfied
      primalFeasible = (boundsViolation <= _rationalFeastol && sideViolation <= _rationalFeastol);
      dualFeasible = (redCostViolation <= _rationalOpttol && dualViolation <= _rationalOpttol);

      if(primalFeasible && dualFeasible)
      {
         if(minRounds < 0)
         {
            MSG_INFO1(spxout, spxout << "Tolerances reached.\n");
            break;
         }
         else
         {
            MSG_INFO1(spxout, spxout <<
                      "Tolerances reached but minRounds forcing additional refinement rounds.\n");
         }
      }

      // terminate if some limit is reached
      if(_isSolveStopped(stoppedTime, stoppedIter))
         break;

      // check progress
      maxViolation = boundsViolation;

      if(sideViolation > maxViolation)
         maxViolation = sideViolation;

      if(redCostViolation > maxViolation)
         maxViolation = redCostViolation;

      if(dualViolation > maxViolation)
         maxViolation = dualViolation;

      bestViolation *= violationImprovementFactor;

      if(maxViolation > bestViolation)
      {
         MSG_INFO2(spxout, spxout << "Failed to reduce violation significantly.\n");
         numFailedRefinements++;
      }
      else
         bestViolation = maxViolation;

      // decide whether to perform rational reconstruction and/or factorization
      bool performRatfac = boolParam(SoPlex::RATFAC)
                           && lastStallRefinements >= intParam(SoPlex::RATFAC_MINSTALLS) && _hasBasis && factorSolNewBasis;
      bool performRatrec = boolParam(SoPlex::RATREC)
                           && (_statistics->refinements >= nextRatrecRefinement || performRatfac);

      // attempt rational reconstruction
      errorCorrection *= errorCorrectionFactor;

      if(performRatrec && maxViolation > 0)
      {
         MSG_INFO1(spxout, spxout << "Performing rational reconstruction . . .\n");

         maxViolation *= errorCorrection; // only used for sign check later
         maxViolation.invert();

         if(_reconstructSolutionRational(sol, _basisStatusRows, _basisStatusCols, maxViolation))
         {
            MSG_INFO1(spxout, spxout << "Tolerances reached.\n");
            primalFeasible = true;
            dualFeasible = true;
            break;
         }

         nextRatrecRefinement = int(_statistics->refinements * realParam(SoPlex::RATREC_FREQ)) + 1;
         MSG_DEBUG(spxout << "Next rational reconstruction after refinement " << nextRatrecRefinement <<
                   ".\n");
      }

      // solve basis systems exactly
      if(performRatfac && maxViolation > 0)
      {
         MSG_INFO1(spxout, spxout << "Performing rational factorization . . .\n");

         bool optimal;
         _factorizeColumnRational(sol, _basisStatusRows, _basisStatusCols, stoppedTime, stoppedIter, error,
                                  optimal);
         factorSolNewBasis = false;

         if(stoppedTime)
         {
            MSG_INFO1(spxout, spxout << "Stopped rational factorization.\n");
         }
         else if(error)
         {
            // message was already printed; reset error flag and continue without factorization
            error = false;
         }
         else if(optimal)
         {
            MSG_INFO1(spxout, spxout << "Tolerances reached.\n");
            primalFeasible = true;
            dualFeasible = true;
            break;
         }
         else if(boolParam(SoPlex::RATFACJUMP))
         {
            MSG_INFO1(spxout, spxout << "Jumping to exact basic solution.\n");
            minRounds++;
            continue;
         }
      }

      // start refinement

      // compute primal scaling factor; limit increase in scaling by tolerance used in floating point solve
      maxScale = primalScale;
      maxScale *= _rationalMaxscaleincr;

      primalScale = boundsViolation > sideViolation ? boundsViolation : sideViolation;

      if(primalScale < redCostViolation)
         primalScale = redCostViolation;

      assert(primalScale >= 0);

      if(primalScale > 0)
      {
         primalScale.invert();

         if(primalScale > maxScale)
            primalScale = maxScale;
      }
      else
         primalScale = maxScale;

      if(boolParam(SoPlex::POWERSCALING))
         primalScale.powRound();

      // apply scaled bounds
      if(primalScale <= 1)
      {
         if(primalScale < 1)
            primalScale = 1;

         for(int c = numColsRational() - 1; c >= 0; c--)
         {
            if(_lowerFinite(_colTypes[c]))
            {
               if(_modLower[c] <= _rationalNegInfty)
                  _solver.changeLower(c, -realParam(SoPlex::INFTY));
               else
                  _solver.changeLower(c, Real(_modLower[c]));
            }

            if(_upperFinite(_colTypes[c]))
            {
               if(_modUpper[c] >= _rationalPosInfty)
                  _solver.changeUpper(c, realParam(SoPlex::INFTY));
               else
                  _solver.changeUpper(c, Real(_modUpper[c]));
            }
         }
      }
      else
      {
         MSG_INFO2(spxout, spxout << "Scaling primal by " << rationalToString(primalScale) << ".\n");

         for(int c = numColsRational() - 1; c >= 0; c--)
         {
            if(_lowerFinite(_colTypes[c]))
            {
               _modLower[c] *= primalScale;

               if(_modLower[c] <= _rationalNegInfty)
                  _solver.changeLower(c, -realParam(SoPlex::INFTY));
               else
                  _solver.changeLower(c, Real(_modLower[c]));
            }

            if(_upperFinite(_colTypes[c]))
            {
               _modUpper[c] *= primalScale;

               if(_modUpper[c] >= _rationalPosInfty)
                  _solver.changeUpper(c, realParam(SoPlex::INFTY));
               else
                  _solver.changeUpper(c, Real(_modUpper[c]));
            }
         }
      }

      // apply scaled sides
      assert(primalScale >= 1);

      if(primalScale == 1)
      {
         for(int r = numRowsRational() - 1; r >= 0; r--)
         {
            if(_lowerFinite(_rowTypes[r]))
            {
               if(_modLhs[r] <= _rationalNegInfty)
                  _solver.changeLhs(r, -realParam(SoPlex::INFTY));
               else
                  _solver.changeLhs(r, Real(_modLhs[r]));
            }

            if(_upperFinite(_rowTypes[r]))
            {
               if(_modRhs[r] >= _rationalPosInfty)
                  _solver.changeRhs(r, realParam(SoPlex::INFTY));
               else
                  _solver.changeRhs(r, Real(_modRhs[r]));
            }
         }
      }
      else
      {
         for(int r = numRowsRational() - 1; r >= 0; r--)
         {
            if(_lowerFinite(_rowTypes[r]))
            {
               _modLhs[r] *= primalScale;

               if(_modLhs[r] <= _rationalNegInfty)
                  _solver.changeLhs(r, -realParam(SoPlex::INFTY));
               else
                  _solver.changeLhs(r, Real(_modLhs[r]));
            }

            if(_upperFinite(_rowTypes[r]))
            {
               _modRhs[r] *= primalScale;

               if(_modRhs[r] >= _rationalPosInfty)
                  _solver.changeRhs(r, realParam(SoPlex::INFTY));
               else
                  _solver.changeRhs(r, Real(_modRhs[r]));
            }
         }
      }

      // compute dual scaling factor; limit increase in scaling by tolerance used in floating point solve
      maxScale = dualScale;
      maxScale *= _rationalMaxscaleincr;

      dualScale = redCostViolation > dualViolation ? redCostViolation : dualViolation;
      assert(dualScale >= 0);

      if(dualScale > 0)
      {
         dualScale.invert();

         if(dualScale > maxScale)
            dualScale = maxScale;
      }
      else
         dualScale = maxScale;

      if(boolParam(SoPlex::POWERSCALING))
         dualScale.powRound();

      if(dualScale > primalScale)
         dualScale = primalScale;

      if(dualScale < 1)
         dualScale = 1;
      else
      {
         MSG_INFO2(spxout, spxout << "Scaling dual by " << rationalToString(dualScale) << ".\n");

         // perform dual scaling
         ///@todo remove _modObj and use dualScale * sol._redCost directly
         _modObj *= dualScale;
      }

      // apply scaled objective function
      for(int c = numColsRational() - 1; c >= 0; c--)
      {
         if(_modObj[c] >= _rationalPosInfty)
            _solver.changeObj(c, realParam(SoPlex::INFTY));
         else if(_modObj[c] <= _rationalNegInfty)
            _solver.changeObj(c, -realParam(SoPlex::INFTY));
         else
            _solver.changeObj(c, Real(_modObj[c]));
      }

      for(int r = numRowsRational() - 1; r >= 0; r--)
      {
         Rational newRowObj;

         if(_rowTypes[r] == RANGETYPE_FIXED)
            _solver.changeRowObj(r, 0.0);
         else
         {
            newRowObj = sol._dual[r];
            newRowObj *= dualScale;

            if(newRowObj >= _rationalPosInfty)
               _solver.changeRowObj(r, -realParam(SoPlex::INFTY));
            else if(newRowObj <= _rationalNegInfty)
               _solver.changeRowObj(r, realParam(SoPlex::INFTY));
            else
               _solver.changeRowObj(r, -Real(newRowObj));
         }
      }

      MSG_INFO1(spxout, spxout << "Refined floating-point solve . . .\n");

      // ensure that artificial slack columns are basic and inequality constraints are nonbasic; otherwise we may end
      // up with dual violation on inequality constraints after removing the slack columns; do not change this in the
      // floating-point solver, though, because the solver may require its original basis to detect optimality
      if(_slackCols.num() > 0 && _hasBasis)
      {
         int numOrigCols = numColsRational() - _slackCols.num();
         assert(_slackCols.num() <= 0 || boolParam(SoPlex::EQTRANS));

         for(int i = 0; i < _slackCols.num(); i++)
         {
            int row = _slackCols.colVector(i).index(0);
            int col = numOrigCols + i;

            assert(row >= 0);
            assert(row < numRowsRational());

            if(_basisStatusRows[row] == SPxSolver::BASIC && _basisStatusCols[col] != SPxSolver::BASIC)
            {
               _basisStatusRows[row] = _basisStatusCols[col];
               _basisStatusCols[col] = SPxSolver::BASIC;
               _rationalLUSolver.clear();
            }
         }
      }

      // load basis
      if(_hasBasis && _solver.basis().status() < SPxBasis::REGULAR)
      {
         MSG_DEBUG(spxout << "basis (status = " << _solver.basis().status() << ") desc before set:\n";
                   _solver.basis().desc().dump());
         _solver.setBasis(_basisStatusRows.get_const_ptr(), _basisStatusCols.get_const_ptr());
         MSG_DEBUG(spxout << "basis (status = " << _solver.basis().status() << ") desc after set:\n";
                   _solver.basis().desc().dump());

         _hasBasis = _solver.basis().status() > SPxBasis::NO_PROBLEM;
         MSG_DEBUG(spxout << "setting basis in solver " << (_hasBasis ? "successful" : "failed") <<
                   " (3)\n");
      }

      // solve modified problem
      int prevIterations = _statistics->iterations;
      _statistics->rationalTime->stop();
      result = _solveRealStable(acceptUnbounded, acceptInfeasible, primalReal, dualReal, _basisStatusRows,
                                _basisStatusCols, _hasBasis, primalScale > 1e20 || dualScale > 1e20);

      // count refinements and remember whether we moved to a new basis
      _statistics->refinements++;

      if(_statistics->iterations <= prevIterations)
      {
         lastStallRefinements++;
         _statistics->stallRefinements++;
      }
      else
      {
         factorSolNewBasis = true;
         lastStallRefinements = 0;
         _statistics->pivotRefinements = _statistics->refinements;
      }

      // evaluate result; if modified problem was not solved to optimality, stop refinement
      switch(result)
      {
      case SPxSolver::OPTIMAL:
         MSG_INFO1(spxout, spxout << "Floating-point optimal.\n");
         break;

      case SPxSolver::INFEASIBLE:
         MSG_INFO1(spxout, spxout << "Floating-point infeasible.\n");
         sol._dualFarkas = dualReal;
         sol._hasDualFarkas = true;
         infeasible = true;
         _solver.clearRowObjs();
         return;

      case SPxSolver::UNBOUNDED:
         MSG_INFO1(spxout, spxout << "Floating-point unbounded.\n");
         unbounded = true;
         _solver.clearRowObjs();
         return;

      case SPxSolver::ABORT_TIME:
         stoppedTime = true;
         return;

      case SPxSolver::ABORT_ITER:
         stoppedIter = true;
         _solver.clearRowObjs();
         return;

      default:
         error = true;
         _solver.clearRowObjs();
         return;
      }

      _statistics->rationalTime->start();

      // correct primal solution and align with basis
      MSG_DEBUG(std::cout << "Correcting primal solution.\n");

      int primalSize = 0;
      Rational primalScaleInverse = primalScale;
      primalScaleInverse.invert();
      _primalDualDiff.clear();

      for(int c = numColsRational() - 1; c >= 0; c--)
      {
         // force values of nonbasic variables to bounds
         SPxSolver::VarStatus& basisStatusCol = _basisStatusCols[c];

         if(basisStatusCol == SPxSolver::ON_LOWER)
         {
            if(sol._primal[c] != lowerRational(c))
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = lowerRational(c);
               _primalDualDiff.value(i) -= sol._primal[c];
               sol._primal[c] = lowerRational(c);
            }
         }
         else if(basisStatusCol == SPxSolver::ON_UPPER)
         {
            if(sol._primal[c] != upperRational(c))
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = upperRational(c);
               _primalDualDiff.value(i) -= sol._primal[c];
               sol._primal[c] = upperRational(c);
            }
         }
         else if(basisStatusCol == SPxSolver::FIXED)
         {
            // it may happen that lower and upper are only equal in the real LP but different in the rational LP; we
            // do not check this to avoid rational comparisons, but simply switch the basis status to the lower
            // bound; this is necessary, because for fixed variables any reduced cost is feasible
            basisStatusCol = SPxSolver::ON_LOWER;

            if(sol._primal[c] != lowerRational(c))
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = lowerRational(c);
               _primalDualDiff.value(i) -= sol._primal[c];
               sol._primal[c] = lowerRational(c);
            }
         }
         else if(basisStatusCol == SPxSolver::ZERO)
         {
            if(sol._primal[c] != 0)
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = sol._primal[c];
               _primalDualDiff.value(i) *= -1;
               sol._primal[c] = 0;
            }
         }
         else
         {
            if(primalReal[c] == 1.0)
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = primalScaleInverse;
               sol._primal[c] += _primalDualDiff.value(i);
            }
            else if(primalReal[c] == -1.0)
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = primalScaleInverse;
               _primalDualDiff.value(i) *= -1;
               sol._primal[c] += _primalDualDiff.value(i);
            }
            else if(primalReal[c] != 0.0)
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(c);
               _primalDualDiff.value(i) = primalReal[c];
               _primalDualDiff.value(i) *= primalScaleInverse;
               sol._primal[c] += _primalDualDiff.value(i);
            }
         }

         if(sol._primal[c] != 0)
            primalSize++;
      }

      // update or recompute slacks depending on which looks faster
      if(_primalDualDiff.size() < primalSize)
      {
         _rationalLP->addPrimalActivity(_primalDualDiff, sol._slacks);
#ifndef NDEBUG
#ifdef SOPLEX_WITH_GMP
         {
            DVectorRational activity(numRowsRational());
            _rationalLP->computePrimalActivity(sol._primal, activity);
            assert(sol._slacks == activity);
         }
#endif
#endif
      }
      else
         _rationalLP->computePrimalActivity(sol._primal, sol._slacks);

      const int numCorrectedPrimals = _primalDualDiff.size();

      // correct dual solution and align with basis
      MSG_DEBUG(std::cout << "Correcting dual solution.\n");

#ifndef NDEBUG
      {
         // compute reduced cost violation
         DVectorRational debugRedCost(numColsRational());
         debugRedCost = DVectorRational(_realLP->maxObj());
         debugRedCost *= -1;
         _rationalLP->subDualActivity(DVectorRational(dualReal), debugRedCost);

         Rational debugRedCostViolation = 0;

         for(int c = numColsRational() - 1; c >= 0; c--)
         {
            if(_colTypes[c] == RANGETYPE_FIXED)
               continue;

            const SPxSolver::VarStatus& basisStatusCol = _basisStatusCols[c];
            assert(basisStatusCol != SPxSolver::FIXED);

            if(((maximizing && basisStatusCol != SPxSolver::ON_LOWER) || (!maximizing
                  && basisStatusCol != SPxSolver::ON_UPPER))
                  && debugRedCost[c] < -debugRedCostViolation)
            {
               MSG_DEBUG(std::cout << "basisStatusCol = " << basisStatusCol
                         << ", lower tight = " << bool(sol._primal[c] <= lowerRational(c))
                         << ", upper tight = " << bool(sol._primal[c] >= upperRational(c))
                         << ", obj[c] = " << _realLP->obj(c)
                         << ", debugRedCost[c] = " << rationalToString(debugRedCost[c])
                         << "\n");
               debugRedCostViolation = -debugRedCost[c];
            }

            if(((maximizing && basisStatusCol != SPxSolver::ON_UPPER) || (!maximizing
                  && basisStatusCol != SPxSolver::ON_LOWER))
                  && debugRedCost[c] > debugRedCostViolation)
            {
               MSG_DEBUG(std::cout << "basisStatusCol = " << basisStatusCol
                         << ", lower tight = " << bool(sol._primal[c] <= lowerRational(c))
                         << ", upper tight = " << bool(sol._primal[c] >= upperRational(c))
                         << ", obj[c] = " << _realLP->obj(c)
                         << ", debugRedCost[c] = " << rationalToString(debugRedCost[c])
                         << "\n");
               debugRedCostViolation = debugRedCost[c];
            }
         }

         // compute dual violation
         Rational debugDualViolation = 0;
         Rational debugBasicDualViolation = 0;

         for(int r = numRowsRational() - 1; r >= 0; r--)
         {
            if(_rowTypes[r] == RANGETYPE_FIXED)
               continue;

            const SPxSolver::VarStatus& basisStatusRow = _basisStatusRows[r];
            assert(basisStatusRow != SPxSolver::FIXED);

            Rational val = (-dualScale * sol._dual[r]) - Rational(dualReal[r]);

            if(((maximizing && basisStatusRow != SPxSolver::ON_LOWER) || (!maximizing
                  && basisStatusRow != SPxSolver::ON_UPPER))
                  && val > debugDualViolation)
            {
               MSG_DEBUG(std::cout << "basisStatusRow = " << basisStatusRow
                         << ", lower tight = " << bool(sol._slacks[r] <= lhsRational(r))
                         << ", upper tight = " << bool(sol._slacks[r] >= rhsRational(r))
                         << ", dualReal[r] = " << rationalToString(val)
                         << ", dualReal[r] = " << dualReal[r]
                         << "\n");
               debugDualViolation = val;
            }

            if(((maximizing && basisStatusRow != SPxSolver::ON_UPPER) || (!maximizing
                  && basisStatusRow != SPxSolver::ON_LOWER))
                  && val < -debugDualViolation)
            {
               MSG_DEBUG(std::cout << "basisStatusRow = " << basisStatusRow
                         << ", lower tight = " << bool(sol._slacks[r] <= lhsRational(r))
                         << ", upper tight = " << bool(sol._slacks[r] >= rhsRational(r))
                         << ", dualReal[r] = " << rationalToString(val)
                         << ", dualReal[r] = " << dualReal[r]
                         << "\n");
               debugDualViolation = -val;
            }

            if(basisStatusRow == SPxSolver::BASIC && spxAbs(val) > debugBasicDualViolation)
            {
               MSG_DEBUG(std::cout << "basisStatusRow = " << basisStatusRow
                         << ", lower tight = " << bool(sol._slacks[r] <= lhsRational(r))
                         << ", upper tight = " << bool(sol._slacks[r] >= rhsRational(r))
                         << ", dualReal[r] = " << rationalToString(val)
                         << ", dualReal[r] = " << dualReal[r]
                         << "\n");
               debugBasicDualViolation = spxAbs(val);
            }
         }

         if(debugRedCostViolation > _solver.opttol() || debugDualViolation > _solver.opttol()
               || debugBasicDualViolation > 1e-9)
         {
            MSG_WARNING(spxout, spxout << "Warning: floating-point dual solution with violation "
                        << rationalToString(debugRedCostViolation) << " / "
                        << rationalToString(debugDualViolation) << " / "
                        << rationalToString(debugBasicDualViolation)
                        << " (red. cost, dual, basic).\n");
         }
      }
#endif

      Rational dualScaleInverseNeg = dualScale;
      dualScaleInverseNeg.invert();
      dualScaleInverseNeg *= -1;
      _primalDualDiff.clear();
      dualSize = 0;

      for(int r = numRowsRational() - 1; r >= 0; r--)
      {
         SPxSolver::VarStatus& basisStatusRow = _basisStatusRows[r];

         // it may happen that left-hand and right-hand side are different in the rational, but equal in the real LP,
         // leading to a fixed basis status; this is critical because rows with fixed basis status are ignored in the
         // computation of the dual violation; to avoid rational comparisons we do not check this but simply switch
         // to the left-hand side status
         if(basisStatusRow == SPxSolver::FIXED)
            basisStatusRow = SPxSolver::ON_LOWER;

         {
            if(dualReal[r] != 0)
            {
               int i = _primalDualDiff.size();
               _ensureDSVectorRationalMemory(_primalDualDiff, maxDimRational);
               _primalDualDiff.add(r);
               _primalDualDiff.value(i) = dualReal[r];
               _primalDualDiff.value(i) *= dualScaleInverseNeg;
               sol._dual[r] -= _primalDualDiff.value(i);

               dualSize++;
            }
            else
            {
               // we do not check whether the dual value is nonzero, because it probably is; this gives us an
               // overestimation of the number of nonzeros in the dual solution
               dualSize++;
            }
         }
      }

      // update or recompute reduced cost values depending on which looks faster; adding one to the length of the
      // dual vector accounts for the objective function vector
      if(_primalDualDiff.size() < dualSize + 1)
      {
         _rationalLP->addDualActivity(_primalDualDiff, sol._redCost);
#ifndef NDEBUG
         {
            DVectorRational activity(_rationalLP->maxObj());
            activity *= -1;
            _rationalLP->subDualActivity(sol._dual, activity);
         }
#endif
      }
      else
      {
         // we assume that the objective function vector has less nonzeros than the reduced cost vector, and so multiplying
         // with -1 first and subtracting the dual activity should be faster than adding the dual activity and negating
         // afterwards
         _rationalLP->getObj(sol._redCost);
         _rationalLP->subDualActivity(sol._dual, sol._redCost);
      }

      const int numCorrectedDuals = _primalDualDiff.size();

      if(numCorrectedPrimals + numCorrectedDuals > 0)
      {
         MSG_INFO2(spxout, spxout << "Corrected " << numCorrectedPrimals << " primal variables and " <<
                   numCorrectedDuals << " dual values.\n");
      }
   }
   while(true);

   // correct basis status for restricted inequalities
   if(_hasBasis)
   {
      for(int r = numRowsRational() - 1; r >= 0; r--)
      {
         assert((lhsRational(r) == rhsRational(r)) == (_rowTypes[r] == RANGETYPE_FIXED));

         if(_rowTypes[r] != RANGETYPE_FIXED && _basisStatusRows[r] == SPxSolver::FIXED)
            _basisStatusRows[r] = (maximizing == (sol._dual[r] < 0))
                                  ? SPxSolver::ON_LOWER
                                  : SPxSolver::ON_UPPER;
      }
   }

   // compute objective function values
   assert(sol._isPrimalFeasible == sol._isDualFeasible);

   if(sol._isPrimalFeasible)
   {
      sol._objVal = sol._primal * _rationalLP->maxObj();

      if(intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MINIMIZE)
         sol._objVal *= -1;
   }

   // set objective coefficients for all rows to zero
   _solver.clearRowObjs();

   // stop rational solving time
   _statistics->rationalTime->stop();
}



/// performs iterative refinement on the auxiliary problem for testing unboundedness
void SoPlex::_performUnboundedIRStable(
   SolRational& sol,
   bool& hasUnboundedRay,
   bool& stopped,
   bool& stoppedIter,
   bool& error)
{
   bool primalFeasible;
   bool dualFeasible;
   bool infeasible;
   bool unbounded;

   // move objective function to constraints and adjust sides and bounds
   _transformUnbounded();

   // invalidate solution
   sol.invalidate();

   // remember current number of refinements
   int oldRefinements = _statistics->refinements;

   // perform iterative refinement
   _performOptIRStable(sol, false, false, 0, primalFeasible, dualFeasible, infeasible, unbounded,
                       stopped, stoppedIter, error);

   // update unbounded refinement counter
   _statistics->unbdRefinements += _statistics->refinements - oldRefinements;

   // stopped due to some limit
   if(stopped)
   {
      sol.invalidate();
      hasUnboundedRay = false;
      error = false;
   }
   // the unbounded problem should always be solved to optimality
   else if(error || unbounded || infeasible || !primalFeasible || !dualFeasible)
   {
      sol.invalidate();
      hasUnboundedRay = false;
      stopped = false;
      error = true;
   }
   else
   {
      const Rational& tau = sol._primal[numColsRational() - 1];

      MSG_DEBUG(std::cout << "tau = " << tau << " (roughly " << rationalToString(tau) << ")\n");

      assert(tau <= 1.0 + 2.0 * realParam(SoPlex::FEASTOL));
      assert(tau >= -realParam(SoPlex::FEASTOL));

      // because the right-hand side and all bounds (but tau's upper bound) are zero, tau should be approximately
      // zero if basic; otherwise at its upper bound 1
      error = !(tau >= _rationalPosone || tau <= _rationalFeastol);
      assert(!error);

      hasUnboundedRay = (tau >= 1);
   }

   // restore problem
   _untransformUnbounded(sol, hasUnboundedRay);
}



/// performs iterative refinement on the auxiliary problem for testing feasibility
void SoPlex::_performFeasIRStable(
   SolRational& sol,
   bool& withDualFarkas,
   bool& stopped,
   bool& stoppedIter,
   bool& error)
{
   bool primalFeasible;
   bool dualFeasible;
   bool infeasible;
   bool unbounded;
   bool success = false;
   error = false;

#if 0
   // if the problem has been found to be infeasible and an approximate Farkas proof is available, we compute a
   // scaled unit box around the origin that provably contains no feasible solution; this currently only works for
   // equality form
   ///@todo check whether approximate Farkas proof can be used
   _computeInfeasBox(_solRational, false);
   ///@todo if approx Farkas proof is good enough then exit without doing any transformation
#endif

   // remove objective function, shift, homogenize
   _transformFeasibility();

   // invalidate solution
   sol.invalidate();

   do
   {
      // remember current number of refinements
      int oldRefinements = _statistics->refinements;

      // perform iterative refinement
      _performOptIRStable(sol, false, false, 0, primalFeasible, dualFeasible, infeasible, unbounded,
                          stopped, stoppedIter, error);

      // update feasible refinement counter
      _statistics->feasRefinements += _statistics->refinements - oldRefinements;

      // stopped due to some limit
      if(stopped)
      {
         sol.invalidate();
         withDualFarkas = false;
         error = false;
      }
      // the feasibility problem should always be solved to optimality
      else if(error || unbounded || infeasible || !primalFeasible || !dualFeasible)
      {
         sol.invalidate();
         withDualFarkas = false;
         stopped = false;
         error = true;
      }
      // else we should have either a refined Farkas proof or an approximate feasible solution to the original
      else
      {
         const Rational& tau = sol._primal[numColsRational() - 1];

         MSG_DEBUG(std::cout << "tau = " << tau << " (roughly " << rationalToString(tau) << ")\n");

         assert(tau >= -realParam(SoPlex::FEASTOL));
         assert(tau <= 1.0 + realParam(SoPlex::FEASTOL));

         error = (tau < -_rationalFeastol || tau > _rationalPosone + _rationalFeastol);
         withDualFarkas = (tau < _rationalPosone);

         if(withDualFarkas)
         {
            _solRational._hasDualFarkas = true;
            _solRational._dualFarkas = _solRational._dual;

#if 0
            // check if we can compute sufficiently large Farkas box
            _computeInfeasBox(_solRational, true);
#endif

            if(true)  //@todo check if computeInfeasBox found a sufficient box
            {

               success = true;
               sol._isPrimalFeasible = false;
            }
         }
         else
         {
            sol._isDualFeasible = false;
            success = true; //successfully found approximate feasible solution
         }
      }
   }
   while(!error && !success && !stopped);

   // restore problem
   _untransformFeasibility(sol, withDualFarkas);
}



/// reduces matrix coefficient in absolute value by the lifting procedure of Thiele et al. 2013
void SoPlex::_lift()
{
   MSG_DEBUG(std::cout << "Reducing matrix coefficients by lifting.\n");

   // start timing
   _statistics->transformTime->start();

   MSG_DEBUG(_realLP->writeFile("beforeLift.lp", 0, 0, 0));

   // remember unlifted state
   _beforeLiftCols = numColsRational();
   _beforeLiftRows = numRowsRational();

   // allocate vector memory
   DSVectorRational colVector;
   SVectorRational::Element liftingRowMem[2];
   SVectorRational liftingRowVector(2, liftingRowMem);

   // search each column for large nonzeros entries
   const Rational maxValue = realParam(SoPlex::LIFTMAXVAL);

   for(int i = 0; i < numColsRational(); i++)
   {
      MSG_DEBUG(std::cout << "in lifting: examining column " << i << "\n");

      // get column vector
      colVector = colVectorRational(i);

      bool addedLiftingRow = false;
      int liftingColumnIndex = -1;

      // go through nonzero entries of the column
      for(int k = colVector.size() - 1; k >= 0; k--)
      {
         const Rational& value = colVector.value(k);

         if(spxAbs(value) > maxValue)
         {
            MSG_DEBUG(std::cout << "   --> nonzero " << k << " has value " << rationalToString(
                         value) << " in row " << colVector.index(k) << "\n");

            // add new column equal to maxValue times original column
            if(!addedLiftingRow)
            {
               MSG_DEBUG(std::cout << "            --> adding lifting row\n");

               assert(liftingRowVector.size() == 0);

               liftingColumnIndex = numColsRational();
               liftingRowVector.add(i, maxValue);
               liftingRowVector.add(liftingColumnIndex, -1);

               _rationalLP->addRow(LPRowRational(0, liftingRowVector, 0));
               _realLP->addRow(LPRowReal(0.0, DSVectorReal(liftingRowVector), 0.0));

               assert(liftingColumnIndex == numColsRational() - 1);
               assert(liftingColumnIndex == numColsReal() - 1);

               _rationalLP->changeBounds(liftingColumnIndex, _rationalNegInfty, _rationalPosInfty);
               _realLP->changeBounds(liftingColumnIndex, -realParam(SoPlex::INFTY), realParam(SoPlex::INFTY));

               liftingRowVector.clear();
               addedLiftingRow = true;
            }

            // get row index
            int rowIndex = colVector.index(k);
            assert(rowIndex >= 0);
            assert(rowIndex < _beforeLiftRows);
            assert(liftingColumnIndex == numColsRational() - 1);

            MSG_DEBUG(std::cout << "            --> changing matrix\n");

            // remove nonzero from original column
            _rationalLP->changeElement(rowIndex, i, 0);
            _realLP->changeElement(rowIndex, i, 0.0);

            // add nonzero divided by maxValue to new column
            Rational newValue(value);
            newValue /= maxValue;
            _rationalLP->changeElement(rowIndex, liftingColumnIndex, newValue);
            _realLP->changeElement(rowIndex, liftingColumnIndex, Real(newValue));
         }
      }
   }

   // search each column for small nonzeros entries
   const Rational minValue = realParam(SoPlex::LIFTMINVAL);

   for(int i = 0; i < numColsRational(); i++)
   {
      MSG_DEBUG(std::cout << "in lifting: examining column " << i << "\n");

      // get column vector
      colVector = colVectorRational(i);

      bool addedLiftingRow = false;
      int liftingColumnIndex = -1;

      // go through nonzero entries of the column
      for(int k = colVector.size() - 1; k >= 0; k--)
      {
         const Rational& value = colVector.value(k);

         if(spxAbs(value) < minValue)
         {
            MSG_DEBUG(std::cout << "   --> nonzero " << k << " has value " << rationalToString(
                         value) << " in row " << colVector.index(k) << "\n");

            // add new column equal to maxValue times original column
            if(!addedLiftingRow)
            {
               MSG_DEBUG(std::cout << "            --> adding lifting row\n");

               assert(liftingRowVector.size() == 0);

               liftingColumnIndex = numColsRational();
               liftingRowVector.add(i, minValue);
               liftingRowVector.add(liftingColumnIndex, -1);

               _rationalLP->addRow(LPRowRational(0, liftingRowVector, 0));
               _realLP->addRow(LPRowReal(0.0, DSVectorReal(liftingRowVector), 0.0));

               assert(liftingColumnIndex == numColsRational() - 1);
               assert(liftingColumnIndex == numColsReal() - 1);

               _rationalLP->changeBounds(liftingColumnIndex, _rationalNegInfty, _rationalPosInfty);
               _realLP->changeBounds(liftingColumnIndex, -realParam(SoPlex::INFTY), realParam(SoPlex::INFTY));

               liftingRowVector.clear();
               addedLiftingRow = true;
            }

            // get row index
            int rowIndex = colVector.index(k);
            assert(rowIndex >= 0);
            assert(rowIndex < _beforeLiftRows);
            assert(liftingColumnIndex == numColsRational() - 1);

            MSG_DEBUG(std::cout << "            --> changing matrix\n");

            // remove nonzero from original column
            _rationalLP->changeElement(rowIndex, i, 0);
            _realLP->changeElement(rowIndex, i, 0.0);

            // add nonzero divided by maxValue to new column
            Rational newValue(value);
            newValue /= minValue;
            _rationalLP->changeElement(rowIndex, liftingColumnIndex, newValue);
            _realLP->changeElement(rowIndex, liftingColumnIndex, Real(newValue));
         }
      }
   }

   // adjust basis
   if(_hasBasis)
   {
      assert(numColsRational() >= _beforeLiftCols);
      assert(numRowsRational() >= _beforeLiftRows);

      _basisStatusCols.append(numColsRational() - _beforeLiftCols, SPxSolver::BASIC);
      _basisStatusRows.append(numRowsRational() - _beforeLiftRows, SPxSolver::FIXED);
      _rationalLUSolver.clear();
   }

   MSG_DEBUG(_realLP->writeFile("afterLift.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();

   if(numColsRational() > _beforeLiftCols || numRowsRational() > _beforeLiftRows)
   {
      MSG_INFO1(spxout, spxout << "Added " << numColsRational() - _beforeLiftCols << " columns and "
                << numRowsRational() - _beforeLiftRows << " rows to reduce large matrix coefficients\n.");
   }
}



/// undoes lifting
void SoPlex::_project(SolRational& sol)
{
   // start timing
   _statistics->transformTime->start();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("beforeProject.lp", 0, 0, 0));

   assert(numColsRational() >= _beforeLiftCols);
   assert(numRowsRational() >= _beforeLiftRows);

   // shrink rational LP to original size
   _rationalLP->removeColRange(_beforeLiftCols, numColsRational() - 1);
   _rationalLP->removeRowRange(_beforeLiftRows, numRowsRational() - 1);

   // shrink real LP to original size
   _realLP->removeColRange(_beforeLiftCols, numColsReal() - 1);
   _realLP->removeRowRange(_beforeLiftRows, numRowsReal() - 1);

   // adjust solution
   if(sol.isPrimalFeasible())
   {
      sol._primal.reDim(_beforeLiftCols);
      sol._slacks.reDim(_beforeLiftRows);
   }

   if(sol.hasPrimalRay())
   {
      sol._primalRay.reDim(_beforeLiftCols);
   }

   ///@todo if we know the mapping between original and lifting columns, we simply need to add the reduced cost of
   ///      the lifting column to the reduced cost of the original column; this is not implemented now, because for
   ///      optimal solutions the reduced costs of the lifting columns are zero
   const Rational maxValue = realParam(SoPlex::LIFTMAXVAL);

   for(int i = _beforeLiftCols; i < numColsRational() && sol._isDualFeasible; i++)
   {
      if(spxAbs(maxValue * sol._redCost[i]) > _rationalOpttol)
      {
         MSG_INFO1(spxout, spxout << "Warning: lost dual solution during project phase.\n");
         sol._isDualFeasible = false;
      }
   }

   if(sol.isDualFeasible())
   {
      sol._redCost.reDim(_beforeLiftCols);
      sol._dual.reDim(_beforeLiftRows);
   }

   if(sol.hasDualFarkas())
   {
      sol._dualFarkas.reDim(_beforeLiftRows);
   }

   // adjust basis
   for(int i = _beforeLiftCols; i < numColsRational() && _hasBasis; i++)
   {
      if(_basisStatusCols[i] != SPxSolver::BASIC)
      {
         MSG_INFO1(spxout, spxout <<
                   "Warning: lost basis during project phase because of nonbasic lifting column.\n");
         _hasBasis = false;
         _rationalLUSolver.clear();
      }
   }

   for(int i = _beforeLiftRows; i < numRowsRational() && _hasBasis; i++)
   {
      if(_basisStatusRows[i] == SPxSolver::BASIC)
      {
         MSG_INFO1(spxout, spxout <<
                   "Warning: lost basis during project phase because of basic lifting row.\n");
         _hasBasis = false;
         _rationalLUSolver.clear();
      }
   }

   if(_hasBasis)
   {
      _basisStatusCols.reSize(_beforeLiftCols);
      _basisStatusRows.reSize(_beforeLiftRows);
      _rationalLUSolver.clear();
   }

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("afterProject.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();
}



/// stores objective, bounds, and sides of real LP
void SoPlex::_storeLPReal()
{
#ifndef SOPLEX_MANUAL_ALT

   if(intParam(SoPlex::SYNCMODE) == SYNCMODE_MANUAL)
   {
      _manualRealLP = *_realLP;
      return;
   }

#endif

   _manualLower = _realLP->lower();
   _manualUpper = _realLP->upper();
   _manualLhs = _realLP->lhs();
   _manualRhs = _realLP->rhs();
   _manualObj.reDim(_realLP->nCols());
   _realLP->getObj(_manualObj);
}



/// restores objective, bounds, and sides of real LP
void SoPlex::_restoreLPReal()
{
   if(intParam(SoPlex::SYNCMODE) == SYNCMODE_MANUAL)
   {
#ifndef SOPLEX_MANUAL_ALT
      _solver.loadLP(_manualRealLP);
#else
      _realLP->changeLower(_manualLower);
      _realLP->changeUpper(_manualUpper);
      _realLP->changeLhs(_manualLhs);
      _realLP->changeRhs(_manualRhs);
      _realLP->changeObj(_manualObj);
#endif

      if(_hasBasis)
      {
         // in manual sync mode, if the right-hand side of an equality constraint is not floating-point
         // representable, the user might have constructed the constraint in the real LP by rounding down the
         // left-hand side and rounding up the right-hand side; if the basis status is fixed, we need to adjust it
         for(int i = 0; i < _solver.nRows(); i++)
         {
            if(_basisStatusRows[i] == SPxSolver::FIXED && _solver.lhs(i) != _solver.rhs(i))
            {
               assert(_solver.rhs(i) == spxNextafter(_solver.lhs(i), infinity));

               if(_hasSolRational && _solRational.isDualFeasible()
                     && ((intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MAXIMIZE && _solRational._dual[i] > 0)
                         || (intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MINIMIZE && _solRational._dual[i] < 0)))
               {
                  _basisStatusRows[i] = SPxSolver::ON_UPPER;
               }
               else
               {
                  _basisStatusRows[i] = SPxSolver::ON_LOWER;
               }
            }
         }

         _solver.setBasis(_basisStatusRows.get_const_ptr(), _basisStatusCols.get_const_ptr());
         _hasBasis = (_solver.basis().status() > SPxBasis::NO_PROBLEM);
      }
   }
   else
   {
      _realLP->changeLower(_manualLower);
      _realLP->changeUpper(_manualUpper);
      _realLP->changeLhs(_manualLhs);
      _realLP->changeRhs(_manualRhs);
      _realLP->changeObj(_manualObj);
   }
}



/// introduces slack variables to transform inequality constraints into equations for both rational and real LP,
/// which should be in sync
void SoPlex::_transformEquality()
{
   MSG_DEBUG(std::cout << "Transforming rows to equation form.\n");

   // start timing
   _statistics->transformTime->start();

   MSG_DEBUG(_realLP->writeFile("beforeTransEqu.lp", 0, 0, 0));

   // clear array of slack columns
   _slackCols.clear();

   // add artificial slack variables to convert inequality to equality constraints
   for(int i = 0; i < numRowsRational(); i++)
   {
      assert((lhsRational(i) == rhsRational(i)) == (_rowTypes[i] == RANGETYPE_FIXED));

      if(_rowTypes[i] != RANGETYPE_FIXED)
      {
         _slackCols.add(_rationalZero, -rhsRational(i), *_unitVectorRational(i), -lhsRational(i));

         if(_rationalLP->lhs(i) != 0)
            _rationalLP->changeLhs(i, _rationalZero);

         if(_rationalLP->rhs(i) != 0)
            _rationalLP->changeRhs(i, _rationalZero);

         assert(_rationalLP->lhs(i) == 0);
         assert(_rationalLP->rhs(i) == 0);
         _realLP->changeRange(i, 0.0, 0.0);
         _colTypes.append(_switchRangeType(_rowTypes[i]));
         _rowTypes[i] = RANGETYPE_FIXED;
      }
   }

   _rationalLP->addCols(_slackCols);
   _realLP->addCols(_slackCols);

   // adjust basis
   if(_hasBasis)
   {
      for(int i = 0; i < _slackCols.num(); i++)
      {
         int row = _slackCols.colVector(i).index(0);

         assert(row >= 0);
         assert(row < numRowsRational());

         switch(_basisStatusRows[row])
         {
         case SPxSolver::ON_LOWER:
            _basisStatusCols.append(SPxSolver::ON_UPPER);
            break;

         case SPxSolver::ON_UPPER:
            _basisStatusCols.append(SPxSolver::ON_LOWER);
            break;

         case SPxSolver::BASIC:
         case SPxSolver::FIXED:
         default:
            _basisStatusCols.append(_basisStatusRows[row]);
            break;
         }

         _basisStatusRows[row] = SPxSolver::FIXED;
      }

      _rationalLUSolver.clear();
   }

   MSG_DEBUG(_realLP->writeFile("afterTransEqu.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();

   if(_slackCols.num() > 0)
   {
      MSG_INFO1(spxout, spxout << "Added " << _slackCols.num() <<
                " slack columns to transform rows to equality form.\n");
   }
}



/// restores original problem
void SoPlex::_untransformEquality(SolRational& sol)
{
   // start timing
   _statistics->transformTime->start();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("beforeUntransEqu.lp", 0, 0, 0));

   int numCols = numColsRational();
   int numOrigCols = numColsRational() - _slackCols.num();

   // adjust solution
   if(sol.isPrimalFeasible())
   {
      for(int i = 0; i < _slackCols.num(); i++)
      {
         int col = numOrigCols + i;
         int row = _slackCols.colVector(i).index(0);

         assert(row >= 0);
         assert(row < numRowsRational());

         sol._slacks[row] -= sol._primal[col];
      }

      sol._primal.reDim(numOrigCols);
   }

   if(sol.hasPrimalRay())
   {
      sol._primalRay.reDim(numOrigCols);
   }

   // adjust basis
   if(_hasBasis)
   {
      for(int i = 0; i < _slackCols.num(); i++)
      {
         int col = numOrigCols + i;
         int row = _slackCols.colVector(i).index(0);

         assert(row >= 0);
         assert(row < numRowsRational());
         assert(_basisStatusRows[row] != SPxSolver::UNDEFINED);
         assert(_basisStatusRows[row] != SPxSolver::ZERO || lhsRational(row) == 0);
         assert(_basisStatusRows[row] != SPxSolver::ZERO || rhsRational(row) == 0);
         assert(_basisStatusRows[row] != SPxSolver::BASIC || _basisStatusCols[col] != SPxSolver::BASIC);

         MSG_DEBUG(std::cout << "slack column " << col << " for row " << row
                   << ": col status=" << _basisStatusCols[col]
                   << ", row status=" << _basisStatusRows[row]
                   << ", redcost=" << rationalToString(sol._redCost[col])
                   << ", dual=" << rationalToString(sol._dual[row]) << "\n");

         if(_basisStatusRows[row] != SPxSolver::BASIC)
         {
            switch(_basisStatusCols[col])
            {
            case SPxSolver::ON_LOWER:
               _basisStatusRows[row] = SPxSolver::ON_UPPER;
               break;

            case SPxSolver::ON_UPPER:
               _basisStatusRows[row] = SPxSolver::ON_LOWER;
               break;

            case SPxSolver::BASIC:
            case SPxSolver::FIXED:
            default:
               _basisStatusRows[row] = _basisStatusCols[col];
               break;
            }
         }
      }

      _basisStatusCols.reSize(numOrigCols);

      if(_slackCols.num() > 0)
         _rationalLUSolver.clear();
   }

   // not earlier because of debug message
   if(sol.isDualFeasible())
   {
      sol._redCost.reDim(numOrigCols);
   }

   // restore sides and remove slack columns
   for(int i = 0; i < _slackCols.num(); i++)
   {
      int col = numOrigCols + i;
      int row = _slackCols.colVector(i).index(0);

      if(upperRational(col) != 0)
         _rationalLP->changeLhs(row, -upperRational(col));

      if(lowerRational(col) != 0)
         _rationalLP->changeRhs(row, -lowerRational(col));

      assert(_rationalLP->lhs(row) == -upperRational(col));
      assert(_rationalLP->rhs(row) == -lowerRational(col));
      _rowTypes[row] = _switchRangeType(_colTypes[col]);
   }

   _rationalLP->removeColRange(numOrigCols, numCols - 1);
   _realLP->removeColRange(numOrigCols, numCols - 1);
   _colTypes.reSize(numOrigCols);

   // objective, bounds, and sides of real LP are restored only after _solveRational()

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("afterUntransEqu.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();
}



/// transforms LP to unboundedness problem by moving the objective function to the constraints, changing right-hand
/// side and bounds to zero, and adding an auxiliary variable for the decrease in the objective function
void SoPlex::_transformUnbounded()
{
   MSG_INFO1(spxout, spxout << "Setting up LP to compute primal unbounded ray.\n");

   // start timing
   _statistics->transformTime->start();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("beforeTransUnbounded.lp", 0, 0, 0));

   // store bounds
   _unboundedLower.reDim(numColsRational());
   _unboundedUpper.reDim(numColsRational());

   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      if(_lowerFinite(_colTypes[c]))
         _unboundedLower[c] = lowerRational(c);

      if(_upperFinite(_colTypes[c]))
         _unboundedUpper[c] = upperRational(c);
   }

   // store sides
   _unboundedLhs.reDim(numRowsRational());
   _unboundedRhs.reDim(numRowsRational());

   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      if(_lowerFinite(_rowTypes[r]))
         _unboundedLhs[r] = lhsRational(r);

      if(_upperFinite(_rowTypes[r]))
         _unboundedRhs[r] = rhsRational(r);
   }

   // make right-hand side zero
   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      assert((lhsRational(r) > _rationalNegInfty) == _lowerFinite(_rowTypes[r]));

      if(_lowerFinite(_rowTypes[r]))
      {
         _rationalLP->changeLhs(r, 0);
         _realLP->changeLhs(r, 0.0);
      }
      else if(_realLP->lhs(r) > -realParam(SoPlex::INFTY))
         _realLP->changeLhs(r, -realParam(SoPlex::INFTY));

      assert((rhsRational(r) < _rationalPosInfty) == _upperFinite(_rowTypes[r]));

      if(_upperFinite(_rowTypes[r]))
      {
         _rationalLP->changeRhs(r, 0);
         _realLP->changeRhs(r, 0.0);
      }
      else if(_realLP->rhs(r) < realParam(SoPlex::INFTY))
         _realLP->changeRhs(r, realParam(SoPlex::INFTY));
   }

   // transform objective function to constraint and add auxiliary variable
   int numOrigCols = numColsRational();
   DSVectorRational obj(numOrigCols + 1);
   ///@todo implement this without copying the objective function
   obj = _rationalLP->maxObj();
   obj.add(numOrigCols, -1);
   _rationalLP->addRow(LPRowRational(0, obj, 0));
   _realLP->addRow(LPRowReal(0, DSVectorReal(obj), 0));
   _rowTypes.append(RANGETYPE_FIXED);

   assert(numColsRational() == numOrigCols + 1);

   // set objective coefficient and bounds for auxiliary variable
   _rationalLP->changeMaxObj(numOrigCols, 1);
   _realLP->changeMaxObj(numOrigCols, 1.0);

   _rationalLP->changeBounds(numOrigCols, _rationalNegInfty, 1);
   _realLP->changeBounds(numOrigCols, -realParam(SoPlex::INFTY), 1.0);
   _colTypes.append(RANGETYPE_UPPER);

   // set objective coefficients to zero and adjust bounds for problem variables
   for(int c = numColsRational() - 2; c >= 0; c--)
   {
      _rationalLP->changeObj(c, 0);
      _realLP->changeObj(c, 0.0);

      assert((lowerRational(c) > _rationalNegInfty) == _lowerFinite(_colTypes[c]));

      if(_lowerFinite(_colTypes[c]))
      {
         _rationalLP->changeLower(c, 0);
         _realLP->changeLower(c, 0.0);
      }
      else if(_realLP->lower(c) > -realParam(SoPlex::INFTY))
         _realLP->changeLower(c, -realParam(SoPlex::INFTY));

      assert((upperRational(c) < _rationalPosInfty) == _upperFinite(_colTypes[c]));

      if(_upperFinite(_colTypes[c]))
      {
         _rationalLP->changeUpper(c, 0);
         _realLP->changeUpper(c, 0.0);
      }
      else if(_realLP->upper(c) < realParam(SoPlex::INFTY))
         _realLP->changeUpper(c, realParam(SoPlex::INFTY));
   }

   // adjust basis
   if(_hasBasis)
   {
      _basisStatusCols.append(SPxSolver::ON_UPPER);
      _basisStatusRows.append(SPxSolver::BASIC);
      _rationalLUSolver.clear();
   }

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("afterTransUnbounded.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();
}



/// undoes transformation to unboundedness problem
void SoPlex::_untransformUnbounded(SolRational& sol, bool unbounded)
{
   // start timing
   _statistics->transformTime->start();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("beforeUntransUnbounded.lp", 0, 0, 0));

   int numOrigCols = numColsRational() - 1;
   int numOrigRows = numRowsRational() - 1;
   const Rational& tau = sol._primal[numOrigCols];

   // adjust solution and basis
   if(unbounded)
   {
      assert(tau >= _rationalPosone);

      sol._isPrimalFeasible = false;
      sol._hasPrimalRay = true;
      sol._isDualFeasible = false;
      sol._hasDualFarkas = false;

      if(tau != 1)
         sol._primal /= tau;

      sol._primalRay = sol._primal;
      sol._primalRay.reDim(numOrigCols);

      _hasBasis = (_basisStatusCols[numOrigCols] != SPxSolver::BASIC
                   && _basisStatusRows[numOrigRows] == SPxSolver::BASIC);
      _basisStatusCols.reSize(numOrigCols);
      _basisStatusRows.reSize(numOrigRows);
   }
   else if(boolParam(SoPlex::TESTDUALINF) && tau < _rationalFeastol)
   {
      const Rational& alpha = sol._dual[numOrigRows];

      assert(sol._isDualFeasible);
      assert(alpha <= _rationalFeastol - _rationalPosone);

      sol._isPrimalFeasible = false;
      sol._hasPrimalRay = false;
      sol._hasDualFarkas = false;

      if(alpha != -1)
      {
         sol._dual /= -alpha;
         sol._redCost /= -alpha;
      }

      sol._dual.reDim(numOrigRows);
      sol._redCost.reDim(numOrigCols);
   }
   else
   {
      sol.invalidate();
      _hasBasis = false;
      _basisStatusCols.reSize(numOrigCols);
      _basisStatusCols.reSize(numOrigRows);
   }

   // recover objective function
   const SVectorRational& objRowVector = _rationalLP->rowVector(numOrigRows);

   for(int i = objRowVector.size() - 1; i >= 0; i--)
   {
      _rationalLP->changeMaxObj(objRowVector.index(i), objRowVector.value(i));
      _realLP->changeMaxObj(objRowVector.index(i), Real(objRowVector.value(i)));
   }

   // remove objective function constraint and auxiliary variable
   _rationalLP->removeRow(numOrigRows);
   _realLP->removeRow(numOrigRows);
   _rowTypes.reSize(numOrigRows);

   _rationalLP->removeCol(numOrigCols);
   _realLP->removeCol(numOrigCols);
   _colTypes.reSize(numOrigCols);

   // restore objective, sides and bounds
   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      if(_lowerFinite(_rowTypes[r]))
      {
         _rationalLP->changeLhs(r, _unboundedLhs[r]);
         _realLP->changeLhs(r, Real(_unboundedLhs[r]));
      }

      if(_upperFinite(_rowTypes[r]))
      {
         _rationalLP->changeRhs(r, _unboundedRhs[r]);
         _realLP->changeRhs(r, Real(_unboundedRhs[r]));
      }

      assert((lhsRational(r) > _rationalNegInfty) == _lowerFinite(_rowTypes[r]));
      assert((rhsRational(r) < _rationalPosInfty) == _upperFinite(_rowTypes[r]));
      assert((lhsReal(r) > -realParam(SoPlex::INFTY)) == _lowerFinite(_rowTypes[r]));
      assert((rhsReal(r) < realParam(SoPlex::INFTY)) == _upperFinite(_rowTypes[r]));
   }

   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      if(_lowerFinite(_colTypes[c]))
      {
         _rationalLP->changeLower(c, _unboundedLower[c]);
         _realLP->changeLower(c, Real(_unboundedLower[c]));
      }

      if(_upperFinite(_colTypes[c]))
      {
         _rationalLP->changeUpper(c, _unboundedUpper[c]);
         _realLP->changeUpper(c, Real(_unboundedUpper[c]));
      }

      assert((lowerRational(c) > _rationalNegInfty) == _lowerFinite(_colTypes[c]));
      assert((upperRational(c) < _rationalPosInfty) == _upperFinite(_colTypes[c]));
      assert((lowerReal(c) > -realParam(SoPlex::INFTY)) == _lowerFinite(_colTypes[c]));
      assert((upperReal(c) < realParam(SoPlex::INFTY)) == _upperFinite(_colTypes[c]));
   }

   // invalidate rational basis factorization
   _rationalLUSolver.clear();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("afterUntransUnbounded.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();
}



/// store basis
void SoPlex::_storeBasis()
{
   assert(!_storedBasis);

   if(_hasBasis)
   {
      _storedBasis = true;
      _storedBasisStatusCols = _basisStatusCols;
      _storedBasisStatusRows = _basisStatusRows;
   }
   else
      _storedBasis = false;
}



/// restore basis
void SoPlex::_restoreBasis()
{
   if(_storedBasis)
   {
      _hasBasis = true;
      _basisStatusCols = _storedBasisStatusCols;
      _basisStatusRows = _storedBasisStatusRows;
      _storedBasis = false;
   }
}



/// transforms LP to feasibility problem by removing the objective function, shifting variables, and homogenizing the
/// right-hand side
void SoPlex::_transformFeasibility()
{
   MSG_INFO1(spxout, spxout << "Setting up LP to test for feasibility.\n");

   // start timing
   _statistics->transformTime->start();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("beforeTransFeas.lp", 0, 0, 0));

   // store objective function
   _feasObj.reDim(numColsRational());

   for(int c = numColsRational() - 1; c >= 0; c--)
      _feasObj[c] = _rationalLP->maxObj(c);

   // store bounds
   _feasLower.reDim(numColsRational());
   _feasUpper.reDim(numColsRational());

   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      if(_lowerFinite(_colTypes[c]))
         _feasLower[c] = lowerRational(c);

      if(_upperFinite(_colTypes[c]))
         _feasUpper[c] = upperRational(c);
   }

   // store sides
   _feasLhs.reDim(numRowsRational());
   _feasRhs.reDim(numRowsRational());

   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      if(_lowerFinite(_rowTypes[r]))
         _feasLhs[r] = lhsRational(r);

      if(_upperFinite(_rowTypes[r]))
         _feasRhs[r] = rhsRational(r);
   }

   // set objective coefficients to zero; shift primal space such as to guarantee that the zero solution is within
   // the bounds
   Rational shiftValue;
   Rational shiftValue2;

   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      _rationalLP->changeMaxObj(c, 0);
      _realLP->changeMaxObj(c, 0.0);

      if(lowerRational(c) > 0)
      {
         const SVectorRational& colVector = colVectorRational(c);

         for(int i = 0; i < colVector.size(); i++)
         {
            shiftValue = colVector.value(i);
            shiftValue *= lowerRational(c);
            int r = colVector.index(i);

            assert((lhsRational(r) > _rationalNegInfty) == _lowerFinite(_rowTypes[r]));
            assert((rhsRational(r) < _rationalPosInfty) == _upperFinite(_rowTypes[r]));

            if(_lowerFinite(_rowTypes[r]) && _upperFinite(_rowTypes[r]))
            {
               shiftValue2 = lhsRational(r);
               shiftValue2 -= shiftValue;
               _rationalLP->changeLhs(r, shiftValue2);
               _realLP->changeLhs(r, Real(shiftValue2));

               shiftValue -= rhsRational(r);
               shiftValue *= -1;
               _rationalLP->changeRhs(r, shiftValue);
               _realLP->changeRhs(r, Real(shiftValue));
            }
            else if(_lowerFinite(_rowTypes[r]))
            {
               shiftValue -= lhsRational(r);
               shiftValue *= -1;
               _rationalLP->changeLhs(r, shiftValue);
               _realLP->changeLhs(r, Real(shiftValue));
            }
            else if(_upperFinite(_rowTypes[r]))
            {
               shiftValue -= rhsRational(r);
               shiftValue *= -1;
               _rationalLP->changeRhs(r, shiftValue);
               _realLP->changeRhs(r, Real(shiftValue));
            }
         }

         assert((upperRational(c) < _rationalPosInfty) == _upperFinite(_colTypes[c]));

         if(_upperFinite(_colTypes[c]))
         {
            _rationalLP->changeBounds(c, 0, upperRational(c) - lowerRational(c));
            _realLP->changeBounds(c, 0.0, Real(upperRational(c)));
         }
         else if(_realLP->upper(c) < realParam(SoPlex::INFTY))
         {
            _rationalLP->changeLower(c, 0);
            _realLP->changeBounds(c, 0.0, realParam(SoPlex::INFTY));
         }
         else
         {
            _rationalLP->changeLower(c, 0);
            _realLP->changeLower(c, 0.0);
         }
      }
      else if(upperRational(c) < 0)
      {
         const SVectorRational& colVector = colVectorRational(c);

         for(int i = 0; i < colVector.size(); i++)
         {
            shiftValue = colVector.value(i);
            shiftValue *= upperRational(c);
            int r = colVector.index(i);

            assert((lhsRational(r) > _rationalNegInfty) == _lowerFinite(_rowTypes[r]));
            assert((rhsRational(r) < _rationalPosInfty) == _upperFinite(_rowTypes[r]));

            if(_lowerFinite(_rowTypes[r]) && _upperFinite(_rowTypes[r]))
            {
               shiftValue2 = lhsRational(r);
               shiftValue2 -= shiftValue;
               _rationalLP->changeLhs(r, shiftValue2);
               _realLP->changeLhs(r, Real(shiftValue2));

               shiftValue -= rhsRational(r);
               shiftValue *= -1;
               _rationalLP->changeRhs(r, shiftValue);
               _realLP->changeRhs(r, Real(shiftValue));
            }
            else if(_lowerFinite(_rowTypes[r]))
            {
               shiftValue -= lhsRational(r);
               shiftValue *= -1;
               _rationalLP->changeLhs(r, shiftValue);
               _realLP->changeLhs(r, Real(shiftValue));
            }
            else if(_upperFinite(_rowTypes[r]))
            {
               shiftValue -= rhsRational(r);
               shiftValue *= -1;
               _rationalLP->changeRhs(r, shiftValue);
               _realLP->changeRhs(r, Real(shiftValue));
            }
         }

         assert((lowerRational(c) > _rationalNegInfty) == _lowerFinite(_colTypes[c]));

         if(_lowerFinite(_colTypes[c]))
         {
            _rationalLP->changeBounds(c, lowerRational(c) - upperRational(c), 0);
            _realLP->changeBounds(c, Real(lowerRational(c)), 0.0);
         }
         else if(_realLP->lower(c) > -realParam(SoPlex::INFTY))
         {
            _rationalLP->changeUpper(c, 0);
            _realLP->changeBounds(c, -realParam(SoPlex::INFTY), 0.0);
         }
         else
         {
            _rationalLP->changeUpper(c, 0);
            _realLP->changeUpper(c, 0.0);
         }
      }
      else
      {
         if(_lowerFinite(_colTypes[c]))
            _realLP->changeLower(c, Real(lowerRational(c)));
         else if(_realLP->lower(c) > -realParam(SoPlex::INFTY))
            _realLP->changeLower(c, -realParam(SoPlex::INFTY));

         if(_upperFinite(_colTypes[c]))
            _realLP->changeUpper(c, Real(upperRational(c)));
         else if(_realLP->upper(c) < realParam(SoPlex::INFTY))
            _realLP->changeUpper(c, realParam(SoPlex::INFTY));
      }

      assert(lowerReal(c) <= upperReal(c));
   }

   // homogenize sides
   _tauColVector.clear();

   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      if(lhsRational(r) > 0)
      {
         _tauColVector.add(r, lhsRational(r));
         assert((rhsRational(r) < _rationalPosInfty) == _upperFinite(_rowTypes[r]));

         if(_upperFinite(_rowTypes[r]))
         {
            _rationalLP->changeRange(r, 0, rhsRational(r) - lhsRational(r));
            _realLP->changeRange(r, 0.0, Real(rhsRational(r)));
         }
         else
         {
            _rationalLP->changeLhs(r, 0);
            _realLP->changeLhs(r, 0.0);

            if(_realLP->rhs(r) < realParam(SoPlex::INFTY))
               _realLP->changeRhs(r, realParam(SoPlex::INFTY));
         }
      }
      else if(rhsRational(r) < 0)
      {
         _tauColVector.add(r, rhsRational(r));
         assert((lhsRational(r) > _rationalNegInfty) == _lowerFinite(_rowTypes[r]));

         if(_lowerFinite(_rowTypes[r]))
         {
            _rationalLP->changeRange(r, lhsRational(r) - rhsRational(r), 0);
            _realLP->changeRange(r, Real(lhsRational(r)), 0.0);
         }
         else
         {
            _rationalLP->changeRhs(r, 0);
            _realLP->changeRhs(r, 0.0);

            if(_realLP->lhs(r) > -realParam(SoPlex::INFTY))
               _realLP->changeLhs(r, -realParam(SoPlex::INFTY));
         }
      }
      else
      {
         if(_lowerFinite(_rowTypes[r]))
            _realLP->changeLhs(r, Real(lhsRational(r)));
         else if(_realLP->lhs(r) > -realParam(SoPlex::INFTY))
            _realLP->changeLhs(r, -realParam(SoPlex::INFTY));

         if(_upperFinite(_rowTypes[r]))
            _realLP->changeRhs(r, Real(rhsRational(r)));
         else if(_realLP->rhs(r) < realParam(SoPlex::INFTY))
            _realLP->changeRhs(r, realParam(SoPlex::INFTY));
      }

      assert(rhsReal(r) <= rhsReal(r));
   }

   ///@todo exploit this case by returning without LP solving
   if(_tauColVector.size() == 0)
   {
      MSG_INFO3(spxout, spxout << "LP is trivially feasible.\n");
   }

   // add artificial column
   SPxColId id;
   _tauColVector *= -1;
   _rationalLP->addCol(id,
                       LPColRational((intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MAXIMIZE ? _rationalPosone :
                                      _rationalNegone),
                                     _tauColVector, 1, 0));
   _realLP->addCol(id,
                   LPColReal((intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MAXIMIZE ? 1.0 : -1.0),
                             DSVectorReal(_tauColVector), 1.0, 0.0));
   _colTypes.append(RANGETYPE_BOXED);

   // adjust basis
   if(_hasBasis)
   {
      _basisStatusCols.append(SPxSolver::ON_UPPER);
   }

   // invalidate rational basis factorization
   _rationalLUSolver.clear();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("afterTransFeas.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();
}



/// undoes transformation to feasibility problem
void SoPlex::_untransformFeasibility(SolRational& sol, bool infeasible)
{
   // start timing
   _statistics->transformTime->start();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("beforeUntransFeas.lp", 0, 0, 0));

   int numOrigCols = numColsRational() - 1;

   // adjust solution and basis
   if(infeasible)
   {
      assert(sol._isDualFeasible);
      assert(sol._primal[numOrigCols] < 1);

      sol._isPrimalFeasible = false;
      sol._hasPrimalRay = false;
      sol._isDualFeasible = false;
      sol._hasDualFarkas = true;

      sol._dualFarkas = sol._dual;

      _hasBasis = false;
      _basisStatusCols.reSize(numOrigCols);
   }
   else if(sol._isPrimalFeasible)
   {
      assert(sol._primal[numOrigCols] >= 1);

      sol._hasPrimalRay = false;
      sol._isDualFeasible = false;
      sol._hasDualFarkas = false;

      if(sol._primal[numOrigCols] != 1)
      {
         sol._slacks /= sol._primal[numOrigCols];

         for(int i = 0; i < numOrigCols; i++)
            sol._primal[i] /= sol._primal[numOrigCols];

         sol._primal[numOrigCols] = 1;
      }

      sol._primal.reDim(numOrigCols);
      sol._slacks -= _rationalLP->colVector(numOrigCols);

      _hasBasis = (_basisStatusCols[numOrigCols] != SPxSolver::BASIC);
      _basisStatusCols.reSize(numOrigCols);
   }
   else
   {
      _hasBasis = false;
      _basisStatusCols.reSize(numOrigCols);
   }

   // restore right-hand side
   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      assert(rhsRational(r) >= _rationalPosInfty || lhsRational(r) <= _rationalNegInfty
             || _feasLhs[r] - lhsRational(r) == _feasRhs[r] - rhsRational(r));

      if(_lowerFinite(_rowTypes[r]))
      {
         _rationalLP->changeLhs(r, _feasLhs[r]);
         _realLP->changeLhs(r, Real(_feasLhs[r]));
      }
      else if(_realLP->lhs(r) > -realParam(SoPlex::INFTY))
         _realLP->changeLhs(r, -realParam(SoPlex::INFTY));

      assert(_lowerFinite(_rowTypes[r]) == (lhsRational(r) > _rationalNegInfty));
      assert(_lowerFinite(_rowTypes[r]) == (lhsReal(r) > -realParam(SoPlex::INFTY)));

      if(_upperFinite(_rowTypes[r]))
      {
         _rationalLP->changeRhs(r, _feasRhs[r]);
         _realLP->changeRhs(r, Real(_feasRhs[r]));
      }
      else if(_realLP->rhs(r) < realParam(SoPlex::INFTY))
         _realLP->changeRhs(r, realParam(SoPlex::INFTY));

      assert(_upperFinite(_rowTypes[r]) == (rhsRational(r) < _rationalPosInfty));
      assert(_upperFinite(_rowTypes[r]) == (rhsReal(r) < realParam(SoPlex::INFTY)));

      assert(lhsReal(r) <= rhsReal(r));
   }

   // unshift primal space and restore objective coefficients
   Rational shiftValue;

   for(int c = numOrigCols - 1; c >= 0; c--)
   {
      bool shifted = (_lowerFinite(_colTypes[c]) && _feasLower[c] > 0) || (_upperFinite(_colTypes[c])
                     && _feasUpper[c] < 0);
      assert(shifted || !_lowerFinite(_colTypes[c]) || _feasLower[c] == lowerRational(c));
      assert(shifted || !_upperFinite(_colTypes[c]) || _feasUpper[c] == upperRational(c));
#ifdef SOPLEX_WITH_GMP
      assert(upperRational(c) >= _rationalPosInfty || lowerRational(c) <= _rationalNegInfty
             || _feasLower[c] - lowerRational(c) == _feasUpper[c] - upperRational(c));
#endif

      if(shifted)
      {
         if(_lowerFinite(_colTypes[c]))
         {
            shiftValue = _feasLower[c];
            shiftValue -= lowerRational(c);
         }
         else if(_upperFinite(_colTypes[c]))
         {
            shiftValue = _feasUpper[c];
            shiftValue -= upperRational(c);
         }

         if(sol._isPrimalFeasible)
         {
            sol._primal[c] += shiftValue;
            sol._slacks.multAdd(shiftValue, _rationalLP->colVector(c));
         }
      }

      if(_lowerFinite(_colTypes[c]))
      {
         if(shifted)
            _rationalLP->changeLower(c, _feasLower[c]);

         _realLP->changeLower(c, Real(_feasLower[c]));
      }
      else if(_realLP->lower(c) > -realParam(SoPlex::INFTY))
         _realLP->changeLower(c, -realParam(SoPlex::INFTY));

      assert(_lowerFinite(_colTypes[c]) == (lowerRational(c) > -_rationalPosInfty));
      assert(_lowerFinite(_colTypes[c]) == (lowerReal(c) > -realParam(SoPlex::INFTY)));

      if(_upperFinite(_colTypes[c]))
      {
         if(shifted)
            _rationalLP->changeUpper(c, _feasUpper[c]);

         _realLP->changeUpper(c, Real(upperRational(c)));
      }
      else if(_realLP->upper(c) < realParam(SoPlex::INFTY))
         _realLP->changeUpper(c, realParam(SoPlex::INFTY));

      assert(_upperFinite(_colTypes[c]) == (upperRational(c) < _rationalPosInfty));
      assert(_upperFinite(_colTypes[c]) == (upperReal(c) < realParam(SoPlex::INFTY)));

      _rationalLP->changeMaxObj(c, _feasObj[c]);
      _realLP->changeMaxObj(c, Real(_feasObj[c]));

      assert(lowerReal(c) <= upperReal(c));
   }

   // remove last column
   _rationalLP->removeCol(numOrigCols);
   _realLP->removeCol(numOrigCols);
   _colTypes.reSize(numOrigCols);

   // invalidate rational basis factorization
   _rationalLUSolver.clear();

   // print LP if in debug mode
   MSG_DEBUG(_realLP->writeFile("afterUntransFeas.lp", 0, 0, 0));

   // stop timing
   _statistics->transformTime->stop();

#ifndef NDEBUG
#ifdef SOPLEX_WITH_GMP

   if(sol._isPrimalFeasible)
   {
      DVectorRational activity(numRowsRational());
      _rationalLP->computePrimalActivity(sol._primal, activity);
      assert(sol._slacks == activity);
   }

#endif
#endif
}

/** computes radius of infeasibility box implied by an approximate Farkas' proof

 Given constraints of the form \f$ lhs <= Ax <= rhs \f$, a farkas proof y should satisfy \f$ y^T A = 0 \f$ and
 \f$ y_+^T lhs - y_-^T rhs > 0 \f$, where \f$ y_+, y_- \f$ denote the positive and negative parts of \f$ y \f$.
 If \f$ y \f$ is approximate, it may not satisfy \f$ y^T A = 0 \f$ exactly, but the proof is still valid as long
 as the following holds for all potentially feasible \f$ x \f$:

 \f[
    y^T Ax < (y_+^T lhs - y_-^T rhs)              (*)
 \f]

 we may therefore calculate \f$ y^T A \f$ and \f$ y_+^T lhs - y_-^T rhs \f$ exactly and check if the upper and lower
 bounds on \f$ x \f$ imply that all feasible \f$ x \f$ satisfy (*), and if not then compute bounds on \f$ x \f$ to
 guarantee (*).  The simplest way to do this is to compute

 \f[
    B = (y_+^T lhs - y_-^T rhs) / \sum_i(|(y^T A)_i|)
 \f]

 noting that if every component of \f$ x \f$ has \f$ |x_i| < B \f$, then (*) holds.

 \f$ B \f$ can be increased by iteratively including variable bounds smaller than \f$ B \f$.  The speed of this
 method can be further improved by using interval arithmetic for all computations.  For related information see
 Sec. 4 of Neumaier and Shcherbina, Mathematical Programming A, 2004.

 Set transformed to true if this method is called after _transformFeasibility().
*/
void SoPlex::_computeInfeasBox(SolRational& sol, bool transformed)
{
   assert(sol.hasDualFarkas());

   const VectorRational& lower = transformed ? _feasLower : lowerRational();
   const VectorRational& upper = transformed ? _feasUpper : upperRational();
   const VectorRational& lhs = transformed ? _feasLhs : lhsRational();
   const VectorRational& rhs = transformed ? _feasRhs : rhsRational();
   const VectorRational& y = sol._dualFarkas;

   const int numRows = numRowsRational();
   const int numCols = transformed ? numColsRational() - 1 : numColsRational();

   SSVectorRational ytransA(numColsRational());
   Rational ytransb;
   Rational temp;

   // prepare ytransA and ytransb; since we want exact arithmetic, we set the zero threshold of the semi-sparse
   // vector to zero
   ytransA.setEpsilon(0);
   ytransA.clear();
   ytransb = 0;

   ///@todo this currently works only if all constraints are equations aggregate rows and sides using the multipliers of the Farkas ray
   for(int r = 0; r < numRows; r++)
   {
      ytransA += y[r] * _rationalLP->rowVector(r);
      ytransb += y[r] * (y[r] > 0 ? lhs[r] : rhs[r]);
   }

   // if we work on the feasibility problem, we ignore the last column
   if(transformed)
      ytransA.reDim(numCols);

   MSG_DEBUG(std::cout << "ytransb = " << rationalToString(ytransb) << "\n");

   // if we choose minus ytransb as vector of multipliers for the bound constraints on the variables, we obtain an
   // exactly feasible dual solution for the LP with zero objective function; we aggregate the bounds of the
   // variables accordingly and store its negation in temp
   temp = 0;
   bool isTempFinite = true;

   for(int c = 0; c < numCols && isTempFinite; c++)
   {
      const Rational& minusRedCost = ytransA[c];

      if(minusRedCost > 0)
      {
         assert((upper[c] < _rationalPosInfty) == _upperFinite(_colTypes[c]));

         if(_upperFinite(_colTypes[c]))
            temp.addProduct(minusRedCost, upper[c]);
         else
            isTempFinite = false;
      }
      else if(minusRedCost < 0)
      {
         assert((lower[c] > _rationalNegInfty) == _lowerFinite(_colTypes[c]));

         if(_lowerFinite(_colTypes[c]))
            temp.addProduct(minusRedCost, lower[c]);
         else
            isTempFinite = false;
      }
   }

   MSG_DEBUG(std::cout << "max ytransA*[x_l,x_u] = " << (isTempFinite ? rationalToString(
                temp) : "infinite") << "\n");

   // ytransb - temp is the increase in the dual objective along the Farkas ray; if this is positive, the dual is
   // unbounded and certifies primal infeasibility
   if(isTempFinite && temp < ytransb)
   {
      MSG_INFO1(spxout, spxout << "Farkas infeasibility proof verified exactly. (1)\n");
      return;
   }

   // ensure that array of nonzero elements in ytransA is available
   assert(ytransA.isSetup());
   ytransA.setup();

   // if ytransb is negative, try to make it zero by including a positive lower bound or a negative upper bound
   if(ytransb < 0)
   {
      for(int c = 0; c < numCols; c++)
      {
         if(lower[c] > 0)
         {
            ytransA.setValue(c, ytransA[c] - ytransb / lower[c]);
            ytransb = 0;
            break;
         }
         else if(upper[c] < 0)
         {
            ytransA.setValue(c, ytransA[c] - ytransb / upper[c]);
            ytransb = 0;
            break;
         }
      }
   }

   // if ytransb is still zero then the zero solution is inside the bounds and cannot be cut off by the Farkas
   // constraint; in this case, we cannot compute a Farkas box
   if(ytransb < 0)
   {
      MSG_INFO1(spxout, spxout <<
                "Approximate Farkas proof to weak.  Could not compute Farkas box. (1)\n");
      return;
   }

   // compute the one norm of ytransA
   temp = 0;
   const int size = ytransA.size();

   for(int n = 0; n < size; n++)
      temp += spxAbs(ytransA.value(n));

   // if the one norm is zero then ytransA is zero the Farkas proof should have been verified above
   assert(temp != 0);

   // initialize variables in loop: size of Farkas box B, flag whether B has been increased, and number of current
   // nonzero in ytransA
   Rational B = ytransb / temp;
   bool success = false;
   int n = 0;

   // loop through nonzeros of ytransA
   MSG_DEBUG(std::cout << "B = " << rationalToString(B) << "\n");
   assert(ytransb >= 0);

   while(true)
   {
      // if all nonzeros have been inspected once without increasing B, we abort; otherwise, we start another round
      if(n >= ytransA.size())
      {
         if(!success)
            break;

         success = false;
         n = 0;
      }

      // get Farkas multiplier of the bound constraint as minus the value in ytransA
      const Rational& minusRedCost = ytransA.value(n);
      int colIdx = ytransA.index(n);

      // if the multiplier is positive we inspect the lower bound: if it is finite and within the Farkas box, we can
      // increase B by including it in the Farkas proof
      assert((upper[colIdx] < _rationalPosInfty) == _upperFinite(_colTypes[colIdx]));
      assert((lower[colIdx] > _rationalNegInfty) == _lowerFinite(_colTypes[colIdx]));

      if(minusRedCost < 0 && lower[colIdx] > -B && _lowerFinite(_colTypes[colIdx]))
      {
         ytransA.clearNum(n);
         ytransb.subProduct(minusRedCost, lower[colIdx]);
         temp += minusRedCost;

         assert(ytransb >= 0);
         assert(temp >= 0);
         assert(temp == 0 || ytransb / temp > B);

         // if ytransA and ytransb are zero, we have 0^T x >= 0 and cannot compute a Farkas box
         if(temp == 0 && ytransb == 0)
         {
            MSG_INFO1(spxout, spxout <<
                      "Approximate Farkas proof to weak.  Could not compute Farkas box. (2)\n");
            return;
         }
         // if ytransb is positive and ytransA is zero, we have 0^T x > 0, proving infeasibility
         else if(temp == 0)
         {
            assert(ytransb > 0);
            MSG_INFO1(spxout, spxout << "Farkas infeasibility proof verified exactly. (2)\n");
            return;
         }
         else
         {
            B = ytransb / temp;
            MSG_DEBUG(std::cout << "B = " << rationalToString(B) << "\n");
         }

         success = true;
      }
      // if the multiplier is negative we inspect the upper bound: if it is finite and within the Farkas box, we can
      // increase B by including it in the Farkas proof
      else if(minusRedCost > 0 && upper[colIdx] < B && _upperFinite(_colTypes[colIdx]))
      {
         ytransA.clearNum(n);
         ytransb.subProduct(minusRedCost, upper[colIdx]);
         temp -= minusRedCost;

         assert(ytransb >= 0);
         assert(temp >= 0);
         assert(temp == 0 || ytransb / temp > B);

         // if ytransA and ytransb are zero, we have 0^T x >= 0 and cannot compute a Farkas box
         if(temp == 0 && ytransb == 0)
         {
            MSG_INFO1(spxout, spxout <<
                      "Approximate Farkas proof to weak.  Could not compute Farkas box. (2)\n");
            return;
         }
         // if ytransb is positive and ytransA is zero, we have 0^T x > 0, proving infeasibility
         else if(temp == 0)
         {
            assert(ytransb > 0);
            MSG_INFO1(spxout, spxout << "Farkas infeasibility proof verified exactly. (2)\n");
            return;
         }
         else
         {
            B = ytransb / temp;
            MSG_DEBUG(std::cout << "B = " << rationalToString(B) << "\n");
         }

         success = true;
      }
      // the multiplier is zero, we can ignore the bound constraints on this variable
      else if(minusRedCost == 0)
         ytransA.clearNum(n);
      // currently this bound cannot be used to increase B; we will check it again in the next round, because B might
      // have increased by then
      else
         n++;
   }

   if(B > 0)
   {
      MSG_INFO1(spxout, spxout <<
                "Computed Farkas box: provably no feasible solutions with components less than "
                << rationalToString(B) << " in absolute value.\n");
   }
}



/// solves real LP during iterative refinement
SPxSolver::Status SoPlex::_solveRealForRational(bool fromscratch, VectorReal& primal,
      VectorReal& dual, DataArray< SPxSolver::VarStatus >& basisStatusRows,
      DataArray< SPxSolver::VarStatus >& basisStatusCols, bool& returnedBasis)
{
   assert(_isConsistent());

   assert(_solver.nRows() == numRowsRational());
   assert(_solver.nCols() == numColsRational());
   assert(primal.dim() == numColsRational());
   assert(dual.dim() == numRowsRational());

   SPxSolver::Status result = SPxSolver::UNKNOWN;

#ifndef SOPLEX_MANUAL_ALT

   if(fromscratch || !_hasBasis)
      _enableSimplifierAndScaler();
   else
      _disableSimplifierAndScaler();

#else
   _disableSimplifierAndScaler();
#endif

   // start timing
   _statistics->syncTime->start();

   // if preprocessing is applied, we need to restore the original LP at the end
   SPxLPRational* rationalLP = 0;

   if(_simplifier != 0 || _scaler != 0)
   {
      spx_alloc(rationalLP);
      rationalLP = new(rationalLP) SPxLPRational(_solver);
   }

   // if preprocessing is applied, the basis may change, hence invalidate the rational basis factorization; if no
   if(_simplifier != 0 || _scaler != 0)
      _rationalLUSolver.clear();

   // stop timing
   _statistics->syncTime->stop();

   returnedBasis = false;

   try
   {
      // apply problem simplification
      SPxSimplifier::Result simplificationStatus = SPxSimplifier::OKAY;

      if(_simplifier != 0)
      {
         // do not remove bounds of boxed variables or sides of ranged rows if bound flipping is used
         bool keepbounds = intParam(SoPlex::RATIOTESTER) == SoPlex::RATIOTESTER_BOUNDFLIPPING;
         simplificationStatus = _simplifier->simplify(_solver, realParam(SoPlex::EPSILON_ZERO),
                                realParam(SoPlex::FPFEASTOL), realParam(SoPlex::FPOPTTOL), keepbounds);
      }

      // apply scaling after the simplification
      if(_scaler != 0 && simplificationStatus == SPxSimplifier::OKAY)
         _scaler->scale(_solver, false);

      // run the simplex method if problem has not been solved by the simplifier
      if(simplificationStatus == SPxSimplifier::OKAY)
      {
         MSG_INFO1(spxout, spxout << std::endl);

         _solveRealLPAndRecordStatistics();

         MSG_INFO1(spxout, spxout << std::endl);
      }

      ///@todo move to private helper methods
      // evaluate status flag
      if(simplificationStatus == SPxSimplifier::INFEASIBLE)
         result = SPxSolver::INFEASIBLE;
      else if(simplificationStatus == SPxSimplifier::DUAL_INFEASIBLE)
         result = SPxSolver::INForUNBD;
      else if(simplificationStatus == SPxSimplifier::UNBOUNDED)
         result = SPxSolver::UNBOUNDED;
      else if(simplificationStatus == SPxSimplifier::VANISHED
              || simplificationStatus == SPxSimplifier::OKAY)
      {
         result = simplificationStatus == SPxSimplifier::VANISHED ? SPxSolver::OPTIMAL : _solver.status();

         ///@todo move to private helper methods
         // process result
         switch(result)
         {
         case SPxSolver::OPTIMAL:

            // unsimplify if simplifier is active and LP is solved to optimality; this must be done here and not at solution
            // query, because we want to have the basis for the original problem
            if(_simplifier != 0)
            {
               assert(!_simplifier->isUnsimplified());
               assert(simplificationStatus == SPxSimplifier::VANISHED
                      || simplificationStatus == SPxSimplifier::OKAY);

               bool vanished = simplificationStatus == SPxSimplifier::VANISHED;

               // get solution vectors for transformed problem
               DVectorReal tmpPrimal(vanished ? 0 : _solver.nCols());
               DVectorReal tmpSlacks(vanished ? 0 : _solver.nRows());
               DVectorReal tmpDual(vanished ? 0 : _solver.nRows());
               DVectorReal tmpRedCost(vanished ? 0 : _solver.nCols());

               if(!vanished)
               {
                  assert(_solver.status() == SPxSolver::OPTIMAL);

                  _solver.getPrimal(tmpPrimal);
                  _solver.getSlacks(tmpSlacks);
                  _solver.getDual(tmpDual);
                  _solver.getRedCost(tmpRedCost);

                  // unscale vectors
                  if(_scaler != 0)
                  {
                     _scaler->unscalePrimal(_solver, tmpPrimal);
                     _scaler->unscaleSlacks(_solver, tmpSlacks);
                     _scaler->unscaleDual(_solver, tmpDual);
                     _scaler->unscaleRedCost(_solver, tmpRedCost);
                  }

                  // get basis of transformed problem
                  basisStatusRows.reSize(_solver.nRows());
                  basisStatusCols.reSize(_solver.nCols());
                  _solver.getBasis(basisStatusRows.get_ptr(), basisStatusCols.get_ptr(), basisStatusRows.size(),
                                   basisStatusCols.size());
               }

               ///@todo catch exception
               _simplifier->unsimplify(tmpPrimal, tmpDual, tmpSlacks, tmpRedCost, basisStatusRows.get_ptr(),
                                       basisStatusCols.get_ptr());

               // store basis for original problem
               basisStatusRows.reSize(numRowsRational());
               basisStatusCols.reSize(numColsRational());
               _simplifier->getBasis(basisStatusRows.get_ptr(), basisStatusCols.get_ptr(), basisStatusRows.size(),
                                     basisStatusCols.size());
               returnedBasis = true;

               primal = _simplifier->unsimplifiedPrimal();
               dual = _simplifier->unsimplifiedDual();
            }
            // if the original problem is not in the solver because of scaling, we also need to store the basis
            else
            {
               _solver.getPrimal(primal);
               _solver.getDual(dual);

               // unscale vectors
               if(_scaler != 0)
               {
                  _scaler->unscalePrimal(_solver, primal);
                  _scaler->unscaleDual(_solver, dual);
               }

               // get basis of transformed problem
               basisStatusRows.reSize(_solver.nRows());
               basisStatusCols.reSize(_solver.nCols());
               _solver.getBasis(basisStatusRows.get_ptr(), basisStatusCols.get_ptr(), basisStatusRows.size(),
                                basisStatusCols.size());
               returnedBasis = true;
            }

            break;

         case SPxSolver::ABORT_CYCLING:
            if(_simplifier == 0 && boolParam(SoPlex::ACCEPTCYCLING))
            {
               _solver.getPrimal(primal);
               _solver.getDual(dual);

               // unscale vectors
               if(_scaler != 0)
               {
                  _scaler->unscalePrimal(_solver, primal);
                  _scaler->unscaleDual(_solver, dual);
               }

               // get basis of transformed problem
               basisStatusRows.reSize(_solver.nRows());
               basisStatusCols.reSize(_solver.nCols());
               _solver.getBasis(basisStatusRows.get_ptr(), basisStatusCols.get_ptr(), basisStatusRows.size(),
                                basisStatusCols.size());
               returnedBasis = true;
               result = SPxSolver::OPTIMAL;
            }

            break;

         case SPxSolver::ABORT_TIME:
         case SPxSolver::ABORT_ITER:
         case SPxSolver::ABORT_VALUE:
         case SPxSolver::REGULAR:
         case SPxSolver::RUNNING:
         case SPxSolver::UNBOUNDED:
            break;

         case SPxSolver::INFEASIBLE:

            // if simplifier is active we cannot return a Farkas ray currently
            if(_simplifier != 0)
               break;

            // return Farkas ray as dual solution
            _solver.getDualfarkas(dual);

            // unscale vectors
            if(_scaler != 0)
               _scaler->unscaleDual(_solver, dual);

            // if the original problem is not in the solver because of scaling, we also need to store the basis
            basisStatusRows.reSize(_solver.nRows());
            basisStatusCols.reSize(_solver.nCols());
            _solver.getBasis(basisStatusRows.get_ptr(), basisStatusCols.get_ptr(), basisStatusRows.size(),
                             basisStatusCols.size());
            returnedBasis = true;
            break;

         case SPxSolver::INForUNBD:
         case SPxSolver::SINGULAR:
         default:
            break;
         }
      }
   }
   catch(...)
   {
      MSG_INFO1(spxout, spxout << "Exception thrown during floating-point solve.\n");
      result = SPxSolver::ERROR;
   }

   // restore original LP if necessary
   if(_simplifier != 0 || _scaler != 0)
   {
      assert(rationalLP != 0);
      _solver.loadLP((SPxLPReal)(*rationalLP));
      rationalLP->~SPxLPRational();
      spx_free(rationalLP);

      if(_hasBasis)
         _solver.setBasis(basisStatusRows.get_ptr(), basisStatusCols.get_ptr());
   }

   return result;
}



/// solves real LP with recovery mechanism
SPxSolver::Status SoPlex::_solveRealStable(bool acceptUnbounded, bool acceptInfeasible,
      VectorReal& primal, VectorReal& dual, DataArray< SPxSolver::VarStatus >& basisStatusRows,
      DataArray< SPxSolver::VarStatus >& basisStatusCols, bool& returnedBasis,
      const bool forceNoSimplifier)
{
   SPxSolver::Status result = SPxSolver::UNKNOWN;

   bool fromScratch = false;
   bool solved = false;
   bool solvedFromScratch = false;
   bool initialSolve = true;
   bool increasedMarkowitz = false;
   bool relaxedTolerances = false;
   bool tightenedTolerances = false;
   bool switchedScaler = false;
   bool switchedSimplifier = false;
   bool switchedRatiotester = false;
   bool switchedPricer = false;
   bool turnedoffPre = false;

   Real markowitz = _slufactor.markowitz();
   int ratiotester = intParam(SoPlex::RATIOTESTER);
   int pricer = intParam(SoPlex::PRICER);
   int simplifier = intParam(SoPlex::SIMPLIFIER);
   int scaler = intParam(SoPlex::SCALER);
   int type = intParam(SoPlex::ALGORITHM);

   if(forceNoSimplifier)
      setIntParam(SoPlex::SIMPLIFIER, SoPlex::SIMPLIFIER_OFF);

   while(true)
   {
      assert(!increasedMarkowitz || GE(_slufactor.markowitz(), 0.9));

      result = _solveRealForRational(fromScratch, primal, dual, basisStatusRows, basisStatusCols,
                                     returnedBasis);

      solved = (result == SPxSolver::OPTIMAL)
               || (result == SPxSolver::INFEASIBLE && acceptInfeasible)
               || (result == SPxSolver::UNBOUNDED && acceptUnbounded);

      if(solved)
         break;

      //         if( _isSolveStopped() )
      //            break;

      if(initialSolve)
      {
         MSG_INFO1(spxout, spxout << "Numerical troubles during floating-point solve." << std::endl);
         initialSolve = false;
      }

      if(!turnedoffPre
            && (intParam(SoPlex::SIMPLIFIER) != SoPlex::SIMPLIFIER_OFF
                || intParam(SoPlex::SCALER) != SoPlex::SCALER_OFF))
      {
         MSG_INFO1(spxout, spxout << "Turning off preprocessing." << std::endl);

         turnedoffPre = true;

         setIntParam(SoPlex::SCALER, SoPlex::SCALER_OFF);
         setIntParam(SoPlex::SIMPLIFIER, SoPlex::SIMPLIFIER_OFF);

         fromScratch = true;
         _solver.reLoad();
         solvedFromScratch = true;
         continue;
      }

      setIntParam(SoPlex::SCALER, scaler);
      setIntParam(SoPlex::SIMPLIFIER, simplifier);

      if(!increasedMarkowitz)
      {
         MSG_INFO1(spxout, spxout << "Increasing Markowitz threshold." << std::endl);

         _slufactor.setMarkowitz(0.9);
         increasedMarkowitz = true;

         try
         {
            _solver.factorize();
            continue;
         }
         catch(...)
         {
            MSG_DEBUG(std::cout << std::endl << "Factorization failed." << std::endl);
         }
      }

      if(!solvedFromScratch)
      {
         MSG_INFO1(spxout, spxout << "Solving from scratch." << std::endl);

         fromScratch = true;
         _solver.reLoad();

         solvedFromScratch = true;
         continue;
      }

      setIntParam(SoPlex::RATIOTESTER, ratiotester);
      setIntParam(SoPlex::PRICER, pricer);

      if(!switchedScaler)
      {
         MSG_INFO1(spxout, spxout << "Switching scaling." << std::endl);

         if(scaler == int(SoPlex::SCALER_OFF))
            setIntParam(SoPlex::SCALER, SoPlex::SCALER_BIEQUI);
         else
            setIntParam(SoPlex::SCALER, SoPlex::SCALER_OFF);

         fromScratch = true;
         _solver.reLoad();

         solvedFromScratch = true;
         switchedScaler = true;
         continue;
      }

      if(!switchedSimplifier && !forceNoSimplifier)
      {
         MSG_INFO1(spxout, spxout << "Switching simplification." << std::endl);

         if(simplifier == int(SoPlex::SIMPLIFIER_OFF))
            setIntParam(SoPlex::SIMPLIFIER, SoPlex::SIMPLIFIER_AUTO);
         else
            setIntParam(SoPlex::SIMPLIFIER, SoPlex::SIMPLIFIER_OFF);

         fromScratch = true;
         _solver.reLoad();

         solvedFromScratch = true;
         switchedSimplifier = true;
         continue;
      }

      setIntParam(SoPlex::SIMPLIFIER, SoPlex::SIMPLIFIER_OFF);

      if(!relaxedTolerances)
      {
         MSG_INFO1(spxout, spxout << "Relaxing tolerances." << std::endl);

         setIntParam(SoPlex::ALGORITHM, SoPlex::ALGORITHM_PRIMAL);
         _solver.setDelta((_solver.feastol() * 1e3 > 1e-3) ? 1e-3 : (_solver.feastol() * 1e3));
         relaxedTolerances = _solver.feastol() >= 1e-3;
         solvedFromScratch = false;
         continue;
      }

      if(!tightenedTolerances && result != SPxSolver::INFEASIBLE)
      {
         MSG_INFO1(spxout, spxout << "Tightening tolerances." << std::endl);

         setIntParam(SoPlex::ALGORITHM, SoPlex::ALGORITHM_DUAL);
         _solver.setDelta(_solver.feastol() * 1e-3 < 1e-9 ? 1e-9 : _solver.feastol() * 1e-3);
         tightenedTolerances = _solver.feastol() <= 1e-9;
         solvedFromScratch = false;
         continue;
      }

      setIntParam(SoPlex::ALGORITHM, type);

      if(!switchedRatiotester)
      {
         MSG_INFO1(spxout, spxout << "Switching ratio test." << std::endl);

         _solver.setType(_solver.type() == SPxSolver::LEAVE ? SPxSolver::ENTER : SPxSolver::LEAVE);

         if(_solver.ratiotester() != (SPxRatioTester*)&_ratiotesterTextbook)
            setIntParam(SoPlex::RATIOTESTER, RATIOTESTER_TEXTBOOK);
         else
            setIntParam(SoPlex::RATIOTESTER, RATIOTESTER_FAST);

         switchedRatiotester = true;
         solvedFromScratch = false;
         continue;
      }

      if(!switchedPricer)
      {
         MSG_INFO1(spxout, spxout << "Switching pricer." << std::endl);

         _solver.setType(_solver.type() == SPxSolver::LEAVE ? SPxSolver::ENTER : SPxSolver::LEAVE);

         if(_solver.pricer() != (SPxPricer*)&_pricerDevex)
            setIntParam(SoPlex::PRICER, PRICER_DEVEX);
         else
            setIntParam(SoPlex::PRICER, PRICER_STEEP);

         switchedPricer = true;
         solvedFromScratch = false;
         continue;
      }

      MSG_INFO1(spxout, spxout << "Giving up." << std::endl);

      break;
   }

   _solver.setFeastol(realParam(SoPlex::FPFEASTOL));
   _solver.setOpttol(realParam(SoPlex::FPOPTTOL));
   _slufactor.setMarkowitz(markowitz);

   setIntParam(SoPlex::RATIOTESTER, ratiotester);
   setIntParam(SoPlex::PRICER, pricer);
   setIntParam(SoPlex::SIMPLIFIER, simplifier);
   setIntParam(SoPlex::SCALER, scaler);
   setIntParam(SoPlex::ALGORITHM, type);

   return result;
}



/// computes rational inverse of basis matrix as defined by _rationalLUSolverBind
void SoPlex::_computeBasisInverseRational()
{
   assert(_rationalLUSolver.status() == SLinSolverRational::UNLOADED
          || _rationalLUSolver.status() == SLinSolverRational::TIME);

   const int matrixdim = numRowsRational();
   assert(_rationalLUSolverBind.size() == matrixdim);

   DataArray< const SVectorRational* > matrix(matrixdim);
   _rationalLUSolverBind.reSize(matrixdim);

   for(int i = 0; i < matrixdim; i++)
   {
      if(_rationalLUSolverBind[i] >= 0)
      {
         assert(_rationalLUSolverBind[i] < numColsRational());
         matrix[i] = &colVectorRational(_rationalLUSolverBind[i]);
      }
      else
      {
         assert(-1 - _rationalLUSolverBind[i] >= 0);
         assert(-1 - _rationalLUSolverBind[i] < numRowsRational());
         matrix[i] = _unitVectorRational(-1 - _rationalLUSolverBind[i]);
      }
   }

   // load and factorize rational basis matrix
   if(realParam(SoPlex::TIMELIMIT) < realParam(SoPlex::INFTY))
      _rationalLUSolver.setTimeLimit(realParam(SoPlex::TIMELIMIT) - _statistics->solvingTime->time());
   else
      _rationalLUSolver.setTimeLimit(-1.0);

   _rationalLUSolver.load(matrix.get_ptr(), matrixdim);

   // record statistics
   _statistics->luFactorizationTimeRational += _rationalLUSolver.getFactorTime();
   _statistics->luFactorizationsRational += _rationalLUSolver.getFactorCount();
   _rationalLUSolver.resetCounters();

   if(_rationalLUSolver.status() == SLinSolverRational::TIME)
   {
      MSG_INFO2(spxout, spxout << "Rational factorization hit time limit.\n");
   }
   else if(_rationalLUSolver.status() != SLinSolverRational::OK)
   {
      MSG_INFO1(spxout, spxout << "Error performing rational LU factorization.\n");
   }

   return;
}



/// factorizes rational basis matrix in column representation
void SoPlex::_factorizeColumnRational(SolRational& sol,
                                      DataArray< SPxSolver::VarStatus >& basisStatusRows,
                                      DataArray< SPxSolver::VarStatus >& basisStatusCols, bool& stoppedTime, bool& stoppedIter,
                                      bool& error, bool& optimal)
{
   // start rational solving time
   _statistics->rationalTime->start();

   stoppedTime = false;
   stoppedIter = false;
   error = false;
   optimal = false;

   const bool maximizing = (intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MAXIMIZE);
   const int matrixdim = numRowsRational();
   bool loadMatrix = (_rationalLUSolver.status() == SLinSolverRational::UNLOADED
                      || _rationalLUSolver.status() == SLinSolverRational::TIME);
   int numBasicRows;

   assert(loadMatrix || matrixdim == _rationalLUSolver.dim());
   assert(loadMatrix || matrixdim == _rationalLUSolverBind.size());

   if(!loadMatrix && (matrixdim != _rationalLUSolver.dim()
                      || matrixdim != _rationalLUSolverBind.size()))
   {
      MSG_WARNING(spxout, spxout <<
                  "Warning: dimensioning error in rational matrix factorization (recovered).\n");
      loadMatrix = true;
   }

   _workSol._primal.reDim(matrixdim);
   _workSol._slacks.reDim(matrixdim);
   _workSol._dual.reDim(matrixdim);
   _workSol._redCost.reDim(numColsRational() > matrixdim ? numColsRational() : matrixdim);

   if(loadMatrix)
      _rationalLUSolverBind.reSize(matrixdim);

   DVectorRational& basicPrimalRhs = _workSol._slacks;
   DVectorRational& basicDualRhs = _workSol._redCost;
   DVectorRational& basicPrimal = _workSol._primal;
   DVectorRational& basicDual = _workSol._dual;

   Rational violation;
   Rational primalViolation;
   Rational dualViolation;
   bool primalFeasible = false;
   bool dualFeasible = false;

   assert(basisStatusCols.size() == numColsRational());
   assert(basisStatusRows.size() == numRowsRational());

   int j = 0;

   for(int i = 0; i < basisStatusRows.size(); i++)
   {
      if(basisStatusRows[i] == SPxSolver::BASIC && j < matrixdim)
      {
         basicPrimalRhs[i] = 0;
         basicDualRhs[j] = 0;

         if(loadMatrix)
            _rationalLUSolverBind[j] = -1 - i;

         j++;
      }
      else if(basisStatusRows[i] == SPxSolver::ON_LOWER)
         basicPrimalRhs[i] = lhsRational(i);
      else if(basisStatusRows[i] == SPxSolver::ON_UPPER)
         basicPrimalRhs[i] = rhsRational(i);
      else if(basisStatusRows[i] == SPxSolver::ZERO)
         basicPrimalRhs[i] = 0;
      else if(basisStatusRows[i] == SPxSolver::FIXED)
      {
         assert(lhsRational(i) == rhsRational(i));
         basicPrimalRhs[i] = lhsRational(i);
      }
      else if(basisStatusRows[i] == SPxSolver::UNDEFINED)
      {
         MSG_INFO1(spxout, spxout << "Undefined basis status of row in rational factorization.\n");
         error = true;
         goto TERMINATE;
      }
      else
      {
         assert(basisStatusRows[i] == SPxSolver::BASIC);
         MSG_INFO1(spxout, spxout << "Too many basic rows in rational factorization.\n");
         error = true;
         goto TERMINATE;
      }
   }

   numBasicRows = j;

   for(int i = 0; i < basisStatusCols.size(); i++)
   {
      if(basisStatusCols[i] == SPxSolver::BASIC && j < matrixdim)
      {
         basicDualRhs[j] = objRational(i);

         if(loadMatrix)
            _rationalLUSolverBind[j] = i;

         j++;
      }
      else if(basisStatusCols[i] == SPxSolver::ON_LOWER)
         basicPrimalRhs.multAdd(-lowerRational(i), colVectorRational(i));
      else if(basisStatusCols[i] == SPxSolver::ON_UPPER)
         basicPrimalRhs.multAdd(-upperRational(i), colVectorRational(i));
      else if(basisStatusCols[i] == SPxSolver::ZERO)
      {}
      else if(basisStatusCols[i] == SPxSolver::FIXED)
      {
         assert(lowerRational(i) == upperRational(i));
         basicPrimalRhs.multAdd(-lowerRational(i), colVectorRational(i));
      }
      else if(basisStatusCols[i] == SPxSolver::UNDEFINED)
      {
         MSG_INFO1(spxout, spxout << "Undefined basis status of column in rational factorization.\n");
         error = true;
         goto TERMINATE;
      }
      else
      {
         assert(basisStatusCols[i] == SPxSolver::BASIC);
         MSG_INFO1(spxout, spxout << "Too many basic columns in rational factorization.\n");
         error = true;
         goto TERMINATE;
      }
   }

   if(j != matrixdim)
   {
      MSG_INFO1(spxout, spxout << "Too few basic entries in rational factorization.\n");
      error = true;
      goto TERMINATE;
   }

   // load and factorize rational basis matrix
   if(loadMatrix)
      _computeBasisInverseRational();

   if(_rationalLUSolver.status() == SLinSolverRational::TIME)
   {
      stoppedTime = true;
      return;
   }
   else if(_rationalLUSolver.status() != SLinSolverRational::OK)
   {
      error = true;
      return;
   }

   assert(_rationalLUSolver.status() == SLinSolverRational::OK);

   // solve for primal solution
   if(realParam(SoPlex::TIMELIMIT) < realParam(SoPlex::INFTY))
      _rationalLUSolver.setTimeLimit(realParam(SoPlex::TIMELIMIT) - _statistics->solvingTime->time());
   else
      _rationalLUSolver.setTimeLimit(-1.0);

   _rationalLUSolver.solveRight(basicPrimal, basicPrimalRhs);

   // record statistics
   _statistics->luSolveTimeRational += _rationalLUSolver.getSolveTime();
   _rationalLUSolver.resetCounters();

   if(_isSolveStopped(stoppedTime, stoppedIter))
   {
      MSG_INFO2(spxout, spxout << "Rational factorization hit time limit while solving for primal.\n");
      return;
   }

   // check bound violation on basic rows and columns
   j = 0;
   primalViolation = 0;
   primalFeasible = true;

   for(int i = 0; i < basisStatusRows.size(); i++)
   {
      if(basisStatusRows[i] == SPxSolver::BASIC)
      {
         assert(j < matrixdim);
         assert(_rationalLUSolverBind[j] == -1 - i);
         violation = lhsRational(i);
         violation += basicPrimal[j];

         if(violation > primalViolation)
         {
            primalFeasible = false;
            primalViolation = violation;
         }

         violation = rhsRational(i);
         violation += basicPrimal[j];
         violation *= -1;

         if(violation > primalViolation)
         {
            primalFeasible = false;
            primalViolation = violation;
         }

         j++;
      }
   }

   for(int i = 0; i < basisStatusCols.size(); i++)
   {
      if(basisStatusCols[i] == SPxSolver::BASIC)
      {
         assert(j < matrixdim);
         assert(_rationalLUSolverBind[j] == i);

         if(basicPrimal[j] < lowerRational(i))
         {
            violation = lowerRational(i);
            violation -= basicPrimal[j];

            if(violation > primalViolation)
            {
               primalFeasible = false;
               primalViolation = violation;
            }
         }

         if(basicPrimal[j] > upperRational(i))
         {
            violation = basicPrimal[j];
            violation -= upperRational(i);

            if(violation > primalViolation)
            {
               primalFeasible = false;
               primalViolation = violation;
            }
         }

         j++;
      }
   }

   if(!primalFeasible)
   {
      MSG_INFO1(spxout, spxout << "Rational solution primal infeasible.\n");
   }

   // solve for dual solution
   if(realParam(SoPlex::TIMELIMIT) < realParam(SoPlex::INFTY))
      _rationalLUSolver.setTimeLimit(realParam(SoPlex::TIMELIMIT) - _statistics->solvingTime->time());
   else
      _rationalLUSolver.setTimeLimit(-1.0);

   _rationalLUSolver.solveLeft(basicDual, basicDualRhs);

   // record statistics
   _statistics->luSolveTimeRational += _rationalLUSolver.getSolveTime();
   _rationalLUSolver.resetCounters();

   if(_isSolveStopped(stoppedTime, stoppedIter))
   {
      MSG_INFO2(spxout, spxout << "Rational factorization hit time limit while solving for dual.\n");
      return;
   }

   // check dual violation on nonbasic rows
   dualViolation = 0;
   dualFeasible = true;

   for(int i = 0; i < basisStatusRows.size(); i++)
   {
      if(_rowTypes[i] == RANGETYPE_FIXED
            && (basisStatusRows[i] == SPxSolver::ON_LOWER || basisStatusRows[i] == SPxSolver::ON_UPPER))
      {
         assert(lhsRational(i) == rhsRational(i));
         basisStatusRows[i] = SPxSolver::FIXED;
      }

      assert(basisStatusRows[i] != SPxSolver::BASIC || basicDual[i] == 0);

      if(basisStatusRows[i] == SPxSolver::BASIC || basisStatusRows[i] == SPxSolver::FIXED)
         continue;
      else if(basicDual[i] < 0)
      {
         if(((maximizing && basisStatusRows[i] != SPxSolver::ON_LOWER) || (!maximizing
               && basisStatusRows[i] != SPxSolver::ON_UPPER))
               && (basisStatusRows[i] != SPxSolver::ZERO || rhsRational(i) != 0))
         {
            dualFeasible = false;
            violation = -basicDual[i];

            if(violation > dualViolation)
               dualViolation = violation;

            MSG_DEBUG(spxout << "negative dual multliplier for row " << i
                      << " with dual " << rationalToString(basicDual[i])
                      << " and status " << basisStatusRows[i]
                      << " and [lhs,rhs] = [" << rationalToString(lhsRational(i)) << "," << rationalToString(rhsRational(
                               i)) << "]"
                      << "\n");
         }
      }
      else if(basicDual[i] > 0)
      {
         if(((maximizing && basisStatusRows[i] != SPxSolver::ON_UPPER) || (!maximizing
               && basisStatusRows[i] != SPxSolver::ON_LOWER))
               && (basisStatusRows[i] != SPxSolver::ZERO || lhsRational(i) == 0))
         {
            dualFeasible = false;

            if(basicDual[i] > dualViolation)
               dualViolation = basicDual[i];

            MSG_DEBUG(spxout << "positive dual multliplier for row " << i
                      << " with dual " << rationalToString(basicDual[i])
                      << " and status " << basisStatusRows[i]
                      << " and [lhs,rhs] = [" << rationalToString(lhsRational(i)) << "," << rationalToString(rhsRational(
                               i)) << "]"
                      << "\n");
         }
      }
   }

   // check reduced cost violation on nonbasic columns
   for(int i = 0; i < basisStatusCols.size(); i++)
   {
      if(_colTypes[i] == RANGETYPE_FIXED
            && (basisStatusCols[i] == SPxSolver::ON_LOWER || basisStatusCols[i] == SPxSolver::ON_UPPER))
      {
         assert(lowerRational(i) == upperRational(i));
         basisStatusCols[i] = SPxSolver::FIXED;
      }

#ifdef SOPLEX_WITH_GMP
      assert(basisStatusCols[i] != SPxSolver::BASIC
             || basicDual * colVectorRational(i) == objRational(i));
#endif

      if(basisStatusCols[i] == SPxSolver::BASIC || basisStatusCols[i] == SPxSolver::FIXED)
         continue;
      else
      {
         _workSol._redCost[i] = basicDual * colVectorRational(i);
         _workSol._redCost[i] -= objRational(i);

         if(_workSol._redCost[i] > 0)
         {
            if(((maximizing && basisStatusCols[i] != SPxSolver::ON_LOWER) || (!maximizing
                  && basisStatusCols[i] != SPxSolver::ON_UPPER))
                  && (basisStatusCols[i] != SPxSolver::ZERO || upperRational(i) != 0))
            {
               dualFeasible = false;

               if(_workSol._redCost[i] > dualViolation)
                  dualViolation = _workSol._redCost[i];
            }

            _workSol._redCost[i] *= -1;
         }
         else if(_workSol._redCost[i] < 0)
         {
            _workSol._redCost[i] *= -1;

            if(((maximizing && basisStatusCols[i] != SPxSolver::ON_UPPER) || (!maximizing
                  && basisStatusCols[i] != SPxSolver::ON_LOWER))
                  && (basisStatusCols[i] != SPxSolver::ZERO || lowerRational(i) != 0))
            {
               dualFeasible = false;

               if(_workSol._redCost[i] > dualViolation)
                  dualViolation = _workSol._redCost[i];
            }
         }
         else
            _workSol._redCost[i] *= -1;
      }
   }

   if(!dualFeasible)
   {
      MSG_INFO1(spxout, spxout << "Rational solution dual infeasible.\n");
   }

   // store solution
   optimal = primalFeasible && dualFeasible;

   if(optimal || boolParam(SoPlex::RATFACJUMP))
   {
      _hasBasis = true;

      if(&basisStatusRows != &_basisStatusRows)
         _basisStatusRows = basisStatusRows;

      if(&basisStatusCols != &_basisStatusCols)
         _basisStatusCols = basisStatusCols;

      sol._primal.reDim(numColsRational());
      j = numBasicRows;

      for(int i = 0; i < basisStatusCols.size(); i++)
      {
         if(basisStatusCols[i] == SPxSolver::BASIC)
         {
            assert(j < matrixdim);
            assert(_rationalLUSolverBind[j] == i);
            sol._primal[i] = basicPrimal[j];
            j++;
         }
         else if(basisStatusCols[i] == SPxSolver::ON_LOWER)
            sol._primal[i] = lowerRational(i);
         else if(basisStatusCols[i] == SPxSolver::ON_UPPER)
            sol._primal[i] = upperRational(i);
         else if(basisStatusCols[i] == SPxSolver::ZERO)
            sol._primal[i] = 0;
         else if(basisStatusCols[i] == SPxSolver::FIXED)
         {
            assert(lowerRational(i) == upperRational(i));
            sol._primal[i] = lowerRational(i);
         }
         else
         {
            assert(basisStatusCols[i] == SPxSolver::UNDEFINED);
            MSG_INFO1(spxout, spxout << "Undefined basis status of column in rational factorization.\n");
            error = true;
            goto TERMINATE;
         }
      }

      sol._slacks.reDim(numRowsRational());
      _rationalLP->computePrimalActivity(sol._primal, sol._slacks);
      sol._isPrimalFeasible = true;

      sol._dual = basicDual;

      for(int i = 0; i < numColsRational(); i++)
      {
         if(basisStatusCols[i] == SPxSolver::BASIC)
            sol._redCost[i] = 0;
         else if(basisStatusCols[i] == SPxSolver::FIXED)
         {
            sol._redCost[i] = basicDual * colVectorRational(i);
            sol._redCost[i] -= objRational(i);
            sol._redCost[i] *= -1;
         }
         else
            sol._redCost[i] = _workSol._redCost[i];
      }

      sol._isDualFeasible  = true;
   }

TERMINATE:
   // stop rational solving time
   _statistics->rationalTime->stop();
   return;
}

/// attempts rational reconstruction of primal-dual solution
bool SoPlex::_reconstructSolutionRational(SolRational& sol,
      DataArray< SPxSolver::VarStatus >& basisStatusRows,
      DataArray< SPxSolver::VarStatus >& basisStatusCols, const Rational& denomBoundSquared)
{
   bool success;
   bool isSolBasic;
   DIdxSet basicIndices(numColsRational());

   success = false;
   isSolBasic = true;

   if(!sol.isPrimalFeasible() || !sol.isDualFeasible())
      return success;

   // start timing and increment statistics counter
   _statistics->reconstructionTime->start();
   _statistics->rationalReconstructions++;

   // reconstruct primal vector
   _workSol._primal = sol._primal;

   for(int j = 0; j < numColsRational(); ++j)
   {
      if(basisStatusCols[j] == SPxSolver::BASIC)
         basicIndices.addIdx(j);
   }

   success = reconstructVector(_workSol._primal, denomBoundSquared, &basicIndices);

   if(!success)
   {
      MSG_INFO1(spxout, spxout << "Rational reconstruction of primal solution failed.\n");
      _statistics->reconstructionTime->stop();
      return success;
   }

   MSG_DEBUG(spxout << "Rational reconstruction of primal solution successful.\n");

   // check violation of bounds
   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      // we want to notify the user whether the reconstructed solution is basic; otherwise, this would be redundant
      SPxSolver::VarStatus& basisStatusCol = _basisStatusCols[c];

      if((basisStatusCol == SPxSolver::FIXED && _workSol._primal[c] != lowerRational(c))
            || (basisStatusCol == SPxSolver::ON_LOWER && _workSol._primal[c] != lowerRational(c))
            || (basisStatusCol == SPxSolver::ON_UPPER && _workSol._primal[c] != upperRational(c))
            || (basisStatusCol == SPxSolver::ZERO && _workSol._primal[c] != 0)
            || (basisStatusCol == SPxSolver::UNDEFINED))
      {
         isSolBasic = false;
      }

      if(_lowerFinite(_colTypes[c]) && _workSol._primal[c] < lowerRational(c))
      {
         MSG_DEBUG(std::cout << "Lower bound of variable " << c << " violated by " << rationalToString(
                      lowerRational(c) - _workSol._primal[c]) << "\n");
         MSG_INFO1(spxout, spxout << "Reconstructed solution primal infeasible (1).\n");
         _statistics->reconstructionTime->stop();
         return false;
      }

      if(_upperFinite(_colTypes[c]) && _workSol._primal[c] > upperRational(c))
      {
         MSG_DEBUG(std::cout << "Upper bound of variable " << c << " violated by " << rationalToString(
                      _workSol._primal[c] - upperRational(c)) << "\n");
         MSG_INFO1(spxout, spxout << "Reconstructed solution primal infeasible (2).\n");
         _statistics->reconstructionTime->stop();
         return false;
      }
   }

   // compute slacks
   ///@todo we should compute them one by one so we can abort when encountering an infeasibility
   _workSol._slacks.reDim(numRowsRational());
   _rationalLP->computePrimalActivity(_workSol._primal, _workSol._slacks);

   // check violation of sides
   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      // we want to notify the user whether the reconstructed solution is basic; otherwise, this would be redundant
      SPxSolver::VarStatus& basisStatusRow = _basisStatusRows[r];

      if((basisStatusRow == SPxSolver::FIXED && _workSol._slacks[r] != lhsRational(r))
            || (basisStatusRow == SPxSolver::ON_LOWER && _workSol._slacks[r] != lhsRational(r))
            || (basisStatusRow == SPxSolver::ON_UPPER && _workSol._slacks[r] != rhsRational(r))
            || (basisStatusRow == SPxSolver::ZERO && _workSol._slacks[r] != 0)
            || (basisStatusRow == SPxSolver::UNDEFINED))
      {
         isSolBasic = false;
      }

      if(_lowerFinite(_rowTypes[r]) && _workSol._slacks[r] < lhsRational(r))
      {
         MSG_DEBUG(std::cout << "Lhs of row " << r << " violated by " << rationalToString(lhsRational(
                      r) - _workSol._slacks[r]) << "\n");
         MSG_INFO1(spxout, spxout << "Reconstructed solution primal infeasible (3).\n");
         _statistics->reconstructionTime->stop();
         return false;
      }

      if(_upperFinite(_rowTypes[r]) && _workSol._slacks[r] > rhsRational(r))
      {
         MSG_DEBUG(std::cout << "Rhs of row " << r << " violated by " << rationalToString(
                      _workSol._slacks[r] - rhsRational(r)) << "\n");
         MSG_INFO1(spxout, spxout << "Reconstructed solution primal infeasible (4).\n");
         _statistics->reconstructionTime->stop();
         return false;
      }
   }

   // reconstruct dual vector
   _workSol._dual = sol._dual;

   success = reconstructVector(_workSol._dual, denomBoundSquared);

   if(!success)
   {
      MSG_INFO1(spxout, spxout << "Rational reconstruction of dual solution failed.\n");
      _statistics->reconstructionTime->stop();
      return success;
   }

   MSG_DEBUG(spxout << "Rational reconstruction of dual vector successful.\n");

   // check dual multipliers before reduced costs because this check is faster since it does not require the
   // computation of reduced costs
   const bool maximizing = (intParam(SoPlex::OBJSENSE) == SoPlex::OBJSENSE_MAXIMIZE);

   for(int r = numRowsRational() - 1; r >= 0; r--)
   {
      int sig = sign(_workSol._dual[r]);

      if((!maximizing && sig > 0) || (maximizing && sig < 0))
      {
         if(!_lowerFinite(_rowTypes[r]) || _workSol._slacks[r] > lhsRational(r))
         {
            MSG_DEBUG(std::cout << "complementary slackness violated by row " << r
                      << " with dual " << rationalToString(_workSol._dual[r])
                      << " and slack " << rationalToString(_workSol._slacks[r])
                      << " not at lhs " << rationalToString(lhsRational(r))
                      << "\n");
            MSG_INFO1(spxout, spxout << "Reconstructed solution dual infeasible (1).\n");
            _statistics->reconstructionTime->stop();
            return false;
         }

         if(_basisStatusRows[r] != SPxSolver::ON_LOWER && _basisStatusRows[r] != SPxSolver::FIXED)
         {
            if(_basisStatusRows[r] == SPxSolver::BASIC || _basisStatusRows[r] == SPxSolver::UNDEFINED)
               isSolBasic = false;
            else
               _basisStatusRows[r] = SPxSolver::ON_LOWER;
         }
      }
      else if((!maximizing && sig < 0) || (maximizing && sig > 0))
      {
         if(!_upperFinite(_rowTypes[r]) || _workSol._slacks[r] < rhsRational(r))
         {
            MSG_DEBUG(std::cout << "complementary slackness violated by row " << r
                      << " with dual " << rationalToString(_workSol._dual[r])
                      << " and slack " << rationalToString(_workSol._slacks[r])
                      << " not at rhs " << rationalToString(rhsRational(r))
                      << "\n");
            MSG_INFO1(spxout, spxout << "Reconstructed solution dual infeasible (2).\n");
            _statistics->reconstructionTime->stop();
            return false;
         }

         if(_basisStatusRows[r] != SPxSolver::ON_UPPER && _basisStatusRows[r] != SPxSolver::FIXED)
         {
            if(_basisStatusRows[r] == SPxSolver::BASIC || _basisStatusRows[r] == SPxSolver::UNDEFINED)
               isSolBasic = false;
            else
               _basisStatusRows[r] = SPxSolver::ON_UPPER;
         }
      }
   }

   // compute reduced cost vector; we assume that the objective function vector has less nonzeros than the reduced
   // cost vector, and so multiplying with -1 first and subtracting the dual activity should be faster than adding
   // the dual activity and negating afterwards
   ///@todo we should compute them one by one so we can abort when encountering an infeasibility
   _workSol._redCost.reDim(numColsRational());
   _rationalLP->getObj(_workSol._redCost);
   _rationalLP->subDualActivity(_workSol._dual, _workSol._redCost);

   // check reduced cost violation
   for(int c = numColsRational() - 1; c >= 0; c--)
   {
      int sig = sign(_workSol._redCost[c]);

      if((!maximizing && sig > 0) || (maximizing && sig < 0))
      {
         if(!_lowerFinite(_colTypes[c]) || _workSol._primal[c] > lowerRational(c))
         {
            MSG_DEBUG(std::cout << "complementary slackness violated by column " << c
                      << " with reduced cost " << rationalToString(_workSol._redCost[c])
                      << " and value " << rationalToString(_workSol._primal[c])
                      << " not at lower bound " << rationalToString(lowerRational(c))
                      << "\n");
            MSG_INFO1(spxout, spxout << "Reconstructed solution dual infeasible (3).\n");
            _statistics->reconstructionTime->stop();
            return false;
         }

         if(_basisStatusCols[c] != SPxSolver::ON_LOWER && _basisStatusCols[c] != SPxSolver::FIXED)
         {
            if(_basisStatusCols[c] == SPxSolver::BASIC || _basisStatusCols[c] == SPxSolver::UNDEFINED)
               isSolBasic = false;
            else
               _basisStatusCols[c] = SPxSolver::ON_LOWER;
         }
      }
      else if((!maximizing && sig < 0) || (maximizing && sig > 0))
      {
         if(!_upperFinite(_colTypes[c]) || _workSol._primal[c] < upperRational(c))
         {
            MSG_DEBUG(std::cout << "complementary slackness violated by column " << c
                      << " with reduced cost " << rationalToString(_workSol._redCost[c])
                      << " and value " << rationalToString(_workSol._primal[c])
                      << " not at upper bound " << rationalToString(upperRational(c))
                      << "\n");
            MSG_INFO1(spxout, spxout << "Reconstructed solution dual infeasible (4).\n");
            _statistics->reconstructionTime->stop();
            return false;
         }

         if(_basisStatusCols[c] != SPxSolver::ON_UPPER && _basisStatusCols[c] != SPxSolver::FIXED)
         {
            if(_basisStatusCols[c] == SPxSolver::BASIC || _basisStatusCols[c] == SPxSolver::UNDEFINED)
               isSolBasic = false;
            else
               _basisStatusCols[c] = SPxSolver::ON_UPPER;
         }
      }
   }

   // update solution
   sol._primal = _workSol._primal;
   sol._slacks = _workSol._slacks;
   sol._dual = _workSol._dual;
   sol._redCost = _workSol._redCost;

   if(!isSolBasic)
   {
      MSG_WARNING(spxout, spxout << "Warning: Reconstructed solution not basic.\n");
      _hasBasis = false;
   }

   // stop timing
   _statistics->reconstructionTime->stop();

   return success;
}
} // namespace soplex