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

  FileName    [bddTcl.c]
  Revision    [$Revision: 77 $]
  Date        [$Date: 2013-04-29 21:10:06 +0200 (pon, 29 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Ales Casar (casar@uni-mb.si)]
  Description [File bddTcl.c contains definitions of Tcl commands,
               which can be used for manipulating with BDDs from
               Tcl interpreter (e.g. tclsh or wish).]
  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"
#include "bddDecls.h"

#include <tcl.h>

extern BddStubs bddStubs;
extern CONST char *Gui_InitStubs (Tcl_Interp *interp, char *version, int exact);

/* on tcl 8.3 use #define USECONST */
/* on tcl 8.4 use #define USECONST const*/
/* this is defined in Makefile */

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

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

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

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

static int BddInitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddExitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddAboutPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTerminalsCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddExprCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddNOTCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddITECmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddECmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddACmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddRestrictCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddComposeCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddOutFunctionCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddOutBDDCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddDrawBDDCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddCmpCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddFindCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableSizeCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableFortifiedCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableFreshCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableBadCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableMaxCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableFoaCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableAddCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableCompareCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddTableGeneratedCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddBlockNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddGarbageNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddListUsedCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddListMaxLengthCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddListAvgLengthCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddIteCacheFindCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddIteCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddRelopCacheFindCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddRelopCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddRelopSimpleCacheFindCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddRelopSimpleCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddRelopComplexCacheFindCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddRelopComplexCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp,
                            int argc, USECONST char **argv);

static int BddNodeNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddNodeMaxLevelCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int BddNodeAvgLevelCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int wordNumber(Est_String s);

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

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

/**Function****************************************************************
  Synopsis    [Function BDD_Init.]
  Description [This function is used by Tcl/Tk only.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

#ifdef __cplusplus
extern "C" {
#endif

int
Bdd_Init(Tcl_Interp *interp)
{

#ifdef USE_TCL_STUBS
  if (Tcl_InitStubs(interp, "8.1", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_GUI_STUBS
  if (Gui_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

  Tcl_CreateCommand(interp, "bdd_initPkg", BddInitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_exitPkg", BddExitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_aboutPkg", BddAboutPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_terminals", BddTerminalsCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_expr", BddExprCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_NOT", BddNOTCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_ITE", BddITECmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_E", BddECmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_A", BddACmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_restrict", BddRestrictCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_compose", BddComposeCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_out_function", BddOutFunctionCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_out_BDD", BddOutBDDCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_draw_BDD", BddDrawBDDCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cmp", BddCmpCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_find", BddFindCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_size", BddTableSizeCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_number", BddTableNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_fortified", BddTableFortifiedCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_fresh", BddTableFreshCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_bad", BddTableBadCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_max", BddTableMaxCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_foa", BddTableFoaCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_add", BddTableAddCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_compare", BddTableCompareCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_table_generated", BddTableGeneratedCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_block_number", BddBlockNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_garbage_number", BddGarbageNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_list_used", BddListUsedCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_list_max_length", BddListMaxLengthCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_list_avg_length", BddListAvgLengthCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_ITE_find", BddIteCacheFindCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_ITE_overwrite", BddIteCacheOverwriteCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_RelOp_find", BddRelopCacheFindCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_RelOp_overwrite", BddRelopCacheOverwriteCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_RelOpSimple_find", BddRelopSimpleCacheFindCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_RelOpSimple_overwrite", BddRelopSimpleCacheOverwriteCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_RelOpComplex_find", BddRelopComplexCacheFindCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_cache_RelOpComplex_overwrite", BddRelopComplexCacheOverwriteCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_node_number", BddNodeNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_node_max_level", BddNodeMaxLevelCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "bdd_node_avg_level", BddNodeAvgLevelCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  return Tcl_PkgProvideEx(interp, "est2ed-bdd", "1.0", &bddStubs);
}

#ifdef __cplusplus
}
#endif

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

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

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

static int
BddInitPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  printf("Initialization of BDD package... ");
  Bdd_InitPkg();
  printf("OK");

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddExitPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  printf("Exit BDD package... ");
  Bdd_ExitPkg();
  printf("OK");

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddAboutPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  Bdd_AboutPkg();

  printf("DEBUG: FALSE = %x, TRUE = %x\n",FALSE,TRUE);
  printf("DEBUG: bdd_termTrue = (%p, %x)\n",bdd_termTrue.p,bdd_termTrue.mark);
  printf("DEBUG: bdd_termFalse = (%p, %x)\n",bdd_termFalse.p,bdd_termFalse.mark);
  printf("DEBUG: bdd_termNull = (%p, %x)\n",bdd_termNull,bdd_termNull.mark);
  printf("\n");

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddTerminalsCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                     USECONST char **argv)
{
  Est_String s1;
  Bdd_Edge sup;
  Est_String name;
  int n,k;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  n = wordNumber(s1);

  name = strtok(s1," ");  /* first terminal name */
  sup = Bdd_FoaTerminal(name);
  Bdd_AddFormula(name,sup);

  for(k=1;k<n; k++){
    name = strtok(NULL," ");  /* next terminals name */
    sup = Bdd_FoaTerminal(name);
    Bdd_AddFormula(name,sup);
  }

  free(s1);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddExprCmd(ClientData clientData, Tcl_Interp *interp, int argc,
               USECONST char **argv)
{
  Est_String s1,s2;
  Bdd_Edge f;

  if (argc != 3) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  f = Bdd_Expr(s1);
  Bdd_AddFormula(s2,f);

  free(s1);
  free(s2);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddNOTCmd(ClientData clientData, Tcl_Interp *interp, int argc,
               USECONST char **argv)
{
  Est_String s1,s2;
  Bdd_Edge f,r;

  if (argc != 3){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  if (Bdd_FindFormula(s1,&f)) {

    r = Bdd_NOT(f);
    Bdd_AddFormula(s2,r);

  } else printf("Missing Boolean function %s.\n",s1);

  free(s1);
  free(s2);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddITECmd(ClientData clientData, Tcl_Interp *interp, int argc,
               USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  Bdd_Edge f,g,h,r;

  if (argc != 5){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  if ( Bdd_FindFormula(s1,&f) && Bdd_FindFormula(s2,&g) &&
       Bdd_FindFormula(s3,&h) ) {

    r = Bdd_ITE(f,g,h);
    Bdd_AddFormula(s4,r);

  } else printf("Missing Boolean function.\n");

  free(s1);
  free(s2);
  free(s3);
  free(s4);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddECmd(ClientData clientData, Tcl_Interp *interp, int argc,
             USECONST char **argv)
{
  Est_String s1,s2,s3;
  Bdd_Edge f,sup;
  Est_String name;
  int n,k;

  if (argc != 4){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);

  if (Bdd_FindFormula(s2,&f)) {

    n = wordNumber(s1);

    name = strtok(s1," ");  /* first terminal name */
    sup = Bdd_FoaTerminal(name);
    f = Bdd_E(f,Bdd_GetVariable(sup));

    for(k=1;k<n; k++){
      name = strtok(NULL," ");  /* next terminals name */
      sup = Bdd_FoaTerminal(name);
      f = Bdd_E(f,Bdd_GetVariable(sup));
    }

    Bdd_AddFormula(s3,f);

  } else printf("Non-existing Boolean function.\n");

  free(s1);
  free(s2);
  free(s3);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddACmd(ClientData clientData, Tcl_Interp *interp, int argc,
             USECONST char **argv)
{
  Est_String s1,s2,s3;
  Bdd_Edge f,sup;
  Est_String name;
  int n,k;

  if (argc != 4){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);

  if (Bdd_FindFormula(s2,&f)) {

    n = wordNumber(s1);

    name = strtok(s1," ");  /* first terminal name */
    sup = Bdd_FoaTerminal(name);
    f = Bdd_A(f,Bdd_GetVariable(sup));

    for(k=1;k<n; k++){
      name = strtok(NULL," ");  /* next terminals name */
      sup = Bdd_FoaTerminal(name);
      f = Bdd_A(f,Bdd_GetVariable(sup));
    }

    Bdd_AddFormula(s3,f);

  } else printf("Non-existing Boolean function.\n");

  free(s1);
  free(s2);
  free(s3);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddRestrictCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  Bdd_Edge f,sup;
  int b;

  if (argc != 5){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  sscanf(s3,"%d",&b);

  if (Bdd_FindFormula(s1,&f)) {

    sup = Bdd_FoaTerminal(s2);
    if (b == 0) f = Bdd_Restrict(f,Bdd_GetVariable(sup),FALSE);
      else f = Bdd_Restrict(f,Bdd_GetVariable(sup),TRUE);
    Bdd_AddFormula(s4,f);

  } else printf("Missing Boolean function.\n");

  free(s1);
  free(s2);
  free(s3);
  free(s4);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddComposeCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  Bdd_Edge f,g,r,sup;

  if (argc != 5){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  if ( Bdd_FindFormula(s1,&f) && Bdd_FindFormula(s3,&g) ) {

    sup = Bdd_FoaTerminal(s2);
    r = Bdd_Compose(f,Bdd_GetVariable(sup),g);
    Bdd_AddFormula(s4,r);

  } else printf("Missing Boolean function.\n");

  free(s1);
  free(s2);
  free(s3);
  free(s4);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddOutFunctionCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                       USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  Bdd_WriteFunction(stdout,s1);

  free(s1);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddOutBDDCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                  USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  Bdd_WriteBDD(stdout,s1);

  free(s1);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddDrawBDDCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                  USECONST char **argv)
{
  Est_String funname;
  FILE *funfile;
  Est_String s1;
  int ERR;
#ifndef ESTWIN32
  pid_t childpid;
#endif

  /* TESTING */
  /*
  Est_String xmlname;
  FILE *xmlfile;
  */

  if (argc != 2) {
    interp->result = "wrong # args";
    Tcl_SetResult(interp, "", TCL_STATIC);
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

#ifdef ESTWIN32
  funname = strdup("C:\\Windows\\Temp\\bdd.bddview");
#else
  funname = strdup(tmpnam(NULL));
#endif

  funfile = fopen(funname,"w");
  if (!funfile) {
    printf("File error (%s)\n",funname);
    Tcl_SetResult(interp, "", TCL_STATIC);
    return TCL_ERROR;
  }

  /* TESTING */
  /*
  xmlname = strdup("bdd.graphml");
  xmlfile = fopen(xmlname,"w");
  */

  ERR = Bdd_WriteBDDView(funfile,s1,-1);
  fclose(funfile);

  /* TESTING */
  /*
  Bdd_WriteGraphML(xmlfile,s1);
  fclose(xmlfile);
  */

  free(s1);

  if (!ERR) {

#ifdef ESTWIN32
    _spawnlp(P_NOWAIT,"wish.exe","wish.exe","bddview.tcl",funname,NULL);
#elif ESTMACOSX
    childpid = fork();
    if (childpid == 0) {
      execlp("wish","wish","../bin/bddview.tcl",funname,NULL);
    }
#else
    childpid = fork();
    if (childpid == 0) {
      execlp("bddview.tcl","bddview.tcl",funname,NULL);
      execlp("/usr/lib/est2ed/bddview.tcl","bddview.tcl",funname,NULL);
      printf("bddview.tcl not found\n");
    }
#endif

  }

  free(funname);

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
BddCmpCmd(ClientData clientData, Tcl_Interp *interp, int argc,
               USECONST char **argv)
{
  Est_String s1,s2;
  Bdd_Edge f,g;
  Est_String sup = NULL;

  if (argc != 3){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  if ( Bdd_FindFormula(s1,&f) && Bdd_FindFormula(s2,&g) ) {

    if (Bdd_isEqv(f,g)) {
      sup = (Est_String) strdup("TRUE");
    } else {
      sup = (Est_String) strdup("FALSE");
    }

  } else {
    sup = (Est_String) strdup("Missing Boolean function.");
  }

  free(s1);
  free(s2);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  if (sup) free(sup);

  return TCL_OK;
}

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

static int
BddFindCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                USECONST char **argv)
{
  Est_String s1;
  Bdd_Edge f;
  Est_String sup;

  if (argc != 2){
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if ( Bdd_FindFormula(s1,&f)) {
    sup = (Est_String) strdup("TRUE");
  } else {
    sup = (Est_String) strdup("FALSE");
  }

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}


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

static int
BddTableSizeCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                     USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableSize());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}


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

static int
BddTableNumberCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                       USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableNum());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableFortifiedCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                          USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableNumF());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableFreshCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(32);
  sprintf(sup,"%s","NOT IMPLEMENTED");
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableBadCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(32);
  sprintf(sup,"%s","NOT IMPLEMENTED");
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableMaxCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableMax());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableFoaCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddNodeTableFOA());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableAddCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddNodeTableAdd());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableCompareCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                        USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddNodeTableCompare());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddTableGeneratedCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                          USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableGenerated());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddBlockNumberCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                         USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableBlockNumber());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddGarbageNumberCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                         USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddNodeTableGarbage());
  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}


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

static int
BddListUsedCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddListUsed());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddListMaxLengthCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                         USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%u",BddListMaxLength());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddListAvgLengthCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                         USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%.2f",BddListAvgLength());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddIteCacheFindCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddIteCacheFind());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddIteCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddIteCacheOverwrite());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddRelopCacheFindCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddRelopCacheFind());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddRelopCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddRelopCacheOverwrite());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddRelopSimpleCacheFindCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddRelopSimpleCacheFind());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddRelopSimpleCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddRelopSimpleCacheOverwrite());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddRelopComplexCacheFindCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddRelopComplexCacheFind());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddRelopComplexCacheOverwriteCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String sup;

  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%lu",BddRelopComplexCacheOverwrite());

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddNodeNumberCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String s1;
  unsigned int i;
  Bdd_Edge f;
  Est_String sup;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (Bdd_FindFormula(s1,&f)) {

    i = BddNodeNumber(f);
    sup = (Est_String) malloc(15);
    sprintf(sup,"%u",i);

  } else {
    printf("Missing Boolean function.\n");
    sup = strdup("");
  }

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddNodeMaxLevelCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                        USECONST char **argv)
{
  Est_String s1;
  unsigned int i;
  Bdd_Edge f;
  Est_String sup;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (Bdd_FindFormula(s1,&f)) {

    i = BddNodeMaxLevel(f);
    sup = (Est_String) malloc(15);
    sprintf(sup,"%u",i);

  } else {
    printf("Missing Boolean function.\n");
    sup = strdup("");
  }

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
BddNodeAvgLevelCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                        USECONST char **argv)
{
  Est_String s1;
  float d;
  Bdd_Edge f;
  Est_String sup;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (Bdd_FindFormula(s1,&f)) {

    d = BddNodeAvgLevel(f);
    sup = (Est_String) malloc(15);
    sprintf(sup,"%.2f",d);

  } else {
    printf("Missing Boolean function.\n");
    sup = strdup("");
  }

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
wordNumber(Est_String s)
{
  int num;
  int token;
  Est_String sup,sup_next;

  num = 0;
  sup = strdup(s);

  token = strspn(sup," ");
  while (strspn(sup," ") < strlen(sup)) {
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    num++;
    token = strcspn(sup," ");
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    token = strspn(sup," ");
  }

  free(sup);
  return num;
}
