source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/testdddmp.c @ 4597

Last change on this file since 4597 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 64.9 KB
Line 
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
57typedef 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
86typedef 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
130Dddmp_RootMatchType rootmatchmode;
131Dddmp_VarMatchType varmatchmode;
132Dddmp_VarInfoType varoutinfo;
133char varname[DDDMPTEST_MAX_STRING_LENGTH];
134
135/*---------------------------------------------------------------------------*/
136/* Macro declarations                                                        */
137/*---------------------------------------------------------------------------*/
138
139/**AutomaticStart*************************************************************/
140
141/*---------------------------------------------------------------------------*/
142/* Static function prototypes                                                */
143/*---------------------------------------------------------------------------*/
144
145static DdManager *ManagerInit (dddmpVarInfo_t *varInfo);
146static void ManagerQuit (DdManager **ddMgr, dddmpVarInfo_t *varInfo);
147static int OneCreate(DdManager *ddMgr, DdNode **operandBdd);
148static int BddZeroCreate(DdManager *ddMgr, DdNode **operandBdd);
149static int LeafCreate(DdManager *ddMgr, DdNode **operandBdd);
150static int BddCreate(DdManager *ddMgr, DdNode **operandBdd);
151static int A2B(void);
152static int B2A(void);
153static int HeaderLoadBdd(dddmpVarInfo_t *varInfo);
154static int HeaderLoadCnf(dddmpVarInfo_t *varInfo);
155static int HeaderWrite(dddmpVarInfo_t *varInfo);
156static int Help(void);
157static int OrderNamesLoad(dddmpVarInfo_t *varInfo);
158static int IntArrayLoad(dddmpVarInfo_t *varInfo, const char *mode);
159static int BddLoad(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
160static int BddArrayLoad(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
161static int AddLoad(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
162static int AddArrayLoad(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
163static int BddLoadCnf(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
164static int BddArrayLoadCnf(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
165static int Operation(DdManager *ddMgr, DdNode **operandBdd);
166static int BddStore(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
167static int BddArrayStore(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
168static int AddStore(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
169static int AddArrayStore(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
170static int BddStoreCnf(DdManager *ddMgr, DdNode **operandBdd, dddmpVarInfo_t *varInfo);
171static int BddArrayStoreCnf(DdManager *ddMgr, DdNode ***operandBddArray, int *operandBddArraySize, dddmpVarInfo_t *varInfo);
172static int DynamicReordering(DdManager *ddMgr);
173static int SetLoadMatchmode();
174static int CompleteInfoStruct(Dddmp_DecompType ddType, int nVars, int nSuppVars, char **suppVarNames, char **orderedVarNames, int *varIds, int *varComposeIds, int *varAuxIds, int nRoots, dddmpVarInfo_t *varInfo);
175static void ReadInt(Dddmp_MessageType message, int *i);
176static void ReadString(Dddmp_MessageType message, char string[]);
177
178/**AutomaticEnd***************************************************************/
179
180int
181main(
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
346static DdManager *
347ManagerInit (
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
400static void
401ManagerQuit (
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
458static int
459OneCreate(
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
487static int
488BddZeroCreate(
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
518static int
519LeafCreate(
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
551static int
552BddCreate (
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
618static int
619A2B(
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
640static int
641B2A(
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
662static int
663HeaderLoadBdd (
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
709static int
710HeaderLoadCnf (
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
755static int
756HeaderWrite(
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
867static int
868Help(
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
957static int
958OrderNamesLoad(
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
1042static int
1043IntArrayLoad (
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
1123static int
1124BddLoad (
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
1171static int
1172BddArrayLoad(
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
1231static int
1232AddLoad(
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
1282static int
1283AddArrayLoad(
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
1342static int
1343BddLoadCnf (
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
1399static int
1400BddArrayLoadCnf (
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
1460static int
1461Operation(
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
1530static int
1531BddStore (
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
1576static int
1577BddArrayStore (
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
1625static int
1626AddStore(
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
1673static int
1674AddArrayStore (
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
1716static int
1717BddStoreCnf(
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
1812static int
1813BddArrayStoreCnf(
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
1905static int
1906DynamicReordering (
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
1935static int
1936SetLoadMatchmode (
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
2007static int
2008CompleteInfoStruct (
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
2168static void
2169ReadInt (
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
2243static void
2244ReadString (
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
Note: See TracBrowser for help on using the repository browser.