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

  FileName    [bddRel.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 [The file bddRel.c contains functions for relational
               operations (e.g. RelProd).]
  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"

/*-----------------------------------------------------------------------*/
/* Constant declarations                                                 */
/*-----------------------------------------------------------------------*/

#define oNULL 0
#define oAND 1
#define oOR 2
#define oIMPL 3

/*-----------------------------------------------------------------------*/
/* Variable declarations                                                 */
/*-----------------------------------------------------------------------*/

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

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

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

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

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

Bdd_Edge
Bdd_RelOp(Bdd_Edge f, Bdd_Edge g, Est_String format, Est_Boolean firsttime)
{
  static int op;
  static unsigned int key;

  BddRelOpCache *p;
  Bdd_Edge f0, f1, g0, g1, h0, h1;

  static Est_String zname; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String v;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean done; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge h;       /* STATIC TO MINIMIZE STACK PROBLEMS */

  Est_Boolean Ex;
  Est_Boolean Ax;
  static Est_Boolean ExA;
  static Est_Boolean AxA;
  static Est_Boolean ExB;
  static Est_Boolean AxB;
  static Est_Boolean ExR;
  static Est_Boolean AxR;
  static Est_Boolean ExS;
  static Est_Boolean AxS;
  static Est_Boolean ExP;
  static Est_Boolean AxP;
  static Est_Boolean ExQ;
  static Est_Boolean AxQ;

  static Est_Boolean A2B;
  static Est_Boolean R2S;
  static Est_Boolean R2P;
  static Est_Boolean R2Q;
  static Est_Boolean S2R;
  static Est_Boolean S2P;
  static Est_Boolean S2Q;
  static Est_Boolean P2Q;
  static Est_Boolean P2R;
  static Est_Boolean Q2P;

  /* IF FIRST-TIME, PARSING FORMAT STRING */

  if (firsttime) {

    if (!BddisOK(f)) {
      fprintf(stderr,"ERROR (Bdd_RelOp): Bad f!\n");
      free((void *)1); /* BREAKPOINT FOR DEBUGGER */
      exit(1);
    }

    if (!BddisOK(g)) {
      fprintf(stderr,"ERROR (Bdd_RelOp): Bad g!\n");
      free((void *)1); /* BREAKPOINT FOR DEBUGGER */
      exit(1);
    }

    key = 0;                               /* 0 * 2^30 */
    op = oNULL;

    if (strstr(format,"#AND")) {
      key = 1073741824U;                   /* 1 * 2^30 */
      op = oAND;
    }

    if (strstr(format,"#OR")) {
      key = 2147483648U;                   /* 2 * 2^30 */
      op = oOR;
    }

    if (strstr(format,"#IMPL")) {
      key = 3221225472U;                   /* 3 * 2^30 */
      op = oIMPL;
    }

    Ex = (strstr(format,"Ex") != NULL);
    Ax = (strstr(format,"Ax") != NULL);

    if (Ex) {
      ExA = (strstr(format,"xA") != NULL);
      ExB = (strstr(format,"xB") != NULL);
      ExR = (strstr(format,"xR") != NULL);
      ExS = (strstr(format,"xS") != NULL);
      ExP = (strstr(format,"xP") != NULL);
      ExQ = (strstr(format,"xQ") != NULL);
    } else {
      ExA = FALSE;
      ExB = FALSE;
      ExR = FALSE;
      ExS = FALSE;
      ExP = FALSE;
      ExQ = FALSE;
    }

    if (Ax) {
      AxA = (strstr(format,"xA") != NULL);
      AxB = (strstr(format,"xB") != NULL);
      AxR = (strstr(format,"xR") != NULL);
      AxS = (strstr(format,"xS") != NULL);
      AxP = (strstr(format,"xP") != NULL);
      AxQ = (strstr(format,"xQ") != NULL);
    } else {
      AxA = FALSE;
      AxB = FALSE;
      AxR = FALSE;
      AxS = FALSE;
      AxP = FALSE;
      AxQ = FALSE;
    }

    A2B = (strstr(format,"A2B") != NULL);
    R2S = (strstr(format,"R2S") != NULL);
    R2P = (strstr(format,"R2P") != NULL);
    R2Q = (strstr(format,"R2Q") != NULL);
    S2R = (strstr(format,"S2R") != NULL);
    S2P = (strstr(format,"S2P") != NULL);
    S2Q = (strstr(format,"S2Q") != NULL);
    P2Q = (strstr(format,"P2Q") != NULL);
    P2R = (strstr(format,"P2R") != NULL);
    Q2P = (strstr(format,"Q2P") != NULL);

    if (ExA) key = key + 1;
    if (AxA) key = key + 2;
    if (ExB) key = key + 4;
    if (AxB) key = key + 8;
    if (ExR) key = key + 16;
    if (AxR) key = key + 32;
    if (ExS) key = key + 64;
    if (AxS) key = key + 128;
    if (ExP) key = key + 256;
    if (AxP) key = key + 512;
    if (ExQ) key = key + 1024;
    if (AxQ) key = key + 2048;

    if (A2B) key = key + 4096;
    if (R2S) key = key + 8192;
    if (R2P) key = key + 16384;
    if (R2Q) key = key + 32768;
    if (S2R) key = key + 65536;
    if (S2P) key = key + 131072;
    if (S2Q) key = key + 262144;
    if (P2Q) key = key + 524288;
    if (P2R) key = key + 1048576;
    if (Q2P) key = key + 2097152;

    h = Bdd_RelOp(f,g,format,FALSE);

  }

  if (!firsttime) {

    if (op == oNULL) {
      if (Bdd_isTerminal(f))
         return f;
    }

    if (op == oAND) {
      if (Bdd_isEqv(f, bdd_termFalse) || Bdd_isEqv(g, bdd_termFalse))
        return bdd_termFalse;
      if (Bdd_isEqv(f, bdd_termTrue) && Bdd_isEqv(g, bdd_termTrue))
        return bdd_termTrue;
    }

    if (op == oOR) {
      if (Bdd_isEqv(f, bdd_termTrue) || Bdd_isEqv(g, bdd_termTrue))
        return bdd_termTrue;
      if (Bdd_isEqv(f, bdd_termFalse) && Bdd_isEqv(g, bdd_termFalse))
        return bdd_termFalse;
    }

    if (op == oIMPL) {
      if (Bdd_isEqv(f, bdd_termFalse) || Bdd_isEqv(g, bdd_termTrue))
        return bdd_termTrue;
      if (Bdd_isEqv(f, bdd_termTrue) && Bdd_isEqv(g, bdd_termFalse))
        return bdd_termFalse;
    }

    /* IF COMUTATIVE OPERATION, DO SIMPLE NORMALIZATION */
    if ((op == oOR) || (op == oAND)) {
      if ((unsigned long) f.p > (unsigned long) g.p) BddExchange(&f, &g);
    }

    /* LOOKUP IN CACHE TABLE */

    bddRelOpCache.search++;
    p = &bddRelOpCache.table[(
                    (unsigned int) key +
                    ((unsigned long) g.p << 15) +
		    (unsigned long) f.p +
		    ((unsigned int) g.mark << 1) +
		    (unsigned int) f.mark
		    ) % bddRelOpCache.size];

    if ((p->key == key) &&
        Bdd_isEqv(p->f,f) &&
        Bdd_isEqv(p->g,g))
    {
      bddRelOpCache.find++;
      h = p->r;
      Bdd_Fresh(h);
      return h;
    }

    /* DETERMINING THE SUCCESSORS */

    if (op == oNULL) {
      f0 = Bdd_TransferMark(Bdd_GetElse(f), f.mark);
      f1 = Bdd_TransferMark(Bdd_GetThen(f), f.mark);
    } else {
      if (Bdd_GetVariableOrder(f) < Bdd_GetVariableOrder(g)) {
        f0 = Bdd_TransferMark(Bdd_GetElse(f), f.mark);
        f1 = Bdd_TransferMark(Bdd_GetThen(f), f.mark);
        g0 = g;
        g1 = g;
      } else if (Bdd_GetVariableOrder(f) > Bdd_GetVariableOrder(g)) {
        f0 = f;
        f1 = f;
        g0 = Bdd_TransferMark(Bdd_GetElse(g), g.mark);
        g1 = Bdd_TransferMark(Bdd_GetThen(g), g.mark);
      } else {
        f0 = Bdd_TransferMark(Bdd_GetElse(f), f.mark);
        f1 = Bdd_TransferMark(Bdd_GetThen(f), f.mark);
        g0 = Bdd_TransferMark(Bdd_GetElse(g), g.mark);
        g1 = Bdd_TransferMark(Bdd_GetThen(g), g.mark);
      }
    }

    /* DO RECURSIVE CALLS */

    if (op == oNULL) {
      h0 = Bdd_RelOp(f0, g, format, firsttime);
      h1 = Bdd_RelOp(f1, g, format, firsttime);
    } else {
      h0 = Bdd_RelOp(f0, g0, format, firsttime);
      h1 = Bdd_RelOp(f1, g1, format, firsttime);
    }

    /* DETERMINING THE SMALLEST TOP VARIABLE */
    if (op == oNULL) {

      /* z = Bdd_GetVariable(f); */
      zname = Bdd_GetVariableName(f);

    } else {

      if (Bdd_GetVariableOrder(f) > Bdd_GetVariableOrder(g)) {

        /* z = Bdd_GetVariable(g); */
        zname = Bdd_GetVariableName(g);

      } else {

        /* z = Bdd_GetVariable(f); */
        zname = Bdd_GetVariableName(f);
      }

    }

    /* COMPOSE PARTIAL RESULTS */
    switch (zname[0]) {

    case 'a':
    {
      done = FALSE;

      if (ExA) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxA) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (A2B) {
        v = strdup(zname);
        v[0] = 'b';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'b':
    {
      done = FALSE;

      if (ExB) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxB) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'r':
    {
      done = FALSE;

      if (ExR) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxR) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (R2S) {
        v = strdup(zname);
        v[0] = 's';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (R2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (R2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 's':
    {
      done = FALSE;

      if (ExS) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxS) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (S2R) {
        v = strdup(zname);
        v[0] = 'r';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (S2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (S2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'p':
    {
      done = FALSE;

      if (ExP) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxP) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (P2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (P2R) {
        v = strdup(zname);
        v[0] = 'r';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'q':
    {
      done = FALSE;

      if (ExQ) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxQ) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (Q2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    } /* switch zname[0] */

    /* STORE IN CACHE TABLE */

    if (p->key) bddRelOpCache.overwrite++;
    p->f = f;
    p->g = g;
    p->r = h;
    p->key = key;

  }

  return h;
}

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

Bdd_Edge
Bdd_RelOpSimple(Bdd_Edge f, Est_String format, Est_Boolean firsttime)
{
  static unsigned int key;

  BddRelOpSimpleCache *p;
  Bdd_Edge f0, f1, h0, h1;

  static Est_String zname; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String v;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean done; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge h;       /* STATIC TO MINIMIZE STACK PROBLEMS */

  Est_Boolean Ex;
  Est_Boolean Ax;
  static Est_Boolean ExA;
  static Est_Boolean AxA;
  static Est_Boolean ExB;
  static Est_Boolean AxB;
  static Est_Boolean ExR;
  static Est_Boolean AxR;
  static Est_Boolean ExS;
  static Est_Boolean AxS;
  static Est_Boolean ExP;
  static Est_Boolean AxP;
  static Est_Boolean ExQ;
  static Est_Boolean AxQ;

  static Est_Boolean A2B;
  static Est_Boolean R2S;
  static Est_Boolean R2P;
  static Est_Boolean R2Q;
  static Est_Boolean S2R;
  static Est_Boolean S2P;
  static Est_Boolean S2Q;
  static Est_Boolean P2Q;
  static Est_Boolean P2R;
  static Est_Boolean Q2P;

  if (Bdd_isTerminal(f)) return f;

  /* IF FIRST-TIME, PARSING FORMAT STRING */

  if (firsttime) {

    if (!BddisOK(f)) {
      fprintf(stderr,"ERROR (Bdd_RelOpSimple): Bad f!\n");
      free((void *)1); /* BREAKPOINT FOR DEBUGGER */
      exit(1);
    }

    key = 0;                               /* 0 * 2^30 */

    Ex = (strstr(format,"Ex") != NULL);
    Ax = (strstr(format,"Ax") != NULL);

    if (Ex) {
      ExA = (strstr(format,"xA") != NULL);
      ExB = (strstr(format,"xB") != NULL);
      ExR = (strstr(format,"xR") != NULL);
      ExS = (strstr(format,"xS") != NULL);
      ExP = (strstr(format,"xP") != NULL);
      ExQ = (strstr(format,"xQ") != NULL);
    } else {
      ExA = FALSE;
      ExB = FALSE;
      ExR = FALSE;
      ExS = FALSE;
      ExP = FALSE;
      ExQ = FALSE;
    }

    if (Ax) {
      AxA = (strstr(format,"xA") != NULL);
      AxB = (strstr(format,"xB") != NULL);
      AxR = (strstr(format,"xR") != NULL);
      AxS = (strstr(format,"xS") != NULL);
      AxP = (strstr(format,"xP") != NULL);
      AxQ = (strstr(format,"xQ") != NULL);
    } else {
      AxA = FALSE;
      AxB = FALSE;
      AxR = FALSE;
      AxS = FALSE;
      AxP = FALSE;
      AxQ = FALSE;
    }

    A2B = (strstr(format,"A2B") != NULL);
    R2S = (strstr(format,"R2S") != NULL);
    R2P = (strstr(format,"R2P") != NULL);
    R2Q = (strstr(format,"R2Q") != NULL);
    S2R = (strstr(format,"S2R") != NULL);
    S2P = (strstr(format,"S2P") != NULL);
    S2Q = (strstr(format,"S2Q") != NULL);
    P2Q = (strstr(format,"P2Q") != NULL);
    P2R = (strstr(format,"P2R") != NULL);
    Q2P = (strstr(format,"Q2P") != NULL);

    if (ExA) key = key + 1;
    if (AxA) key = key + 2;
    if (ExB) key = key + 4;
    if (AxB) key = key + 8;
    if (ExR) key = key + 16;
    if (AxR) key = key + 32;
    if (ExS) key = key + 64;
    if (AxS) key = key + 128;
    if (ExP) key = key + 256;
    if (AxP) key = key + 512;
    if (ExQ) key = key + 1024;
    if (AxQ) key = key + 2048;

    if (A2B) key = key + 4096;
    if (R2S) key = key + 8192;
    if (R2P) key = key + 16384;
    if (R2Q) key = key + 32768;
    if (S2R) key = key + 65536;
    if (S2P) key = key + 131072;
    if (S2Q) key = key + 262144;
    if (P2Q) key = key + 524288;
    if (P2R) key = key + 1048576;
    if (Q2P) key = key + 2097152;

    h = Bdd_RelOpSimple(f,format,FALSE);

  }

  if (!firsttime) {

    /* LOOKUP IN CACHE TABLE */

    bddRelOpSimpleCache.search++;
    p = &bddRelOpSimpleCache.table[(
                    (unsigned int) key +
		    (unsigned long) f.p +
		    (unsigned int) f.mark
		    ) % bddRelOpSimpleCache.size];

    if ((p->key == key) &&
        Bdd_isEqv(p->f,f))
    {
      bddRelOpSimpleCache.find++;
      h = p->r;
      Bdd_Fresh(h);
      return h;
    }

    /* DETERMINING THE SUCCESSORS */

    f0 = Bdd_TransferMark(Bdd_GetElse(f), f.mark);
    f1 = Bdd_TransferMark(Bdd_GetThen(f), f.mark);

    /* DO RECURSIVE CALLS */

    h0 = Bdd_RelOpSimple(f0, format, firsttime);
    h1 = Bdd_RelOpSimple(f1, format, firsttime);

    /* DETERMINING TOP VARIABLE */

    /* z = Bdd_GetVariable(f); */
    zname = Bdd_GetVariableName(f);

    /* COMPOSE PARTIAL RESULTS */
    switch (zname[0]) {

    case 'a':
    {
      done = FALSE;

      if (ExA) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxA) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (A2B) {
        v = strdup(zname);
        v[0] = 'b';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'b':
    {
      done = FALSE;

      if (ExB) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxB) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'r':
    {
      done = FALSE;

      if (ExR) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxR) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (R2S) {
        v = strdup(zname);
        v[0] = 's';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (R2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (R2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 's':
    {
      done = FALSE;

      if (ExS) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxS) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (S2R) {
        v = strdup(zname);
        v[0] = 'r';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (S2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (S2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'p':
    {
      done = FALSE;

      if (ExP) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxP) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (P2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (P2R) {
        v = strdup(zname);
        v[0] = 'r';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    case 'q':
    {
      done = FALSE;

      if (ExQ) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxQ) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (Q2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

      break;
    }

    } /* switch zname[0] */

    /* STORE IN CACHE TABLE */

    if (p->key) bddRelOpSimpleCache.overwrite++;
    p->f = f;
    p->r = h;
    p->key = key;

  }

  return h;
}

/**Function****************************************************************
  Synopsis    []
  Description [Ex, Ax, R2S, and S2R can have a process specified.
               Symbol * means all processes.
               Symbol ^ means all other processes.
               Examples: "Ex xR<%s>", "S2R^<%s><%s>" ]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_RelOpComplex(Bdd_Edge f, Est_String format, Est_Boolean firsttime)
{
  static unsigned int key;

  BddRelOpComplexCache *p;
  Bdd_Edge f0, f1, h0, h1;

  static int n;            /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String t;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String zname; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String pname; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String v;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean done; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge h;       /* STATIC TO MINIMIZE STACK PROBLEMS */

  Est_Boolean Ex;
  Est_Boolean Ax;
  static Est_Boolean ExA;
  static Est_Boolean AxA;
  static Est_String ExR;
  static Est_String AxR;
  static Est_String ExS;
  static Est_String AxS;
  static Est_String ExP;
  static Est_String AxP;
  static Est_String ExQ;
  static Est_String AxQ;

  static Est_String R2S;
  static Est_String S2R;

  static Est_Boolean R2P;
  static Est_Boolean R2Q;
  static Est_Boolean S2P;
  static Est_Boolean S2Q;
  static Est_Boolean P2Q;
  static Est_Boolean Q2P;

  if (Bdd_isTerminal(f)) return f;

  /* IF FIRSTIME, PARSING FORMAT STRING */

  if (firsttime) {

    if (!BddisOK(f)) {
      fprintf(stderr,"ERROR (Bdd_RelOpComplex): Bad f!\n");
      free((void *)1); /* BREAKPOINT FOR DEBUGGER */
      exit(1);
    }

    key = 0;                              /* 0 * 2^30 */

    Ex = (strstr(format,"Ex") != NULL);
    Ax = (strstr(format,"Ax") != NULL);

    if (Ex) {

      ExA = (strstr(format,"xA") != NULL);

      if ((t = strstr(format,"xR"))) {
        n = strcspn(&t[2]," ");
        if (!(ExR = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(ExR,&t[2],n);
        ExR[n] = 0;

	/*
        ExR = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        ExR = NULL;
      }

      if ((t = strstr(format,"xS"))) {
        n = strcspn(&t[2]," ");
        if (!(ExS = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(ExS,&t[2],n);
        ExS[n] = 0;

	/*
        ExS = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        ExS = NULL;
      }

      if ((t = strstr(format,"xP"))) {
        n = strcspn(&t[2]," ");
        if (!(ExP = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(ExP,&t[2],n);
        ExP[n] = 0;

	/*
        ExP = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        ExP = NULL;
      }

      if ((t = strstr(format,"xQ"))) {
        n = strcspn(&t[2]," ");
        if (!(ExQ = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(ExQ,&t[2],n);
        ExQ[n] = 0;

	/*
        ExQ = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        ExQ = NULL;
      }

    } else {
      ExA = FALSE;
      ExR = NULL;
      ExS = NULL;
      ExP = NULL;
      ExQ = NULL;
    }

    if (Ax) {
      AxA = (strstr(format,"xA") != NULL);

      if ((t = strstr(format,"xR"))) {
        n = strcspn(&t[2]," ");
        if (!(AxR = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(AxR,&t[2],n);
        AxR[n] = 0;

	/*
        AxR = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        AxR = NULL;
      }

      if ((t = strstr(format,"xS"))) {
        n = strcspn(&t[2]," ");
        if (!(AxS = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(AxS,&t[2],n);
        AxS[n] = 0;

	/*
        AxS = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        AxS = NULL;
      }

      if ((t = strstr(format,"xP"))) {
        n = strcspn(&t[2]," ");
        if (!(AxP = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(AxP,&t[2],n);
        AxP[n] = 0;

	/*
        AxP = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        AxP = NULL;
      }

      if ((t = strstr(format,"xQ"))) {
        n = strcspn(&t[2]," ");
        if (!(AxQ = (Est_String) malloc(n+1))) {
          fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
          exit(1);
        }
        memcpy(AxQ,&t[2],n);
        AxQ[n] = 0;

	/*
        AxQ = (Est_String) strtok(strdup(&t[2]), " ");
	*/
      } else {
        AxQ = NULL;
      }

    } else {
      AxA = FALSE;
      AxR = NULL;
      AxS = NULL;
      AxP = NULL;
      AxQ = NULL;
    }

    if ((t = strstr(format,"R2S"))) {
      n = strcspn(&t[3]," ");
      if (!(R2S = (Est_String) malloc(n+1))) {
        fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
        exit(1);
      }
      memcpy(R2S,&t[3],n);
      R2S[n] = 0;
    } else {
      R2S = NULL;
    }

    if ((t = strstr(format,"S2R"))) {
      n = strcspn(&t[3]," ");
      if (!(S2R = (Est_String) malloc(n+1))) {
        fprintf(stderr,"Bdd_RelOpComplex: Out of memory!\n");
        exit(1);
      }
      memcpy(S2R,&t[3],n);
      S2R[n] = 0;

    } else {
      S2R = NULL;
    }

    R2P = (strstr(format,"R2P") != NULL);
    R2Q = (strstr(format,"R2Q") != NULL);
    S2P = (strstr(format,"S2P") != NULL);
    S2Q = (strstr(format,"S2Q") != NULL);
    P2Q = (strstr(format,"P2Q") != NULL);
    Q2P = (strstr(format,"Q2P") != NULL);

    if (ExA) key = key + 1;
    if (AxA) key = key + 2;
    if (ExR) key = key + 4;
    if (AxR) key = key + 8;
    if (ExS) key = key + 16;
    if (AxS) key = key + 32;
    if (ExP) key = key + 64;
    if (AxP) key = key + 128;
    if (ExQ) key = key + 256;
    if (AxQ) key = key + 512;

    if (R2S) key = key + 1024;
    if (R2P) key = key + 2048;
    if (R2Q) key = key + 4096;
    if (S2R) key = key + 8192;
    if (S2P) key = key + 16384;
    if (S2Q) key = key + 32768;
    if (P2Q) key = key + 65536;
    if (Q2P) key = key + 131072;

    if (ExR && (ExR[0]=='*')) {
      key = key + 4194304;
    }

    if (AxR && (AxR[0]=='*')) {
      key = key + 4194304;
    }

    if (ExS && (ExS[0]=='*')) {
      key = key + 8388608;
    }

    if (AxS && (AxS[0]=='*')) {
      key = key + 8388608;
    }

    if (ExP && (ExP[0]=='*')) {
      key = key + 16777216;
    }

    if (AxP && (AxP[0]=='*')) {
      key = key + 16777216;
    }

    if (ExQ && (ExQ[0]=='*')) {
      key = key + 33554432;
    }

    if (AxQ && (AxQ[0]=='*')) {
      key = key + 33554432;
    }

    h = Bdd_RelOpComplex(f,format,FALSE);

    if (ExR) free(ExR);
    if (AxR) free(AxR);
    if (ExS) free(ExS);
    if (AxS) free(AxS);
    if (ExP) free(ExP);
    if (AxP) free(AxP);
    if (ExQ) free(ExQ);
    if (AxQ) free(AxQ);
  }

  if (!firsttime) {

    /* LOOKUP IN CACHE TABLE */

    bddRelOpComplexCache.search++;
    p = &bddRelOpComplexCache.table[(
                    (unsigned int) key +
		    (unsigned long) f.p +
		    (unsigned int) f.mark
		    ) % bddRelOpComplexCache.size];

    if ((p->key == key) &&
        Bdd_isEqv(p->f,f) &&
        !strcmp(p->name,format))
    {
      bddRelOpComplexCache.find++;
      h = p->r;
      Bdd_Fresh(h);
      return h;
    }

    /* DETERMINING THE SUCCESSORS */

    f0 = Bdd_TransferMark(Bdd_GetElse(f), f.mark);
    f1 = Bdd_TransferMark(Bdd_GetThen(f), f.mark);

    /* DO RECURSIVE CALLS */

    h0 = Bdd_RelOpComplex(f0, format, firsttime);
    h1 = Bdd_RelOpComplex(f1, format, firsttime);

    /* DETERMINING TOP VARIABLE */

    /* z = Bdd_GetVariable(f); */
    zname = Bdd_GetVariableName(f);

    /* FIND OUT THE NAME OF THE PROCESS */

    if (zname[0] != 'a') {
      pname = &zname[1+strspn(&zname[1],"0123456789")];
    }

    /* COMPOSE PARTIAL RESULTS */

    if (zname[0] == 'a') {
      done = FALSE;

      if (ExA) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxA) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

    } /* zname[0] == 'a' */

    if (zname[0] == 'r') {
      done = FALSE;

      if (ExR && ((ExR[0]=='*') || (ExR[0]!='^' && strstr(ExR,pname)) || (ExR[0]=='^' && !strstr(ExR,pname)))) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxR && ((AxR[0]=='*') || (AxR[0]!='^' && strstr(AxR,pname)) || (AxR[0]=='^' && !strstr(AxR,pname)))) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (R2S && ((R2S[0]=='*') || (R2S[0]!='^' && strstr(R2S,pname)) || (R2S[0]=='^' && !strstr(R2S,pname)))) {
        v = strdup(zname);
        v[0] = 's';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (R2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (R2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

    } /* zname[0] == 'r' */

    if (zname[0] == 's') {
      done = FALSE;

      if (ExS && ((ExS[0]=='*') || (ExS[0]!='^' && strstr(ExS,pname)) || (ExS[0]=='^' && !strstr(ExS,pname)))) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxS && ((AxS[0]=='*') || (AxS[0]!='^' && strstr(AxS,pname)) || (AxS[0]=='^' && !strstr(AxS,pname)))) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (S2R && ((S2R[0]=='*') || (S2R[0]!='^' && strstr(S2R,pname)) || (S2R[0]=='^' && !strstr(S2R,pname)))) {
        v = strdup(zname);
        v[0] = 'r';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (S2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (S2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

    } /* zname[0] == 's' */

    if (zname[0] == 'p') {
      done = FALSE;

      if (ExP && ((ExP[0]=='*') || (ExP[0]!='^' && strstr(ExP,pname)) || (ExP[0]=='^' && !strstr(ExP,pname)))) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxP && ((AxP[0]=='*') || (AxP[0]!='^' && strstr(AxP,pname)) || (AxP[0]=='^' && !strstr(AxP,pname)))) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (P2Q) {
        v = strdup(zname);
        v[0] = 'q';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

    } /* zname[0] == 'p' */

    if (zname[0] == 'q') {
      done = FALSE;

      if (ExQ && ((ExQ[0]=='*') || (ExQ[0]!='^' && strstr(ExQ,pname)) || (ExQ[0]=='^' && !strstr(ExQ,pname)))) {
        h = Bdd_ITE(h0, bdd_termTrue, h1);
        done = TRUE;
      }

      if (AxQ && ((AxQ[0]=='*') || (AxQ[0]!='^' && strstr(AxQ,pname)) || (AxQ[0]=='^' && !strstr(AxQ,pname)))) {
        h = Bdd_ITE(h0, h1, bdd_termFalse);
        done = TRUE;
      }

      if (Q2P) {
        v = strdup(zname);
        v[0] = 'p';
        h = Bdd_ITE(Bdd_FoaTerminal(v), h1, h0);
        free(v);
        done = TRUE;
      }

      if (!done) {
        h = Bdd_ITE(Bdd_FoaTerminal(zname), h1, h0);
      }

    } /* zname[0] == 'q' */


    /* STORE IN CACHE TABLE */

    if (p->key) {
      bddRelOpComplexCache.overwrite++;
      free(p->name);
    }
    p->f = f;
    p->r = h;
    p->key = key;
    p->name = strdup(format);

  }

  return h;
}

/**Function****************************************************************
  Synopsis    [NewState]
  Description ['s' variables replaces with 'r'. Performs existential
               quantification over all other variables.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_NewState(Bdd_Edge f)
{
  return Bdd_RelOpSimple(f,"Ex xR xA xP xQ S2R",TRUE);
}

/**Function****************************************************************
  Synopsis    [NewState1]
  Description ['s' variables replaces with 'r'.
               Performs existential quatification over 'r' variables
               of the given process and existential quatification over
               other variables.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_NewState1(Bdd_Edge f, Est_String name)
{
  Est_String s;
  Bdd_Edge r;

  s = (Est_String) malloc(255);
  sprintf(s,"Ex xA xR<%s> xP* xQ* S2R*",name);
  r = Bdd_RelOpComplex(f,s,TRUE);
  free(s);
  return r;
}

/**Function****************************************************************
  Synopsis    []
  Description ['s' variables replaces with 'r'.
               Performs existential quantification over 'r' variables
               of the given two processes and existential quantification
               over other variables.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_NewState2(Bdd_Edge f, Est_String name1, Est_String name2)
{
  Est_String s;
  Bdd_Edge r;

  s = (Est_String) malloc(255);
  sprintf(s,"Ex xA xR<%s><%s> xP* xQ* S2R*",name1,name2);
  r = Bdd_RelOpComplex(f,s,TRUE);
  free(s);
  return r;
}

/**Function****************************************************************
  Synopsis    []
  Description [Calculate f->g. Performs universal quantification over
               'a', 's' and 'q'.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Bdd_NewEq(Bdd_Edge f, Bdd_Edge g)
{
  return Bdd_RelOp(f,g,"#IMPL Ax xA xS xQ",TRUE);
}

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

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