/*******************************************************************************
   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
   *
   * All rights reserved. This program and the accompanying materials
   * are made available under the terms of the Eclipse Public License v1.0
   * which accompanies this distribution, and is available at
   * http://www.eclipse.org/legal/epl-v10.html
   *
   * Alternatively, the contents of this file may be used under the terms of
  * either the GNU Lesser General Public License Version 2.1 or later (the
  * "LGPL"), in which case the provisions of the LGPL are applicable instead
  * of those above. If you wish to allow use of your version of this file only
  * under the terms of the LGPL, and not to allow others to use your version of
  * this file under the terms of the EPL, indicate your decision by deleting
  * the provisions above and replace them with the notice and other provisions
  * required by the LGPL. If you do not delete the provisions above, a recipient
  * may use your version of this file under the terms of the EPL or the LGPL.
  * 
  * Based on the pseudo boolean algorithms described in:
  * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
  * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
  * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
  * 
  * and 
  * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
  * Framework. Ph.D. Dissertation, University of Oregon.
  *******************************************************************************/
  package org.sat4j.pb.constraints.pb;
  
  import java.math.BigInteger;
  
  import org.sat4j.core.VecInt;
  import org.sat4j.minisat.constraints.cnf.Lits;
  import org.sat4j.minisat.core.ILits;
  import org.sat4j.minisat.core.VarActivityListener;
  import org.sat4j.specs.IteratorInt;
  
  /**
   * @author parrain TODO To change the template for this generated type comment
   *         go to Window - Preferences - Java - Code Style - Code Templates
   */
  public class ConflictMap extends MapPb implements IConflict {
  
      private final ILits voc;
  
      /**
       * to store the slack of the current resolvant
       */
      protected BigInteger currentSlack;
  
      protected int currentLevel;
  
      /**
       * allows to access directly to all variables belonging to a particular
       * level At index 0, unassigned literals are stored (usually level -1); so
       * there is always a step between index and levels.
       */
      protected VecInt[] byLevel;
  
      /**
       * constructs the data structure needed to perform cutting planes
       * 
       * @param cpb
       *                pseudo-boolean constraint which rosed the conflict
       * @param level
       *                current decision level
       * @return a conflict on which cutting plane can be performed.
       */
      public static IConflict createConflict(PBConstr cpb, int level) {
          return new ConflictMap(cpb, level);
      }
  
      ConflictMap(PBConstr cpb, int level) {
          super(cpb);
          this.voc = cpb.getVocabulary();
          this.currentLevel = level;
          initStructures();
      }
  
      private void initStructures() {
          currentSlack = BigInteger.ZERO;
          byLevel = new VecInt[levelToIndex(currentLevel) + 1];
          int ilit, litLevel, index;
          BigInteger tmp;
          for (int i = 0; i < size(); i++) {
              ilit = weightedLits.getLit(i);
              litLevel = voc.getLevel(ilit);
              // eventually add to slack
              tmp = weightedLits.getCoef(i);
              if ((tmp.signum() > 0)
                      && (((!voc.isFalsified(ilit)) || litLevel == currentLevel)))
                  currentSlack = currentSlack.add(tmp);
              // add to byLevel structure
              index = levelToIndex(litLevel);
              if (byLevel[index] == null) {
                  byLevel[index] = new VecInt();
              }
              byLevel[index].push(ilit);
          }
     }
 
     /**
      * convert level into an index in the byLevel structure
      * 
      * @param level
      * @return
      */
     private static final int levelToIndex(int level) {
         return level + 1;
     }
 
     /**
      * convert index in the byLevel structure into a level
      * 
      * @param indLevel
      * @return
      */
     private static final int indexToLevel(int indLevel) {
         return indLevel - 1;
     }
 
     /*
      * coefficient to be computed.
      * 
      */
     protected BigInteger coefMult = BigInteger.ZERO;
 
     protected BigInteger coefMultCons = BigInteger.ZERO;
 
     /**
      * computes a cutting plane with a pseudo-boolean constraint. this method
      * updates the current instance (of ConflictMap).
      * 
      * @param cpb
      *                constraint to compute with the cutting plane
      * @param litImplied
      *                literal that must be resolved by the cutting plane
      * @return an update of the degree of the current instance
      */
     public BigInteger resolve(PBConstr cpb, int litImplied,
             VarActivityListener val) {
         assert litImplied > 1;
         int nLitImplied = litImplied ^ 1;
         if (cpb == null || !weightedLits.containsKey(nLitImplied)) {
             // no resolution
             // undo operation should be anticipated
             int litLevel = levelToIndex(voc.getLevel(litImplied));
             int lit = 0;
             if (byLevel[litLevel] != null) {
                 if (byLevel[litLevel].contains(litImplied)) {
                     lit = litImplied;
                     assert weightedLits.containsKey(litImplied);
                 } else if (byLevel[litLevel].contains(nLitImplied)) {
                     lit = nLitImplied;
                     assert weightedLits.containsKey(nLitImplied);
                 }
             }
 
             if (lit > 0) {
                 byLevel[litLevel].remove(lit);
                 if (byLevel[0] == null)
                     byLevel[0] = new VecInt();
                 byLevel[0].push(lit);
             }
             return degree;
         }
 
         assert slackConflict().signum() <= 0;
         assert degree.signum() >= 0;
 
         // coefficients of the constraint must be copied in an other structure
         // in order to make reduction operations.
         BigInteger[] coefsCons = null;
         BigInteger degreeCons = cpb.getDegree();
 
         // search of the index of the implied literal
         int ind = 0;
         while (cpb.get(ind) != litImplied)
             ind++;
 
         assert cpb.get(ind) == litImplied;
         assert cpb.getCoef(ind) != BigInteger.ZERO;
 
         if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
             // then we know that the resolvant will still be a conflict (cf.
             // Dixon's property)
             coefMultCons = weightedLits.get(nLitImplied);
             coefMult = BigInteger.ONE;
             // updating of the degree of the conflict
             degreeCons = degreeCons.multiply(coefMultCons);
         } else {
             if (weightedLits.get(nLitImplied).equals(BigInteger.ONE)) {
                 // then we know that the resolvant will still be a conflict (cf.
                 // Dixon's property)
                 coefMult = cpb.getCoef(ind);
                 coefMultCons = BigInteger.ONE;
                 // updating of the degree of the conflict
                 degree = degree.multiply(coefMult);
             } else {
                 // pb-constraint has to be reduced
                 // to obtain a conflictual result from the cutting plane
                 WatchPb wpb = (WatchPb) cpb; // DLB Findbugs warning ok
                 coefsCons = wpb.getCoefs();
                 assert positiveCoefs(coefsCons);
                 degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
                         wpb);
                 // updating of the degree of the conflict
                 degreeCons = degreeCons.multiply(coefMultCons);
                 degree = degree.multiply(coefMult);
             }
 
             // coefficients of the conflict must be multiplied by coefMult
             if (!coefMult.equals(BigInteger.ONE))
                 for (int i = 0; i < size(); i++) {
                     changeCoef(i, weightedLits.getCoef(i).multiply(coefMult));
                 }
         }
 
         assert slackConflict().signum() <= 0;
 
         // cutting plane
         degree = cuttingPlane(cpb, degreeCons, coefsCons, coefMultCons, val);
 
         // neither litImplied nor nLitImplied is present in coefs structure
         assert !weightedLits.containsKey(litImplied);
         assert !weightedLits.containsKey(nLitImplied);
         // neither litImplied nor nLitImplied is present in byLevel structure
         assert getLevelByLevel(litImplied) == -1;
         assert getLevelByLevel(nLitImplied) == -1;
         assert degree.signum() > 0;
         assert slackConflict().signum() <= 0;
 
         // saturation
         degree = saturation();
         assert slackConflict().signum() <= 0;
 
         return degree;
     }
 
     protected BigInteger reduceUntilConflict(int litImplied, int ind,
             BigInteger[] reducedCoefs, WatchPb wpb) {
         BigInteger slackResolve = BigInteger.ONE.negate();
         BigInteger slackThis = BigInteger.ZERO;
         BigInteger slackIndex;
         BigInteger slackConflict = slackConflict();
         BigInteger ppcm;
         BigInteger reducedDegree = wpb.getDegree();
         BigInteger previousCoefLitImplied = BigInteger.ZERO;
         BigInteger tmp;
         BigInteger coefLitImplied = weightedLits.get(litImplied ^ 1);
 
         do {
             if (slackResolve.signum() >= 0) {
                 assert slackThis.signum() > 0;
                 tmp = reduceInConstraint(wpb, reducedCoefs, ind, reducedDegree);
                 assert ((tmp.compareTo(reducedDegree) < 0) && (tmp
                         .compareTo(BigInteger.ONE) >= 0));
                 reducedDegree = tmp;
             }
             // search of the multiplying coefficients
             assert weightedLits.get(litImplied ^ 1).signum() > 0;
             assert reducedCoefs[ind].signum() > 0;
 
             if (!reducedCoefs[ind].equals(previousCoefLitImplied)) {
                 assert coefLitImplied.equals(weightedLits.get(litImplied ^ 1));
                 ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
                 assert ppcm.signum() > 0;
                 coefMult = ppcm.divide(coefLitImplied);
                 coefMultCons = ppcm.divide(reducedCoefs[ind]);
 
                 assert coefMultCons.signum() > 0;
                 assert coefMult.signum() > 0;
                 assert coefMult.multiply(coefLitImplied).equals(
                         coefMultCons.multiply(reducedCoefs[ind]));
                 previousCoefLitImplied = reducedCoefs[ind];
             }
 
             // slacks computed for each constraint
             slackThis = wpb.slackConstraint(reducedCoefs, reducedDegree)
                     .multiply(coefMultCons);
             assert slackConflict.equals(slackConflict());
             slackIndex = slackConflict.multiply(coefMult);
             assert slackIndex.signum() <= 0;
             // estimate of the slack after the cutting plane
             slackResolve = slackThis.add(slackIndex);
         } while (slackResolve.signum() >= 0);
         assert coefMult.multiply(weightedLits.get(litImplied ^ 1)).equals(
                 coefMultCons.multiply(reducedCoefs[ind]));
         return reducedDegree;
 
     }
 
     /**
      * computes the slack of the current instance
      */
     public BigInteger slackConflict() {
         BigInteger poss = BigInteger.ZERO;
         BigInteger tmp;
         // for each literal
         for (int i = 0; i < size(); i++) {
             tmp = weightedLits.getCoef(i);
             if (tmp.signum() != 0 && !voc.isFalsified(weightedLits.getLit(i)))
                 poss = poss.add(tmp);
         }
         return poss.subtract(degree);
     }
 
     public boolean oldIsAssertive(int dl) {
         BigInteger tmp;
         int lit;
         BigInteger slack = computeSlack(dl).subtract(degree);
         if (slack.signum() < 0)
             return false;
         for (int i = 0; i < size(); i++) {
             tmp = weightedLits.getCoef(i);
             lit = weightedLits.getLit(i);
             if ((tmp.signum() > 0)
                     && (voc.isUnassigned(lit) || voc.getLevel(lit) >= dl)
                     && (slack.compareTo(tmp) < 0))
                 return true;
         }
         return false;
     }
 
     // computes a slack with respect to a particular decision level
     private BigInteger computeSlack(int dl) {
         BigInteger slack = BigInteger.ZERO;
         int lit;
         BigInteger tmp;
         for (int i = 0; i < size(); i++) {
             tmp = weightedLits.getCoef(i);
             lit = weightedLits.getLit(i);
             if ((tmp.signum() > 0)
                     && (((!voc.isFalsified(lit)) || voc.getLevel(lit) >= dl)))
                 slack = slack.add(tmp);
         }
         return slack;
     }
 
     /**
      * tests if the conflict is assertive (allows to imply a literal) at a
      * particular decision level
      * 
      * @param dl
      *                the decision level
      * @return true if the conflict is assertive at the decision level
      */
     public boolean isAssertive(int dl) {
         assert dl <= currentLevel;
         assert dl <= currentLevel;
 
         currentLevel = dl;
         // assert currentSlack.equals(computeSlack(dl));
         BigInteger slack = currentSlack.subtract(degree);
         if (slack.signum() < 0)
             return false;
         return isImplyingLiteral(slack);
     }
 
     // given the slack already computed, tests if a literal could be implied at
     // a particular level
     // uses the byLevel data structure to parse each literal by decision level
     private boolean isImplyingLiteral(BigInteger slack) {
         // unassigned literals are tried first
         int unassigned = levelToIndex(-1);
         if (byLevel[unassigned] != null) {
             for (IteratorInt iterator = byLevel[unassigned].iterator(); iterator
                     .hasNext();) {
                 if (slack.compareTo(weightedLits.get(iterator.next())) < 0)
                     return true;
             }
         }
         // then we have to look at every literal at a decision level >=dl
         BigInteger tmp;
         int level = levelToIndex(currentLevel);
         if (byLevel[level] != null)
             for (IteratorInt iterator = byLevel[level].iterator(); iterator
                     .hasNext();) {
                 tmp = weightedLits.get(iterator.next());
                 if (tmp != null && slack.compareTo(tmp) < 0)
                     return true;
             }
         return false;
     }
 
     // given the slack already computed, tests if a literal could be implied at
     // a particular level
     // uses the coefs data structure (where coefficients are decreasing ordered)
     // to parse each literal
     private boolean isImplyingLiteralOrdered(int dl, BigInteger slack) {
         int ilit, litLevel;
         for (int i = 0; i < size(); i++) {
             ilit = weightedLits.getLit(i);
             litLevel = voc.getLevel(ilit);
             if ((litLevel >= dl || voc.isUnassigned(ilit))
                     && (slack.compareTo(weightedLits.getCoef(i)) < 0))
                 return true;
         }
         return false;
     }
 
     /**
      * computes the least common factor of two integers (Plus Petit Commun
      * Multiple in french)
      * 
      * @param a
      *                first integer
      * @param b
      *                second integer
      * @return the least common factor
      */
     protected static BigInteger ppcm(BigInteger a, BigInteger b) {
         return a.divide(a.gcd(b)).multiply(b);
     }
 
     /**
      * constraint reduction : removes a literal of the constraint. The literal
      * should be either unassigned or satisfied. The literal can not be the
      * literal that should be resolved.
      * 
      * @param wpb
      *                the initial constraint to reduce
      * @param coefsBis
      *                the coefficients of the constraint wrt which the reduction
      *                will be proposed
      * @param indLitImplied
      *                index in wpb of the literal that should be resolved
      * @param degreeBis
      *                the degree of the constraint wrt which the reduction will
      *                be proposed
      * @return new degree of the reduced constraint
      */
     public BigInteger reduceInConstraint(WatchPb wpb,
             final BigInteger[] coefsBis, final int indLitImplied,
             final BigInteger degreeBis) {
         // logger.entering(this.getClass().getName(),"reduceInConstraint");
         assert degreeBis.compareTo(BigInteger.ONE) > 0;
         // search of an unassigned literal
         int lit = -1;
         for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
             if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.lits[ind])) {
                 assert coefsBis[ind].compareTo(degreeBis) < 0;
                 lit = ind;
             }
 
         // else, search of a satisfied literal
         if (lit == -1)
             for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
                 if ((coefsBis[ind].signum() != 0)
                         && (voc.isSatisfied(wpb.lits[ind]))
                         && (ind != indLitImplied))
                     lit = ind;
 
         // a literal has been found
         assert lit != -1;
 
         assert lit != indLitImplied;
         // logger.finer("Found literal "+Lits.toString(lits[lit]));
         // reduction can be done
         BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
         coefsBis[lit] = BigInteger.ZERO;
 
         // saturation of the constraint
         degUpdate = saturation(coefsBis, degUpdate);
 
         assert coefsBis[indLitImplied].signum() > 0;
         assert degreeBis.compareTo(degUpdate) > 0;
         return degUpdate;
     }
 
     static BigInteger saturation(BigInteger[] coefs, BigInteger degree) {
         assert degree.signum() > 0;
         BigInteger minimum = degree;
         for (int i = 0; i < coefs.length; i++) {
             if (coefs[i].signum() > 0)
                 minimum = minimum.min(coefs[i]);
             coefs[i] = degree.min(coefs[i]);
         }
         if (minimum.equals(degree) && !degree.equals(BigInteger.ONE)) {
             // the result is a clause
             // there is no more possible reduction
             degree = BigInteger.ONE;
             for (int i = 0; i < coefs.length; i++)
                 if (coefs[i].signum() > 0)
                     coefs[i] = degree;
         }
         return degree;
     }
 
     private static boolean positiveCoefs(final BigInteger[] coefsCons) {
         for (int i = 0; i < coefsCons.length; i++) {
             if (coefsCons[i].signum() <= 0)
                 return false;
         }
         return true;
     }
 
     /**
      * computes the level for the backtrack : the highest decision level for
      * which the conflict is assertive.
      * 
      * @param maxLevel
      *                the lowest level for which the conflict is assertive
      * @return the highest level (smaller int) for which the constraint is
      *         assertive.
      */
     public int getBacktrackLevel(int maxLevel) {
         // we are looking for a level higher than maxLevel
         // where the constraint is still assertive
         VecInt lits;
         int level;
         int indStop = levelToIndex(maxLevel) - 1;
         int indStart = levelToIndex(0);
         BigInteger slack = computeSlack(0).subtract(degree);
         int previous = 0;
         for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
             if (byLevel[indLevel] != null) {
                 level = indexToLevel(indLevel);
                 assert computeSlack(level).subtract(degree).equals(slack);
                 if (isImplyingLiteralOrdered(level, slack)) {
                     break;
                 }
                 // updating the new slack
                 lits = byLevel[indLevel];
                 int lit;
                 for (IteratorInt iterator = lits.iterator(); iterator.hasNext();) {
                     lit = iterator.next();
                     if (voc.isFalsified(lit)
                             && voc.getLevel(lit) == indexToLevel(indLevel))
                         slack = slack.subtract(weightedLits.get(lit));
                 }
                 if (!lits.isEmpty())
                     previous = level;
             }
         }
         assert previous == oldGetBacktrackLevel(maxLevel);
         return previous;
     }
 
     public int oldGetBacktrackLevel(int maxLevel) {
         int litLevel;
         int borneMax = maxLevel;
         assert oldIsAssertive(borneMax);
         int borneMin = -1;
         // borneMax is the highest level in the search tree where the constraint is assertive
         for (int i = 0; i < size() ; i++) {
             litLevel = voc.getLevel(weightedLits.getLit(i));
             if (litLevel < borneMax && litLevel > borneMin
                     && oldIsAssertive(litLevel))
                 borneMax = litLevel;
         }
         // the level returned is the first level below borneMax
         // where there is a literal belonging to the constraint
         int retour = 0;
         for (int i = 0; i < size(); i++) {
             litLevel = voc.getLevel(weightedLits.getLit(i));
             if (litLevel > retour && litLevel < borneMax) {
                 retour = litLevel;
             }
         }
         return retour;
     }
 
     public void updateSlack(int level) {
         int dl = levelToIndex(level);
         if (byLevel[dl] != null) {
             int lit;
             for (IteratorInt iterator = byLevel[dl].iterator(); iterator
                     .hasNext();) {
                 lit = iterator.next();
                 if (voc.isFalsified(lit))
                     currentSlack = currentSlack.add(weightedLits.get(lit));
             }
         }
     }
 
     @Override
     void increaseCoef(int lit, BigInteger incCoef) {
         if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
             currentSlack = currentSlack.add(incCoef);
         }
         assert byLevel[levelToIndex(voc.getLevel(lit))].contains(lit);
         super.increaseCoef(lit, incCoef);
     }
 
     @Override
     void decreaseCoef(int lit, BigInteger decCoef) {
         if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
             currentSlack = currentSlack.subtract(decCoef);
         }
         assert byLevel[levelToIndex(voc.getLevel(lit))].contains(lit);
         super.decreaseCoef(lit, decCoef);
     }
 
     @Override
     void setCoef(int lit, BigInteger newValue) {
         int litLevel = voc.getLevel(lit);
         if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
             if (weightedLits.containsKey(lit))
                 currentSlack = currentSlack.subtract(weightedLits.get(lit));
             currentSlack = currentSlack.add(newValue);
         }
         int indLitLevel = levelToIndex(litLevel);
         if (!weightedLits.containsKey(lit)) {
             if (byLevel[indLitLevel] == null) {
                 byLevel[indLitLevel] = new VecInt();
             }
             byLevel[indLitLevel].push(lit);
 
         }
         assert byLevel[indLitLevel] != null;
         assert byLevel[indLitLevel].contains(lit);
         super.setCoef(lit, newValue);
     }
 
     @Override
     void changeCoef(int indLit, BigInteger newValue) {
     	int lit = weightedLits.getLit(indLit);
         int litLevel = voc.getLevel(lit);
         if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
             if (weightedLits.containsKey(lit))
                 currentSlack = currentSlack.subtract(weightedLits.get(lit));
             currentSlack = currentSlack.add(newValue);
         }
         int indLitLevel = levelToIndex(litLevel);
         assert weightedLits.containsKey(lit);
         assert byLevel[indLitLevel] != null;
         assert byLevel[indLitLevel].contains(lit);
         super.changeCoef(indLit, newValue);
     }
 
 
     @Override
     void removeCoef(int lit) {
         int litLevel = voc.getLevel(lit);
         if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
             currentSlack = currentSlack.subtract(weightedLits.get(lit));
         }
         int indLitLevel = levelToIndex(litLevel);
         assert indLitLevel < byLevel.length;
         assert byLevel[indLitLevel] != null;
         assert byLevel[indLitLevel].contains(lit);
         byLevel[indLitLevel].remove(lit);
         super.removeCoef(lit);
     }
     
     
     private int getLevelByLevel(int lit) {
         for (int i = 0; i < byLevel.length; i++)
             if (byLevel[i] != null && byLevel[i].contains(lit))
                 return i;
         return -1;
     }
 
     public boolean slackIsCorrect(int dl) {
         return currentSlack.equals(computeSlack(dl));
     }
 
     @Override
     public String toString() {
         int lit;
         StringBuffer stb = new StringBuffer();
         for (int i = 0; i < size(); i++) {
             lit = weightedLits.getLit(i);
             stb.append(weightedLits.getCoef(i));
             stb.append(".");
             stb.append(Lits.toString(lit));
             stb.append(" ");
             stb.append("[");
             stb.append(voc.valueToString(lit));
             stb.append("@");
             stb.append(voc.getLevel(lit));
             stb.append("]");
         }
         return stb.toString() + " >= " + degree; //$NON-NLS-1$
     }
 
 }