/**CFile*******************************************************************
  PackageName [bdd]
  Synopsis    [Package 'bdd' enable symbolic computations by representing
               Boolean functions with ROBDDs.]

  FileName    [bddUtil.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Ales Casar (casar@uni-mb.si)]
  Description [File bddUtil.c contains useful functions.]
  SeeAlso     [bdd.h, bddInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#include "bddInt.h"

#define oAND 1
#define oOR 2
#define oEXOR 3

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Static function prototypes                                            */
/*-----------------------------------------------------------------------*/

static Bdd_Edge Izraz(Est_String s, int *i, Est_String *ch);

static void NextCh(Est_String s, int *i, Est_String *ch);

static Bdd_Edge Izrazi(Est_String s, int *i, Est_String *ch, Bdd_Edge g,
                        int op);

static int Op(Est_String s, int *i, Est_String *ch);

static Est_Boolean DoberZnak(char c);

/**AutomaticEnd***********************************************************/

/*-----------------------------------------------------------------------*/
/* Definition of exported functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Bdd_SystemStat(FILE *s)
{
  fprintf(s,"  bddNodeTable.size = %u\n",BddNodeTableSize());
  fprintf(s,"  bddNodeTable.max = %u\n",BddNodeTableMax());
  fprintf(s,"  bddNodeTable.num = %u\n",BddNodeTableNum());
  fprintf(s,"  bddNodeTable.fortified = %u\n",BddNodeTableNumF());
  fprintf(s,"  bddNodeTable.FOA = %lu\n",BddNodeTableFOA());
  fprintf(s,"  bddNodeTable.compare = %lu\n",BddNodeTableCompare());
  fprintf(s,"  bddNodeTable.add = %lu\n",BddNodeTableAdd());
  fprintf(s,"  bddNodeTable.garbage = %u\n",BddNodeTableGarbage());
  fprintf(s,"  bddNodeTable.generated = %u\n",BddNodeTableGenerated());
  fprintf(s,"  bddNodeTable.blockNumber = %u\n",BddNodeTableBlockNumber());
  fprintf(s,"  bddNodeTable.listUsed = %u\n",BddListUsed());
  fprintf(s,"  bddNodeTable.listMaxLength = %u\n",BddListMaxLength());
  fprintf(s,"  bddNodeTable.listAvgLength = %f\n",BddListAvgLength());
  fprintf(s,"  bddIteCache.find = %lu\n",BddIteCacheFind());
  fprintf(s,"  bddIteCache.overwrite = %lu\n",BddIteCacheOverwrite());
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Bdd_FunctionStat(FILE *s, Bdd_Edge f)
{
  int num;

  num = BddNodeNumber(f);

  /* BDD.nodeNumber / BDD.nodeMaxLevel / BDD.nodeAvgLevel */

  fprintf(s,"%d/",num);
  fprintf(s,"%d/",BddNodeMaxLevel(f));
  fprintf(s,"%f",BddNodeAvgLevel(f));

  return num;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_FindFormula]
  Description [Bdd_FindFormula find formula in Fomulea tree.]
  SideEffects []
  SeeAlso     [Bdd_AddFormula]
  ************************************************************************/

Est_Boolean
Bdd_FindFormula(Est_String x, Bdd_Edge *f)
{
  BddFormula *sup;

  sup = bddFormulaeTree;
  while (sup && strcmp(sup->name, x)) {
    sup = (strcmp(x, sup->name) < 0) ? sup->l : sup->r;
  }
  if (!sup) return FALSE;
  *f = sup->f;
  return TRUE;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_AddFormula]
  Description [Bdd_AddFormula add formula to the Formulae tree.]
  SideEffects [If bddFormulaeTree does not exist, function create it.
               If such formula already exists, function overwrite it!
               Bdd_AddFormula fortify BDD.]
  SeeAlso     [Bdd_FindFormula]
  ************************************************************************/

void
Bdd_AddFormula(Est_String x, Bdd_Edge f)
{
  BddFormula *sup;
  Est_Boolean end, overwrite;

  overwrite = FALSE;
  if (!bddFormulaeTree) {

    if (!(bddFormulaeTree = (BddFormula *) malloc(sizeof(BddFormula)))) {
      fprintf(stdout,"Bdd_AddFormula: Out of memoy!\n");
      exit(1);
    }

    bddFormulaeTree->l = bddFormulaeTree->r = NULL;
    bddFormulaeTree->name = strdup(x);
    bddFormulaeTree->f = f;
  } else {
    end = FALSE;
    sup = bddFormulaeTree;
    while (!end) {
      if (strcmp(x, sup->name) < 0) {
	    if (sup->l) sup = sup->l;
        else end = TRUE;
      } else {
        if (strcmp(x, sup->name) > 0) {
	      if (sup->r) sup = sup->r;
          else end = TRUE;
        } else {
          sup->f = f;
          overwrite = TRUE;
          end = TRUE;
        }
      }
    }

    if (!overwrite) {
      if (strcmp(x, sup->name) < 0) {

        if (!(sup->l = (BddFormula *) malloc(sizeof(BddFormula)))) {
          fprintf(stdout,"Bdd_AddFormula: Out of memoy!\n");
          exit(1);
        }

	    sup = sup->l;

      } else {

        if (!(sup->r = (BddFormula *) malloc(sizeof(BddFormula)))) {
          fprintf(stdout,"Bdd_AddFormula: Out of memoy!\n");
          exit(1);
        }

	    sup = sup->r;

      }

      sup->l = sup->r = NULL;
      sup->name = strdup(x);
      sup->f = f;

      if (!Bdd_isNull(f)) {
        Bdd_Fortify(f);
      }
    }
  }
}


/**Function****************************************************************
  Synopsis    [Function Bdd_SaveFormula]
  Description [Bdd_SaveFormula add formula to the Formulae tree.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Bdd_SaveFormula(Est_String prefix, Est_String name, Bdd_Edge f)
{
  Est_String s;

  s = (Est_String) malloc(strlen(prefix) + strlen(name) + 1);
  sprintf(s,"%s%s",prefix,name);
  Bdd_AddFormula(s,f);
  free(s);
}

/**Function****************************************************************
  Synopsis    [Function Bdd_ExtractBranch]
  Description [Returns sub-BDD with only one (left-most) one-path.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_ExtractBranch(Bdd_Edge f)
{
  if (Bdd_isTerminal(f)) return f;
  if (!f.mark) {
    if (!Bdd_isEqv(Bdd_GetElse(f),bdd_termFalse)) {
      return BddFoaNode(Bdd_GetVariable(f),Bdd_ExtractBranch(Bdd_GetElse(f)),bdd_termFalse);
    } else {
      return BddFoaNode(Bdd_GetVariable(f),bdd_termFalse,Bdd_ExtractBranch(Bdd_GetThen(f)));
    }
  } else {
    if (!Bdd_isEqv(Bdd_GetElse(f),bdd_termTrue)) {
      return BddFoaNode(Bdd_GetVariable(f),Bdd_ExtractBranch(Bdd_NOT(Bdd_GetElse(f))),bdd_termFalse);
    } else {
      return BddFoaNode(Bdd_GetVariable(f),bdd_termFalse,Bdd_ExtractBranch(Bdd_NOT(Bdd_GetThen(f))));
    }
  }

  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_Expand]
  Description [Bdd_Expand expands Boolean function in such a way, that
               it substitute all variables with functions.]
  SideEffects [In some cases, some subfunctions are also expanded]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_Expand(Est_String fname, Bdd_Edge f)
{
  Est_String topname;
  Bdd_Edge g;
  int topF,topG;

  topname = Bdd_GetVariableName(f);

  /*
  printf("START Bdd_Expand %s\n",fname);
  Bdd_WriteFunction(f);
  Bdd_WriteBDD(f);
  */

  if (Bdd_isTerminal(f)) {
    return f;
  }

  if (!Bdd_FindFormula(topname,&g)) {
    return f;
  };

  topF = Bdd_GetVariableOrder(f);
  topG = Bdd_GetVariableOrder(g);

  if (topF == topG) {
    /*
    printf("top ==\n");
    */
  }

  else if (topF < topG) {
    /*
    printf("top <<\n");
    */
    f = Bdd_Compose(f,Bdd_GetVariable(f),g); /* SUBSTITUTE SUBFUNCTION ... */
    Bdd_AddFormula(fname,f);                 /* STORE THE RESULT ... */
    f = Bdd_Expand(fname,f);                 /* AND THEN TRY EXPANDING f AGAIN */
  }

  else if (topF > topG) {
    /*
    printf("top >>\n");
    */
    g = Bdd_Expand(topname,g); /* EXPAND SUBFUNCTION FIRST ... */
    f = Bdd_Expand(fname,f);   /* AND THEN TRY EXPANDING f AGAIN */
  }

  return f;
}

/**Function****************************************************************
  Synopsis    [Function Bdd_Expr]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_Expr(Est_String s)
{
  Bdd_Edge pom;
  Est_String ch;
  int i;

  ch = (Est_String) malloc(255);

  i = 0;
  NextCh(s,&i,&ch);
  pom = Izraz(s,&i,&ch);

  free(ch);
  return pom;
}

/*-----------------------------------------------------------------------*/
/* Definition of internal functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description [BddExchange exchange two Boolean functions.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
BddExchange(Bdd_Edge *f, Bdd_Edge *g)
{
  Bdd_Edge sup;

  sup = *f;
  *f = *g;
  *g = sup;
}

/*-----------------------------------------------------------------------*/
/* Definition of static functions                                        */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Function Izraz]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Bdd_Edge
Izraz(Est_String s, int *i, Est_String *ch)
{
  Bdd_Edge f;
  int op;

  if (!strcmp(*ch,"(")) {
    NextCh(s,i,ch);

    if (!strcmp(*ch, "NOT")) {
      NextCh(s,i,ch);
      f = Bdd_NOT(Izraz(s,i,ch));
    } else {
      if ((op = Op(s,i,ch))) {
	f = Izrazi(s, i, ch, Izraz(s,i,ch), op);
      } else {
	f = Izraz(s,i,ch);
      }
    }

    if (!strcmp(*ch, ")")) NextCh(s,i,ch);

    return f;
  }

  if (DoberZnak(*ch[0])) {
    if (!Bdd_FindFormula(*ch, &f)) f = Bdd_FoaTerminal(*ch);
    NextCh(s,i,ch);
    return f;
  }

  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    [Function Izrazi]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Bdd_Edge
Izrazi(Est_String s, int *i, Est_String *ch, Bdd_Edge g, int op)
{
  Bdd_Edge f, h;

  h = Izraz(s,i,ch);
  if (!Bdd_isNull(h)) {
    switch (op) {
	    case oAND:  f = Bdd_ITE(g, h, bdd_termFalse);
	                break;
	    case oOR:  f = Bdd_ITE(g, bdd_termTrue, h);
	                break;
	    case oEXOR:  f = Bdd_ITE(g, Bdd_NOT(h), h);
    }
    return Izrazi(s, i, ch, f, op);
  }
  return g;
}

/**Function****************************************************************
  Synopsis    [Function NextCh]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
NextCh(Est_String s, int *i, Est_String *ch)
{
  char c;
  int j;

    while (s[*i] == ' ' || s[*i] == '\t') (*i)++;
    j = *i;
    c = s[*i];

    if (c == '(') {
      (*i)++;
      strcpy(*ch,"(");
      return;
    }

    if (c == ')') {
      (*i)++;
      strcpy(*ch,")");
      return;
    }

    if (DoberZnak(c)) {
      (*i)++;
      while (DoberZnak(s[*i])) (*i)++;
      c = s[*i];

      if ( (c == ' ') || (c == '\t') || (c == '(') || (c == ')') ) {
        strncpy(*ch, &(s[j]), *i-j);
        (*ch)[*i-j] = 0;
        return;
      }
    }

    strcpy(*ch,"");
    return;
}

/**Function****************************************************************
  Synopsis    [Function Op]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
Op(Est_String s, int *i, Est_String *ch)
{
  if (!strcmp(*ch, "AND")) {
    NextCh(s,i,ch);
    return oAND;
  }

  if (!strcmp(*ch, "OR")) {
    NextCh(s,i,ch);
    return oOR;
  }

  if (!strcmp(*ch, "EXOR")) {
    NextCh(s,i,ch);
    return oEXOR;
  }

  return 0;
}

/**Function****************************************************************
  Synopsis    [Function DoberZnak]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
DoberZnak(char c)
{
  return (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z') ||
         (c >= '0' && c <= '9') || c == '_' || c == '[' || c == ']' ||
         c == '$' || c == '.' || c == '&';
}

/**Function****************************************************************
  Synopsis    [Function UpCase]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_String
UpCase(Est_String s)
  {
    Est_String p;

    p = s;
    while (p[0])
      {
	p[0] = toupper(p[0]);
	p = &p[1];
      }
    return s;
  }
