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

  FileName    [bddMain.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File bddMain.c contains main functions for
               representation and manipulation of boolean functions
               with ROBDDs.]
  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 <biddy.h>
#include "bddInt.h"

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

#define SMALL_RELOP_CACHE  1009
#define MEDIUM_RELOP_CACHE 10007
#define BIG_RELOP_CACHE    100043
#define HUGE_RELOP_CACHE   500057

/*-----------------------------------------------------------------------*/
/* Macro definitions                                                     */
/*-----------------------------------------------------------------------*/

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

/* EXPORTED VARIABLES */

int bdd_status = 0;                             /* initialization status */

Bdd_Edge bdd_termTrue = {NULL,FALSE};                   /* terminal node */
Bdd_Edge bdd_termFalse = {NULL,FALSE};                  /* terminal node */
Bdd_Edge bdd_termNull = {NULL,FALSE};                       /* null edge */

/* INTERNAL VARIABLES */

unsigned int bddRelOpCacheSize = HUGE_RELOP_CACHE;
unsigned int bddRelOpSimpleCacheSize = BIG_RELOP_CACHE;
unsigned int bddRelOpComplexCacheSize = BIG_RELOP_CACHE;

BddFormula *bddFormulaeTree = NULL;                     /* formulae Tree */
BddRelOpCacheTable bddRelOpCache
                   = {NULL,0,0,0,0,0};                     /* user cache */
BddRelOpSimpleCacheTable bddRelOpSimpleCache
                         = {NULL,0,0,0,0,0};               /* user cache */
BddRelOpComplexCacheTable bddRelOpComplexCache
                          = {NULL,0,0,0,0,0};              /* user cache */

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

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

static void RelOpGarbage();

static void RelOpSimpleGarbage();

static void RelOpComplexGarbage();

static void deleteFormulaeTree(BddFormula *f);

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

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

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

/* To simplify building on MS WINDOWS - Bdd_Init is stated in *.def file */

#ifndef TCLOUT
   void Bdd_Init(void) {}
#endif

/**Function****************************************************************
  Synopsis    [Bdd_GetThen]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_GetThen]
  CUDD        [Cudd_T]
  ************************************************************************/

Bdd_Edge Bdd_GetThen(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff,rr;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_GetThen(ff);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_GetThen((Biddy_Edge) f.p);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

  /* CUDD ?? NOT TESTED */
  /*
  Bdd_Edge r;
  r.p = (void *) Cudd_T((DdNode) f.p);
  r.mark = Cudd_IsComplement((DdNode) r.p);
  return r;
  */

}

/**Function****************************************************************
  Synopsis    [Bdd_GetElse]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_GetElse]
  CUDD        [Cudd_E]
  ************************************************************************/

Bdd_Edge Bdd_GetElse(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff,rr;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_GetElse(ff);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_GetElse((Biddy_Edge) f.p);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

  /* CUDD ?? NOT TESTED */
  /*
  Bdd_Edge r;
  r.p = (void *) Cudd_E((DdNode) f.p);
  r.mark = Cudd_IsComplement((DdNode) r.p);
  return r;
  */

}

/**Function****************************************************************
  Synopsis    [Bdd_GetVariable]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_GetVariable]
  CUDD        [-]
  ************************************************************************/

Bdd_Variable Bdd_GetVariable(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return (Bdd_Variable) Biddy_GetVariable(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return (Bdd_Variable) Biddy_GetVariable((Biddy_Edge) f.p);
  /**/

  /* CUDD ?? NOT TESTED */
  /*
  return (Bdd_Variable) (Cudd_Regular((DdNode) r.p))->index;
  */

}

/**Function****************************************************************
  Synopsis    [Bdd_GetVariableName]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       []
  CUDD        []
  ************************************************************************/

Est_String Bdd_GetVariableName(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return (Est_String) Biddy_GetVariableName(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return (Est_String) Biddy_GetVariableName((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_GetVariableChar]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       []
  CUDD        []
  ************************************************************************/

char Bdd_GetVariableChar(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return Biddy_GetVariableChar(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return Biddy_GetVariableChar((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_GetIthVariableName]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       []
  CUDD        []
  ************************************************************************/

Est_String Bdd_GetIthVariableName(int i)
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return (Est_String) Biddy_GetIthVariableName(i);
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_GetVariableOrder]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       []
  CUDD        []
  ************************************************************************/

int Bdd_GetVariableOrder(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return Biddy_GetVariableOrder(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return Biddy_GetVariableOrder((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_FoaTerminal]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_FoaTerminal]
  CUDD        []
  ************************************************************************/

Bdd_Edge Bdd_FoaTerminal(Est_String x)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr;
  Bdd_Edge r;
  rr = Biddy_FoaTerminal((Biddy_String) x);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_FoaTerminal((Biddy_String) x);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_NOT]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NOT]
  CUDD        [Cudd_Not]
  ************************************************************************/

Bdd_Edge Bdd_NOT(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_NOT(ff);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_NOT((Biddy_Edge) f.p);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_TransferMark]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_TransferMark]
  CUDD        [Cudd_NotCond]
  ************************************************************************/

Bdd_Edge Bdd_TransferMark(Bdd_Edge f, Est_Boolean mark)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_TransferMark(ff, (Biddy_Boolean) mark);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_TransferMark((Biddy_Edge) f.p, (Biddy_Boolean) mark);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_ITE]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_ITE]
  CUDD        []
  ************************************************************************/

Bdd_Edge Bdd_ITE(Bdd_Edge f, Bdd_Edge g, Bdd_Edge h)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff,gg,hh;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  gg.p = g.p;
  gg.mark = g.mark;
  hh.p = h.p;
  hh.mark = h.mark;
  rr = Biddy_ITE(ff,gg,hh);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_ITE((Biddy_Edge) f.p, (Biddy_Edge) g.p, (Biddy_Edge) h.p);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_Restrict]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_Restrict]
  CUDD        []
  ************************************************************************/

Bdd_Edge Bdd_Restrict(Bdd_Edge f, Bdd_Variable v, Est_Boolean value)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_Restrict(ff, (Biddy_Variable) v, (Biddy_Boolean) value);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_Restrict((Biddy_Edge) f.p, (Biddy_Variable) v, (Biddy_Boolean) value);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_Compose]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_Compose]
  CUDD        []
  ************************************************************************/

Bdd_Edge Bdd_Compose(Bdd_Edge f, Bdd_Variable v, Bdd_Edge g)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff,gg;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  gg.p = g.p;
  gg.mark = g.mark;
  rr = Biddy_Compose(ff, (Biddy_Variable) v, gg);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_Compose((Biddy_Edge) f.p, (Biddy_Variable) v, (Biddy_Edge) g.p);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_E]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_E]
  CUDD        []
  ************************************************************************/

Bdd_Edge Bdd_E(Bdd_Edge f, Bdd_Variable v)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_E(ff, (Biddy_Variable) v);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_E((Biddy_Edge) f.p, (Biddy_Variable) v);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_A]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_A]
  CUDD        []
  ************************************************************************/

Bdd_Edge Bdd_A(Bdd_Edge f, Bdd_Variable v)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,ff;
  Bdd_Edge r;
  ff.p = f.p;
  ff.mark = f.mark;
  rr = Biddy_A(ff, (Biddy_Variable) v)
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_A((Biddy_Edge) f.p, (Biddy_Variable) v);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_IncCounter]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_IncCounter]
  CUDD        []
  ************************************************************************/

void Bdd_IncCounter()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  Biddy_IncCounter();
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_Fresh]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_Fresh]
  CUDD        []
  ************************************************************************/

void Bdd_Fresh(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark
  Biddy_Fresh(ff);
  */

  /* BIDDY 1.1 */
  /**/
  Biddy_Fresh((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_Fortify]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_Fortify]
  CUDD        []
  ************************************************************************/

void Bdd_Fortify(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  Biddy_Fortify(ff);
  */

  /* BIDDY 1.1 */
  /**/
  Biddy_Fortify((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [Bdd_Garbage]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_Garbage]
  CUDD        []
  ************************************************************************/

void Bdd_Garbage()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  Biddy_Garbage();
  /**/

}

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

void
Bdd_InitPkg()
{
    int i;

    if (bdd_status == 1) {
      printf("\nBDD package is already initialized. ");
      return;
    } else {
      bdd_status = 1;
    }

    Biddy_Init();

    /* INITIALIZATION OF TERMINAL EDGES */
    bdd_termTrue.p = (void *) biddy_termTrue;
    bdd_termTrue.mark = Biddy_GetMark(biddy_termTrue);
    bdd_termFalse.p = (void *) biddy_termFalse;
    bdd_termFalse.mark = Biddy_GetMark(biddy_termFalse);
    bdd_termNull.p = (void *) biddy_termNull;
    bdd_termNull.mark = Biddy_GetMark(biddy_termNull);

    /* INITIALIZATION OF FORMULAE TREE */
    bddFormulaeTree = NULL;
    Bdd_AddFormula("1",bdd_termTrue);
    Bdd_AddFormula("0",bdd_termFalse);

    /* INITIALIZATION OF RelOp CACHE - USED FOR RELATIONAL OPERATIONS */
    bddRelOpCache.size = bddRelOpCacheSize;
    bddRelOpCache.search = 0;
    bddRelOpCache.find = 0;
    bddRelOpCache.write = 0;
    bddRelOpCache.overwrite = 0;
    if (!(bddRelOpCache.table = (BddRelOpCache *)
          malloc(bddRelOpCache.size * sizeof(BddRelOpCache)))) {
      fprintf(stdout,"Bdd_InitPkg (RelOp): Out of memoy!\n");
      exit(1);
    }
    for (i=0;i<bddRelOpCache.size;i++) {
      bddRelOpCache.table[i].key = 0;
    }
    BddAddCache(RelOpGarbage);

    /* INITIALIZATION OF RelOpSimple CACHE - SIMPLIFIED RELATIONAL OPERATIONS */
    bddRelOpSimpleCache.size = bddRelOpSimpleCacheSize;
    bddRelOpSimpleCache.search = 0;
    bddRelOpSimpleCache.find = 0;
    bddRelOpSimpleCache.write = 0;
    bddRelOpSimpleCache.overwrite = 0;
    if (!(bddRelOpSimpleCache.table = (BddRelOpSimpleCache *)
          malloc(bddRelOpSimpleCache.size * sizeof(BddRelOpSimpleCache)))) {
      fprintf(stdout,"Bdd_InitPkg (RelOpSimple): Out of memoy!\n");
      exit(1);
    }
    for (i=0;i<bddRelOpSimpleCache.size;i++) {
      bddRelOpSimpleCache.table[i].key = 0;
    }
    BddAddCache(RelOpSimpleGarbage);

    /* INITIALIZATION OF RelOpComplex CACHE - ADVANCED RELATIONAL OPERAT. */
    bddRelOpComplexCache.size = bddRelOpComplexCacheSize;
    bddRelOpCache.search = 0;;
    bddRelOpComplexCache.search = 0;
    bddRelOpComplexCache.find = 0;
    bddRelOpComplexCache.write = 0;
    bddRelOpComplexCache.overwrite = 0;
    if (!(bddRelOpComplexCache.table = (BddRelOpComplexCache *)
          malloc(bddRelOpComplexCache.size * sizeof(BddRelOpComplexCache)))) {
      fprintf(stdout,"Bdd_InitPkg (RelOpComplex): Out of memoy!\n");
      exit(1);
    }
    for (i=0;i<bddRelOpComplexCache.size;i++) {
      bddRelOpComplexCache.table[i].key = 0;
    }
    BddAddCache(RelOpComplexGarbage);

}

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

void
Bdd_ExitPkg()
{
  int i;

  if (bdd_status == 0) {
    printf("\nBDD package is not initialized. ");
    return;
  } else {
    bdd_status = 0;
  }

  Biddy_Exit();

  /* DELETE FORMULAE TREE */
  /*
  printf("Delete formulae tree...\n");
  */
  deleteFormulaeTree(bddFormulaeTree);

  /* DELETE RelOp CACHE TABLE */
  /*
  printf("Delete RelOp cache...\n");
  */
  free(bddRelOpCache.table);

  /* DELETE RelOpSimple CACHE TABLE */
  /*
  printf("Delete RelOpSimple cache...\n");
  */
  free(bddRelOpSimpleCache.table);

  /* DELETE RelOpComplex CACHE TABLE */
  /*
  printf("Delete RelOpComplex cache...\n");
  */
  for (i=0; i<bddRelOpComplexCache.size; i++) {
    if (bddRelOpComplexCache.table[i].key) {
      free(bddRelOpComplexCache.table[i].name);
    }
  }
  free(bddRelOpComplexCache.table);

}

/**Function****************************************************************
  Synopsis    []
  Description [Bdd_AboutPkg reports type and version of BDD package.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Bdd_AboutPkg()
{
  printf("EST ");
  printf(EDITION);
  printf(", version ");
  printf(VERSION);
  printf(", ");
  printf("Bdd package");
  printf("\n");

  Biddy_About();
}

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

/**Function****************************************************************
  Synopsis    [BddisOK]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_isOK]
  CUDD        []
  ************************************************************************/

Est_Boolean BddisOK(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return (Est_Boolean) Biddy_isOK(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return (Est_Boolean) Biddy_isOK((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddSelectNode]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_SelectNode]
  CUDD        []
  ************************************************************************/

void BddSelectNode(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  Biddy_SelectNode(ff);
  */

  /* BIDDY 1.1 */
  /**/
  Biddy_SelectNode((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddDeselectNode]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_DeselectNode]
  CUDD        []
  ************************************************************************/

void BddDeselectNode(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  Biddy_DeselectNode(ff);
  */

  /* BIDDY 1.1 */
  /**/
  Biddy_DeselectNode((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddisSelected]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_isSelected]
  CUDD        []
  ************************************************************************/

Est_Boolean BddisSelected(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff
  ff.p = f.p;
  ff.mark = f.mark;
  return (Est_Boolean) Biddy_isSelected(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return (Est_Boolean) Biddy_isSelected((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeSelect]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeSelect]
  CUDD        []
  ************************************************************************/

void BddNodeSelect(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff
  ff.p = f.p;
  ff.mark = f.mark;
  Biddy_NodeSelect(ff);
  */

  /* BIDDY 1.1 */
  /**/
  Biddy_NodeSelect((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeRepair]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeRepair]
  CUDD        []
  ************************************************************************/

void BddNodeRepair(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  Biddy_NodeRepair(ff);
  */

  /* BIDDY 1.1 */
  /**/
  Biddy_NodeRepair((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddFindTerminal]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_FindTerminal]
  CUDD        []
  ************************************************************************/

Bdd_Edge BddFindTerminal(Est_String x)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr;
  Bdd_Edge r;
  rr = Biddy_FindTerminal((Biddy_String) x);
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_FindTerminal((Biddy_String) x);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [BddFoaNode]
  Description []
  SideEffects [Using BddFoaNode you can create node with bad ordering.
               It is much more safe to use Bdd_ITE!]
  SeeAlso     []
  Biddy       [Biddy_FoaNode]
  CUDD        [cuddUniqueInter]
  ************************************************************************/

Bdd_Edge BddFoaNode(Bdd_Variable v, Bdd_Edge pf, Bdd_Edge pt)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge rr,pff,ptt;
  Bdd_Edge r;
  pff.p = pf.p;
  pff.mark = pf.mark;
  ptt.p = pt.p;
  ptt.mark = pt.mark;
  rr = Biddy_FoaNode((Biddy_Variable) v, pff, ptt)
  r.p = rr.p;
  r.mark = rr.mark;
  return r;
  */

  /* BIDDY 1.1 */
  /**/
  Bdd_Edge r;
  r.p = (void *) Biddy_FoaNode((Biddy_Variable) v, (Biddy_Edge) pf.p, (Biddy_Edge) pt.p);
  r.mark = Biddy_GetMark((Biddy_Edge) r.p);
  return r;
  /**/

}

/**Function****************************************************************
  Synopsis    [BddAddCache]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_AddCache]
  CUDD        []
  ************************************************************************/

void BddAddCache(Bdd_UserFunction gc)
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  Biddy_AddCache((Biddy_UserFunction) gc);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableSize]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableSize]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableSize()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableSize();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableMax]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableMax]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableMax()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableMax();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableNum]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableNum]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableNum()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableNum();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableNumF]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableNumF]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableNumF()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableNumF();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableFOA]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableFOA]
  CUDD        []
  ************************************************************************/

unsigned long int BddNodeTableFOA()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableFOA();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableCompare]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableCompare]
  CUDD        []
  ************************************************************************/

unsigned long int BddNodeTableCompare()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableCompare();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableAdd]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableAdd]
  CUDD        []
  ************************************************************************/

unsigned long int BddNodeTableAdd()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableAdd();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableGarbage]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableGarbage]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableGarbage()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableGarbage();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableGenerated]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableGenerated]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableGenerated()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableGenerated();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeTableBlockNumber]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeTableBlockNumber]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeTableBlockNumber()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_NodeTableBlockNumber();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddListUsed]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_ListUsed]
  CUDD        []
  ************************************************************************/

unsigned int BddListUsed()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_ListUsed();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddListMaxLength]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_ListMaxLength]
  CUDD        []
  ************************************************************************/

unsigned int BddListMaxLength()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_ListMaxLength();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddListAvgLength]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_ListAvgLength]
  CUDD        []
  ************************************************************************/

float BddListAvgLength()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_ListAvgLength();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddIteCacheFind]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_IteCacheFind]
  CUDD        []
  ************************************************************************/

unsigned long int BddIteCacheFind()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_IteCacheFind();
  /**/

}

/**Function****************************************************************
  Synopsis    [BddIteCacheOverwrite]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_IteCacheOverwrite]
  CUDD        []
  ************************************************************************/

unsigned long int BddIteCacheOverwrite()
{

  /* BIDDY 1.0, BIDDY 1.1 */
  /**/
  return Biddy_IteCacheOverwrite();
  /**/

}

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

unsigned long int BddRelopCacheFind()
{
  return bddRelOpCache.find;
}

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

unsigned long int BddRelopCacheOverwrite()
{
  return bddRelOpCache.overwrite;
}

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

unsigned long int BddRelopSimpleCacheFind()
{
  return bddRelOpSimpleCache.find;
}

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

unsigned long int BddRelopSimpleCacheOverwrite()
{
  return bddRelOpSimpleCache.overwrite;
}

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

unsigned long int BddRelopComplexCacheFind()
{
  return bddRelOpComplexCache.find;
}

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

unsigned long int BddRelopComplexCacheOverwrite()
{
  return bddRelOpComplexCache.overwrite;
}

/**Function****************************************************************
  Synopsis    [BddNodeNumber]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeNumber]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeNumber(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return Biddy_NodeNumber(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return Biddy_NodeNumber((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeMaxLevel]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeMaxLevel]
  CUDD        []
  ************************************************************************/

unsigned int BddNodeMaxLevel(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return Biddy_NodeMaxLevel(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return Biddy_NodeMaxLevel((Biddy_Edge) f.p);
  /**/

}

/**Function****************************************************************
  Synopsis    [BddNodeAvgLevel]
  Description []
  SideEffects []
  SeeAlso     []
  Biddy       [Biddy_NodeAvgLevel]
  CUDD        []
  ************************************************************************/

float BddNodeAvgLevel(Bdd_Edge f)
{

  /* BIDDY 1.0 */
  /*
  Biddy_Edge ff;
  ff.p = f.p;
  ff.mark = f.mark;
  return Biddy_NodeAvgLevel(ff);
  */

  /* BIDDY 1.1 */
  /**/
  return Biddy_NodeAvgLevel((Biddy_Edge) f.p);
  /**/

}

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

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

static void
RelOpGarbage()
{
  int i;
  BddRelOpCache *p;

  for (i=0; i<bddRelOpCache.size; i++) {
    if (bddRelOpCache.table[i].key) {
      p = &bddRelOpCache.table[i];
      if (!BddisOK(p->f) || !BddisOK(p->g) || !BddisOK(p->r))
      {
        p->key = 0;
      }
    }
  }
}

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

static void
RelOpSimpleGarbage()
{
  int i;
  BddRelOpSimpleCache *p;

  for (i=0; i<bddRelOpSimpleCache.size; i++) {
    if (bddRelOpSimpleCache.table[i].key) {
      p = &bddRelOpSimpleCache.table[i];
      if (!BddisOK(p->f) || !BddisOK(p->r))
      {
        p->key = 0;
      }
    }
  }
}

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

static void
RelOpComplexGarbage()
{
  int i;
  BddRelOpComplexCache *p;

  for (i=0; i<bddRelOpComplexCache.size; i++) {
    if (bddRelOpComplexCache.table[i].key) {
      p = &bddRelOpComplexCache.table[i];
      if (!BddisOK(p->f) || !BddisOK(p->r))
      {
        free(p->name);
        p->key = 0;
      }
    }
  }
}

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

static void
deleteFormulaeTree(BddFormula *f)
{
  if (f != NULL) {
    deleteFormulaeTree(f->l);
    deleteFormulaeTree(f->r);
    free(f->name);
    free(f);
  }
}
