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

  FileName    [bddInt.h]
  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 bddInt.h contains declaration of internal
               data structures.]
  SeeAlso     [bdd.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.]
  ************************************************************************/

#ifndef _BDDINT
#define _BDDINT

#include "bdd.h"

#ifdef TCLOUT
#  include <gui.h>
#  define printf Gui_Printf
#  ifdef USE_GUI_STUBS
#    include <guiDecls.h>
#  endif
#endif

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

/*-----------------------------------------------------------------------*/
/* Structure declarations                                                */
/*-----------------------------------------------------------------------*/

/* FORMULAE TREE = a binary tree */
typedef struct BddFormula {
  struct BddFormula *l, *r;
  Bdd_Edge f;
  Est_String name;
} BddFormula;

/* RelOp Cache */
typedef struct {
  unsigned int key;            /* 0 = not valid node! */
  Bdd_Edge f;
  Bdd_Edge g;
  Bdd_Edge r;
} BddRelOpCache;

typedef struct {
  BddRelOpCache *table;
  unsigned int size;
  unsigned long int search;
  unsigned long int find;
  unsigned long int write;
  unsigned long int overwrite;
} BddRelOpCacheTable;

/* RelOpSimple Cache */
typedef struct {
  unsigned int key;            /* 0 = not valid node! */
  Bdd_Edge f;
  Bdd_Edge r;
} BddRelOpSimpleCache;

typedef struct {
  BddRelOpSimpleCache *table;
  unsigned int size;
  unsigned long int search;
  unsigned long int find;
  unsigned long int write;
  unsigned long int overwrite;
} BddRelOpSimpleCacheTable;

/* RelOpComplex Cache */
typedef struct {
  unsigned int key;            /* 0 = not valid node! */
  Bdd_Edge f;
  Bdd_Edge r;
  Est_String name;
} BddRelOpComplexCache;

typedef struct {
  BddRelOpComplexCache *table;
  unsigned int size;
  unsigned long int search;
  unsigned long int find;
  unsigned long int write;
  unsigned long int overwrite;
} BddRelOpComplexCacheTable;

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

extern BddFormula *bddFormulaeTree;

extern BddRelOpCacheTable bddRelOpCache;

extern BddRelOpSimpleCacheTable bddRelOpSimpleCache;

extern BddRelOpComplexCacheTable bddRelOpComplexCache;

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

/*-----------------------------------------------------------------------*/
/* Function prototypes                                                   */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* FUNCTIONS DEFINED IN  bddMain.c                                       */
/*-----------------------------------------------------------------------*/

extern Est_Boolean BddisOK(Bdd_Edge f);

extern void BddSelectNode(Bdd_Edge f);

extern void BddDeselectNode(Bdd_Edge f);

extern Est_Boolean BddisSelected(Bdd_Edge f);

extern void BddNodeSelect(Bdd_Edge f);

extern void BddNodeRepair(Bdd_Edge f);

extern Bdd_Edge BddFindTerminal(Est_String x);

extern Bdd_Edge BddFoaNode(Bdd_Variable v, Bdd_Edge pf, Bdd_Edge pt);

extern void BddAddCache(Est_UserFunction gc);

extern unsigned int BddNodeTableSize();

extern unsigned int BddNodeTableMax();

extern unsigned int BddNodeTableNum();

extern unsigned int BddNodeTableNumF();

extern unsigned long int BddNodeTableFOA();

extern unsigned long int BddNodeTableCompare();

extern unsigned long int BddNodeTableAdd();

extern unsigned int BddNodeTableGarbage();

extern unsigned int BddNodeTableGenerated();

extern unsigned int BddNodeTableBlockNumber();

extern unsigned int BddListUsed();

extern unsigned int BddListMaxLength();

extern float BddListAvgLength();

extern unsigned long int BddIteCacheFind();

extern unsigned long int BddIteCacheOverwrite();

extern unsigned long int BddRelopCacheFind();

extern unsigned long int BddRelopCacheOverwrite();

extern unsigned long int BddRelopSimpleCacheFind();

extern unsigned long int BddRelopSimpleCacheOverwrite();

extern unsigned long int BddRelopComplexCacheFind();

extern unsigned long int BddRelopComplexCacheOverwrite();

extern unsigned int BddNodeNumber(Bdd_Edge f);

extern unsigned int BddNodeMaxLevel(Bdd_Edge f);

extern float BddNodeAvgLevel(Bdd_Edge f);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS DEFINED IN  bddUtil.c                                        */
/*-----------------------------------------------------------------------*/

extern void BddExchange(Bdd_Edge *f, Bdd_Edge *g);

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

#endif  /* _BDDINT */
