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/ClauseVivifier.h"
  #include "cmsat/ClauseCleaner.h"
  #include "cmsat/time_mem.h"
  #include <iomanip>
  
  //#define ASSYM_DEBUG
  
  using namespace CMSat;
  
  ClauseVivifier::ClauseVivifier(Solver& _solver) :
      lastTimeWentUntil(0)
      , numCalls(0)
      , solver(_solver)
  {}
  
  
  /**
  @brief Performs clause vivification (by Hamadi et al.)
  
  This is the only thing that does not fit under the aegis of tryBoth(), since
  it is not part of failed literal probing, really. However, it is here because
  it seems to be a function that fits into the idology of failed literal probing.
  Maybe I am off-course and it should be in another class, or a class of its own.
  */
  bool ClauseVivifier::vivifyClauses()
  {
      assert(solver.ok);
      #ifdef VERBOSE_DEBUG
      std::cout << "c clauseVivifier started" << std::endl;
      //solver.printAllClauses();
      #endif //VERBOSE_DEBUG
  
  
      solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
      numCalls++;
  
      if (solver.ok) {
          if (!vivifyClauses2(solver.clauses)) return false;
          if (!vivifyClauses2(solver.learnts)) return false;
      }
  
      bool failed;
      uint32_t effective = 0;
      uint32_t effectiveLit = 0;
      double myTime = cpuTime();
      uint64_t maxNumProps = 20*1000*1000;
      if (solver.clauses_literals + solver.learnts_literals < 500000)
          maxNumProps *=2;
      uint64_t extraDiff = 0;
      uint64_t oldProps = solver.propagations;
      bool needToFinish = false;
      uint32_t checkedClauses = 0;
      uint32_t potentialClauses = solver.clauses.size();
      if (lastTimeWentUntil + 500 > solver.clauses.size())
          lastTimeWentUntil = 0;
      uint32_t thisTimeWentUntil = 0;
      vec<Lit> lits;
      vec<Lit> unused;
  
      if (solver.clauses.size() < 1000000) {
          //if too many clauses, random order will do perfectly well
          std::sort(solver.clauses.getData(), solver.clauses.getDataEnd(), sortBySize());
      }
  
      uint32_t queueByBy = 2;
      if (numCalls > 8
          && (solver.clauses_literals + solver.learnts_literals < 4000000)
          && (solver.clauses.size() < 50000))
          queueByBy = 1;
  
      Clause **i, **j;
      i = j = solver.clauses.getData();
      for (Clause **end = solver.clauses.getDataEnd(); i != end; i++) {
          if (needToFinish || lastTimeWentUntil > 0) {
              if (!needToFinish) {
                  lastTimeWentUntil--;
                  thisTimeWentUntil++;
              }
              *j++ = *i;
              continue;
          }
  
          //if done enough, stop doing it
          if (solver.propagations-oldProps + extraDiff > maxNumProps) {
              //std::cout << "Need to finish -- ran out of prop" << std::endl;
              needToFinish = true;
          }
  
          //if bad performance, stop doing it
          /*if ((i-solver.clauses.getData() > 5000 && effectiveLit < 300)) {
              std::cout << "Need to finish -- not effective" << std::endl;
              needToFinish = true;
          }*/
  
          Clause& c = **i;
          extraDiff += c.size();
          checkedClauses++;
          thisTimeWentUntil++;
  
          assert(c.size() > 2);
          assert(!c.learnt());
  
          unused.clear();
          lits.clear();
          lits.growTo(c.size());
          memcpy(lits.getData(), c.getData(), c.size() * sizeof(Lit));
  
          failed = false;
          uint32_t done = 0;
          solver.newDecisionLevel();
          for (; done < lits.size();) {
              uint32_t i2 = 0;
              for (; (i2 < queueByBy) && ((done+i2) < lits.size()); i2++) {
                  lbool val = solver.value(lits[done+i2]);
                  if (val == l_Undef) {
                      solver.uncheckedEnqueueLight(~lits[done+i2]);
                  } else if (val == l_False) {
                      unused.push(lits[done+i2]);
                  }
              }
              done += i2;
              failed = (!solver.propagate<false>(false).isNULL());
              if (numCalls > 3 && failed) break;
          }
          solver.cancelUntilLight();
          assert(solver.ok);
  
          if (unused.size() > 0 || (failed && done < lits.size())) {
              effective++;
              uint32_t origSize = lits.size();
              #ifdef ASSYM_DEBUG
              std::cout << "Assym branch effective." << std::endl;
              std::cout << "-- Orig clause:"; c.plainPrint();
              #endif
              solver.detachClause(c);
  
              lits.shrink(lits.size() - done);
              for (uint32_t i2 = 0; i2 < unused.size(); i2++) {
                  remove(lits, unused[i2]);
              }
  
              Clause *c2 = solver.addClauseInt(lits);
              #ifdef ASSYM_DEBUG
              std::cout << "-- Origsize:" << origSize << " newSize:" << (c2 == NULL ? 0 : c2->size()) << " toRemove:" << c.size() - done << " unused.size():" << unused.size() << std::endl;
              #endif
              extraDiff += 20;
              //TODO cheating here: we don't detect a NULL return that is in fact a 2-long clause
              effectiveLit += origSize - (c2 == NULL ? 0 : c2->size());
              solver.clauseAllocator.clauseFree(&c);
  
              if (c2 != NULL) {
                  #ifdef ASSYM_DEBUG
                  std::cout << "-- New clause:"; c2->plainPrint();
                  #endif
                  *j++ = c2;
              }
  
              if (!solver.ok) needToFinish = true;
          } else {
              *j++ = *i;
          }
      }
      solver.clauses.shrink(i-j);
  
      lastTimeWentUntil = thisTimeWentUntil;
  
      if (solver.conf.verbosity  >= 1) {
          std::cout << "c asymm "
          << " cl-useful: " << effective << "/" << checkedClauses << "/" << potentialClauses
          << " lits-rem:" << effectiveLit
          << " time: " << cpuTime() - myTime
          << std::endl;
      }
  
      return solver.ok;
  }
  
  
  bool ClauseVivifier::vivifyClauses2(vec<Clause*>& clauses)
  {
      assert(solver.ok);
  
      vec<char> seen;
      seen.growTo(solver.nVars()*2, 0);
      vec<char> seen_subs;
      seen_subs.growTo(solver.nVars()*2, 0);
  
      uint32_t litsRem = 0;
      uint32_t clShrinked = 0;
      uint64_t countTime = 0;
      uint64_t maxCountTime = 800*1000*1000;
      maxCountTime *= 6;
      if (solver.clauses_literals + solver.learnts_literals < 500000)
          maxCountTime *= 2;
      uint32_t clTried = 0;
      vec<Lit> lits;
      bool needToFinish = false;
      double myTime = cpuTime();
      uint32_t subsumed_tri_num = 0;
      uint32_t subsumed_bin_num = 0;
  
      Clause** i = clauses.getData();
      Clause** j = i;
      for (Clause** end = clauses.getDataEnd(); i != end; i++) {
          if (needToFinish) {
              *j++ = *i;
              continue;
          }
          if (countTime > maxCountTime)
              needToFinish = true;
  
          Clause& cl = **i;
          countTime += cl.size()*2;
          clTried++;
  
          bool subsumed = false;
          const bool learnt = cl.learnt();
          for (uint32_t i2 = 0; i2 < cl.size(); i2++) {
              seen[cl[i2].toInt()] = 1; //for strengthening
              seen_subs[cl[i2].toInt()] = 1; //for subsumption
          }
  
          for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) {
              const Lit *l_other = l;
              l_other++;
              if (l_other != end)
                  __builtin_prefetch(solver.watches[(~*l_other).toInt()].getData());
  
              const vec<Watched>& ws = solver.watches[(~*l).toInt()];
              countTime += ws.size()*2;
              for(vec<Watched>::const_iterator it = ws.getData(), end = ws.getDataEnd(); it != end; it++) {
                  //Handle tri clause
                  if (it->isTriClause() && cl.size() > 3)
                  {
                      if (learnt //we cannot decide if TRI is learnt or not
                          && seen_subs[it->getOtherLit().toInt()]
                          && seen_subs[it->getOtherLit2().toInt()]
                      ) {
                          subsumed_tri_num++;
                          subsumed = true;
                      }
  
                      if (seen[l->toInt()]) { //we may have removed it already
                          //one way
                          if (seen[(it->getOtherLit2()).toInt()])
                              seen[(~it->getOtherLit()).toInt()] = 0;
  
                          //other way
                          if (seen[(it->getOtherLit()).toInt()])
                              seen[(~it->getOtherLit2()).toInt()] = 0;
                      }
                  }
  
                  //Handle Binary clause
                  if (it->isBinary()) {
                      if (seen_subs[it->getOtherLit().toInt()])
                      {
                          if (!learnt && it->getLearnt())
                              makeNonLearntBin(*l, it->getOtherLit(), it->getLearnt());
                          subsumed_bin_num++;
                          subsumed = true;
                      }
  
                      if (seen[l->toInt()]) //we may have removed it already
                          seen[(~it->getOtherLit()).toInt()] = 0;
  
                  }
              }
  
              if (seen[l->toInt()] == 0)
                  continue;
  
              countTime += solver.transOTFCache[l->toInt()].lits.size();
              for (vector<Lit>::const_iterator it2 = solver.transOTFCache[l->toInt()].lits.begin()
                  , end2 = solver.transOTFCache[l->toInt()].lits.end(); it2 != end2; it2++) {
                  seen[(~(*it2)).toInt()] = 0;
              }
          }
  
          lits.clear();
          for (const Lit *it2 = cl.getData(), *end2 = cl.getDataEnd(); it2 != end2; it2++) {
              if (seen[it2->toInt()]) lits.push(*it2);
              else litsRem++;
              seen[it2->toInt()] = 0;
              seen_subs[it2->toInt()] = 0;
          }
  
          if (subsumed) {
              solver.removeClause(cl);
          } else if (lits.size() < cl.size()) {
              solver.detachClause(cl);
              clShrinked++;
              Clause* c2 = solver.addClauseInt(lits, cl.learnt(), cl.getGlue(), cl.getMiniSatAct());
              solver.clauseAllocator.clauseFree(&cl);
  
              if (c2 != NULL) *j++ = c2;
              if (!solver.ok) needToFinish = true;
          } else {
              *j++ = *i;
          }
      }
  
      clauses.shrink(i-j);
  
      if (solver.conf.verbosity >= 1) {
          std::cout << "c vivif2 -- "
          << " cl tried " << std::setw(8) << clTried
          << " cl rem " << std::setw(8) << (subsumed_bin_num + subsumed_tri_num)
          << " cl shrink " << std::setw(8) << clShrinked
          << " lits rem " << std::setw(10) << litsRem
          << " time: " << cpuTime() - myTime
          << std::endl;
      }
  
      return solver.ok;
  }
  
  void ClauseVivifier::makeNonLearntBin(const Lit lit1, const Lit lit2, const bool learnt)
  {
      assert(learnt == true);
      findWatchedOfBin(solver.watches, lit1 ,lit2, learnt).setLearnt(false);
      findWatchedOfBin(solver.watches, lit2 ,lit1, learnt).setLearnt(false);
      solver.learnts_literals -= 2;
      solver.clauses_literals += 2;
  }
  