/**
    * 
    */
   package org.sat4j.reader;
   
   import java.io.IOException;
   import java.math.BigInteger;
   import java.util.HashMap;
   import java.util.Map;
  
  import org.sat4j.core.Vec;
  import org.sat4j.core.VecInt;
  import org.sat4j.specs.ContradictionException;
  import org.sat4j.specs.ISolver;
  import org.sat4j.specs.IVec;
  import org.sat4j.specs.IVecInt;
  
  /**
   * @author parrain
   * 
   */
  public class OPBReader2007 extends OPBReader2006 {
  
      /**
       * 
       */
      private static final long serialVersionUID = 1L;
  
      private int nbProducts;
  
      // MetaData: #products and productSize in file.
  
      /**
       * @param solver
       */
      public OPBReader2007(ISolver solver) {
          super(solver);
          // TODO Auto-generated constructor stub
      }
  
      @Override
      protected boolean isGoodFirstCharacter(char c) {
          return Character.isLetter(c) || c == '_' || c == '~';
      }
  
      @Override
      protected void checkId(StringBuffer s) throws ParseFormatException {
          // Small check on the coefficient ID to make sure everything is ok
          int cpt = 1;
          if (s.charAt(0) == '~')
              cpt = 2;
          int varID = Integer.parseInt(s.substring(cpt));
          if (varID > nbVars) {
              throw new ParseFormatException(
                      "Variable identifier larger than #variables in metadata.");
          }
      }
  
      /**
       * contains the number of new symbols generated to linearize products
       */
      private int nbNewSymbols;
  
      @Override
      protected void readTerm(StringBuffer coeff, StringBuffer var)
              throws IOException, ParseFormatException, ContradictionException {
          readInteger(coeff);
  
          skipSpaces();
  
          var.setLength(0);
          IVec<String> tmpLit = new Vec<String>();
          StringBuffer tmpVar = new StringBuffer();
          while (readIdentifier(tmpVar)) {
              tmpLit = tmpLit.push(tmpVar.toString());
              skipSpaces();
          }
          if (tmpLit.size() == 0)
              throw new ParseFormatException("identifier expected");
          if (tmpLit.size() == 1) {
              // it is a "normal" term
              var.append(tmpLit.last());
              tmpLit.pop();
          } else {
              // it is a product term
              var.append(linearizeProduct(tmpLit));
          }
      }
  
      /**
       * callback called when we read a term of a constraint
       * 
       * @param var
       *                the identifier of the variable
       * @param lits
       *                a set of literals in DIMACS format in which var once
       *                translated will be added.
       */
      protected void literalInAProduct(String var, IVecInt lits) {
         int beginning = ((var.charAt(0) == '~') ? 2 : 1);
         int id = Integer.parseInt(var.substring(beginning));
         int lid = ((var.charAt(0) == '~') ? -1 : 1) * id;
         lits.push(lid);
     }
 
     /**
      * callback called when we read a term of a constraint
      * 
      * @param var
      *                the identifier of the variable
      * @param lits
      *                a set of literals in DIMACS format in which var once
      *                translated will be added.
      */
     protected void negateLiteralInAProduct(String var, IVecInt lits) {
         int beginning = ((var.charAt(0) == '~') ? 2 : 1);
         int id = Integer.parseInt(var.substring(beginning));
         int lid = ((var.charAt(0) == '~') ? 1 : -1) * id;
         lits.push(lid);
     }
 
     /**
      * read the first comment line to get the number of variables and the number
      * of constraints in the file calls metaData with the data that was read
      * 
      * @throws IOException
      * @throws ParseException
      */
     @Override
     protected void readMetaData() throws IOException, ParseFormatException {
         char c;
         String s;
 
         // get the number of variables and constraints
         c = get();
         if (c != '*')
             throw new ParseFormatException(
                     "First line of input file should be a comment");
 
         s = readWord();
         if (eof() || !"#variable=".equals(s))
             throw new ParseFormatException(
                     "First line should contain #variable= as first keyword");
 
         nbVars = Integer.parseInt(readWord());
         nbNewSymbols = nbVars + 1;
 
         s = readWord();
         if (eof() || !"#constraint=".equals(s))
             throw new ParseFormatException(
                     "First line should contain #constraint= as second keyword");
 
         nbConstr = Integer.parseInt(readWord());
 
         s = readWord();
         // if (eof() || !"#product=".equals(s))
         // throw new ParseFormatException(
         // "First line should contain #product= as third keyword");
         if (s.equals("#product=")) {
             nbProducts = Integer.parseInt(readWord());
             nbVars += nbProducts;
             nbConstr += 2 * nbProducts;
         }
 
         s = readWord();
         // if (eof() || !"sizeproduct=".equals(s))
         // throw new ParseFormatException(
         // "First line should contain sizeproduct= as fourth keyword");
 
         if (s.equals("sizeproduct="))
             readWord();
 
         // skip the rest of the line
         in.readLine();
 
         // callback to transmit the data
         metaData(nbVars, nbConstr);
     }
 
     @Override
     protected int translateVarToId(String var) {
         int beginning = ((var.charAt(0) == '~') ? 2 : 1);
         int id = Integer.parseInt(var.substring(beginning));
         return ((var.charAt(0) == '~') ? -1 : 1) * id;
     }
 
     private String linearizeProduct(IVec<String> tmpLit)
             throws ContradictionException {
         tmpLit.sort(String.CASE_INSENSITIVE_ORDER);
         String newVar = getProductVariable(tmpLit);
         if (newVar == null) {
             // generate a new symbol
             newVar = "X" + String.valueOf(nbNewSymbols++);
             // linearization proposed by O. Roussel (PB07)
             // generate the clause
             // product => newSymbol (this is a clause)
             // not x1 or not x2 ... or not xn or newSymbol
             productStore.put(newVar, tmpLit);
             IVecInt newLits = new VecInt();
             for (String lit : tmpLit)
                 negateLiteralInAProduct(lit, newLits);
             literalInAProduct(newVar, newLits);
             solver.addClause(newLits);
             // generate the PB-constraint
             // newSymbol => product translated as
             // x1+x2+x3...+xn-n*newSymbol>=0
             newLits.clear();
             IVec<BigInteger> newCoefs = new Vec<BigInteger>();
             for (String lit : tmpLit) {
                 literalInAProduct(lit, newLits);
                 newCoefs.push(BigInteger.ONE);
             }
             literalInAProduct(newVar, newLits);
             newCoefs.push(new BigInteger(String.valueOf(-tmpLit.size())));
             solver.addPseudoBoolean(newLits, newCoefs, true, BigInteger.ZERO);
             nbConstraintsRead += 2;
         }
         return newVar;
     }
 
     private Map<String, IVec<String>> productStore = new HashMap<String, IVec<String>>();
 
     private String getProductVariable(IVec<String> lits) {
         for (Map.Entry<String, IVec<String>> c : productStore.entrySet())
             if (c.getValue().equals(lits))
                 return c.getKey();
         return null;
     }
 
 }