text: /***************************************************************************************[Solver.cc]
  Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  Copyright (c) 2007-2009, Niklas Sorensson
  Copyright (c) 2009-2012, Mate Soos
  
  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  associated documentation files (the "Software"), to deal in the Software without restriction,
  including without limitation the rights to use, copy, modify, merge, publish, distribute,
  sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  furnished to do so, subject to the following conditions:
  
  The above copyright notice and this permission notice shall be included in all copies or
  substantial portions of the Software.
  
  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  **************************************************************************************************/
  
  #include "cmsat/Solver.h"
  #include "cmsat/VarReplacer.h"
  #include "cmsat/Subsumer.h"
  #include "cmsat/XorSubsumer.h"
  #include "cmsat/time_mem.h"
  #include "cmsat/DimacsParser.h"
  #include "cmsat/FailedLitSearcher.h"
  #include "cmsat/DataSync.h"
  #include "cmsat/SCCFinder.h"
  #include <iomanip>
  #include <omp.h>
  
  #ifdef USE_GAUSS
  #include "cmsat/Gaussian.h"
  #endif
  
  #ifndef _MSC_VER
  #include <sys/time.h>
  #include <sys/resource.h>
  #endif
  
  using namespace CMSat;
  
  static const int space = 10;
  
  bool Solver::dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize)
  {
      FILE* outfile = fopen(fileName.c_str(), "w");
      if (!outfile)
          return false;
  
      fprintf(outfile, "c \nc ---------\n");
      fprintf(outfile, "c unitaries\n");
      fprintf(outfile, "c ---------\n");
      for (uint32_t i = 0, end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size() ; i < end; i++) {
          trail[i].printFull(outfile);
      }
  
      fprintf(outfile, "c conflicts %lu\n", (unsigned long)conflicts);
      if (maxSize == 1) goto end;
  
      fprintf(outfile, "c \nc ---------------------------------\n");
      fprintf(outfile, "c learnt binary clauses (extracted from watchlists)\n");
      fprintf(outfile, "c ---------------------------------\n");
      dumpBinClauses(true, false, outfile);
  
      fprintf(outfile, "c \nc ---------------------------------------\n");
      fprintf(outfile, "c clauses representing 2-long XOR clauses\n");
      fprintf(outfile, "c ---------------------------------------\n");
      {
          const vector<Lit>& table = varReplacer->getReplaceTable();
          for (Var var = 0; var != table.size(); var++) {
              Lit lit = table[var];
              if (lit.var() == var)
                  continue;
  
              fprintf(outfile, "%s%d %d 0\n", (!lit.sign() ? "-" : ""), lit.var()+1, var+1);
              fprintf(outfile, "%s%d -%d 0\n", (lit.sign() ? "-" : ""), lit.var()+1, var+1);
          }
      }
      fprintf(outfile, "c \nc --------------------\n");
      fprintf(outfile, "c clauses from learnts\n");
      fprintf(outfile, "c --------------------\n");
      if (lastSelectedRestartType == dynamic_restart)
          std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
      else
          std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
      for (int i = learnts.size()-1; i >= 0 ; i--) {
          if (learnts[i]->size() <= maxSize) {
              learnts[i]->print(outfile);
          }
      }
  
      end:
  
      fclose(outfile);
      return true;
  }
  
  void Solver::printStrangeBinLit(const Lit lit) const
  {
      const vec<Watched>& ws = watches[(~lit).toInt()];
      for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
          if (it2->isBinary()) {
              std::cout << "bin: " << lit << " , " << it2->getOtherLit() << " learnt : " <<  (it2->getLearnt()) << std::endl;
          } else if (it2->isTriClause()) {
              std::cout << "tri: " << lit << " , " << it2->getOtherLit() << " , " <<  (it2->getOtherLit2()) << std::endl;
          } else if (it2->isClause()) {
              std::cout << "cla:" << it2->getNormOffset() << std::endl;
          } else {
              assert(it2->isXorClause());
              std::cout << "xor:" << it2->getXorOffset() << std::endl;
          }
      }
  }
  
  uint32_t Solver::countNumBinClauses(const bool alsoLearnt, const bool alsoNonLearnt) const
  {
      uint32_t num = 0;
  
      uint32_t wsLit = 0;
      for (const vec<Watched> *it = watches.getData(), *end = watches.getDataEnd(); it != end; it++, wsLit++) {
          const vec<Watched>& ws = *it;
          for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
              if (it2->isBinary()) {
                  if (it2->getLearnt()) num += alsoLearnt;
                  else num+= alsoNonLearnt;
              }
          }
      }
  
      assert(num % 2 == 0);
      return num/2;
  }
  
  void Solver::dumpBinClauses(const bool alsoLearnt, const bool alsoNonLearnt, FILE* outfile) const
  {
      uint32_t wsLit = 0;
      for (const vec<Watched> *it = watches.getData(), *end = watches.getDataEnd(); it != end; it++, wsLit++) {
          Lit lit = ~Lit::toLit(wsLit);
          const vec<Watched>& ws = *it;
          for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
              if (it2->isBinary() && lit.toInt() < it2->getOtherLit().toInt()) {
                  bool toDump = false;
                  if (it2->getLearnt() && alsoLearnt) toDump = true;
                  if (!it2->getLearnt() && alsoNonLearnt) toDump = true;
  
                  if (toDump) it2->dump(outfile, lit);
              }
          }
      }
  }
  
  uint32_t Solver::getBinWatchSize(const bool alsoLearnt, const Lit lit)
  {
      uint32_t num = 0;
      const vec<Watched>& ws = watches[lit.toInt()];
      for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
          if (it2->isBinary() && (alsoLearnt || !it2->getLearnt())) {
              num++;
          }
      }
  
      return num;
  }
  
  void Solver::printBinClause(const Lit litP1, const Lit litP2, FILE* outfile) const
  {
      if (value(litP1) == l_True) {
          litP1.printFull(outfile);
      } else if (value(litP1) == l_False) {
          litP2.printFull(outfile);
      } else if (value(litP2) == l_True) {
          litP2.printFull(outfile);
      } else if (value(litP2) == l_False) {
          litP1.printFull(outfile);
      } else {
          litP1.print(outfile);
          litP2.printFull(outfile);
      }
  }
  
  bool Solver::dumpOrigClauses(const std::string& fileName) const
  {
      FILE* outfile;
      if (fileName != std::string("stdout")) {
          outfile = fopen(fileName.c_str(), "w");
          if (!outfile)
              return false;
      } else  {
          outfile = stdout;
      }
  
      uint32_t numClauses = 0;
      //unitary clauses
      for (uint32_t i = 0, end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size() ; i < end; i++)
          numClauses++;
  
      //binary XOR clauses
      const vector<Lit>& table = varReplacer->getReplaceTable();
      for (Var var = 0; var != table.size(); var++) {
          Lit lit = table[var];
          if (lit.var() == var)
              continue;
          numClauses += 2;
      }
  
      //binary normal clauses
      numClauses += countNumBinClauses(false, true);
  
      //normal clauses
      numClauses += clauses.size();
  
      //xor clauses
      numClauses += xorclauses.size();
  
      //previously eliminated clauses
      const map<Var, vector<vector<Lit> > >& elimedOutVar = subsumer->getElimedOutVar();
      for (map<Var, vector<vector<Lit> > >::const_iterator it = elimedOutVar.begin(); it != elimedOutVar.end(); it++) {
          const vector<vector<Lit> >& cs = it->second;
          numClauses += cs.size();
      }
      const map<Var, vector<std::pair<Lit, Lit> > >& elimedOutVarBin = subsumer->getElimedOutVarBin();
      for (map<Var, vector<std::pair<Lit, Lit> > >::const_iterator it = elimedOutVarBin.begin(); it != elimedOutVarBin.end(); it++) {
          numClauses += it->second.size();
      }
  
      const map<Var, vector<XorSubsumer::XorElimedClause> >& xorElimedOutVar = xorSubsumer->getElimedOutVar();
      for (map<Var, vector<XorSubsumer::XorElimedClause> >::const_iterator it = xorElimedOutVar.begin(); it != xorElimedOutVar.end(); it++) {
          const vector<XorSubsumer::XorElimedClause>& cs = it->second;
          numClauses += cs.size();
      }
  
      fprintf(outfile, "p cnf %d %d\n", nVars(), numClauses);
  
      ////////////////////////////////////////////////////////////////////
  
      fprintf(outfile, "c \nc ---------\n");
      fprintf(outfile, "c unitaries\n");
      fprintf(outfile, "c ---------\n");
      for (uint32_t i = 0, end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size() ; i < end; i++) {
          trail[i].printFull(outfile);
      }
  
      fprintf(outfile, "c \nc ---------------------------------------\n");
      fprintf(outfile, "c clauses representing 2-long XOR clauses\n");
      fprintf(outfile, "c ---------------------------------------\n");
      for (Var var = 0; var != table.size(); var++) {
          Lit lit = table[var];
          if (lit.var() == var)
              continue;
  
          Lit litP1 = ~lit;
          Lit litP2 = Lit(var, false);
          printBinClause(litP1, litP2, outfile);
          printBinClause(~litP1, ~litP2, outfile);
      }
  
      fprintf(outfile, "c \nc ------------\n");
      fprintf(outfile, "c binary clauses\n");
      fprintf(outfile, "c ---------------\n");
      dumpBinClauses(false, true, outfile);
  
      fprintf(outfile, "c \nc ------------\n");
      fprintf(outfile, "c normal clauses\n");
      fprintf(outfile, "c ---------------\n");
      for (Clause *const *i = clauses.getData(); i != clauses.getDataEnd(); i++) {
          assert(!(*i)->learnt());
          (*i)->print(outfile);
      }
  
      fprintf(outfile, "c \nc ------------\n");
      fprintf(outfile, "c xor clauses\n");
      fprintf(outfile, "c ---------------\n");
      for (XorClause *const *i = xorclauses.getData(); i != xorclauses.getDataEnd(); i++) {
          assert(!(*i)->learnt());
          (*i)->print(outfile);
      }
  
      fprintf(outfile, "c -------------------------------\n");
      fprintf(outfile, "c previously eliminated variables\n");
      fprintf(outfile, "c -------------------------------\n");
      for (map<Var, vector<vector<Lit> > >::const_iterator it = elimedOutVar.begin(); it != elimedOutVar.end(); it++) {
          fprintf(outfile, "c ########### cls for eliminated var %d ### start\n", it->first + 1);
          const vector<vector<Lit> >& cs = it->second;
          for (vector<vector<Lit> >::const_iterator it2 = cs.begin(); it2 != cs.end(); it2++) {
              printClause(outfile, *it2);
          }
          fprintf(outfile, "c ########### cls for eliminated var %d ### finish\n", it->first + 1);
      }
      for (map<Var, vector<std::pair<Lit, Lit> > >::const_iterator it = elimedOutVarBin.begin(); it != elimedOutVarBin.end(); it++) {
          for (uint32_t i = 0; i < it->second.size(); i++) {
              it->second[i].first.print(outfile);
              it->second[i].second.printFull(outfile);
          }
      }
  
      fprintf(outfile, "c -------------------------------\n");
      fprintf(outfile, "c previously xor-eliminated variables\n");
      fprintf(outfile, "c -------------------------------\n");
      for (map<Var, vector<XorSubsumer::XorElimedClause> >::const_iterator it = xorElimedOutVar.begin(); it != xorElimedOutVar.end(); it++) {
          for (vector<XorSubsumer::XorElimedClause>::const_iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
              it2->plainPrint(outfile);
          }
      }
  
      if (fileName != "stdout") fclose(outfile);
      return true;
  }
  
  vector<RetClause> Solver::dumpOrigClauses() const
  {
  
      vector<RetClause> ret;
      vector<Lit> tmpCl;
  
      //Unitaries
      for (uint32_t i = 0
          , end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size()
          ; i < end
          ; i++
      ) {
          tmpCl.clear();
          tmpCl.push_back(trail[i]);
          ret.push_back(RetClause(tmpCl));
      }
  
  
      //2-long XORs
      const vector<Lit>& table = varReplacer->getReplaceTable();
      for (Var var = 0; var != table.size(); var++) {
          Lit lit = table[var];
          if (lit.var() == var)
              continue;
  
          Lit litP1 = ~lit;
          Lit litP2 = Lit(var, false);
          // a v b
          //-a v -b
          //-> a + b = 1
          //-> litP1 + litP2 == 1
          bool rhs = true;
          rhs ^= litP1.sign();
          rhs ^= litP2.sign();
  
          tmpCl.clear();
          tmpCl.push_back(litP1.unsign());
          tmpCl.push_back(litP2.unsign());
          ret.push_back(RetClause(true, rhs, tmpCl));
      }
  
      //Bins -- implicit, so more complicated
      uint32_t wsLit = 0;
      for (const vec<Watched>
          *it = watches.getData(), *end = watches.getDataEnd()
          ; it != end
          ; it++, wsLit++
      ) {
          Lit lit = ~Lit::toLit(wsLit);
          const vec<Watched>& ws = *it;
          for (vec<Watched>::const_iterator
              it2 = ws.getData(), end2 = ws.getDataEnd()
              ; it2 != end2
              ; it2++
          ) {
              //Only dump once
              if (it2->isBinary() && lit.toInt() < it2->getOtherLit().toInt()) {
                  if (it2->getLearnt())
                      continue;
  
                  tmpCl.clear();
                  tmpCl.push_back(lit);
                  tmpCl.push_back(it2->getOtherLit());
                  ret.push_back(RetClause(tmpCl));
              }
          }
      }
  
      //Longs
      for (Clause *const *i = clauses.getData(); i != clauses.getDataEnd(); i++) {
          const Clause& cl = **i;
          if (cl.learnt())
              continue;
  
          tmpCl.clear();
          for(size_t i2 = 0; i2 < cl.size(); i2++) {
              tmpCl.push_back(cl[i2]);
          }
          ret.push_back(RetClause(tmpCl));
      }
  
      //xor clauses
      for (XorClause *const *i = xorclauses.getData(); i != xorclauses.getDataEnd(); i++) {
          const XorClause& cl = **i;
          tmpCl.clear();
          for(size_t i2 = 0; i2 < cl.size(); i2++) {
              tmpCl.push_back(cl[i2].unsign());
          }
          ret.push_back(RetClause(true, true ^ cl.xorEqualFalse(), tmpCl));
      }
  
      //elimed
      const map<Var, vector<vector<Lit> > >& elimedOutVar = subsumer->getElimedOutVar();
      for (map<Var, vector<vector<Lit> > >::const_iterator
          it = elimedOutVar.begin()
          ; it != elimedOutVar.end()
          ; it++
      ) {
          const vector<vector<Lit> >& cs = it->second;
          for (vector<vector<Lit> >::const_iterator
              it2 = cs.begin()
              ; it2 != cs.end()
              ; it2++
          ) {
              ret.push_back(RetClause(*it2));
          }
      }
      const map<Var, vector<std::pair<Lit, Lit> > >& elimedOutVarBin = subsumer->getElimedOutVarBin();
      for (map<Var, vector<std::pair<Lit, Lit> > >::const_iterator
          it = elimedOutVarBin.begin()
          ; it != elimedOutVarBin.end()
          ; it++
      ) {
          for (uint32_t i = 0; i < it->second.size(); i++) {
              tmpCl.clear();
              tmpCl.push_back(it->second[i].first);
              tmpCl.push_back(it->second[i].second);
              ret.push_back(RetClause(tmpCl));
          }
      }
  
      //previously xor-eliminated variables\n");
      const map<Var, vector<XorSubsumer::XorElimedClause> >& xorElimedOutVar = xorSubsumer->getElimedOutVar();
      for (map<Var, vector<XorSubsumer::XorElimedClause> >::const_iterator
          it = xorElimedOutVar.begin()
          ; it != xorElimedOutVar.end()
          ; it++
      ) {
          for (vector<XorSubsumer::XorElimedClause>::const_iterator
              it2 = it->second.begin(), end2 = it->second.end()
              ; it2 != end2
              ; it2++
          ) {
              ret.push_back(RetClause(true, true ^ it2->xorEqualFalse, it2->lits));
          }
      }
  
      return ret;
  }
  
  
  vec<Lit> Solver::get_unitary_learnts() const
  {
      vec<Lit> unitaries;
      if (decisionLevel() > 0) {
          for (uint32_t i = 0; i != trail_lim[0]; i++) {
              unitaries.push(trail[i]);
          }
      }
  
      return unitaries;
  }
  
  const vec<Clause*>& Solver::get_learnts() const
  {
      return learnts;
  }
  
  const vec<Clause*>& Solver::get_sorted_learnts()
  {
      if (lastSelectedRestartType == dynamic_restart)
          std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
      else
          std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
      return learnts;
  }
  
  uint32_t Solver::getNumElimSubsume() const
  {
      return subsumer->getNumElimed();
  }
  
  uint32_t Solver::getNumElimXorSubsume() const
  {
      return xorSubsumer->getNumElimed();
  }
  
  uint32_t Solver::getNumXorTrees() const
  {
      return varReplacer->getNumTrees();
  }
  
  uint32_t Solver::getNumXorTreesCrownSize() const
  {
      return varReplacer->getNumReplacedVars();
  }
  
  double Solver::getTotalTimeSubsumer() const
  {
      return subsumer->getTotalTime();
  }
  
  double Solver::getTotalTimeFailedLitSearcher() const
  {
      return failedLitSearcher->getTotalTime();
  }
  
  double Solver::getTotalTimeXorSubsumer() const
  {
      return xorSubsumer->getTotalTime();
  }
  
  double Solver::getTotalTimeSCC() const
  {
      return  sCCFinder->getTotalTime();
  }
  
  void Solver::printStatHeader() const
  {
      if (conf.verbosity >= 2) {
          std::cout << "c "
          << "========================================================================================="
          << std::endl;
          std::cout << "c"
          << " types(t): F = full restart, N = normal restart" << std::endl;
          std::cout << "c"
          << " types(t): S = simplification begin/end, E = solution found" << std::endl;
          std::cout << "c"
          << " restart types(rt): st = static, dy = dynamic" << std::endl;
  
          std::cout << "c "
          << std::setw(2) << "t"
          << std::setw(3) << "rt"
          << std::setw(6) << "Rest"
          << std::setw(space) << "Confl"
          << std::setw(space) << "Vars"
          << std::setw(space) << "NormCls"
          << std::setw(space) << "XorCls"
          << std::setw(space) << "BinCls"
          << std::setw(space) << "Learnts"
          << std::setw(space) << "ClLits"
          << std::setw(space) << "LtLits"
          << std::setw(space) << "LGlueHist"
          << std::setw(space) << "SGlueHist"
          << std::endl;
      }
  }
  
  void Solver::printRestartStat(const char* type)
  {
      if (conf.verbosity >= 2) {
          //printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)(nClauses()-nbBin), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart+nbCompensateSubsumer), (int)(nLearnts()+nbBin), (double)learnts_literals/(double)(nLearnts()+nbBin));
  
          std::cout << "c "
          << std::setw(2) << type
          << std::setw(3) << ((restartType == static_restart) ? "st" : "dy")
          << std::setw(6) << starts
          << std::setw(space) << conflicts
          << std::setw(space) << order_heap.size()
          << std::setw(space) << clauses.size()
          << std::setw(space) << xorclauses.size()
          << std::setw(space) << numBins
          << std::setw(space) << learnts.size()
          << std::setw(space) << clauses_literals
          << std::setw(space) << learnts_literals;
  
          if (glueHistory.getTotalNumeElems() > 0) {
              std::cout << std::setw(space) << std::fixed << std::setprecision(2) << glueHistory.getAvgAllDouble();
          } else {
              std::cout << std::setw(space) << "no data";
          }
          if (glueHistory.isvalid()) {
              std::cout << std::setw(space) << std::fixed << std::setprecision(2) << glueHistory.getAvgDouble();
          } else {
              std::cout << std::setw(space) << "no data";
          }
  
          #ifdef RANDOM_LOOKAROUND_SEARCHSPACE
          if (conf.doPrintAvgBranch) {
              if (avgBranchDepth.isvalid())
                  std::cout << std::setw(space) << avgBranchDepth.getAvgUInt();
              else
                  std::cout << std::setw(space) << "no data";
          }
          #endif //RANDOM_LOOKAROUND_SEARCHSPACE
  
          #ifdef USE_GAUSS
          print_gauss_sum_stats();
          #endif //USE_GAUSS
  
          std::cout << std::endl;
      }
  }
  
  void Solver::printEndSearchStat()
  {
      if (conf.verbosity >= 1) {
          printRestartStat("E");
      }
  }
  
  #ifdef USE_GAUSS
  void Solver::print_gauss_sum_stats()
  {
      if (gauss_matrixes.size() == 0 && conf.verbosity >= 2) {
          std::cout << "  --";
          return;
      }
  
      uint32_t called = 0;
      uint32_t useful_prop = 0;
      uint32_t useful_confl = 0;
      uint32_t disabled = 0;
      for (vector<Gaussian*>::const_iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) {
          disabled += (*gauss)->get_disabled();
          called += (*gauss)->get_called();
          useful_prop += (*gauss)->get_useful_prop();
          useful_confl += (*gauss)->get_useful_confl();
          sum_gauss_unit_truths += (*gauss)->get_unit_truths();
          //gauss->print_stats();
          //gauss->print_matrix_stats();
      }
      sum_gauss_called += called;
      sum_gauss_confl += useful_confl;
      sum_gauss_prop += useful_prop;
  
      if (conf.verbosity >= 2) {
          if (called == 0) {
              std::cout << " --";
          } else {
              std::cout << " "
              << std::fixed << std::setprecision(1) << std::setw(5)
              << ((double)useful_prop/(double)called*100.0) << "% "
              << std::fixed << std::setprecision(1) << std::setw(5)
              << ((double)useful_confl/(double)called*100.0) << "% "
              << std::fixed << std::setprecision(1) << std::setw(5)
              << (100.0-(double)disabled/(double)gauss_matrixes.size()*100.0) << "%";
          }
      }
  }
  #endif //USE_GAUSS
  
  /**
  @brief Sorts the watchlists' clauses as: binary, tertiary, normal, xor
  */
  void Solver::sortWatched()
  {
      #ifdef VERBOSE_DEBUG
      std::cout << "Sorting watchlists:" << std::endl;
      #endif
      double myTime = cpuTime();
      for (vec<Watched> *i = watches.getData(), *end = watches.getDataEnd(); i != end; i++) {
          if (i->size() == 0) continue;
          #ifdef VERBOSE_DEBUG
          vec<Watched>& ws = *i;
          std::cout << "Before sorting:" << std::endl;
          for (uint32_t i2 = 0; i2 < ws.size(); i2++) {
              if (ws[i2].isBinary()) std::cout << "Binary,";
              if (ws[i2].isTriClause()) std::cout << "Tri,";
              if (ws[i2].isClause()) std::cout << "Normal,";
              if (ws[i2].isXorClause()) std::cout << "Xor,";
          }
          std::cout << std::endl;
          #endif //VERBOSE_DEBUG
  
          std::sort(i->getData(), i->getDataEnd(), WatchedSorter());
  
          #ifdef VERBOSE_DEBUG
          std::cout << "After sorting:" << std::endl;
          for (uint32_t i2 = 0; i2 < ws.size(); i2++) {
              if (ws[i2].isBinary()) std::cout << "Binary,";
              if (ws[i2].isTriClause()) std::cout << "Tri,";
              if (ws[i2].isClause()) std::cout << "Normal,";
              if (ws[i2].isXorClause()) std::cout << "Xor,";
          }
          std::cout << std::endl;
          #endif //VERBOSE_DEBUG
      }
  
      if (conf.verbosity >= 3) {
          std::cout << "c watched "
          << "sorting time: " << cpuTime() - myTime
          << std::endl;
      }
  }
  
  void Solver::addSymmBreakClauses()
  {
      if (xorclauses.size() > 0) {
          std::cout << "c xor clauses present -> no saucy" << std::endl;
          return;
      }
      double myTime = cpuTime();
      std::cout << "c Doing saucy" << std::endl;
      dumpOrigClauses("origProblem.cnf");
  
      int rvalue;
      rvalue= system("grep -v \"^c\" origProblem.cnf > origProblem2.cnf");
      if (rvalue >= 2) { // unsuccessful grep in POSIX standard
          std::cout << "c impossible to complete saucy" << std::endl;
          return;
      }
      rvalue= system("python saucyReader.py origProblem2.cnf > output");
      if (rvalue != 0) { // unsuccessful saucyReader.py
          std::cout << "c impossible to complete saucy" << std::endl;
          return;
      }
  
  
      DimacsParser parser(this, false, false, false, true);
  
      #ifdef DISABLE_ZLIB
      FILE * in = fopen("output", "rb");
      #else
      gzFile in = gzopen("output", "rb");
      #endif // DISABLE_ZLIB
      parser.parse_DIMACS(in);
      #ifdef DISABLE_ZLIB
      fclose(in);
      #else
      gzclose(in);
      #endif // DISABLE_ZLIB
      std::cout << "c Finished saucy, time: " << (cpuTime() - myTime) << std::endl;
  }
  
  /**
  @brief Pretty-prints a literal
  */
  void Solver::printLit(const Lit l) const
  {
      printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
  }
  
  /**
  @brief Sets that we need a CNF file that documents all commands
  
  newVar() and addClause(), addXorClause() commands are logged to this CNF
  file and then can be re-read with special arguments to the main program. This
  can help simulate a segfaulting library-call
  */
  bool Solver::needLibraryCNFFile(const std::string& fileName)
  {
      libraryCNFFile = fopen(fileName.c_str(), "w");
      return libraryCNFFile != NULL;
  }
  
  template<class T, class T2>
  void Solver::printStatsLine(std::string left, T value, T2 value2, std::string extra)
  {
      std::cout << std::fixed << std::left << std::setw(27) << left << ": " << std::setw(11) << std::setprecision(2) << value << " (" << std::left << std::setw(9) << std::setprecision(2) << value2 << " " << extra << ")" << std::endl;
  }
  
  template<class T>
  void Solver::printStatsLine(std::string left, T value, std::string extra)
  {
      std::cout << std::fixed << std::left << std::setw(27) << left << ": " << std::setw(11) << std::setprecision(2) << value << extra << std::endl;
  }
  
  /**
  @brief prints the statistics line at the end of solving
  
  Prints all sorts of statistics, like number of restarts, time spent in
  SatELite-type simplification, number of unit claues found, etc.
  */
  void Solver::printStats()
  {
      double   cpu_time = cpuTime();
      uint64_t mem_used = memUsed();
  
      int numThreads;
  #ifdef _OPENMP
      numThreads = omp_get_num_threads();
  #else
      numThreads = 1;
  #endif
  
      if (numThreads > 1) {
          std::cout << "c Following stats are for *FIRST FINISHED THREAD ONLY*" << std::endl;
          #if !defined(_MSC_VER) && !defined(RUSAGE_THREAD)
          std::cout << "c There is no platform-independent way to measure time per thread" << std::endl;
          std::cout << "c All times indicated are sum of ALL threads" << std::endl;
          std::cout << "c Use a utilty provided by your platform to get total thread time, etc." << std::endl;
          #endif
      }
      printStatsLine("c num threads" , numThreads);
  
      //Restarts stats
      printStatsLine("c restarts", starts);
      printStatsLine("c dynamic restarts", dynStarts);
      printStatsLine("c static restarts", staticStarts);
      printStatsLine("c full restarts", fullStarts);
      printStatsLine("c total simplify time", totalSimplifyTime);
  
      //Learnts stats
      printStatsLine("c learnts DL2", nbGlue2);
      printStatsLine("c learnts size 2", numNewBin);
      printStatsLine("c learnts size 1", get_unitary_learnts_num(), (double)get_unitary_learnts_num()/(double)nVars()*100.0, "% of vars");
      printStatsLine("c filedLit time", getTotalTimeFailedLitSearcher(), getTotalTimeFailedLitSearcher()/cpu_time*100.0, "% time");
  
      //Subsumer stats
      printStatsLine("c v-elim SatELite", getNumElimSubsume(), (double)getNumElimSubsume()/(double)nVars()*100.0, "% vars");
      printStatsLine("c SatELite time", getTotalTimeSubsumer(), getTotalTimeSubsumer()/cpu_time*100.0, "% time");
  
      //XorSubsumer stats
      printStatsLine("c v-elim xor", getNumElimXorSubsume(), (double)getNumElimXorSubsume()/(double)nVars()*100.0, "% vars");
      printStatsLine("c xor elim time", getTotalTimeXorSubsumer(), getTotalTimeXorSubsumer()/cpu_time*100.0, "% time");
  
      //VarReplacer stats
      printStatsLine("c num binary xor trees", getNumXorTrees());
      printStatsLine("c binxor trees' crown", getNumXorTreesCrownSize(), (double)getNumXorTreesCrownSize()/(double)getNumXorTrees(), "leafs/tree");
      printStatsLine("c bin xor find time", getTotalTimeSCC());
  
      //OTF clause improvement stats
      printStatsLine("c OTF clause improved", improvedClauseNo, (double)improvedClauseNo/(double)conflicts, "clauses/conflict");
      printStatsLine("c OTF impr. size diff", improvedClauseSize, (double)improvedClauseSize/(double)improvedClauseNo, " lits/clause");
  
      //Clause-shrinking through watchlists
      printStatsLine("c OTF cl watch-shrink", numShrinkedClause, (double)numShrinkedClause/(double)conflicts, "clauses/conflict");
      printStatsLine("c OTF cl watch-sh-lit", numShrinkedClauseLits, (double)numShrinkedClauseLits/(double)numShrinkedClause, " lits/clause");
      printStatsLine("c tried to recurMin cls", moreRecurMinLDo, (double)moreRecurMinLDo/(double)conflicts*100.0, " % of conflicts");
      printStatsLine("c updated cache", updateTransCache, updateTransCache/(double)moreRecurMinLDo, " lits/tried recurMin");
  
      //Multi-threading
      if (numThreads > 1 && dataSync) {
          printStatsLine("c unit cls received", dataSync->getRecvUnitData(), (double)dataSync->getRecvUnitData()/(double)get_unitary_learnts_num()*100.0, "% of units");
          printStatsLine("c unit cls sent", dataSync->getSentUnitData(), (double)dataSync->getSentUnitData()/(double)get_unitary_learnts_num()*100.0, "% of units");
          printStatsLine("c bin cls received", dataSync->getRecvBinData());
          printStatsLine("c bin cls sent", dataSync->getSentBinData());
      }
  
      #ifdef USE_GAUSS
      if (gaussconfig.decision_until > 0) {
          std::cout << "c " << std::endl;
          printStatsLine("c gauss unit truths ", get_sum_gauss_unit_truths());
          printStatsLine("c gauss called", get_sum_gauss_called());
          printStatsLine("c gauss conflicts ", get_sum_gauss_confl(), (double)get_sum_gauss_confl() / (double)get_sum_gauss_called() * 100.0, " %");
          printStatsLine("c gauss propagations ", get_sum_gauss_prop(), (double)get_sum_gauss_prop() / (double)get_sum_gauss_called() * 100.0, " %");
          printStatsLine("c gauss useful", ((double)get_sum_gauss_prop() + (double)get_sum_gauss_confl())/ (double)get_sum_gauss_called() * 100.0, " %");
          std::cout << "c " << std::endl;
      }
      #endif
  
      printStatsLine("c clauses over max glue", nbClOverMaxGlue, (double)nbClOverMaxGlue/(double)conflicts*100.0, "% of all clauses");
  
      //Search stats
      printStatsLine("c conflicts", conflicts, (double)conflicts/cpu_time, "/ sec");
      printStatsLine("c decisions", decisions, (double)rnd_decisions*100.0/(double)decisions, "% random");
      printStatsLine("c bogo-props", propagations, (double)propagations/cpu_time, "/ sec");
      printStatsLine("c conflict literals", tot_literals, (double)(max_literals - tot_literals)*100.0/ (double)max_literals, "% deleted");
  
      //General stats
      printStatsLine("c Memory used", (double)mem_used / 1048576.0, " MB");
      if (numThreads > 1) {
          #if !defined(_MSC_VER) && defined(RUSAGE_THREAD)
          printStatsLine("c single-thread CPU time", cpu_time, " s");
          printStatsLine("c all-threads sum CPU time", cpuTimeTotal(), " s");
          #else
          printStatsLine("c all-threads sum CPU time", cpu_time, " s");
          #endif
      } else {
          printStatsLine("c CPU time", cpu_time, " s");
      }
  }
  