//
// parser.cpp
//

#include "parser.h"
#include <sstream>

//
// nacte data ze vstupniho souboru do objektu vnitrni formy
//
void parseCNF(const char *inputFile, InnerForm *inner)
{
  ifstream *src=NULL;
//  ifstream src(inputFile, ios::in);
  src=new ifstream(inputFile, ios::in);
  src->seekg (0, ios::beg);

  if (src->fail())
  {
    src->close();
    delete src;
    throw "Unable to read from input file!\n";
  }
  int *var=new int[maxVariablesInOneClause];

  int clausePtr=0;
  readline=0;

  while(src->getline(line, sizeof(line))!=NULL)
//  while(src.getline(line, sizeof(line))!=NULL)
  {
    readline++;
    actual = line;

    if (*actual == 'c' ){}//skip comment
    else if (*actual == 'p') //parse parameters
    {
      actual++;
      skipWhitespace(actual);
      if (*(actual++)!='c' || *(actual++)!='n' || *(actual++)!='f')
      {
        delete src;
        throw "PARSE ERROR! CNF form expected!\n";
      }
      int a= parseInt(actual);
      int b= parseInt(actual);
      #ifdef consoleOut
        #ifndef testMethod
          cout << "number of variables:" << a << endl;
          cout << "number of clauses:" << b << endl;
        #endif
      #endif

      inner->numberOfVariables=a;
      inner->numberOfClauses=b;
      inner->clauses = new int *[inner->numberOfClauses];
    }
    else
    {
      int a, b=0;

      while((a = parseInt(actual))!=0)
      {
        var[b]=a;
        b++;
        if (b>=maxVariablesInOneClause) throw "Too long clauses. Max 100 variables in clause allowed!";
      }


      inner->clauses[clausePtr]=new int[b+1];
      inner->clauses[clausePtr][0]=b; //pocet polozek v klauzuli
      for(int hh=1; hh<b+1;hh++)       //jednotlive polozky v klauzuli
      {
        inner->clauses[clausePtr][hh]=var[hh-1];
      }

      clausePtr++;
    }
  }
  src->close();
  delete src;
  delete var;
}

//
// preved retezec na integer
//
int parseInt(char*& in)
{
    stringstream ss;
    int     val = 0;
    bool    neg = false;
    skipWhitespace(in);
    if      (*in == '-') neg = true, in++;
    else if (*in == '+') in++;
    if (*in < '0' || *in > '9')
    {
      ss << "PARSE ERROR! Unexpected character at " << readline << " line.\n";
      throw ss.str().c_str();
    }
    while (*in >= '0' && *in <= '9')
        val = val*10 + (*in - '0'),
        in++;
    return neg ? -val : val;
}

//
// vynechej "prazdne" znaky mezi slovy
//
void skipWhitespace(char*& in)
{
  while ((*in >= 9 && *in <= 13) || *in == 32)
    in++;
}

//
// vynechej "prazdne" radky mezi slovy
//
void skipLine(char*& in)
{
  for (;;)
  {
    if (*in == 0) return;
    if (*in == '\n') { in++; return; }
    in++;
  }
}


//
// naparcovani parametru z textoveho pole - urcene pro vazeny SAT
//
void parseParameters(const char *inputData, int *weightTable, int & sumOfWeights, int numberOfVariables, int &unsatPenalty)
{
  char *in=(char*)inputData;
  int val, ii, jj;
  sumOfWeights=0;
  unsatPenalty=10;

  try
  {
    for(ii=0; ii<numberOfVariables+1;ii++)
    {
      val=parseInt(in);
      if (ii==0)
      {
        unsatPenalty=val;
      }else{
        weightTable[ii-1]=val;
        sumOfWeights+=val;
      }
    }
  }catch(const char *msg){
  }
  for(int i=ii; i<numberOfVariables+1;i++) //pokud najde nekde chybu, tak vsechny ostatni vahy, pocinaje od nalezene chyby, budou 1
  {
    weightTable[ii++ -1]=1;
    sumOfWeights++;
  }
  if (sumOfWeights==0)sumOfWeights=1;
  if (unsatPenalty<10)unsatPenalty=10;
}
