/*=============================================================================
 * parser for pseudo-Boolean instances
 * 
 * Copyright (c) 2005-2007 Olivier ROUSSEL and Vasco MANQUINHO
 * 
 * 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 <iostream>
#include <fstream>
#include <iomanip>
#include <stdexcept>
using namespace std;

#ifdef useGMP
#include <gmpxx.h>

typedef 
  mpz_class IntegerType;
#else
#warning this IntegerType may not be suitable for some input file. Consider using GMP
typedef
  long IntegerType;
#endif

class SimpleParser
{
protected:
  /*
   * This protected section defines the callback that are used by the
   * parser to send data back to the program.
   *
   * These functions must be redefined in a subclass.
   */

  /**
   * callback called when we get the number of variables and the
   * expected number of constraints
   * @param nbvar: the number of variables
   * @param nbconstr: the number of contraints
   */
  void metaData(int nbvar, int nbconstr)
  {
    cout << "[nbvar=" << nbvar << "]" << endl;
    cout << "[nbconstr=" << nbconstr << "]" << endl;
  }

  /**
   * callback called before we read the objective function
   */
  void beginObjective()
  {
    cout << "objective:  ";
  }

  /**
   * callback called after we've read the objective function
   */
  void endObjective()
  {
    cout << endl;
  }


  /**
   * callback called when we read a term of the objective function
   *
   * @param coeff: the coefficient of the term
   * @param var: the identifier of the variable
   */
  void objectiveTerm(IntegerType coeff, string var)
  {
    cout << "[" << showpos << coeff << "*" << var << "] ";
  }

  /**
   * callback called before we read a constraint
   */
  void beginConstraint()
  {
    cout << "constraint: ";
  }

  /**
   * callback called after we've read a constraint
   */
  void endConstraint()
  {
    cout << endl;
  }

  /**
   * callback called when we read a term of a constraint
   *
   * @param coeff: the coefficient of the term
   * @param var: the identifier of the variable
   */
  void constraintTerm(IntegerType coeff, string var)
  {
    cout << "[" << showpos << coeff << "*" << var << "] ";
  }

  /**
   * callback called when we read the relational operator of a constraint
   *
   * @param relop: the relational oerator (>= or =)
   */
  void constraintRelOp(string relop)
  {
    cout << "[" << relop << "] ";
  }

  /**
   * callback called when we read the right term of a constraint (also
   * known as the degree)
   *
   * @param val: the degree of the constraint
   */
  void constraintRightTerm(IntegerType val)
  {
    cout << "[" << val << "]";
  }

private:
  ifstream in; // the stream we're reading from

  /**
   * get the next character from the stream
   */
  char get()
  {
    return in.get();
  }

  /**
   * put back a character into the stream (only one chr can be put back)
   */
  void putback(char c)
  {
    in.putback(c);
  }

  /**
   * return true iff we've reached EOF
   */
  bool eof()
  {
    return !in.good();
  }

  /**
   * skip white spaces
   */
  void skipSpaces()
  {
    char c;

    while(isspace(c=get()));

    putback(c);
  }

  /**
   * read an identifier from stream and store it in s
   * @param s: the variable to hold the identifier we read
   * @return true iff an identifier was correctly read
   */
  bool readIdentifier(string &s)
  {
    char c;

    skipSpaces();

    // first char (must be a letter or underscore)
    c=get();
    if (eof())
      return false;

    if (!isalpha(c) && c!='_')
    {
      putback(c);
      return false;
    }

    s=c;

    // next chars (must be a letter, a digit or an underscore)
    while(true)
    {
      c=get();
      if (eof())
	break;

      if (isalpha(c) || isdigit(c) || c=='_')
	s+=c;
      else
      {
	putback(c);
	break;
      }
    }

    return true;
  }

  /**
   * read a relational operator from stream and store it in s
   * @param s: the variable to hold the relational operator we read
   * @return true iff a relational operator was correctly read
   */
  bool readRelOp(string &s)
  {
    char c;

    skipSpaces();

    c=get();
    if (eof())
      return false;

    if (c=='=')
    {
      s="=";
      return true;
    }

    if (c=='>' && get()=='=')
    {
      s=">=";
      return true;
    }

    return false;
  }

  /**
   * 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
   */
  void readMetaData()
  {
    char c;
    string s;
    int nbVars,nbConstr;

    // get the number of variables and constraints
    c=get();
    if (c!='*')
      throw runtime_error("First line of input file should be a comment");

    in >> s;
    if (eof() || s!="#variable=")
      throw runtime_error("First line should contain #variable= as first keyword");

    in >> nbVars;

    in >> s;
    if (eof() || s!="#constraint=")
      throw runtime_error("First line should contain #constraint= as second keyword");

    in >> nbConstr;

    // skip the rest of the line
    getline(in,s);

    // callback to transmit the data
    metaData(nbVars,nbConstr);
  }


  /**
   * skip the comments at the beginning of the file
   */
  void skipComments()
  {
    string s;
    char c;

    // skip further comments

    while(!eof() && (c=get())=='*')
    {
      getline(in,s);
    }

    putback(c);
  }


  /**
   * read a term into coeff and var
   * @param coeff: the coefficient of the variable
   * @param var: the indentifier we read
   */
  void readTerm(IntegerType &coeff, string &var)
  {
    char c;

    in >> coeff;
    
    skipSpaces();
    c=get();
    if (c!='*')
      throw runtime_error("'*' expected between a coefficient and a variable");

    if (!readIdentifier(var))
      throw runtime_error("identifier expected");
  }

  /**
   * read the objective line (if any)
   *
   * calls beginObjective, objectiveTerm and endObjective
   */
  void readObjective()
  {
    char c;
    string s,var;
    IntegerType coeff;

    // read objective line (if any)

    skipSpaces();
    c=get();
    if (c!='m')
    {
      // no objective line
      putback(c);
      return;
    }

    if (get()=='i' && get()=='n' && get()==':')
    {
      beginObjective(); // callback

      while(!eof())
      {
	readTerm(coeff,var);
	objectiveTerm(coeff,var); // callback

	skipSpaces();
	c=get();
	if (c==';')
	  break; // end of objective
	else
	  if (c=='-' || c=='+' || isdigit(c))
	    putback(c);
	  else
	    throw runtime_error("unexpected character in objective function");
      }

      endObjective();
    }
    else
      throw runtime_error("input format error: 'min:' expected");
  }

  /**
   * read a constraint
   *
   * calls beginConstraint, constraintTerm and endConstraint
   */
  void readConstraint()
  {
    string s, var;
    char c;
    IntegerType coeff;

    beginConstraint();

    while(!eof())
    {
      readTerm(coeff,var);
      constraintTerm(coeff,var);

      skipSpaces();
      c=get();
      if (c=='>' || c=='=')
      {
	// relational operator found
	putback(c);
	break;
      }
      else
	if (c=='-' || c=='+' || isdigit(c))
	  putback(c);
	else
	  throw runtime_error("unexpected character in constraint");
    }

    if (eof())
      throw runtime_error("unexpected EOF before end of constraint");
      
    if (readRelOp(s))
      constraintRelOp(s);
    else
      throw runtime_error("unexpected relational operator in constraint");

    in >> coeff;
    constraintRightTerm(coeff);

    skipSpaces();
    c=get();
    if (eof() || c!=';')
      throw runtime_error("semicolon expected at end of constraint");

    endConstraint();
  }

public:

  /**
   * constructor which only opens the file
   */
  SimpleParser(char *filename)
  {
    in.open(filename,ios_base::in);

    if (!in.good())
      throw runtime_error("error opening input file");
  }

  /**
   * parses the file and uses the callbacks to send to send the data
   * back to the program
   */
  void parse()
  {
    readMetaData();

    skipComments();

    readObjective();

    // read constraints
    while(!eof())
    {
      skipSpaces();
      if (eof())
	break;

      readConstraint();
    }
  }
}; // class SimpleParser


int main(int argc, char *argv[])
{
  try
  {
    if (argc!=2)
      cout << "usage: SimpleParser <filename>" << endl;
    else
    {
      SimpleParser parser(argv[1]);

      parser.parse();
    }
  }
  catch(exception &e)
  {
    cout.flush();
    cerr << e.what() << endl;
  }

  return 0;
}