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

  FileName    [bdd.h]
  Revision    [$Revision: 77 $]
  Date        [$Date: 2013-04-29 21:10:06 +0200 (pon, 29 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File bdd.h contains declaration of all external
               data structures.]
  SeeAlso     [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.]
  ************************************************************************/

#ifndef _BDD
#define _BDD

#include <est.h>

/* ON WIN32 THERE HAS TO BE DEFINED ESTWIN32 */
/* ON UNIX THERE HAS TO BE DEFINED ESTUNIX */
/* ON MACOSX THERE HAS TO BE DEFINED ESTMACOSX */

#ifdef ESTUNIX
#  ifndef EXTERN
#    define EXTERN extern
#  endif
#  ifndef DATAEXTERN
#    define DATAEXTERN extern
#  endif
#endif

#ifdef ESTMACOSX
#  ifndef EXTERN
#    define EXTERN extern
#  endif
#  ifndef DATAEXTERN
#    define DATAEXTERN extern
#  endif
#endif

#ifdef ESTWIN32
#  ifdef TCL
#    undef EXTERN
#    define EXTERN extern
#    undef DATAEXTERN
#    define DATAEXTERN extern
#  else
#    if defined(BUILD_EST) || defined(BUILD_BDD)
#      undef EXTERN
#      define EXTERN __declspec (dllexport)
#      undef DATAEXTERN
#      define DATAEXTERN extern __declspec (dllexport)
#    else
#      if defined(USE_EST) || defined(USE_BDD)
#        undef EXTERN
#        define EXTERN __declspec (dllimport)
#        undef DATAEXTERN
#        define DATAEXTERN __declspec (dllimport)
#      else
#        undef EXTERN
#        define EXTERN extern
#        undef DATAEXTERN
#        define DATAEXTERN extern
#      endif
#    endif
#  endif
#endif

/*-----------------------------------------------------------------------*/
/* Constant definitions                                                  */
/*-----------------------------------------------------------------------*/

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

/* BIDDY 1.0 */
/*
#define Bdd_isEqv(f,g) ((((f).p == (g).p) && ((f).mark == (g).mark)))
#define Bdd_isTerminal(f) ((f).p == bdd_termTrue.p)
#define Bdd_isNull(f) ((f).p == bdd_termNull.p)
*/

/* BIDDY 1.1 */
/**/
#define Bdd_isEqv(f,g) ((f).p == (g).p)
#define Bdd_isTerminal(f) (((f).p == bdd_termTrue.p || (f).p == bdd_termFalse.p))
#define Bdd_isNull(f) ((f).p == bdd_termNull.p)
/**/

/*-----------------------------------------------------------------------*/
/* Type declarations                                                     */
/*-----------------------------------------------------------------------*/

typedef void (*Bdd_UserFunction)();

/* BIDDY 1.0, BIDDY 1.1 */
/**/
typedef unsigned short int Bdd_Variable; /* must be the same as Biddy_Variable */
/**/

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

/* EDGE - THE ONLY VISIBLE PART OF A BDD PACKAGE */
typedef struct {
  void *p;                                    /* pointer into node table */
  Est_Boolean mark;                                              /* mark */
} Bdd_Edge;

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

DATAEXTERN int bdd_status;

DATAEXTERN Bdd_Edge bdd_termTrue;                           /* terminal node */

DATAEXTERN Bdd_Edge bdd_termFalse;                          /* terminal node */

DATAEXTERN Bdd_Edge bdd_termNull;                               /* null edge */

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

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

/*-----------------------------------------------------------------------*/
/* FUNCTIONS EXPORTED FROM bddMain.c                                     */
/*-----------------------------------------------------------------------*/

EXTERN void Bdd_InitPkg();

EXTERN void Bdd_ExitPkg();

EXTERN void Bdd_AboutPkg();

EXTERN Bdd_Edge Bdd_GetThen(Bdd_Edge f);

EXTERN Bdd_Edge Bdd_GetElse(Bdd_Edge f);

EXTERN Bdd_Variable Bdd_GetVariable(Bdd_Edge f);

EXTERN Est_String Bdd_GetVariableName(Bdd_Edge f);

EXTERN char Bdd_GetVariableChar(Bdd_Edge f);

EXTERN Est_String Bdd_GetIthVariableName(int i);

EXTERN int Bdd_GetVariableOrder(Bdd_Edge f);

EXTERN Bdd_Edge Bdd_FoaTerminal(Est_String x);

EXTERN Bdd_Edge Bdd_NOT(Bdd_Edge f);

EXTERN Bdd_Edge Bdd_TransferMark(Bdd_Edge f, Est_Boolean mark);

EXTERN Bdd_Edge Bdd_ITE(Bdd_Edge f, Bdd_Edge g, Bdd_Edge h);

EXTERN Bdd_Edge Bdd_Restrict(Bdd_Edge f, Bdd_Variable v, Est_Boolean value);

EXTERN Bdd_Edge Bdd_Compose(Bdd_Edge f, Bdd_Variable v, Bdd_Edge g);

EXTERN Bdd_Edge Bdd_E(Bdd_Edge f, Bdd_Variable v);

EXTERN Bdd_Edge Bdd_A(Bdd_Edge f, Bdd_Variable v);

EXTERN void Bdd_IncCounter();

EXTERN void Bdd_Fresh(Bdd_Edge f);

EXTERN void Bdd_Fortify(Bdd_Edge f);

EXTERN void Bdd_Garbage();

/*-----------------------------------------------------------------------*/
/* FUNCTIONS EXPORTED FROM bddUtil.c                                     */
/*-----------------------------------------------------------------------*/

EXTERN void Bdd_SystemStat(FILE *s);

EXTERN int Bdd_FunctionStat(FILE *s, Bdd_Edge f);

EXTERN Est_Boolean Bdd_FindFormula(Est_String x, Bdd_Edge *f);

EXTERN void Bdd_AddFormula(Est_String x, Bdd_Edge f);

EXTERN void Bdd_SaveFormula(Est_String prefix, Est_String name, Bdd_Edge f);

EXTERN Bdd_Edge Bdd_ExtractBranch(Bdd_Edge f);

EXTERN Bdd_Edge Bdd_Expand(Est_String fname, Bdd_Edge f);

EXTERN Bdd_Edge Bdd_Expr(Est_String s);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS EXPORTED FROM bddOutput.c                                   */
/*-----------------------------------------------------------------------*/

EXTERN void Bdd_WriteFunction(FILE *s, Est_String name);

EXTERN void Bdd_WriteBDD(FILE *s, Est_String name);

EXTERN int Bdd_WriteDot(FILE *s, Est_String name, int id);

EXTERN int Bdd_WriteBDDView(FILE *s, Est_String name, int id);

EXTERN int Bdd_WriteGraphML(FILE *s, Est_String name);

EXTERN int Bdd_ReadGraphML(FILE *s);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS EXPORTED FROM bddRel.c                                      */
/*-----------------------------------------------------------------------*/

EXTERN Bdd_Edge Bdd_RelOp(Bdd_Edge f, Bdd_Edge g,
                          Est_String format, Est_Boolean firsttime);

EXTERN Bdd_Edge Bdd_RelOpSimple(Bdd_Edge f,
                                 Est_String format, Est_Boolean firsttime);

EXTERN Bdd_Edge Bdd_RelOpComplex(Bdd_Edge f,
                                 Est_String format, Est_Boolean firsttime);

EXTERN Bdd_Edge Bdd_NewState(Bdd_Edge f);

EXTERN Bdd_Edge Bdd_NewState1(Bdd_Edge f, Est_String name);

EXTERN Bdd_Edge Bdd_NewState2(
                  Bdd_Edge f, Est_String name1, Est_String name2);

EXTERN Bdd_Edge Bdd_NewEq(Bdd_Edge f, Bdd_Edge g);

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

#endif  /* _BDD */
