distr/dddmp/testdddmp.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [testdddmp.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [A simple test function for Dddmp package]
   8
   9   Description  [This program constitutes a simple test program
  10     for the dddmp library (version 2.0).
  11     A simple interactive command selection allow the users to perform the
  12     main operation on BDDs, ADDs, and CNF, such as loading and storing.
  13     It can work also as a BDD calculators.
  14     ]
  15
  16   Author       [Gianpiero Cabodi and Stefano Quer]
  17
  18   Copyright    [
  19     Copyright (c) 2004 by Politecnico di Torino.
  20     All Rights Reserved. This software is for educational purposes only.
  21     Permission is given to academic institutions to use, copy, and modify
  22     this software and its documentation provided that this introductory
  23     message is not removed, that this software and its documentation is
  24     used for the institutions' internal research and educational purposes,
  25     and that no monies are exchanged. No guarantee is expressed or implied
  26     by the distribution of this code.
  27     Send bug-reports and/or questions to:
  28     {gianpiero.cabodi,stefano.quer}@polito.it.
  29     ]
  30
  31 ******************************************************************************/
  32
  33 #include <string.h>
  34 #include <stdio.h>
  35 #include "dddmpInt.h"
  36
  37 /*---------------------------------------------------------------------------*/
  38 /* Constant declarations                                                     */
  39 /*---------------------------------------------------------------------------*/
  40
  41 #define DDDMPTEST_MAX_FILENAME_LENGTH 256
  42 #define DDDMPTEST_MAX_STRING_LENGTH 80
  43 #define DDDMPTEST_MAX_OPERAND  20
  44 #define DDDMPTEST_MAX_VARIABLE 50
  45 #define DDDMP_MAX_BDDARRAY_LEN 1000
  46
  47 /**Enum************************************************************************
  48
  49   Synopsis    [Message type for output messages]
  50
  51   Description [Type supported by the output function to print-out
  52     the proper message.
  53     ]
  54
  55 ******************************************************************************/
  56
  57 typedef enum {
  58   /* Int Messages */
  59   DDDMP_MESSAGE_MANAGER_VAR,
  60   DDDMP_MESSAGE_BDD,
  61   DDDMP_MESSAGE_BDD_ARRAY,
  62   DDDMP_MESSAGE_SOURCE1,
  63   DDDMP_MESSAGE_SOURCE2,
  64   DDDMP_MESSAGE_DESTINATION,
  65   DDDMP_MESSAGE_CUBE,
  66   DDDMP_MESSAGE_INDEX,
  67   DDDMP_MESSAGE_I_ID,
  68   DDDMP_MESSAGE_EDGE_MAX,
  69   DDDMP_MESSAGE_LENGHT_MAX,
  70   DDDMP_MESSAGE_REORDERING,
  71   /* String Messages */
  72   DDDMP_MESSAGE_PROMPT,
  73   DDDMP_MESSAGE_FILE,
  74   DDDMP_MESSAGE_OP,
  75   DDDMP_MESSAGE_FORMAT
  76 } Dddmp_MessageType;
  77
  78 #if !defined(RAND_MAX) && defined(sun) && defined(sparc)
  79 #define RAND_MAX 2147483647
  80 #endif
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Stucture declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86 typedef struct dddmpVarInfo {
  87   /*
  88    *  Local Information
  89    */
  90
  91   int nDdVars;       /* Local Manager Number of Variables */
  92   char **rootNames;  /* Root Names */
  93
  94   /*
  95    *  Header File Information
  96    */
  97
  98   Dddmp_DecompType ddType;
  99
 100   int nVars;      /* File Manager Number of Variables */
 101   int nSuppVars;  /* File Structure Number of Variables */
 102
 103   int varNamesFlagUpdate;      /* 0 to NOT Update */
 104   char **suppVarNames;
 105   char **orderedVarNames;
 106
 107   int varIdsFlagUpdate;        /* 0 to NOT Update */
 108   int *varIds;                 /* File ids - nSuppVars size */
 109   int *varIdsAll;              /* ALL ids - nVars size */
 110
 111   int varComposeIdsFlagUpdate; /* 0 to NOT Update */
 112   int *varComposeIds;          /* File permids - nSuppVars size */
 113   int *varComposeIdsAll;       /* ALL permids - nVars size */
 114
 115   int varAuxIdsFlagUpdate;     /* 0 to NOT Update */
 116   int *varAuxIds;              /* File auxids - nSuppVars size */
 117   int *varAuxIdsAll;           /* ALL auxids  - nVars size */
 118
 119   int nRoots;
 120 } dddmpVarInfo_t;
 121
 122 /*---------------------------------------------------------------------------*/
 123 /* Type declarations                                                         */
 124 /*---------------------------------------------------------------------------*/
 125
 126 /*---------------------------------------------------------------------------*/
 127 /* Variable declarations                                                     */
 128 /*---------------------------------------------------------------------------*/
 129
 130 Dddmp_RootMatchType rootmatchmode;
 131 Dddmp_VarMatchType varmatchmode;
 132 Dddmp_VarInfoType varoutinfo;
 133 char varname[DDDMPTEST_MAX_STRING_LENGTH];
 134
 135 /*---------------------------------------------------------------------------*/
 136 /* Macro declarations                                                        */
 137 /*---------------------------------------------------------------------------*/
 138
 139 /**AutomaticStart*************************************************************/
 140
 141 /*---------------------------------------------------------------------------*/
 142 /* Static function prototypes                                                */
 143 /*---------------------------------------------------------------------------*/
 144
 145 static DdManager *ManagerInit (dddmpVarInfo_t *varInfo);
 146 static void ManagerQuit (DdManager **ddMgr, dddmpVarInfo_t *varInfo);
 147 static int OneCreate(DdManager *ddMgr, DdNode **operandBdd);
 148 static int BddZeroCreate(DdManager *ddMgr, DdNode **operandBdd);
 149 static int LeafCreate(DdManager *ddMgr, DdNode **operandBdd);
 150 static int BddCreate(DdManager *ddMgr, DdNode **operandBdd);
 151 static int A2B(void);
 152 static int B2A(void);
 153 static int HeaderLoadBdd(dddmpVarInfo_t *varInfo);
 154 static int HeaderLoadCnf(dddmpVarInfo_t *varInfo);
 155 static int HeaderWrite(dddmpVarInfo_t *varInfo);
 156 static int Help(void);
 157 static int OrderNamesLoad(dddmpVarInfo_t *varInfo);
 158 static int IntArrayLoad(dddmpVarInfo_t *varInfo, const char *mode);
 159 static int BddLoad(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
 160 static int BddArrayLoad(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
 161 static int AddLoad(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
 162 static int AddArrayLoad(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
 163 static int BddLoadCnf(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
 164 static int BddArrayLoadCnf(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
 165 static int Operation(DdManager *ddMgr, DdNode **operandBdd);
 166 static int BddStore(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
 167 static int BddArrayStore(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
 168 static int AddStore(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
 169 static int AddArrayStore(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
 170 static int BddStoreCnf(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
 171 static int BddArrayStoreCnf(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
 172 static int DynamicReordering(DdManager *ddMgr);
 173 static int SetLoadMatchmode();
 174 static int CompleteInfoStruct(Dddmp_DecompType ddType, int nVars, int nSuppVars, char **suppVarNames, char **orderedVarNames, int *varIds, int *varComposeIds, int *varAuxIds, int nRoots, dddmpVarInfo_t *varInfo);
 175 static void ReadInt(Dddmp_MessageType message, int *i);
 176 static void ReadString(Dddmp_MessageType message, char string[]);
 177
 178 /**AutomaticEnd***************************************************************/
 179
 180 int
 181 main(
 182   int argc,
 183   char **argv
 184   )
 185 {
 186   DdManager *ddMgr = NULL;
 187   DdNode **operandBdd = NULL;
 188   DdNode ***operandBddArray = NULL;
 189   int *operandBddArraySize = NULL;
 190   char *row = NULL;
 191   dddmpVarInfo_t varInfo;
 192   int i;
 193
 194   /*--------------------- Echo command line and arguments -------------------*/
 195
 196   fprintf (stdout, "#");
 197   for (i=0; i<argc; i++) {
 198     fprintf (stdout, "%s Version 2.0.2 (use command help)", argv[i]);
 199   }
 200   fprintf (stdout, "\n");
 201   if (argc>1) {
 202     Help();
 203   }
 204
 205   /*-------------------------- Init Array of BDDs ---------------------------*/
 206
 207  rootmatchmode = DDDMP_ROOT_MATCHLIST;
 208 #if 1
 209   varmatchmode = DDDMP_VAR_MATCHIDS;
 210 #else
 211   varmatchmode = DDDMP_VAR_MATCHNAMES;
 212 #endif
 213   varoutinfo = DDDMP_VARIDS;
 214
 215   row = DDDMP_ALLOC (char, DDDMPTEST_MAX_STRING_LENGTH);
 216   Dddmp_CheckAndReturn (row==NULL, "Allocation error.");
 217
 218   operandBdd = DDDMP_ALLOC (DdNode *, DDDMPTEST_MAX_OPERAND);
 219   Dddmp_CheckAndReturn (operandBdd==NULL, "Allocation error.");
 220
 221   operandBddArray = DDDMP_ALLOC (DdNode **, DDDMPTEST_MAX_OPERAND);
 222   Dddmp_CheckAndReturn (operandBddArray==NULL, "Allocation error.");
 223
 224   operandBddArraySize = DDDMP_ALLOC (int, DDDMPTEST_MAX_OPERAND);
 225   Dddmp_CheckAndReturn (operandBddArraySize==NULL, "Allocation error.");
 226
 227   for (i=0; i<DDDMPTEST_MAX_OPERAND; i++) {
 228     operandBdd[i] = NULL;
 229     operandBddArray[i] = NULL;
 230     operandBddArraySize[i] = 0;
 231   }
 232
 233   /*--------------------- Manage command line parameters --------------------*/
 234
 235   while (1) {
 236     ReadString (DDDMP_MESSAGE_PROMPT, row);
 237     if (row[0]=='\n') {
 238       continue;
 239     }
 240     if (strncmp (row, "help", 4)==0) {
 241       Help();
 242     } else if (strncmp (row, "mi", 2)==0) {
 243       ddMgr = ManagerInit (&varInfo);
 244     } else if (strncmp (row, "mq", 2)==0) {
 245       ManagerQuit (&ddMgr, &varInfo);
 246     } else if (strncmp (row, "onl", 3)==0) {
 247       OrderNamesLoad (&varInfo);
 248     } else if (strncmp (row, "oil", 3)==0) {
 249       IntArrayLoad (&varInfo, "oil");
 250     } else if (strncmp (row, "cil", 3)==0) {
 251       IntArrayLoad (&varInfo, "cil");
 252     } else if (strncmp (row, "slm", 3)==0) {
 253       SetLoadMatchmode ();
 254     } else if (strncmp (row, "op", 2)==0) {
 255       Operation (ddMgr, operandBdd);
 256     } else if (strncmp (row, "oc", 2)==0) {
 257       OneCreate (ddMgr, operandBdd);
 258     } else if (strncmp (row, "zc", 2)==0) {
 259       BddZeroCreate (ddMgr, operandBdd);
 260     } else if (strncmp (row, "lc", 2)==0) {
 261       LeafCreate (ddMgr, operandBdd);
 262     } else if (strncmp (row, "bc", 2)==0) {
 263       BddCreate (ddMgr, operandBdd);
 264     } else if (strncmp (row, "a2b", 3)==0) {
 265       A2B ();
 266     } else if (strncmp (row, "b2a", 3)==0) {
 267       B2A ();
 268     } else if (strncmp (row, "hlb", 3)==0) {
 269       HeaderLoadBdd (&varInfo);
 270     } else if (strncmp (row, "hlc", 3)==0) {
 271       HeaderLoadCnf (&varInfo);
 272     } else if (strncmp (row, "bl", 3)==0) {
 273       BddLoad (ddMgr, operandBdd, &varInfo);
 274     } else if (strncmp (row, "bal", 3)==0) {
 275       BddArrayLoad (ddMgr, operandBddArray, operandBddArraySize, &varInfo);
 276     } else if (strncmp (row, "al", 2)==0) {
 277       AddLoad (ddMgr, operandBdd, &varInfo);
 278     } else if (strncmp (row, "aal", 3)==0) {
 279       AddArrayLoad (ddMgr, operandBddArray, operandBddArraySize, &varInfo);
 280     } else if (strncmp (row, "cl", 2)==0) {
 281       BddLoadCnf (ddMgr, operandBdd, &varInfo);
 282     } else if (strncmp (row, "cal", 3)==0) {
 283       BddArrayLoadCnf (ddMgr, operandBddArray, operandBddArraySize, &varInfo);
 284     } else if (strncmp (row, "hw", 2)==0) {
 285       HeaderWrite (&varInfo);
 286     } else if (strncmp (row, "bs", 2)==0) {
 287       BddStore (ddMgr, operandBdd, &varInfo);
 288     } else if (strncmp (row, "bas", 3)==0) {
 289       BddArrayStore (ddMgr, operandBddArray, operandBddArraySize, &varInfo);
 290     } else if (strncmp (row, "as", 2)==0) {
 291       AddStore (ddMgr, operandBdd, &varInfo);
 292     } else if (strncmp (row, "aas", 2)==0) {
 293       AddArrayStore (ddMgr, operandBddArray, operandBddArraySize, &varInfo);
 294     } else if (strncmp (row, "cs", 2)==0) {
 295       BddStoreCnf (ddMgr, operandBdd, &varInfo);
 296     } else if (strncmp (row, "cas", 2)==0) {
 297       BddArrayStoreCnf (ddMgr, operandBddArray, operandBddArraySize, &varInfo);
 298     } else if (strncmp (row, "dr", 2)==0) {
 299       DynamicReordering (ddMgr);
 300     } else if (strncmp (row, "quit", 4)==0) {
 301       break;
 302     } else {
 303       fprintf (stderr, "Command not found: %s\n", row);
 304     }
 305   }
 306
 307   /*-------------------------------- Free Memory ----------------------------*/
 308
 309   ManagerQuit (&ddMgr, &varInfo);
 310
 311   DDDMP_FREE (row);
 312   DDDMP_FREE (operandBdd);
 313   for (i=0; i<DDDMPTEST_MAX_OPERAND; i++) {
 314     if (operandBddArray[i] != NULL) {
 315       DDDMP_FREE (operandBddArray[i]);
 316     }
 317   }
 318   DDDMP_FREE (operandBddArray);
 319   DDDMP_FREE (operandBddArraySize);
 320
 321   fprintf (stdout, "End of test.\n");
 322
 323   return (DDDMP_SUCCESS);
 324 }
 325
 326 /*---------------------------------------------------------------------------*/
 327 /* Definition of internal functions                                          */
 328 /*---------------------------------------------------------------------------*/
 329
 330 /*---------------------------------------------------------------------------*/
 331 /* Definition of static functions                                            */
 332 /*---------------------------------------------------------------------------*/
 333
 334 /**Function********************************************************************
 335
 336   Synopsis     [Create a CUDD Manager with nVars variables.]
 337
 338   Description  [Create a CUDD Manager with nVars variables.]
 339
 340   SideEffects  []
 341
 342   SeeAlso      []
 343
 344 ******************************************************************************/
 345
 346 static DdManager *
 347 ManagerInit (
 348   dddmpVarInfo_t *varInfo
 349   )
 350 {
 351   DdManager *ddMgr = NULL;
 352   int nVars;
 353
 354   ReadInt (DDDMP_MESSAGE_MANAGER_VAR, &nVars);
 355
 356   /*----------------------- Init Var Information Structure ------------------*/
 357
 358   varInfo->nDdVars = nVars;
 359
 360   varInfo->rootNames = NULL;
 361   varInfo->ddType = DDDMP_NONE;
 362   varInfo->nVars = (-1);
 363   varInfo->nSuppVars = (-1);
 364   varInfo->varNamesFlagUpdate = 1;
 365   varInfo->suppVarNames = NULL;
 366   varInfo->orderedVarNames = NULL;
 367   varInfo->varIdsFlagUpdate = 1;
 368   varInfo->varIds = NULL;
 369   varInfo->varIdsAll = NULL;
 370   varInfo->varComposeIdsFlagUpdate = 1;
 371   varInfo->varComposeIds = NULL;
 372   varInfo->varComposeIdsAll = NULL;
 373   varInfo->varAuxIdsFlagUpdate = 1;
 374   varInfo->varAuxIds = NULL;
 375   varInfo->varAuxIdsAll = NULL;
 376   varInfo->nRoots = (-1);
 377
 378   /*------------------------------ Init DD Manager --------------------------*/
 379
 380   ddMgr = Cudd_Init (nVars, 0, CUDD_UNIQUE_SLOTS,
 381     CUDD_CACHE_SLOTS, 0);
 382
 383   Dddmp_CheckAndReturn (ddMgr==NULL, "DdManager NOT inizializated.");
 384
 385   return (ddMgr);
 386 }
 387
 388 /**Function********************************************************************
 389
 390   Synopsis     [Quit a CUDD Manager.]
 391
 392   Description  [Quit a CUDD Manager.]
 393
 394   SideEffects  []
 395
 396   SeeAlso      []
 397
 398 ******************************************************************************/
 399
 400 static void
 401 ManagerQuit (
 402   DdManager **ddMgrPtr      /* IN: CUDD Manager */,
 403   dddmpVarInfo_t *varInfo   /* IN: Internal Manager */
 404   )
 405 {
 406   if (*ddMgrPtr == NULL) {
 407     return;
 408   }
 409
 410   fprintf (stdout, "Quitting CUDD Manager.\n");
 411   Cudd_Quit (*ddMgrPtr);
 412   *ddMgrPtr = NULL;
 413
 414   DddmpStrArrayFree (varInfo->rootNames, varInfo->nRoots);
 415   DddmpStrArrayFree (varInfo->suppVarNames, varInfo->nSuppVars);
 416   DddmpStrArrayFree (varInfo->orderedVarNames, varInfo->nVars);
 417   DDDMP_FREE (varInfo->varIds);
 418   DDDMP_FREE (varInfo->varIdsAll);
 419   DDDMP_FREE (varInfo->varComposeIds);
 420   DDDMP_FREE (varInfo->varComposeIdsAll);
 421   DDDMP_FREE (varInfo->varAuxIds);
 422   DDDMP_FREE (varInfo->varAuxIdsAll);
 423
 424   varInfo->nDdVars = (-1);
 425   varInfo->rootNames = NULL;
 426   varInfo->ddType = DDDMP_NONE;
 427   varInfo->nVars = (-1);
 428   varInfo->nSuppVars = (-1);
 429   varInfo->varNamesFlagUpdate = 1;
 430   varInfo->suppVarNames = NULL;
 431   varInfo->orderedVarNames = NULL;
 432   varInfo->varIdsFlagUpdate = 1;
 433   varInfo->varIds = NULL;
 434   varInfo->varIdsAll = NULL;
 435   varInfo->varComposeIdsFlagUpdate = 1;
 436   varInfo->varComposeIds = NULL;
 437   varInfo->varComposeIdsAll = NULL;
 438   varInfo->varAuxIdsFlagUpdate = 1;
 439   varInfo->varAuxIds = NULL;
 440   varInfo->varAuxIdsAll = NULL;
 441   varInfo->nRoots = (-1);
 442
 443   return;
 444 }
 445
 446 /**Function********************************************************************
 447
 448   Synopsis     [Create a One-BDD Leaf.]
 449
 450   Description  [Create a One-BDD Leaf.]
 451
 452   SideEffects  []
 453
 454   SeeAlso      []
 455
 456 ******************************************************************************/
 457
 458 static int
 459 OneCreate(
 460   DdManager *ddMgr      /* IN: CUDD Manager */,
 461   DdNode **operandBdd   /* In/OUT: Array of operand */
 462   )
 463 {
 464   int i;
 465
 466   /*------------------------ Read Operation Operands ------------------------*/
 467
 468   ReadInt (DDDMP_MESSAGE_BDD, &i);
 469
 470   operandBdd[i] = Cudd_ReadOne (ddMgr);
 471
 472   return (DDDMP_SUCCESS);
 473 }
 474
 475 /**Function********************************************************************
 476
 477   Synopsis     [Create a Zero-BDD Leaf.]
 478
 479   Description  [Create a Zero-BDD Leaf.]
 480
 481   SideEffects  []
 482
 483   SeeAlso      []
 484
 485 ******************************************************************************/
 486
 487 static int
 488 BddZeroCreate(
 489   DdManager *ddMgr      /* IN: CUDD Manager */,
 490   DdNode **operandBdd   /* IN/OUT: array of operand */
 491   )
 492 {
 493   int i;
 494   DdNode *one = NULL;
 495
 496   /*------------------------ Read Operation Operands ------------------------*/
 497
 498   ReadInt (DDDMP_MESSAGE_BDD, &i);
 499
 500   one = Cudd_ReadOne(ddMgr);
 501   operandBdd[i] = Cudd_Not(one);
 502
 503   return (DDDMP_SUCCESS);
 504 }
 505
 506 /**Function********************************************************************
 507
 508   Synopsis     [Create a One-Node BDD.]
 509
 510   Description  [Create a One-Node BDD.]
 511
 512   SideEffects  []
 513
 514   SeeAlso      []
 515
 516 ******************************************************************************/
 517
 518 static int
 519 LeafCreate(
 520   DdManager *ddMgr      /* IN: CUDD Manager */,
 521   DdNode **operandBdd   /* IN/OUT: Array of operandBdd */
 522   )
 523 {
 524   int i, j;
 525   DdNode *f = NULL;
 526
 527   /*------------------------ Read Operation Operands ------------------------*/
 528
 529   ReadInt (DDDMP_MESSAGE_BDD, &i);
 530   ReadInt (DDDMP_MESSAGE_INDEX, &j);
 531
 532   f = Cudd_bddIthVar (ddMgr, j);
 533   Cudd_Ref(f);
 534   operandBdd[i] = f;
 535
 536   return (DDDMP_SUCCESS);
 537 }
 538
 539 /**Function********************************************************************
 540
 541   Synopsis     [Create a BDD.]
 542
 543   Description  [Create a BDD: Variable index and number of cubes selection.]
 544
 545   SideEffects  []
 546
 547   SeeAlso      []
 548
 549 ******************************************************************************/
 550
 551 static int
 552 BddCreate (
 553   DdManager *ddMgr      /* IN: CUDD Manager */,
 554   DdNode **operandBdd   /* array of operandBdd */
 555   )
 556 {
 557   DdNode **vet, *f, *g, *h;
 558   int nb, nv, vi0, vi1, nc, i, j;
 559   char row[DDDMPTEST_MAX_FILENAME_LENGTH];
 560
 561   /*------------------------ Read Operation Operands ------------------------*/
 562
 563   ReadInt (DDDMP_MESSAGE_BDD, &nb);
 564
 565   fprintf (stdout, "Variables Index [n-m] (m-n = number of variables): ");
 566   fgets (row, DDDMPTEST_MAX_STRING_LENGTH, stdin);
 567   sscanf (row, "%d-%d", &vi0, &vi1);
 568   nv = vi1-vi0+1;
 569
 570   ReadInt (DDDMP_MESSAGE_CUBE, &nc);
 571
 572   /* Leaf Creation */
 573   vet = DDDMP_ALLOC (DdNode *, nv);
 574   for (i=0; i<nv; i++) {
 575      vet[i] = Cudd_bddIthVar (ddMgr, vi0+i);
 576   }
 577
 578   /* Cubes and BDD creation */
 579   f = Cudd_Not (Cudd_ReadOne (ddMgr));
 580   for (i=0; i<nc; i++)
 581     {
 582     g = Cudd_ReadOne (ddMgr);
 583     for (j=0; j<nv; j++)
 584       {
 585       if ( ((float) rand())/((float) RAND_MAX) > 0.5 ) {
 586         h = Cudd_bddAnd (ddMgr, g, vet[j]);
 587       } else {
 588         h = Cudd_bddAnd (ddMgr, g, Cudd_Not (vet[j]));
 589       }
 590       Cudd_Ref (h);
 591       Cudd_RecursiveDeref (ddMgr, g);
 592       g = h;
 593       }
 594     h = Cudd_bddOr (ddMgr, f, g);
 595     Cudd_Ref (h);
 596     Cudd_RecursiveDeref (ddMgr, f);
 597     Cudd_RecursiveDeref (ddMgr, g);
 598     f = h;
 599     }
 600
 601   operandBdd[nb] = f;
 602
 603   return (DDDMP_SUCCESS);
 604 }
 605
 606 /**Function********************************************************************
 607
 608   Synopsis     [Transform a BDD from the ASCII to the Binary format].]
 609
 610   Description  [Input and Output file selection.]
 611
 612   SideEffects  []
 613
 614   SeeAlso      []
 615
 616 ******************************************************************************/
 617
 618 static int
 619 A2B(
 620   void
 621 )
 622 {
 623   fprintf (stderr, "Not yet Implemented!!!\n");
 624
 625   return (DDDMP_FAILURE);
 626 }
 627
 628 /**Function********************************************************************
 629
 630   Synopsis     [Transform a BDD from the Binary to the ASCII format].]
 631
 632   Description  [Input and Output file selection.]
 633
 634   SideEffects  []
 635
 636   SeeAlso      []
 637
 638 ******************************************************************************/
 639
 640 static int
 641 B2A(
 642   void
 643 )
 644 {
 645   fprintf (stderr, "Not yet Implemented!!!\n");
 646
 647   return (DDDMP_FAILURE);
 648 }
 649
 650 /**Function********************************************************************
 651
 652   Synopsis     [Read the Header of a file containing a BDD.]
 653
 654   Description  [File name Selection.]
 655
 656   SideEffects  []
 657
 658   SeeAlso      []
 659
 660 ******************************************************************************/
 661
 662 static int
 663 HeaderLoadBdd (
 664   dddmpVarInfo_t *varInfo      /* IN/OUT: Variable Information */
 665   )
 666 {
 667   Dddmp_DecompType ddType;
 668   int retValue, nRoots, nVars, nSuppVars;
 669   int *tmpVarIds = NULL;
 670   int *tmpVarAuxIds = NULL;
 671   int *tmpVarComposeIds = NULL;
 672   char **tmpOrderedVarNames = NULL;
 673   char **tmpSuppVarNames = NULL;
 674   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
 675
 676   /*------------------------ Read Operation Operands ------------------------*/
 677
 678   ReadString (DDDMP_MESSAGE_FILE, fileName);
 679
 680   retValue = Dddmp_cuddHeaderLoad (&ddType, &nVars, &nSuppVars,
 681     &tmpSuppVarNames, &tmpOrderedVarNames, &tmpVarIds, &tmpVarComposeIds,
 682     &tmpVarAuxIds, &nRoots, fileName, NULL);
 683
 684   if (retValue == DDDMP_FAILURE) {
 685     return (DDDMP_FAILURE);
 686   }
 687
 688   /*---------------------------- Tail Operations ----------------------------*/
 689
 690   CompleteInfoStruct (ddType, nVars, nSuppVars,
 691     tmpSuppVarNames, tmpOrderedVarNames, tmpVarIds, tmpVarComposeIds,
 692     tmpVarAuxIds, nRoots, varInfo);
 693
 694   return (DDDMP_SUCCESS);
 695 }
 696
 697 /**Function********************************************************************
 698
 699   Synopsis     [Read the Header of a file containing a CNF formula.]
 700
 701   Description  [File name Selection.]
 702
 703   SideEffects  []
 704
 705   SeeAlso      []
 706
 707 ******************************************************************************/
 708
 709 static int
 710 HeaderLoadCnf (
 711   dddmpVarInfo_t *varInfo      /* IN/OUT: Variable Information */
 712   )
 713 {
 714   int retValue, nRoots, nVars, nSuppVars;
 715   int *tmpVarIds = NULL;
 716   int *tmpVarComposeIds = NULL;
 717   int *tmpVarAuxIds = NULL;
 718   char **tmpOrderedVarNames = NULL;
 719   char **tmpSuppVarNames = NULL;
 720   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
 721
 722   /*------------------------ Read Operation Operands ------------------------*/
 723
 724   ReadString (DDDMP_MESSAGE_FILE, fileName);
 725
 726   retValue = Dddmp_cuddHeaderLoadCnf (&nVars, &nSuppVars,
 727    &tmpSuppVarNames, &tmpOrderedVarNames, &tmpVarIds, &tmpVarComposeIds,
 728    &tmpVarAuxIds, &nRoots, fileName, NULL);
 729
 730   if (retValue == DDDMP_FAILURE) {
 731     return (DDDMP_FAILURE);
 732   }
 733
 734   /*---------------------------- Tail Operations ----------------------------*/
 735
 736   CompleteInfoStruct (DDDMP_CNF, nVars, nSuppVars,
 737     tmpSuppVarNames, tmpOrderedVarNames, tmpVarIds, tmpVarComposeIds,
 738     tmpVarAuxIds, nRoots, varInfo);
 739
 740   return (DDDMP_SUCCESS);
 741 }
 742
 743 /**Function********************************************************************
 744
 745   Synopsis     [Read the Header of a filke containing a BDD.]
 746
 747   Description  [File name Selection.]
 748
 749   SideEffects  []
 750
 751   SeeAlso      []
 752
 753 ******************************************************************************/
 754
 755 static int
 756 HeaderWrite(
 757   dddmpVarInfo_t *varInfo      /* IN/OUT: Variable Information */
 758   )
 759 {
 760   int i;
 761
 762   switch (varInfo->ddType) {
 763     case DDDMP_BDD:
 764       fprintf (stdout, "DD TYPE: DDDMP_BDD\n");
 765       break;
 766     case DDDMP_ADD:
 767       fprintf (stdout, "DD TYPE: DDDMP_ADD\n");
 768       break;
 769     case DDDMP_CNF:
 770       fprintf (stdout, "DD TYPE: DDDMP_CNF\n");
 771       break;
 772     case DDDMP_NONE:
 773       fprintf (stdout, "DD TYPE: NONE - Error\n");
 774       break;
 775   }
 776
 777   fprintf (stdout, "Number of variables: %d\n", varInfo->nVars);
 778   fprintf (stdout, "Number of support variables: %d\n", varInfo->nSuppVars);
 779
 780   if (varInfo->suppVarNames != NULL) {
 781     fprintf (stdout, "suppVarNames: ");
 782     for (i=0; i<varInfo->nSuppVars; i++) {
 783       if (varInfo->suppVarNames[i] != NULL) {
 784         fprintf (stdout, "%s ", varInfo->suppVarNames[i]);
 785       }
 786     }
 787     fprintf (stdout, "\n");
 788   }
 789
 790   if (varInfo->orderedVarNames != NULL) {
 791     fprintf (stdout, "orderedVarNames: ");
 792     for (i=0; i<varInfo->nVars; i++) {
 793       if (varInfo->orderedVarNames[i] != NULL) {
 794         fprintf (stdout, "%s ", varInfo->orderedVarNames[i]);
 795       }
 796     }
 797     fprintf (stdout, "\n");
 798   }
 799
 800   if (varInfo->varIds != NULL) {
 801     fprintf (stdout, "varIds: ");
 802     for (i=0; i<varInfo->nSuppVars; i++) {
 803       fprintf (stdout, "%d ", varInfo->varIds[i]);
 804     }
 805     fprintf (stdout, "\n");
 806   }
 807
 808   if (varInfo->varIdsAll != NULL) {
 809     fprintf (stdout, "varIds for ALL Manager Variables: ");
 810     for (i=0; i<varInfo->nVars; i++) {
 811       fprintf (stdout, "%d ", varInfo->varIdsAll[i]);
 812     }
 813     fprintf (stdout, "\n");
 814   }
 815
 816   if (varInfo->varComposeIds != NULL) {
 817     fprintf (stdout, "varComposeIds: ");
 818     for (i=0; i<varInfo->nSuppVars; i++) {
 819       fprintf (stdout, "%d ", varInfo->varComposeIds[i]);
 820     }
 821     fprintf (stdout, "\n");
 822   }
 823
 824   if (varInfo->varComposeIdsAll != NULL) {
 825     fprintf (stdout, "varComposeIds for ALL Manager Variables: ");
 826     for (i=0; i<varInfo->nVars; i++) {
 827       fprintf (stdout, "%d ", varInfo->varComposeIdsAll[i]);
 828     }
 829     fprintf (stdout, "\n");
 830   }
 831
 832   if (varInfo->varAuxIds != NULL) {
 833     fprintf (stdout, "varAuxIds: ");
 834     for (i=0; i<varInfo->nSuppVars; i++) {
 835       fprintf (stdout, "%d ", varInfo->varAuxIds[i]);
 836     }
 837     fprintf (stdout, "\n");
 838   }
 839
 840   if (varInfo->varAuxIdsAll != NULL) {
 841     fprintf (stdout, "varAuxIds for ALL Manager Variables: ");
 842     for (i=0; i<varInfo->nVars; i++) {
 843       fprintf (stdout, "%d ", varInfo->varAuxIdsAll[i]);
 844     }
 845     fprintf (stdout, "\n");
 846   }
 847
 848   fprintf (stdout, "Number of roots: %d\n", varInfo->nRoots);
 849
 850   fflush (stdout);
 851
 852   return (DDDMP_SUCCESS);
 853 }
 854
 855 /**Function********************************************************************
 856
 857   Synopsis     [Print the Help messages.]
 858
 859   Description  [Print the Help messages.]
 860
 861   SideEffects  []
 862
 863   SeeAlso      []
 864
 865 ******************************************************************************/
 866
 867 static int
 868 Help(
 869   void
 870   )
 871 {
 872   fprintf (stdout, "Commands:\n");
 873   fprintf (stdout, "MAIN\n");
 874
 875   fprintf (stdout, "\thelp : Print this set of messages.\n");
 876   fprintf (stdout, "\tquit : Quit the test program.\n");
 877
 878   fprintf (stdout, "MANAGER OPERATIONs\n");
 879
 880   fprintf (stdout,
 881     "\thmi  : Manager Init (To do BEFORE any BDD/ADD operation).\n");
 882   fprintf (stdout, "\thmq  : Manager Quit.\n");
 883
 884   fprintf (stdout, "LOAD\n");
 885
 886   fprintf (stdout, "\thlb  : Load the header from a BDD/ADD file.\n");
 887   fprintf (stdout, "\thlc  : Load the header from a CNF file.\n");
 888   fprintf (stdout, "\tbl   : Load a BDD from a file.\n");
 889   fprintf (stdout, "\tbal  : Load an Array-BDD from a file.\n");
 890   fprintf (stdout, "\tal   : Load an ADD from a file.\n");
 891   fprintf (stdout, "\taal  : Load an Array-ADD from a file.\n");
 892   fprintf (stdout, "\tcl   : Load a CNF Formula from a file.\n");
 893   fprintf (stdout, "\tcal  : Load an Array of CNF Formulas from a file.\n");
 894
 895   fprintf (stdout, "STORE\n");
 896
 897   fprintf (stdout,
 898     "\thw   : (Header) Write variable information on stdout.\n");
 899   fprintf (stdout, "\tbs   : Store a BDD into a file.\n");
 900   fprintf (stdout, "\tbas  : Store an Array-BDD from a file.\n");
 901   fprintf (stdout, "\tas   : Store an ADD into a file.\n");
 902   fprintf (stdout, "\taas  : Store an Array-ADD into a file.\n");
 903   fprintf (stdout, "\tcs   : Store BDD as a CNF formula.\n");
 904   fprintf (stdout, "\tcas  : Store and Array of BDDs as a CNF formula.\n");
 905
 906   fprintf (stdout, "MISC\n");
 907
 908   fprintf (stdout, "\tdr   : Activate Dynamic Reordering.\n");
 909   fprintf (stdout, "\tonl  : Load the order from a file (varNames).\n");
 910   fprintf (stdout, "\toil  : Load the order from a file (varAuxIds).\n");
 911   fprintf (stdout, "\tcil  : Load compose IDs from a file.\n");
 912   fprintf (stdout, "\tslm  : Set Load matchmode for variables.\n");
 913   fprintf (stdout,
 914     "\top   : Operation (or, and, xor, not, =) between BDDs.\n");
 915   fprintf (stdout, "\toc   : Create a terminal-one BDD.\n");
 916   fprintf (stdout, "\tzc   : Create a terminal-zero BDD.\n");
 917   fprintf (stdout, "\tlc   : Create a single variable BDD (1 node).\n");
 918   fprintf (stdout, "\tbc   : Create a random BDD.\n");
 919
 920   fprintf (stdout, "NOT YET IMPLEMENTED\n");
 921
 922   fprintf (stdout,
 923     "\ta2b  : Convert a file from the ASCII format to the binary one.\n");
 924   fprintf (stdout,
 925     "\tb2a  : Convert a file from the binary format to the ASCII one.\n");
 926
 927   fprintf (stdout, "HINT\n");
 928
 929   fprintf (stdout,
 930     "  Command 'mi' has to be the first instruction to build:\n");
 931   fprintf (stdout, "  a) The CUDD manager.\n");
 932   fprintf (stdout,
 933     "  b) The internal manager (containing name and variable IDs).\n");
 934   fprintf (stdout,
 935     "  After that load an header file with 'hlb' or 'hlc' to have proper\n");
 936   fprintf (stdout,
 937     "  names and ids for each subsequent load/store operation.\n");
 938
 939   return (DDDMP_SUCCESS);
 940 }
 941
 942 /**Function********************************************************************
 943
 944   Synopsis     [Load the BDD order from a file (varNames).]
 945
 946   Description  [Load the BDD order from a file (varNames).
 947     Force the orderedVarNames field of the varInfo structure,
 948     i.e., the local manager, to be stucked to this array of values.
 949     ]
 950
 951   SideEffects  []
 952
 953   SeeAlso      []
 954
 955 ******************************************************************************/
 956
 957 static int
 958 OrderNamesLoad(
 959   dddmpVarInfo_t *varInfo      /* IN/OUT: Variable Information */
 960   )
 961 {
 962   FILE *fp = NULL;
 963   int i;
 964   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
 965   char tmpBuf[DDDMPTEST_MAX_STRING_LENGTH];
 966   char tmpName[DDDMPTEST_MAX_STRING_LENGTH];
 967   char **tmpOrderedVarNames = NULL;
 968
 969   /*-------------------------  Red New Var Names Array ----------------------*/
 970
 971   ReadString (DDDMP_MESSAGE_FILE, fileName);
 972
 973   fp = fopen (fileName, "r");
 974   Dddmp_CheckAndReturn (fp==NULL, "Cannot open file.");
 975
 976   varoutinfo = DDDMP_VARNAMES;
 977   tmpOrderedVarNames = DDDMP_ALLOC (char *, varInfo->nDdVars);
 978
 979   i=0;
 980   while (fgets (tmpBuf, DDDMPTEST_MAX_STRING_LENGTH, fp)!=NULL) {
 981     if (tmpBuf[0]=='#') {
 982       continue;
 983     }
 984
 985     if (i>=varInfo->nDdVars) {
 986       fprintf (stdout,
 987         "Number of variables in files higher than DD manager vars (%d)\n",
 988         varInfo->nDdVars);
 989       fprintf (stdout, "Exceeding variables ignored\n");
 990       fprintf (stdout,
 991         "You might increase the DDDMPTEST_MAX_VARIABLE constant\n");
 992       break;
 993     }
 994
 995     sscanf (tmpBuf, "%s", tmpName);
 996     tmpOrderedVarNames[i] = DDDMP_ALLOC (char, (strlen (tmpName) + 1));
 997     if (tmpOrderedVarNames[i]==NULL) {
 998       fprintf (stdout, "Error allocating memory\n");
 999     } else {
1000       strcpy (tmpOrderedVarNames[i], tmpName);
1001     }
1002     i++;
1003   }
1004
1005   for ( ;i<varInfo->nDdVars; i++) {
1006     tmpOrderedVarNames[i] = NULL;
1007   }
1008
1009   fclose(fp);
1010
1011   /*----------------------- Free and Set Var Names Array --------------------*/
1012
1013   DddmpStrArrayFree (varInfo->orderedVarNames, varInfo->nVars);
1014   varInfo->orderedVarNames = tmpOrderedVarNames;
1015   varInfo->nVars = varInfo->nDdVars;
1016
1017   /* DO NOT ALLOW FURTHER UPDATES */
1018   varInfo->varNamesFlagUpdate = 0;
1019
1020   return (DDDMP_SUCCESS);
1021 }
1022
1023 /**Function********************************************************************
1024
1025   Synopsis     [Load the BDD order from a file (varauxids).]
1026
1027   Description  [Load the BDD order from a file (varauxids).
1028     Force the
1029     varAuxIds and varAuxIdsAll
1030     or the
1031     varComposeIds and varComposeIdsAll
1032     fields of the varInfo structure, i.e., the local manager, to be
1033     stucked to this array of values.
1034     ]
1035
1036   SideEffects  []
1037
1038   SeeAlso      []
1039
1040 ******************************************************************************/
1041
1042 static int
1043 IntArrayLoad (
1044   dddmpVarInfo_t *varInfo      /* IN/OUT: Variable Information */,
1045   const char *mode
1046   )
1047 {
1048   FILE *fp = NULL;
1049   int i;
1050   int *tmpArray1 = NULL;
1051   int *tmpArray2 = NULL;
1052   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1053   char buf[DDDMPTEST_MAX_STRING_LENGTH];
1054
1055   ReadString (DDDMP_MESSAGE_FILE, fileName);
1056
1057   fp = fopen(fileName, "r");
1058   Dddmp_CheckAndReturn (fp==NULL, "Cannot open file.");
1059
1060   tmpArray1 = DDDMP_ALLOC (int, varInfo->nDdVars);
1061   tmpArray2 = DDDMP_ALLOC (int, varInfo->nDdVars);
1062   Dddmp_CheckAndReturn (tmpArray1==NULL, "Error allocating memory.");
1063   Dddmp_CheckAndReturn (tmpArray2==NULL, "Error allocating memory.");
1064
1065   i=0;
1066   while (fgets(buf, DDDMPTEST_MAX_STRING_LENGTH, fp)!=NULL) {
1067     if (buf[0]=='#') {
1068       continue;
1069     }
1070     if (i>=varInfo->nDdVars) {
1071       fprintf (stdout,
1072         "Number of variables in files higher than DD manager vars (%d)\n",
1073         varInfo->nDdVars);
1074       fprintf (stdout, "Exceeding variables ignored.\n");
1075       fprintf (stdout, "(Increase the DDDMPTEST_MAX_VARIABLE constant.)\n");
1076       break;
1077     }
1078     sscanf(buf, "%d", &tmpArray1[i]);
1079     sscanf(buf, "%d", &tmpArray2[i++]);
1080   }
1081
1082   for (;i<varInfo->nDdVars;i++) {
1083     tmpArray1[i]= -1;
1084     tmpArray2[i]= -1;
1085   }
1086
1087   fclose(fp);
1088
1089   if (strcmp (mode, "oil") == 0) {
1090     varInfo->varAuxIds = tmpArray1;
1091     varInfo->varAuxIdsAll = tmpArray2;
1092
1093     /* DO NOT ALLOW FURTHER UPDATES */
1094     varInfo->varAuxIdsFlagUpdate = 0;
1095   } else {
1096     if (strcmp (mode, "cil") == 0) {
1097       varInfo->varComposeIds = tmpArray1;
1098       varInfo->varComposeIdsAll = tmpArray2;
1099
1100       /* DO NOT ALLOW FURTHER UPDATES */
1101       varInfo->varComposeIdsFlagUpdate = 0;
1102     }
1103   }
1104
1105   varInfo->nVars = varInfo->nDdVars;
1106   varInfo->nSuppVars = varInfo->nDdVars;
1107
1108   return (DDDMP_SUCCESS);
1109 }
1110
1111 /**Function********************************************************************
1112
1113   Synopsis     [Load a BDD from a file.]
1114
1115   Description  [Load a BDD from a file.]
1116
1117   SideEffects  []
1118
1119   SeeAlso      []
1120
1121 ******************************************************************************/
1122
1123 static int
1124 BddLoad (
1125   DdManager *ddMgr         /* IN: CUDD Manager */,
1126   DdNode **operandBdd      /* IN: Operand BDD */,
1127   dddmpVarInfo_t *varInfo  /* IN/OUT: Variable Information */
1128   )
1129 {
1130   DdNode *f = NULL;
1131   int i;
1132   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1133
1134   /*------------------------ Read Operation Operands ------------------------*/
1135
1136   ReadString (DDDMP_MESSAGE_FILE, fileName);
1137   ReadInt (DDDMP_MESSAGE_BDD, &i);
1138
1139   /*-------------------------------- Load BDD -------------------------------*/
1140
1141   fprintf (stdout, "Loading %s ...\n", fileName);
1142
1143   f = Dddmp_cuddBddLoad (ddMgr, varmatchmode, varInfo->orderedVarNames,
1144     varInfo->varIdsAll, varInfo->varComposeIdsAll, DDDMP_MODE_DEFAULT,
1145     fileName, NULL);
1146
1147   if (f==NULL) {
1148     fprintf (stderr, "Dddmp Test Error : %s is not loaded from file\n",
1149       fileName);
1150   } else {
1151     operandBdd[i] = f;
1152   }
1153
1154   /*---------------------------- Tail Operations ----------------------------*/
1155
1156   return (DDDMP_SUCCESS);
1157 }
1158
1159 /**Function********************************************************************
1160
1161   Synopsis     [Load an array of BDDs from a file.]
1162
1163   Description  [Load an array of BDDs from a file.]
1164
1165   SideEffects  []
1166
1167   SeeAlso      []
1168
1169 ******************************************************************************/
1170
1171 static int
1172 BddArrayLoad(
1173   DdManager *ddMgr            /* IN: CUDD Manager */,
1174   DdNode ***operandBddArray   /* IN: Array of operand BDD */,
1175   int *operandBddArraySize    /* IN: Number of ADD in the Array */,
1176   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1177   )
1178 {
1179   DdNode **bddArray = NULL;
1180   int i, j, nRoots;
1181   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1182
1183   /*------------------------ Read Operation Operands ------------------------*/
1184
1185   ReadString (DDDMP_MESSAGE_FILE, fileName);
1186   ReadInt (DDDMP_MESSAGE_BDD_ARRAY, &i);
1187
1188   /*---------------------------- Load BDDs ----------------------------------*/
1189
1190   nRoots = Dddmp_cuddBddArrayLoad (ddMgr, rootmatchmode,
1191     varInfo->rootNames, varmatchmode,
1192     varInfo->orderedVarNames, varInfo->varIdsAll, varInfo->varComposeIdsAll,
1193     DDDMP_MODE_DEFAULT, fileName, NULL, &bddArray);
1194
1195   Dddmp_CheckAndReturn (nRoots>DDDMP_MAX_BDDARRAY_LEN,
1196     "DDDMP_MAX_BDDARRAY_LEN exceeded by BDD array len (increase it).");
1197
1198   if (nRoots<=0) {
1199     return (DDDMP_FAILURE);
1200   }
1201
1202   varInfo->nRoots = nRoots;
1203   operandBddArray[i] = DDDMP_ALLOC (DdNode *, nRoots);
1204   Dddmp_CheckAndReturn (operandBddArray[i]==NULL, "Allocation error.");
1205
1206   for (j=0; j<nRoots; j++) {
1207     operandBddArray[i][j] = bddArray[j];
1208   }
1209   operandBddArraySize[i] = nRoots;
1210
1211   /*---------------------------- Tail Operations ----------------------------*/
1212
1213   /* free array */
1214   DDDMP_FREE (bddArray);
1215
1216   return (DDDMP_SUCCESS);
1217 }
1218
1219 /**Function********************************************************************
1220
1221   Synopsis     [Load an ADD from a file.]
1222
1223   Description  [Load an ADD from a file.]
1224
1225   SideEffects  []
1226
1227   SeeAlso      []
1228
1229 ******************************************************************************/
1230
1231 static int
1232 AddLoad(
1233   DdManager *ddMgr            /* IN: CUDD Manager */,
1234   DdNode **operandBdd         /* IN: Operand BDD */,
1235   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1236   )
1237 {
1238   DdNode *f = NULL;
1239   int i;
1240   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1241
1242   /*------------------------ Read Operation Operands ------------------------*/
1243
1244   ReadString (DDDMP_MESSAGE_FILE, fileName);
1245   ReadInt (DDDMP_MESSAGE_BDD, &i);
1246
1247   /*-------------------------------- Load ADD -------------------------------*/
1248
1249   fprintf (stdout, "Loading %s ...\n", fileName);
1250
1251   f = Dddmp_cuddAddLoad (ddMgr, varmatchmode, varInfo->orderedVarNames,
1252     varInfo->varIdsAll, varInfo->varComposeIdsAll, DDDMP_MODE_DEFAULT,
1253     fileName, NULL);
1254
1255   if (f==NULL) {
1256     fprintf (stderr, "Dddmp Test Error : %s is not loaded from file\n",
1257       fileName);
1258   } else {
1259     operandBdd[i] = f;
1260   }
1261
1262   /*---------------------------- Tail Operations ----------------------------*/
1263
1264   fprintf (stdout, "Load:\n");
1265   Cudd_PrintMinterm (ddMgr, f);
1266
1267   return (DDDMP_SUCCESS);
1268 }
1269
1270 /**Function********************************************************************
1271
1272   Synopsis     [Load an array of ADDs from a file.]
1273
1274   Description  [Load an array of ADDs from a file.]
1275
1276   SideEffects  []
1277
1278   SeeAlso      []
1279
1280 ******************************************************************************/
1281
1282 static int
1283 AddArrayLoad(
1284   DdManager *ddMgr            /* IN: CUDD Manager */,
1285   DdNode ***operandBddArray   /* IN: Array of operand BDD */,
1286   int *operandBddArraySize    /* IN: Number of ADD in the Array */,
1287   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1288   )
1289 {
1290   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1291   int i, j, nRoots;
1292   DdNode **bddArray = NULL;
1293
1294   /*------------------------ Read Operation Operands ------------------------*/
1295
1296   ReadString (DDDMP_MESSAGE_FILE, fileName);
1297   ReadInt (DDDMP_MESSAGE_BDD_ARRAY, &i);
1298
1299   /*------------------------------- Load ADDs -------------------------------*/
1300
1301   nRoots = Dddmp_cuddAddArrayLoad (ddMgr, rootmatchmode,
1302     varInfo->rootNames, varmatchmode,
1303     varInfo->orderedVarNames, varInfo->varIdsAll, varInfo->varComposeIdsAll,
1304     DDDMP_MODE_DEFAULT, fileName, NULL, &bddArray);
1305
1306   Dddmp_CheckAndReturn (nRoots>DDDMP_MAX_BDDARRAY_LEN,
1307     "DDDMP_MAX_BDDARRAY_LEN exceeded by BDD array len (increase it).");
1308
1309   if (nRoots<=0) {
1310     return (DDDMP_FAILURE);
1311   }
1312
1313   varInfo->nRoots = nRoots;
1314   operandBddArray[i] = DDDMP_ALLOC (DdNode *, nRoots);
1315   Dddmp_CheckAndReturn (operandBddArray[i]==NULL, "Allocation error.");
1316
1317   for (j=0; j<nRoots; j++) {
1318     operandBddArray[i][j] = bddArray[j];
1319   }
1320   operandBddArraySize[i] = nRoots;
1321
1322   /*---------------------------- Tail Operations ----------------------------*/
1323
1324   /* Free array */
1325   DDDMP_FREE (bddArray);
1326
1327   return (DDDMP_SUCCESS);
1328 }
1329
1330 /**Function********************************************************************
1331
1332   Synopsis     [Load a CNF formula from a file, and create a BDD.]
1333
1334   Description  [Load a CNF formula from a file, and create a BDD.]
1335
1336   SideEffects  []
1337
1338   SeeAlso      []
1339
1340 ******************************************************************************/
1341
1342 static int
1343 BddLoadCnf (
1344   DdManager *ddMgr            /* IN: CUDD Manager */,
1345   DdNode **operandBdd         /* IN: Operand BDD */,
1346   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1347   )
1348 {
1349   DdNode **rootsPtr = NULL;
1350   Dddmp_DecompCnfLoadType loadingMode = DDDMP_CNF_MODE_CONJ_QUANT;
1351   int i, retValue, nRoots;
1352   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1353
1354   /*------------------------ Read Operation Operands ------------------------*/
1355
1356   ReadString (DDDMP_MESSAGE_FILE, fileName);
1357   ReadInt (DDDMP_MESSAGE_BDD, &i);
1358
1359   /*------------------------------- Load BDDs -------------------------------*/
1360
1361   fprintf (stdout, "Loading %s ...\n", fileName);
1362
1363   retValue = Dddmp_cuddBddLoadCnf (ddMgr, varmatchmode,
1364     varInfo->orderedVarNames, varInfo->varAuxIdsAll, varInfo->varComposeIdsAll,
1365     loadingMode, fileName, NULL, &rootsPtr, &nRoots);
1366
1367   Dddmp_CheckAndGotoLabel (retValue==DDDMP_FAILURE,
1368     "Dddmp Test: Load From File Error.\n", failure);
1369
1370   operandBdd[i] = rootsPtr[0];
1371
1372   /*---------------------------- Tail Operations ----------------------------*/
1373
1374   /* Free array */
1375   DDDMP_FREE (rootsPtr);
1376
1377   return (DDDMP_SUCCESS);
1378
1379   failure:
1380     return(DDDMP_FAILURE);
1381 }
1382
1383 /**Function********************************************************************
1384
1385   Synopsis     [Load a CNF formula from a file, and create an array of
1386     BDDs.
1387   ]
1388
1389   Description  [Load a CNF formula from a file, and create an array of
1390     BDDs.
1391   ]
1392
1393   SideEffects  []
1394
1395   SeeAlso      []
1396
1397 ******************************************************************************/
1398
1399 static int
1400 BddArrayLoadCnf (
1401   DdManager *ddMgr            /* IN: CUDD Manager */,
1402   DdNode ***operandBddArray   /* IN: Array of operand BDD */,
1403   int *operandBddArraySize    /* IN: Number of ADD in the Array */,
1404   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1405   )
1406 {
1407   DdNode **rootsPtr = NULL;
1408   Dddmp_DecompCnfLoadType loadingMode = DDDMP_CNF_MODE_CONJ_QUANT;
1409   int i, j, nRoots, retValue;
1410   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1411
1412   /*------------------------ Read Operation Operands ------------------------*/
1413
1414   ReadString (DDDMP_MESSAGE_FILE, fileName);
1415   ReadInt (DDDMP_MESSAGE_BDD_ARRAY, &i);
1416
1417   /*--------------------------- Loading BDDs --------------------------------*/
1418
1419   retValue = Dddmp_cuddBddArrayLoadCnf (ddMgr, rootmatchmode,
1420     varInfo->rootNames, varmatchmode,
1421     varInfo->orderedVarNames, varInfo->varIdsAll, varInfo->varComposeIdsAll,
1422     loadingMode, fileName, NULL, &rootsPtr, &nRoots);
1423
1424   Dddmp_CheckAndReturn (nRoots>DDDMP_MAX_BDDARRAY_LEN,
1425     "DDDMP_MAX_BDDARRAY_LEN exceeded by BDD array len (increase it).");
1426
1427   if (nRoots<=0) {
1428     return (DDDMP_FAILURE);
1429   }
1430
1431   varInfo->nRoots = nRoots;
1432   operandBddArray[i] = DDDMP_ALLOC (DdNode *, nRoots);
1433   Dddmp_CheckAndReturn (operandBddArray[i]==NULL, "Allocation error.");
1434
1435   for (j=0; j<nRoots; j++) {
1436     operandBddArray[i][j] = rootsPtr[j];
1437   }
1438   operandBddArraySize[i] = nRoots;
1439
1440   /*---------------------------- Tail Operations ----------------------------*/
1441
1442   /* Free array */
1443   DDDMP_FREE (rootsPtr);
1444
1445   return (DDDMP_SUCCESS);
1446 }
1447
1448 /**Function********************************************************************
1449
1450   Synopsis     [Perform an Operation among BDDs.]
1451
1452   Description  [Perform an Operation among BDDs.]
1453
1454   SideEffects  []
1455
1456   SeeAlso      []
1457
1458 ******************************************************************************/
1459
1460 static int
1461 Operation(
1462   DdManager *ddMgr      /* IN: CUDD Manager */,
1463   DdNode **operandBdd   /* IN: Array of operandBdd */
1464   )
1465 {
1466   DdNode *f, *g, *h;
1467   char buf[DDDMPTEST_MAX_STRING_LENGTH];
1468   int i;
1469
1470   /*------------------------ Read Operation Operands ------------------------*/
1471
1472   ReadString (DDDMP_MESSAGE_OP, buf);
1473   ReadInt (DDDMP_MESSAGE_SOURCE1, &i);
1474
1475   f = operandBdd[i];
1476
1477   /*-------------------------- Compute Operation ----------------------------*/
1478
1479   if ((strcmp(buf, "or")==0)|| (strcmp(buf, "OR")==0)) {
1480     ReadInt (DDDMP_MESSAGE_SOURCE2, &i);
1481     g = operandBdd[i];
1482     h = Cudd_bddOr(ddMgr, f, g);
1483     Cudd_RecursiveDeref(ddMgr, f);
1484     Cudd_Ref(h);
1485     Cudd_RecursiveDeref(ddMgr, g);
1486   } else if ((strcmp(buf, "and")==0) || (strcmp(buf, "AND")==0)) {
1487       ReadInt (DDDMP_MESSAGE_SOURCE2, &i);
1488       g = operandBdd[i];
1489       h = Cudd_bddAnd(ddMgr, f, g);
1490       Cudd_Ref(h);
1491       Cudd_RecursiveDeref(ddMgr, f);
1492       Cudd_RecursiveDeref(ddMgr, g);
1493   } else if ((strcmp(buf, "xor")==0) || (strcmp(buf, "XOR")==0)) {
1494       ReadInt (DDDMP_MESSAGE_SOURCE2, &i);
1495       g = operandBdd[i];
1496       h = Cudd_bddXor(ddMgr, f, g);
1497       Cudd_Ref(h);
1498       Cudd_RecursiveDeref(ddMgr, f);
1499       Cudd_RecursiveDeref(ddMgr, g);
1500   } else if (strcmp(buf, "!")==0) {
1501       h = Cudd_Not(f);
1502       Cudd_Ref(h);
1503       Cudd_RecursiveDeref(ddMgr, f);
1504   } else if ((strcmp(buf, "buf")==0)|| (strcmp(buf, "BUF")==0)) {
1505       h = f;
1506   } else {
1507       fprintf (stderr, "Dddmp Test Error : Operation %s unknown\n", buf);
1508       h = NULL;
1509   }
1510
1511   ReadInt (DDDMP_MESSAGE_DESTINATION, &i);
1512
1513   operandBdd[i] = h;
1514
1515   return (DDDMP_SUCCESS);
1516 }
1517
1518 /**Function********************************************************************
1519
1520   Synopsis     [Store a BDD in a file.]
1521
1522   Description  [Store a BDD in a file.]
1523
1524   SideEffects  []
1525
1526   SeeAlso      []
1527
1528 ******************************************************************************/
1529
1530 static int
1531 BddStore (
1532   DdManager *ddMgr            /* IN: CUDD Manager */,
1533   DdNode **operandBdd         /* IN: Operand BDD */,
1534   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1535   )
1536 {
1537   DdNode *f = NULL;
1538   int i, retValue;
1539   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1540
1541   /*------------------------ Read Operation Operands ------------------------*/
1542
1543   ReadString (DDDMP_MESSAGE_FILE, fileName);
1544   ReadInt (DDDMP_MESSAGE_BDD, &i);
1545
1546   fprintf (stdout, "Storing %s ...\n", fileName);
1547   fflush (stdout);
1548   f = operandBdd[i];
1549
1550   /*----------------------------- Store BDDs -------------------------------*/
1551
1552   retValue = Dddmp_cuddBddStore(ddMgr, NULL, f, varInfo->orderedVarNames,
1553     varInfo->varAuxIdsAll, DDDMP_MODE_TEXT, varoutinfo, fileName, NULL);
1554
1555   Dddmp_CheckAndGotoLabel (retValue!=DDDMP_SUCCESS, "BDD NOT stored.",
1556     failure);
1557
1558   return (DDDMP_SUCCESS);
1559
1560   failure:
1561     return(DDDMP_FAILURE);
1562 }
1563
1564 /**Function********************************************************************
1565
1566   Synopsis     [Store an Array of BDD in a file.]
1567
1568   Description  [Store an Array of BDD in a file.]
1569
1570   SideEffects  []
1571
1572   SeeAlso      []
1573
1574 ******************************************************************************/
1575
1576 static int
1577 BddArrayStore (
1578   DdManager *ddMgr            /* IN: CUDD Manager */,
1579   DdNode ***operandBddArray   /* IN: Array of operand BDD */,
1580   int *operandBddArraySize    /* IN: Number of ADD in the Array */,
1581   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1582   )
1583 {
1584   int i, retValue, nRoots;
1585   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1586
1587   /*------------------------ Read Operation Operands ------------------------*/
1588
1589   ReadString (DDDMP_MESSAGE_FILE, fileName);
1590   ReadInt (DDDMP_MESSAGE_BDD_ARRAY, &i);
1591
1592   nRoots = operandBddArraySize[i];
1593
1594   /*----------------------------- Store BDDs -------------------------------*/
1595
1596   fprintf (stdout, "Storing Array of BDDs in file %s ...\n", fileName);
1597   fflush (stdout);
1598
1599   retValue = Dddmp_cuddBddArrayStore (ddMgr, NULL, nRoots, operandBddArray[i],
1600     NULL, varInfo->orderedVarNames, varInfo->varAuxIdsAll, DDDMP_MODE_TEXT,
1601     DDDMP_VARIDS, fileName, NULL);
1602
1603   Dddmp_CheckAndGotoLabel (retValue!=DDDMP_SUCCESS, "BDD NOT stored.",
1604     failure);
1605   fprintf (stdout, "done.\n");
1606
1607   return (DDDMP_SUCCESS);
1608
1609   failure:
1610     return(DDDMP_FAILURE);
1611 }
1612
1613 /**Function********************************************************************
1614
1615   Synopsis     [Store an ADD in a file.]
1616
1617   Description  [Store an ADD in a file.]
1618
1619   SideEffects  []
1620
1621   SeeAlso      []
1622
1623 ******************************************************************************/
1624
1625 static int
1626 AddStore(
1627   DdManager *ddMgr            /* IN: CUDD Manager */,
1628   DdNode **operandBdd         /* IN: operand Bdd */,
1629   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1630   )
1631 {
1632   DdNode *f;
1633   int i, retValue;
1634   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1635
1636   /*------------------------ Read Operation Operands ------------------------*/
1637
1638   ReadString (DDDMP_MESSAGE_FILE, fileName);
1639   ReadInt (DDDMP_MESSAGE_BDD, &i);
1640
1641   fprintf (stdout, "Storing %s ...\n", fileName);
1642   fflush (stdout);
1643   f = operandBdd[i];
1644
1645 #if 0
1646   /* StQ Patch - CREATE temporary ADD to Store */
1647   f = Cudd_addResidue (ddMgr, 4, 3, 1, 1);
1648   fprintf (stderr, "Store:\n");
1649   Cudd_PrintMinterm (ddMgr, f);
1650   /* end ... StQ Patch */
1651 #endif
1652
1653   retValue = Dddmp_cuddAddStore (ddMgr, NULL, f, varInfo->orderedVarNames,
1654     varInfo->varAuxIdsAll, DDDMP_MODE_TEXT, varoutinfo, fileName, NULL);
1655
1656   Dddmp_CheckAndReturn (retValue!=DDDMP_SUCCESS, "BDD NOT stored.");
1657
1658   return (DDDMP_SUCCESS);
1659 }
1660
1661 /**Function********************************************************************
1662
1663   Synopsis     [Store a BDD in a file.]
1664
1665   Description  [Store a BDD in a file.]
1666
1667   SideEffects  []
1668
1669   SeeAlso      []
1670
1671 ******************************************************************************/
1672
1673 static int
1674 AddArrayStore (
1675   DdManager *ddMgr            /* IN: CUDD Manager */,
1676   DdNode ***operandBddArray   /* IN: Array of operand ADD */,
1677   int *operandBddArraySize    /* IN: Number of ADD in the Array */,
1678   dddmpVarInfo_t *varInfo
1679   )
1680 {
1681   int i, retValue, nRoots;
1682   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1683
1684   /*------------------------ Read Operation Operands ------------------------*/
1685
1686   ReadString (DDDMP_MESSAGE_FILE, fileName);
1687   ReadInt (DDDMP_MESSAGE_BDD_ARRAY, &i);
1688
1689   nRoots = operandBddArraySize[i];
1690
1691   fprintf (stdout, "Storing Array of BDDs in file %s ...\n", fileName);
1692   fflush (stdout);
1693
1694   retValue = Dddmp_cuddAddArrayStore (ddMgr, NULL, nRoots, operandBddArray[i],
1695     NULL, varInfo->orderedVarNames, varInfo->varAuxIdsAll, DDDMP_MODE_TEXT,
1696     DDDMP_VARIDS, fileName, NULL);
1697
1698   Dddmp_CheckAndReturn (retValue!=DDDMP_SUCCESS, "BDD NOT stored.");
1699
1700   fprintf (stdout, "done.\n");
1701   return (DDDMP_SUCCESS);
1702 }
1703
1704 /**Function********************************************************************
1705
1706   Synopsis     [Store a BDD as CNF format in a file.]
1707
1708   Description  [Store a BDD as CNF format in a file.]
1709
1710   SideEffects  []
1711
1712   SeeAlso      []
1713
1714 ******************************************************************************/
1715
1716 static int
1717 BddStoreCnf(
1718   DdManager *ddMgr            /* IN: CUDD Manager */,
1719   DdNode **operandBdd         /* IN: Array of operand ADD */,
1720   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1721   )
1722 {
1723   DdNode *f = NULL;
1724   Dddmp_DecompCnfStoreType storingMode = DDDMP_CNF_MODE_BEST;
1725   int noHeader = 0;
1726   int i, nVars, retValue, idInitial, varNewN, clauseNewN;
1727   int edgeInTh = (-1);
1728   int pathLengthTh = (-1);
1729   int *tmpBddIds = NULL;
1730   int *tmpCnfIds = NULL;
1731   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1732   char row[DDDMPTEST_MAX_FILENAME_LENGTH];
1733
1734   /*------------------------ Read Operation Operands ------------------------*/
1735
1736   ReadString (DDDMP_MESSAGE_FILE, fileName);
1737   ReadInt (DDDMP_MESSAGE_BDD, &i);
1738   ReadString (DDDMP_MESSAGE_FORMAT, row);
1739
1740   switch (row[0]) {
1741     case 'N':
1742       storingMode = DDDMP_CNF_MODE_NODE;
1743       break;
1744     case 'M':
1745       storingMode = DDDMP_CNF_MODE_MAXTERM;
1746       break;
1747     case 'B':
1748       storingMode = DDDMP_CNF_MODE_BEST;
1749       ReadInt (DDDMP_MESSAGE_EDGE_MAX, &edgeInTh);
1750       ReadInt (DDDMP_MESSAGE_LENGHT_MAX, &pathLengthTh);
1751       break;
1752   }
1753   ReadInt (DDDMP_MESSAGE_I_ID, &idInitial);
1754
1755   fprintf (stdout, "Storing %s ...\n", fileName);
1756   fflush (stdout);
1757
1758   f = operandBdd[i];
1759
1760   nVars = varInfo->nDdVars;
1761
1762   /*------------ From BDD and CNF ids to Proper Array of ids ----------------*/
1763
1764   tmpBddIds = DDDMP_ALLOC (int, nVars);
1765   Dddmp_CheckAndGotoLabel (tmpBddIds==NULL, "Error allocating memory.",
1766     failure);
1767   tmpCnfIds = DDDMP_ALLOC (int, nVars);
1768   Dddmp_CheckAndGotoLabel (tmpBddIds==NULL, "Error allocating memory.",
1769     failure);
1770
1771   for (i=0; i<nVars; i++) {
1772     tmpBddIds[i] = i;
1773     tmpCnfIds[i] = i+1;
1774   }
1775
1776   retValue = Dddmp_cuddBddStoreCnf (ddMgr, f, storingMode, noHeader,
1777     varInfo->orderedVarNames, tmpBddIds, NULL, tmpCnfIds, idInitial,
1778     edgeInTh, pathLengthTh, fileName, NULL, &clauseNewN, &varNewN);
1779
1780   Dddmp_CheckAndGotoLabel (retValue!=DDDMP_SUCCESS, "BDD NOT stored.",
1781     failure);
1782
1783   fprintf (stdout, "Number of Clauses Stored = %d\n", clauseNewN);
1784   fprintf (stdout, "Number of New Variable Created Storing = %d\n",
1785     varNewN);
1786   fflush (stdout);
1787
1788   DDDMP_FREE (tmpBddIds);
1789   DDDMP_FREE (tmpCnfIds);
1790
1791   return (DDDMP_SUCCESS);
1792
1793   failure:
1794     DDDMP_FREE (tmpBddIds);
1795     DDDMP_FREE (tmpCnfIds);
1796
1797     return(DDDMP_FAILURE);
1798 }
1799
1800 /**Function********************************************************************
1801
1802   Synopsis     [Store a BDD as CNF format in a file.]
1803
1804   Description  [Store a BDD as CNF format in a file.]
1805
1806   SideEffects  []
1807
1808   SeeAlso      []
1809
1810 ******************************************************************************/
1811
1812 static int
1813 BddArrayStoreCnf(
1814   DdManager *ddMgr            /* IN: CUDD Manager */,
1815   DdNode ***operandBddArray   /* IN: Array of operand ADD */,
1816   int *operandBddArraySize    /* IN: Number of ADD in the Array */,
1817   dddmpVarInfo_t *varInfo     /* IN/OUT: Variable Information */
1818   )
1819 {
1820   Dddmp_DecompCnfStoreType storingMode = DDDMP_CNF_MODE_BEST;
1821   int noHeader = 0;
1822   int i, nVars, bddN, retValue, idInitial, varNewN, clauseNewN;
1823   int edgeInTh = (-1);
1824   int pathLengthTh = (-1);
1825   int *tmpBddIds = NULL;
1826   int *tmpCnfIds = NULL;
1827   char fileName[DDDMPTEST_MAX_FILENAME_LENGTH];
1828   char row[DDDMPTEST_MAX_FILENAME_LENGTH];
1829
1830   /*------------------------ Read Operation Operands ------------------------*/
1831
1832   ReadString (DDDMP_MESSAGE_FILE, fileName);
1833   ReadInt (DDDMP_MESSAGE_BDD_ARRAY, &bddN);
1834   ReadString (DDDMP_MESSAGE_FORMAT, row);
1835   switch (row[0]) {
1836     case 'N':
1837       storingMode = DDDMP_CNF_MODE_NODE;
1838       break;
1839     case 'M':
1840       storingMode = DDDMP_CNF_MODE_MAXTERM;
1841       break;
1842     case 'B':
1843       storingMode = DDDMP_CNF_MODE_BEST;
1844       ReadInt (DDDMP_MESSAGE_EDGE_MAX, &edgeInTh);
1845       ReadInt (DDDMP_MESSAGE_LENGHT_MAX, &pathLengthTh);
1846       break;
1847   }
1848   ReadInt (DDDMP_MESSAGE_I_ID, &idInitial);
1849
1850   nVars = varInfo->nDdVars;
1851
1852   /*------------ From BDD and CNF ids to Proper Array of ids ----------------*/
1853
1854   tmpBddIds = DDDMP_ALLOC (int, nVars);
1855   Dddmp_CheckAndReturn (tmpBddIds==NULL, "Allocation error.");
1856   tmpCnfIds = DDDMP_ALLOC (int, nVars);
1857   Dddmp_CheckAndReturn (tmpCnfIds==NULL, "Allocation error.");
1858
1859   for (i=0; i<nVars; i++) {
1860     tmpBddIds[i] = i;
1861     tmpCnfIds[i] = i*10+1;
1862   }
1863
1864   fprintf (stdout, "Storing %s ...\n", fileName);
1865   fflush (stdout);
1866
1867   retValue = Dddmp_cuddBddArrayStoreCnf (ddMgr, operandBddArray[bddN],
1868     operandBddArraySize[bddN], storingMode, noHeader, varInfo->orderedVarNames,
1869     tmpBddIds, NULL, tmpCnfIds, idInitial, edgeInTh, pathLengthTh, fileName,
1870     NULL, &varNewN, &clauseNewN);
1871
1872   Dddmp_CheckAndGotoLabel (retValue!=DDDMP_SUCCESS, "BDD NOT stored.",
1873     failure);
1874
1875   fprintf (stdout, "Number of Clauses Stored = %d\n", clauseNewN);
1876   fprintf (stdout, "Number of New Variable Created Storing = %d\n",
1877     varNewN);
1878   fflush (stdout);
1879
1880   DDDMP_FREE (tmpBddIds);
1881   DDDMP_FREE (tmpCnfIds);
1882
1883   return (DDDMP_SUCCESS);
1884
1885   failure:
1886     DDDMP_FREE (tmpBddIds);
1887     DDDMP_FREE (tmpCnfIds);
1888
1889     return(DDDMP_FAILURE);
1890 }
1891
1892 /**Function********************************************************************
1893
1894   Synopsis     [Dynamic Reordering BDDs.]
1895
1896   Description  [Dynamic Reordering BDDs using one of the allowed CUDD
1897     methods.]
1898
1899   SideEffects  []
1900
1901   SeeAlso      []
1902
1903 ******************************************************************************/
1904
1905 static int
1906 DynamicReordering (
1907   DdManager *ddMgr            /* IN: CUDD Manager */
1908   )
1909 {
1910   Cudd_ReorderingType approach = CUDD_REORDER_SIFT;
1911   int method;
1912
1913   /*------------------------ Read Operation Operands ------------------------*/
1914
1915   ReadInt (DDDMP_MESSAGE_REORDERING, &method);
1916   approach = (Cudd_ReorderingType) method;
1917
1918   Cudd_ReduceHeap (ddMgr, approach, 5);
1919
1920   return (DDDMP_SUCCESS);
1921 }
1922
1923 /**Function********************************************************************
1924
1925   Synopsis     [Selects variable matching mode.]
1926
1927   Description  [Selects variable matching mode.]
1928
1929   SideEffects  []
1930
1931   SeeAlso      []
1932
1933 ******************************************************************************/
1934
1935 static int
1936 SetLoadMatchmode (
1937   )
1938 {
1939   int sel;
1940   char row[DDDMPTEST_MAX_FILENAME_LENGTH];
1941
1942   fprintf (stdout, "Variable matchmode:\n");
1943   fprintf (stdout, "Match IDs                                (1)\n");
1944   fprintf (stdout, "Match permIDs                            (2)\n");
1945   fprintf (stdout, "Match names      (must have been loaded) (3)\n");
1946   fprintf (stdout, "Match auxids     (must have been loaded) (4)\n");
1947   fprintf (stdout, "Match composeids (must have been loaded) (5)\n");
1948   fprintf (stdout, "Your choice: ");
1949   fflush (stdout);
1950
1951   fgets (row, DDDMPTEST_MAX_STRING_LENGTH, stdin);
1952   sscanf (row, "%d", &sel);
1953
1954   switch (sel) {
1955     case 1:
1956       varmatchmode = DDDMP_VAR_MATCHIDS;
1957       break;
1958     case 2:
1959       varmatchmode = DDDMP_VAR_MATCHPERMIDS;
1960       break;
1961     case 3:
1962       varmatchmode = DDDMP_VAR_MATCHNAMES;
1963       break;
1964     case 4:
1965       varmatchmode = DDDMP_VAR_MATCHAUXIDS;
1966       break;
1967     case 5:
1968       varmatchmode = DDDMP_VAR_COMPOSEIDS;
1969       break;
1970     default:
1971       fprintf (stderr, "Wrong choice!\n");
1972       break;
1973   }
1974
1975   return (DDDMP_SUCCESS);
1976 }
1977
1978 /**Function********************************************************************
1979
1980   Synopsis     [Complete the internal manager structure for subsequent
1981     BDD/ADD/CNF operations.
1982   ]
1983
1984   Description  [Complete the internal manager structure for subsequent
1985     BDD/ADD/CNF operations.
1986     The phylosophy is simple: to have proper names and ids it is necessary
1987     to load an header before each actual load/store operation.
1988     An header load should initialize variable names, variable ids,
1989     variable compose ids, and variable auxiliary ids for all variables
1990     stored in the file.
1991     This information has to be extended for all variables in the
1992     *current* CUDD manager (before any store operation).
1993     CompleteInfoStruct does this job.
1994     Arrays varIds, varComposeIds, and varAuxIds contain information for
1995     all the variable in the BDD/ADD/CNF while arrays varIdsAll,
1996     varComposeIdsAll, and varAuxIdsAll contain information for *all*
1997     variable in the current CUDD manager.
1998   ]
1999
2000
2001   SideEffects  []
2002
2003   SeeAlso      []
2004
2005 ******************************************************************************/
2006
2007 static int
2008 CompleteInfoStruct (
2009   Dddmp_DecompType ddType  /* IN: selects the proper decomp type */,
2010   int nVars                /* IN: number of DD variables */,
2011   int nSuppVars            /* IN: number of support variables */,
2012   char **suppVarNames      /* IN: array of support variable names */,
2013   char **orderedVarNames   /* IN: array of variable names */,
2014   int *varIds              /* IN: array of variable ids */,
2015   int *varComposeIds       /* IN: array of permids ids */,
2016   int *varAuxIds           /* IN: array of variable aux ids */,
2017   int nRoots               /* IN: number of root in the file */,
2018   dddmpVarInfo_t *varInfo  /* IN: Variable Information */
2019   )
2020 {
2021   int i;
2022   char tmpString[DDDMPTEST_MAX_STRING_LENGTH];
2023
2024   /*------------------------- Updates Variable Names ------------------------*/
2025
2026   DddmpStrArrayFree (varInfo->suppVarNames, varInfo->nSuppVars);
2027   varInfo->suppVarNames = suppVarNames;
2028
2029   if (varInfo->varNamesFlagUpdate == 1) {
2030
2031     DddmpStrArrayFree (varInfo->orderedVarNames, varInfo->nVars);
2032
2033     if (orderedVarNames != NULL) {
2034       varInfo->orderedVarNames = orderedVarNames;
2035     } else {
2036       varInfo->orderedVarNames = DDDMP_ALLOC (char *, nVars);
2037       Dddmp_CheckAndReturn (varInfo->orderedVarNames==NULL,
2038         "Allocation error.");
2039
2040       for (i=0; i<nVars; i++) {
2041         varInfo->orderedVarNames[i] = NULL;
2042       }
2043
2044       if (varInfo->suppVarNames != NULL) {
2045         for (i=0; i<nSuppVars; i++) {
2046           varInfo->orderedVarNames[i] = DDDMP_ALLOC (char,
2047             (strlen (varInfo->suppVarNames[i]) + 1));
2048           strcpy (varInfo->orderedVarNames[i], varInfo->suppVarNames[i]);
2049         }
2050       }
2051
2052       for (i=0; i<nVars; i++) {
2053         if (varInfo->orderedVarNames[i] == NULL) {
2054           sprintf (tmpString, "DUMMY%d", i);
2055           varInfo->orderedVarNames[i] = DDDMP_ALLOC (char,
2056             (strlen (tmpString) + 1));
2057           strcpy (varInfo->orderedVarNames[i], tmpString);
2058         }
2059       }
2060     }
2061   }
2062
2063   /*------------------------------ Updates IDs ------------------------------*/
2064
2065   DDDMP_FREE (varInfo->varIds);
2066   varInfo->varIds = varIds;
2067
2068   if (varInfo->varIdsFlagUpdate == 1) {
2069
2070     /* Free Previously Allocated Memory */
2071     DDDMP_FREE (varInfo->varIdsAll);
2072
2073     /* Allocate New Memory and Check */
2074     varInfo->varIdsAll = DDDMP_ALLOC (int, nVars);
2075     Dddmp_CheckAndReturn (varInfo->varIdsAll==NULL, "Allocation error.");
2076
2077     /* Set New Values */
2078     for (i=0; i<nVars; i++) {
2079       varInfo->varIdsAll[i] = (-1);
2080     }
2081
2082     if (varInfo->varIds != NULL) {
2083       for (i=0; i<nSuppVars; i++) {
2084         varInfo->varIdsAll[varInfo->varIds[i]] = varInfo->varIds[i];
2085       }
2086     }
2087   }
2088
2089
2090   /*-------------------------- Updates Compose IDs --------------------------*/
2091
2092   DDDMP_FREE (varInfo->varComposeIds);
2093   varInfo->varComposeIds = varComposeIds;
2094
2095   if (varInfo->varComposeIdsFlagUpdate == 1) {
2096
2097     /* Free Previously Allocated Memory */
2098     DDDMP_FREE (varInfo->varComposeIdsAll);
2099
2100     /* Allocate New Memory and Check */
2101     varInfo->varComposeIdsAll = DDDMP_ALLOC (int, nVars);
2102     Dddmp_CheckAndReturn (varInfo->varComposeIdsAll==NULL,
2103       "Allocation error.");
2104
2105     /* Set New Values */
2106     for (i=0; i<nVars; i++) {
2107       varInfo->varComposeIdsAll[i] = (-1);
2108     }
2109
2110     if (varInfo->varComposeIds != NULL) {
2111       for (i=0; i<nSuppVars; i++) {
2112         varInfo->varComposeIdsAll[varInfo->varIds[i]] =
2113           varInfo->varComposeIds[i];
2114       }
2115     }
2116   }
2117
2118   /*------------------------- Updates Auxiliary IDs -------------------------*/
2119
2120   DDDMP_FREE (varInfo->varAuxIds);
2121   varInfo->varAuxIds = varAuxIds;
2122
2123   if (varInfo->varAuxIdsFlagUpdate == 1) {
2124
2125     /* Free Previously Allocated Memory */
2126     DDDMP_FREE (varInfo->varAuxIdsAll);
2127
2128     /* Allocate New Memory and Check */
2129     varInfo->varAuxIdsAll = DDDMP_ALLOC (int, nVars);
2130     Dddmp_CheckAndReturn (varInfo->varAuxIdsAll==NULL, "Allocation error.");
2131
2132     /* Set New Values */
2133     for (i=0; i<nVars; i++) {
2134       varInfo->varAuxIdsAll[i] = (-1);
2135     }
2136
2137     if (varInfo->varAuxIds != NULL) {
2138       for (i=0; i<nSuppVars; i++) {
2139         varInfo->varAuxIdsAll[varInfo->varIds[i]] = varInfo->varAuxIds[i];
2140       }
2141     }
2142   }
2143
2144   /*----------------------------- Updates Sizes -----------------------------*/
2145
2146   varInfo->ddType = ddType;
2147   varInfo->nVars = nVars;
2148   varInfo->nSuppVars = nSuppVars;
2149   Dddmp_CheckAndReturn (varInfo->nDdVars<varInfo->nVars,
2150     "Local Manager with Not Enough Variables.");
2151   varInfo->nRoots = nRoots;
2152
2153   return (DDDMP_SUCCESS);
2154 }
2155
2156 /**Function********************************************************************
2157
2158   Synopsis     [Reads an integer value from standard input.]
2159
2160   Description  [Reads an integer value from standard input.]
2161
2162   SideEffects  []
2163
2164   SeeAlso      []
2165
2166 ******************************************************************************/
2167
2168 static void
2169 ReadInt (
2170   Dddmp_MessageType message,
2171   int *i
2172   )
2173 {
2174   char row[DDDMPTEST_MAX_FILENAME_LENGTH];
2175
2176   switch (message) {
2177     case DDDMP_MESSAGE_MANAGER_VAR:
2178       fprintf (stdout, "Number of Variables: ");
2179       break;
2180     case DDDMP_MESSAGE_BDD:
2181       fprintf (stdout, "Which BDDs [0..%d]: ",
2182         DDDMPTEST_MAX_OPERAND-1);
2183       break;
2184     case DDDMP_MESSAGE_BDD_ARRAY:
2185       fprintf (stdout, "Which Array of BDDs [0..%d]: ",
2186         DDDMPTEST_MAX_OPERAND-1);
2187       break;
2188     case DDDMP_MESSAGE_CUBE:
2189       fprintf (stdout, "How many cubes [1..]: ");
2190       break;
2191     case DDDMP_MESSAGE_INDEX:
2192       fprintf (stdout, "Index: ");
2193       break;
2194     case DDDMP_MESSAGE_SOURCE1:
2195       fprintf (stdout, "Source1 [0..%d]: ", DDDMPTEST_MAX_OPERAND-1);
2196       break;
2197     case DDDMP_MESSAGE_SOURCE2:
2198       fprintf (stdout, "Source2 [0..%d]: ", DDDMPTEST_MAX_OPERAND-1);
2199       break;
2200     case DDDMP_MESSAGE_DESTINATION:
2201       fprintf (stdout, "Destination [0..%d]: ", DDDMPTEST_MAX_OPERAND-1);
2202       break;
2203     case DDDMP_MESSAGE_I_ID:
2204       fprintf (stdout, "Initial ID : ");
2205       break;
2206     case DDDMP_MESSAGE_EDGE_MAX:
2207       fprintf (stdout,
2208         "Max Number of Edges (Insert cut-point from there on) : ");
2209       break;
2210      case DDDMP_MESSAGE_LENGHT_MAX:
2211       fprintf (stdout,
2212         "Max BDD-Path Length (Insert cut-point from there on) : ");
2213       break;
2214     case DDDMP_MESSAGE_REORDERING:
2215       fprintf (stdout, "Reordering Approach (1..17): ");
2216       break;
2217     default:
2218       fprintf (stdout, "Input Generic Integer: ");
2219       break;
2220   }
2221   fflush (stdout);
2222
2223   fgets (row, DDDMPTEST_MAX_STRING_LENGTH, stdin);
2224   sscanf (row, "%d", i);
2225   fflush (stdin);
2226
2227   return;
2228 }
2229
2230
2231 /**Function********************************************************************
2232
2233   Synopsis     [Reads a string from standard input.]
2234
2235   Description  [Reads a string from standard input.]
2236
2237   SideEffects  []
2238
2239   SeeAlso      []
2240
2241 ******************************************************************************/
2242
2243 static void
2244 ReadString (
2245   Dddmp_MessageType message,
2246   char string[]
2247   )
2248 {
2249   char localString[DDDMPTEST_MAX_STRING_LENGTH];
2250
2251   switch (message) {
2252     case DDDMP_MESSAGE_PROMPT:
2253       fprintf (stdout, "TestDddmp> ");
2254       break;
2255     case DDDMP_MESSAGE_FILE:
2256       fprintf (stdout, "File : ");
2257       break;
2258     case DDDMP_MESSAGE_OP:
2259       fprintf (stdout, "Operation [or,and,xor,!,buf(=)] : ");
2260       break;
2261     case DDDMP_MESSAGE_FORMAT:
2262       fprintf (stdout, "Format (Node=N, Maxterm=M, Best=B) : ");
2263       break;
2264     default:
2265       fprintf (stdout, "Input Generic String : ");
2266       break;
2267   }
2268   fflush (stdout);
2269
2270   fgets (localString, DDDMPTEST_MAX_STRING_LENGTH, stdin);
2271   sscanf (localString, "%s", string);
2272   fflush (stdin);
2273
2274   return;
2275 }
2276
2277
2278
2279