Biddy  2.1.1
A multi-platform Binary Decision Diagrams package
biddyInOut.c
Go to the documentation of this file.
1 /***************************************************************************/
46 #include "biddyInt.h"
47 
48 /* the following constants are used in Biddy_Eval1() and Biddy_Eval2() */
49 #define EVAL_SIZE 4096
50 #define oNOT 0
51 #define oAND 1
52 #define oBUTNOT 2
53 #define oNOTBUT 4
54 #define oXOR 6
55 #define oOR 7
56 #define oNOR 8
57 #define oXNOR 9
58 #define oIMPLEFT 11
59 #define oIMPRIGHT 13
60 #define oNAND 14
61 
62 /* the following constants are used in Biddy_ReadVerilogFile() */
63 #define LINESIZE 999 /* maximum length of each input line read */
64 #define BUFSIZE 99999 /* maximum length of a buffer */
65 #define INOUTNUM 999 /* maximum number of inputs and outputs */
66 #define REGNUM 9999 /* maximum number of registers */
67 #define TOKENNUM 9999 /* maximum number of tokens */
68 #define GATENUM 9999 /* maximum number of gates */
69 #define LINENUM 99999 /* maximum number of lines */
70 #define WIRENUM 99999 /* maximum number of wires */
71 
72 /* the following constant and type are used in Biddy_ReadVerilogFile() */
73 /* these are recognized Verilog Boolean operators */
74 /* some of them are not common but they are used in some benchmarks */
75 /* we are trying to accept everything which is not in direct conflict with the standard */
76 /* https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ite_r_verilog_reserved_words.htm */
77 /* http://sutherland-hdl.com/pdfs/verilog_2001_ref_guide.pdf, page 3 */
78 /* http://www.externsoft.ch/download/verilog.html */
79 #define GATESNUM 9
80 const char* VerilogFileGateName[] = {
81  "buf",
82  "and",
83  "nand",
84  "or",
85  "nor",
86  "xor",
87  "xnor",
88  "not", "inv"
89 };
90 
91 /*----------------------------------------------------------------------------*/
92 /* Static function prototypes */
93 /*----------------------------------------------------------------------------*/
94 
95 /* The following functions are used in Biddy_Eval0(), Biddy_Eval1(), and Biddy_Eval1x(). */
96 
97 static Biddy_Boolean charOK(char c);
98 static void nextCh(Biddy_String s, int *i, Biddy_String *ch);
99 
100 /* Function ReadBDD()is used in Biddy_Eval0(). */
101 
102 static Biddy_Edge ReadBDD(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch);
103 
104 /* Functions createVariablesFromBTree and createBddFromBTree() are used in Biddy_Eval1() and Biddy_Eval2(). */
105 
106 static void createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, Biddy_LookupFunction lf);
107 static Biddy_Edge createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i, Biddy_LookupFunction lf);
108 
109 /* The following functions are used in Biddy_Eval1() and Biddy_Eval1x(). */
110 
111 static void evaluate1(Biddy_Manager MNG, BiddyBTreeContainer *tree, Biddy_String s, int *i, Biddy_String *ch, Biddy_LookupFunction lf);
112 static void evaluateN(Biddy_Manager MNG, BiddyBTreeContainer *tree, Biddy_String s, int *i, Biddy_String *ch, int op, Biddy_LookupFunction lf);
113 static int Op(Biddy_String s, int *i, Biddy_String *ch);
114 
115 /* The following functions are used in Biddy_ReadVerilogFile(). */
116 static void parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt);
117 static void createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c);
118 static void createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix);
119 static void parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count);
120 /* static void printModuleSummary(BiddyVerilogModule *m); */ /* currently, not used */
121 /* static void printCircuitSummary(BiddyVerilogCircuit *c); */ /* currently, not used */
122 static Biddy_Boolean isGate(Biddy_String word);
123 static Biddy_Boolean isSignalVector(Biddy_String word);
124 static Biddy_Boolean isEndOfLine(Biddy_String source);
125 static Biddy_Boolean isDefined(BiddyVerilogCircuit *c, Biddy_String name);
126 static void buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name);
127 static void buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name);
128 static int getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name);
129 static BiddyVerilogWire *getWireById(BiddyVerilogCircuit *c, int id);
130 static BiddyVerilogWire *getWireByName(BiddyVerilogCircuit *c, Biddy_String name);
131 static Biddy_String trim(Biddy_String source);
132 static void concat(char **s1, const char *s2);
133 
134 /* Function WriteBDD() is used in Biddy_PrintBDD() */
135 
136 static void WriteBDD(Biddy_Manager MNG, Biddy_String *var, FILE *s, Biddy_Edge f, unsigned int *line);
137 
138 /* The following functions are used in Biddy_PrintSOP() and Biddy_PrintMinterms() */
139 
140 static Biddy_Boolean WriteProduct(Biddy_Manager MNG, Biddy_String *var, FILE *s, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first);
141 /* static void WriteProductAlphabetic(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first); */ /* currently, not used */
142 static Biddy_Boolean WriteSOP(Biddy_Manager MNG, Biddy_String *var, FILE *s, Biddy_Edge f, Biddy_Variable top, Biddy_Boolean mark, BiddyVarList *l, unsigned int *maxsize, Biddy_Boolean combinationset);
143 
144 /* The following functions are used in Biddy_WriteDot() */
145 
146 static unsigned int enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n);
147 static void WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd);
148 static void WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd);
149 
150 /* The following functions are used in Biddy_WriteBddview() */
151 
152 static void WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f);
153 
154 /* Other functions that may be used everywhere */
155 
156 static Biddy_String getname(Biddy_Manager MNG, void *p);
157 static Biddy_String getshortname(Biddy_Manager MNG, void *p, int n);
158 
159 /*----------------------------------------------------------------------------*/
160 /* Static functions for debugging */
161 /*----------------------------------------------------------------------------*/
162 
163 
164 static void
165 printBiddyBTreeContainer(BiddyBTreeContainer *tree)
166 {
167  int i;
168  if (tree->availableNode > 0) printf("availableNode=%d\n",tree->availableNode);
169  for (i = tree->availableNode; i >= 0; i--) {
170  printf("[%d]parent=%d,left=%d,right=%d,op=%u",i,
171  tree->tnode[i].parent,
172  tree->tnode[i].left,
173  tree->tnode[i].right,
174  tree->tnode[i].op
175  );
176  if (tree->tnode[i].index != -1) {
177  printf(",index=%d",tree->tnode[i].index);
178  }
179  if (tree->tnode[i].name) {
180  printf(",name=%s\n",tree->tnode[i].name);
181  } else {
182  printf("\n");
183  }
184  }
185 }
186 
187 static void
188 printPrefixFromBTree(BiddyBTreeContainer *tree, int i)
189 {
190  if (i == -1) return;
191  if (tree->tnode[i].op == 255) {
192  if (tree->tnode[i].name) {
193  printf("%s",tree->tnode[i].name);
194  } else {
195  printf("NULL");
196  }
197  return;
198  }
199  if (tree->tnode[i].op == oNOT) printf("(NOT");
200  else if (tree->tnode[i].op == oAND) printf("(AND ");
201  else if (tree->tnode[i].op == oBUTNOT) printf("(BUTNOT ");
202  else if (tree->tnode[i].op == oNOTBUT) printf("(NOTBUT ");
203  else if (tree->tnode[i].op == oXOR) printf("(XOR ");
204  else if (tree->tnode[i].op == oOR) printf("(OR ");
205  else if (tree->tnode[i].op == oNOR) printf("(NOR ");
206  else if (tree->tnode[i].op == oXNOR) printf("(XNOR ");
207  else if (tree->tnode[i].op == oIMPLEFT) printf("(<= ");
208  else if (tree->tnode[i].op == oIMPRIGHT) printf("(=> ");
209  else if (tree->tnode[i].op == oNAND) printf("(NAND ");
210  else printf("(? ");
211  printPrefixFromBTree(tree,tree->tnode[i].left);
212  printf(" ");
213  printPrefixFromBTree(tree,tree->tnode[i].right);
214  printf(")");
215 }
216 
217 
218 /*----------------------------------------------------------------------------*/
219 /* Definition of exported functions */
220 /*----------------------------------------------------------------------------*/
221 
222 /***************************************************************************/
235 #ifdef __cplusplus
236 extern "C" {
237 #endif
238 
241 {
242  if (!MNG) MNG = biddyAnonymousManager;
243 
244  if (biddyManagerType == BIDDYTYPEOBDD) {
245  /* IMPLEMENTED */
246  }
247  else if (biddyManagerType == BIDDYTYPEOBDDC) {
248  /* IMPLEMENTED */
249  }
250 #ifndef COMPACT
251  else if (biddyManagerType == BIDDYTYPEZBDD) {
252  fprintf(stderr,"Biddy_Managed_Eval0: this BDD type is not supported, yet!\n");
253  return NULL;
254  }
255  else if (biddyManagerType == BIDDYTYPEZBDDC) {
256  fprintf(stderr,"Biddy_Managed_Eval0: this BDD type is not supported, yet!\n");
257  return NULL;
258  }
259  else if (biddyManagerType == BIDDYTYPETZBDD) {
260  fprintf(stderr,"Biddy_Managed_Eval0: this BDD type is not supported, yet!\n");
261  return NULL;
262  }
263 #endif
264  else {
265  fprintf(stderr,"Biddy_Managed_Eval0: Unsupported BDD type!\n");
266  return 0;
267  }
268 
269  return BiddyManagedEval0(MNG,s);
270 }
271 
272 #ifdef __cplusplus
273 }
274 #endif
275 
276 /***************************************************************************/
291 #ifdef __cplusplus
292 extern "C" {
293 #endif
294 
297 {
298  if (!MNG) MNG = biddyAnonymousManager;
299 
300  if (biddyManagerType == BIDDYTYPEOBDD) {
301  /* IMPLEMENTED */
302  }
303  else if (biddyManagerType == BIDDYTYPEOBDDC) {
304  /* IMPLEMENTED */
305  }
306 #ifndef COMPACT
307  else if (biddyManagerType == BIDDYTYPEZBDD) {
308  /* IMPLEMENTED */
309  }
310  else if (biddyManagerType == BIDDYTYPEZBDDC) {
311  /* IMPLEMENTED */
312  }
313  else if (biddyManagerType == BIDDYTYPETZBDD) {
314  /* IMPLEMENTED */
315  }
316 #endif
317  else {
318  fprintf(stderr,"Biddy_Managed_Eval1x: Unsupported BDD type!\n");
319  return 0;
320  }
321 
322  return BiddyManagedEval1x(MNG,s,lf);
323 }
324 
325 #ifdef __cplusplus
326 }
327 #endif
328 
329 /***************************************************************************/
347 #ifdef __cplusplus
348 extern "C" {
349 #endif
350 
353 {
354  if (!MNG) MNG = biddyAnonymousManager;
355 
356  if (biddyManagerType == BIDDYTYPEOBDD) {
357  /* IMPLEMENTED */
358  }
359  else if (biddyManagerType == BIDDYTYPEOBDDC) {
360  /* IMPLEMENTED */
361  }
362 #ifndef COMPACT
363  else if (biddyManagerType == BIDDYTYPEZBDD) {
364  /* IMPLEMENTED */
365  }
366  else if (biddyManagerType == BIDDYTYPEZBDDC) {
367  /* IMPLEMENTED */
368  }
369  else if (biddyManagerType == BIDDYTYPETZBDD) {
370  /* IMPLEMENTED */
371  }
372 #endif
373  else {
374  fprintf(stderr,"Biddy_Managed_Eval2: Unsupported BDD type!\n");
375  return 0;
376  }
377 
378  return BiddyManagedEval2(MNG,boolFunc);
379 }
380 
381 #ifdef __cplusplus
382 }
383 #endif
384 
385 /***************************************************************************/
403 #ifdef __cplusplus
404 extern "C" {
405 #endif
406 
408 Biddy_Managed_ReadBddview(Biddy_Manager MNG, const char filename[],
409  Biddy_String name)
410 {
411  if (!MNG) MNG = biddyAnonymousManager;
412 
413  if (biddyManagerType == BIDDYTYPEOBDD) {
414  /* IMPLEMENTED */
415  }
416  else if (biddyManagerType == BIDDYTYPEOBDDC) {
417  /* IMPLEMENTED */
418  }
419 #ifndef COMPACT
420  else if (biddyManagerType == BIDDYTYPEZBDD) {
421  /* IMPLEMENTED */
422  }
423  else if (biddyManagerType == BIDDYTYPEZBDDC) {
424  /* IMPLEMENTED */
425  }
426  else if (biddyManagerType == BIDDYTYPETZBDD) {
427  /* IMPLEMENTED */
428  }
429 #endif
430  else {
431  fprintf(stderr,"Biddy_Managed_ReadBddview: Unsupported BDD type!\n");
432  return 0;
433  }
434 
435  return BiddyManagedReadBddview(MNG,filename,name);
436 }
437 
438 #ifdef __cplusplus
439 }
440 #endif
441 
442 /***************************************************************************/
458 #ifdef __cplusplus
459 extern "C" {
460 #endif
461 
462 void
463 Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[],
464  Biddy_String prefix)
465 {
466  if (!MNG) MNG = biddyAnonymousManager;
467 
468  if (biddyManagerType == BIDDYTYPEOBDD) {
469  /* IMPLEMENTED */
470  }
471  else if (biddyManagerType == BIDDYTYPEOBDDC) {
472  /* IMPLEMENTED */
473  }
474 #ifndef COMPACT
475  else if (biddyManagerType == BIDDYTYPEZBDD) {
476  /* IMPLEMENTED */
477  }
478  else if (biddyManagerType == BIDDYTYPEZBDDC) {
479  /* IMPLEMENTED */
480  }
481  else if (biddyManagerType == BIDDYTYPETZBDD) {
482  /* IMPLEMENTED */
483  }
484 #endif
485  else {
486  fprintf(stderr,"Biddy_Managed_ReadVerilogFile: Unsupported BDD type!\n");
487  return;
488  }
489 
490  BiddyManagedReadVerilogFile(MNG,filename,prefix);
491 }
492 
493 #ifdef __cplusplus
494 }
495 #endif
496 
497 /***************************************************************************/
511 #ifdef __cplusplus
512 extern "C" {
513 #endif
514 
515 void
516 Biddy_Managed_PrintBDD(Biddy_Manager MNG, Biddy_String *var, const char filename[],
517  Biddy_Edge f, Biddy_String label)
518 {
519  if (!MNG) MNG = biddyAnonymousManager;
520 
521  if (biddyManagerType == BIDDYTYPEOBDD) {
522  /* IMPLEMENTED */
523  }
524  else if (biddyManagerType == BIDDYTYPEOBDDC) {
525  /* IMPLEMENTED */
526  }
527 #ifndef COMPACT
528  else if (biddyManagerType == BIDDYTYPEZBDD) {
529  /* IMPLEMENTED */
530  }
531  else if (biddyManagerType == BIDDYTYPEZBDDC) {
532  /* IMPLEMENTED */
533  }
534  else if (biddyManagerType == BIDDYTYPETZBDD) {
535  /* IMPLEMENTED */
536  }
537 #endif
538  else {
539  fprintf(stderr,"Biddy_Managed_PrintBDD: Unsupported BDD type!\n");
540  return;
541  }
542 
543  BiddyManagedPrintBDD(MNG,var,filename,f,label);
544 }
545 
546 #ifdef __cplusplus
547 }
548 #endif
549 
550 /***************************************************************************/
565 #ifdef __cplusplus
566 extern "C" {
567 #endif
568 
569 void
570 Biddy_Managed_PrintTable(Biddy_Manager MNG, Biddy_String *var, const char filename[],
571  Biddy_Edge f)
572 {
573  if (!MNG) MNG = biddyAnonymousManager;
574 
575  if (biddyManagerType == BIDDYTYPEOBDD) {
576  /* IMPLEMENTED */
577  }
578  else if (biddyManagerType == BIDDYTYPEOBDDC) {
579  /* IMPLEMENTED */
580  }
581 #ifndef COMPACT
582  else if (biddyManagerType == BIDDYTYPEZBDD) {
583  /* IMPLEMENTED */
584  }
585  else if (biddyManagerType == BIDDYTYPEZBDDC) {
586  /* IMPLEMENTED */
587  }
588  else if (biddyManagerType == BIDDYTYPETZBDD) {
589  /* IMPLEMENTED */
590  }
591 #endif
592  else {
593  fprintf(stderr,"Biddy_Managed_PrintTable: Unsupported BDD type!\n");
594  return;
595  }
596 
597  BiddyManagedPrintTable(MNG,var,filename,f);
598 }
599 
600 #ifdef __cplusplus
601 }
602 #endif
603 
604 /***************************************************************************/
618 #ifdef __cplusplus
619 extern "C" {
620 #endif
621 
622 void
623 Biddy_Managed_PrintSOP(Biddy_Manager MNG, Biddy_String *var, const char filename[],
624  Biddy_Edge f)
625 {
626  if (!MNG) MNG = biddyAnonymousManager;
627 
628  if (biddyManagerType == BIDDYTYPEOBDD) {
629  /* IMPLEMENTED */
630  }
631  else if (biddyManagerType == BIDDYTYPEOBDDC) {
632  /* IMPLEMENTED */
633  }
634 #ifndef COMPACT
635  else if (biddyManagerType == BIDDYTYPEZBDD) {
636  /* IMPLEMENTED */
637  }
638  else if (biddyManagerType == BIDDYTYPEZBDDC) {
639  /* IMPLEMENTED */
640  }
641  else if (biddyManagerType == BIDDYTYPETZBDD) {
642  /* IMPLEMENTED */
643  }
644 #endif
645  else {
646  fprintf(stderr,"Biddy_Managed_PrintSOP: Unsupported BDD type!\n");
647  return;
648  }
649 
650  BiddyManagedPrintSOP(MNG,var,filename,f);
651 }
652 
653 #ifdef __cplusplus
654 }
655 #endif
656 
657 /***************************************************************************/
675 #ifdef __cplusplus
676 extern "C" {
677 #endif
678 
679 void
680 Biddy_Managed_PrintMinterms(Biddy_Manager MNG, Biddy_String *var, const char filename[],
681  Biddy_Edge f, Biddy_Boolean negative)
682 {
683  if (!MNG) MNG = biddyAnonymousManager;
684 
685  if (biddyManagerType == BIDDYTYPEOBDD) {
686  /* IMPLEMENTED */
687  }
688  else if (biddyManagerType == BIDDYTYPEOBDDC) {
689  /* IMPLEMENTED */
690  }
691 #ifndef COMPACT
692  else if (biddyManagerType == BIDDYTYPEZBDD) {
693  /* IMPLEMENTED */
694  }
695  else if (biddyManagerType == BIDDYTYPEZBDDC) {
696  /* IMPLEMENTED */
697  }
698  else if (biddyManagerType == BIDDYTYPETZBDD) {
699  /* IMPLEMENTED */
700  }
701 #endif
702  else {
703  fprintf(stderr,"Biddy_Managed_PrintMinterms: Unsupported BDD type!\n");
704  return;
705  }
706 
707  BiddyManagedPrintMinterms(MNG,var,filename,f,negative);
708 }
709 
710 #ifdef __cplusplus
711 }
712 #endif
713 
714 /***************************************************************************/
731 #ifdef __cplusplus
732 extern "C" {
733 #endif
734 
735 unsigned int
736 Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f,
737  const char label[], int id, Biddy_Boolean cudd)
738 {
739  if (!MNG) MNG = biddyAnonymousManager;
740 
741  if (biddyManagerType == BIDDYTYPEOBDD) {
742  /* IMPLEMENTED */
743  }
744  else if (biddyManagerType == BIDDYTYPEOBDDC) {
745  /* IMPLEMENTED */
746  }
747 #ifndef COMPACT
748  else if (biddyManagerType == BIDDYTYPEZBDD) {
749  /* IMPLEMENTED */
750  }
751  else if (biddyManagerType == BIDDYTYPEZBDDC) {
752  /* IMPLEMENTED */
753  }
754  else if (biddyManagerType == BIDDYTYPETZBDD) {
755  /* IMPLEMENTED */
756  }
757 #endif
758  else {
759  fprintf(stderr,"Biddy_Managed_WriteDot: Unsupported BDD type!\n");
760  return 0;
761  }
762 
763  return BiddyManagedWriteDot(MNG,filename,f,label,id,cudd);
764 }
765 
766 #ifdef __cplusplus
767 }
768 #endif
769 
770 /***************************************************************************/
787 #ifdef __cplusplus
788 extern "C" {
789 #endif
790 
791 unsigned int
792 Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[],
793  Biddy_Edge f, const char label[], void *xytable)
794 {
795  if (!MNG) MNG = biddyAnonymousManager;
796 
797  if (biddyManagerType == BIDDYTYPEOBDD) {
798  /* IMPLEMENTED */
799  }
800  else if (biddyManagerType == BIDDYTYPEOBDDC) {
801  /* IMPLEMENTED */
802  }
803 #ifndef COMPACT
804  else if (biddyManagerType == BIDDYTYPEZBDD) {
805  /* IMPLEMENTED */
806  }
807  else if (biddyManagerType == BIDDYTYPEZBDDC) {
808  /* IMPLEMENTED */
809  }
810  else if (biddyManagerType == BIDDYTYPETZBDD) {
811  /* IMPLEMENTED */
812  }
813 #endif
814  else {
815  fprintf(stderr,"Biddy_Managed_WriteBddview: Unsupported BDD type!\n");
816  return 0;
817  }
818 
819  return BiddyManagedWriteBddview(MNG,filename,f,label,xytable);
820 }
821 
822 #ifdef __cplusplus
823 }
824 #endif
825 
826 /*----------------------------------------------------------------------------*/
827 /* Definition of internal functions used to implement external functions */
828 /*----------------------------------------------------------------------------*/
829 
830 /***************************************************************************/
840 BiddyManagedEval0(Biddy_Manager MNG, Biddy_String s)
841 {
842  int i;
843  Biddy_String ch;
844  Biddy_String name;
845  Biddy_Edge f;
846 
847  assert( MNG );
848 
849  ch = (Biddy_String) malloc(255); /* max variable name length */
850 
851  i = 0;
852  nextCh(s,&i,&ch);
853  name = strdup(ch);
854 
855  f = ReadBDD(MNG,s,&i,&ch);
856 
857  if (BiddyIsNull(f)) {
858  printf("(BiddyManagedEval0) ERROR: char %d\n",i);
859  free(ch);
860  return((Biddy_String)"");
861  } else {
862  BiddyManagedAddPersistentFormula(MNG,name,f);
863  }
864 
865  nextCh(s,&i,&ch);
866  if (strcmp(ch,"")) {
867  printf("(BiddyManagedEval0) ERROR: extra characters\n");
868  free(ch);
869  return((Biddy_String)"");
870  }
871 
872  free(ch);
873 
874  return(name);
875 }
876 
877 /***************************************************************************/
891 BiddyManagedEval1x(Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
892 {
893  Biddy_String ch;
894  int i;
895  BiddyBTreeContainer *tree;
896  Biddy_Edge fbdd; /* result */
897 
898  assert( MNG );
899 
900  /* DEBUGGING */
901  /*
902  printf("BiddyManagedEval1x: %s\n",s);
903  */
904 
905  tree = (BiddyBTreeContainer *) calloc(1, sizeof(BiddyBTreeContainer));
906  if (!tree) return biddyNull;
907  tree->tnode = (BiddyBTreeNode*) malloc(EVAL_SIZE * sizeof(BiddyBTreeNode));
908  if (!tree->tnode) return biddyNull;
909  tree->availableNode = -1;
910  for (i = EVAL_SIZE-1; i >= 0; i--) {
911  tree->tnode[i].name = NULL;
912  tree->tnode[i].op = -1;
913  tree->tnode[i].index = -1; /* not used in Eval1 */
914  tree->tnode[i].left = -1;
915  tree->tnode[i].right = -1;
916  tree->tnode[i].parent = tree->availableNode;
917  tree->availableNode = i;
918  }
919 
920  ch = (Biddy_String) malloc(255);
921 
922  i = 0;
923  nextCh(s,&i,&ch);
924 
925  evaluate1(MNG,tree,s,&i,&ch,lf);
926 
927  tree->tnode[0].parent = 0;
928  tree->tnode[0].right = tree->availableNode;
929  tree->tnode[tree->availableNode].parent = 0;
930 
931  free(ch);
932 
933  /*
934  printBiddyBTreeContainer(tree);
935  */
936 
937  /*
938  printf("%s\n",s);
939  printPrefixFromBTree(tree,tree->tnode[0].right);
940  printf("\n");
941  */
942 
943 #ifndef COMPACT
944 
945  /* FOR SOME BDD TYPES, IT IS NECESSARY TO CREATE ALL VARIABLES IN ADVANCE */
946  /* createBddFromBTree DOES NOT STORE TMP RESULTS AS FORMULAE AND THUS */
947  /* TMP RESULTS BECOME WRONG IF NEW VARIABLES ARE ADDED ON-THE-FLY */
948 
949  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
950  {
951  createVariablesFromBTree(MNG,tree,NULL);
952  }
953 
954  if (biddyManagerType == BIDDYTYPETZBDD)
955  {
956  createVariablesFromBTree(MNG,tree,NULL);
957  }
958 
959 #endif
960 
961  fbdd = createBddFromBTree(MNG,tree,tree->tnode[0].right,lf);
962 
963  for (i = EVAL_SIZE-1; i >= 0; i--) {
964  if (tree->tnode[i].name) free(tree->tnode[i].name);
965  }
966  free(tree->tnode);
967  free(tree);
968 
969  return fbdd;
970 }
971 
972 /***************************************************************************/
981 /*
982 boolOperators[] should be compatible with global macros:
983 #define oNOT 0
984 #define oAND 1
985 #define oBUTNOT 2
986 #define oNOTBUT 4
987 #define oXOR 6
988 #define oOR 7
989 #define oNOR 8
990 #define oXNOR 9
991 #define oIMPLEFT 11
992 #define oIMPRIGHT 13
993 #define oNAND 14
994 */
995 
997 BiddyManagedEval2(Biddy_Manager MNG, Biddy_String boolFunc)
998 {
999  /* NOT (~!), AND (&*), BUTNOT (\), NOTBUT (/), XOR (^%), OR (|+), NOR (#), XNOR(-), IMPLIES-LEFT (<), IMPLIES-RIGHT (>), NAND (@) */
1000  char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' };
1001  int tempPos,currStringPos,currTreePos,oldTreePos; /* tmp variables */
1002  int offset; /* this is used for implementation of parenthesis and operator's priority */
1003  char currS;
1004  int i,j;
1005  BiddyBTreeContainer *tree;
1006  Biddy_Edge fbdd; /* result */
1007  Biddy_String expression;
1008 
1009  assert( MNG );
1010 
1011  i = 0; j = 0;
1012  tree = (BiddyBTreeContainer *) calloc(1, sizeof(BiddyBTreeContainer));
1013  if (!tree) return biddyNull;
1014  tree->tnode = (BiddyBTreeNode*) malloc(EVAL_SIZE * sizeof(BiddyBTreeNode));
1015  if (!tree->tnode) return biddyNull;
1016  tree->availableNode = -1;
1017  for (i = EVAL_SIZE-1; i > 0; i--) {
1018  tree->tnode[i].name = NULL;
1019  tree->tnode[i].parent = tree->availableNode;
1020  tree->availableNode = i;
1021  }
1022  tree->tnode[0].index = 0;
1023  tree->tnode[0].name = NULL;
1024 
1025  tempPos = 0;
1026  currStringPos = 0;
1027  currTreePos = 1;
1028  oldTreePos = 0;
1029  offset = 0;
1030  expression = strdup(boolFunc);
1031  currS = expression[currStringPos];
1032  while (currS > '\n') {
1033  if (currS == ' ') {
1034  /* WHITE SPACE */
1035  currStringPos++;
1036  currS = expression[currStringPos];
1037  continue;
1038  }
1039  currTreePos = tree->availableNode;
1040  if (currTreePos != -1) {
1041  tree->availableNode = tree->tnode[tree->availableNode].parent;
1042  } else {
1043  fprintf(stderr,"BiddyManagedEval2: ERROR WITH tree->availableNode\n");
1044  return biddyNull;
1045  }
1046  if (j == 0) {
1047  tree->tnode[oldTreePos].right = currTreePos;
1048  tree->tnode[currTreePos].parent = oldTreePos;
1049  tree->tnode[currTreePos].left = -1;
1050  if (currS == '!') currS = '~'; /* operator '!' is also allowed for negation */
1051  if (currS == boolOperators[0]) {
1052  /* UNARY OPERATOR NOT */
1053  tree->tnode[currTreePos].op = 0;
1054  tree->tnode[currTreePos].index = offset + 3;
1055  }
1056  else if ((currS == '(') || (currS == '[') || (currS == '{')) {
1057  /* OPEN PARENTHESIS */
1058  offset += 4; currStringPos++;
1059  currS = expression[currStringPos];
1060  continue;
1061  }
1062  else if ((currS == '_') || ((currS >= '0') && (currS <= '9')) || ((currS >= 'A') && (currS <= 'Z')) || ((currS >= 'a') && (currS <= 'z'))) {
1063  /* CONSTANT OR VARIABLE NAME */
1064  tree->tnode[currTreePos].right = -1;
1065  tree->tnode[currTreePos].op = 255;
1066  tree->tnode[currTreePos].index = currStringPos;
1067  while ((currS == '_') || ((currS >= '0') && (currS <= '9')) || ((currS >= 'A') && (currS <= 'Z')) || ((currS >= 'a') && (currS <= 'z'))) {
1068  currStringPos++;
1069  currS = expression[currStringPos];
1070  }
1071  expression[currStringPos] = 0;
1072  tree->tnode[currTreePos].name = strdup(&expression[tree->tnode[currTreePos].index]);
1073  tree->tnode[currTreePos].index = (int) strlen(tree->tnode[currTreePos].name); /* length of the variable name */
1074  expression[currStringPos] = currS;
1075  currStringPos--;
1076  j = 1;
1077  }
1078  else {
1079  /* printf("ERROR: MISSING OR INVALID VARIABLE NAME\n"); */
1080  break;
1081  }
1082  }
1083  else if (j == 1) {
1084  /* CLOSE PARENTHESIS */
1085  if ((currS == ')') || (currS == ']') || (currS == '}')) {
1086  offset -= 4; currStringPos++;
1087  currS = expression[currStringPos];
1088  if (offset < 0) {
1089  /* printf("ERROR: INVALID CLOSE PARENTHESIS\n"); */
1090  j = 0;
1091  break;
1092  }
1093  continue;
1094  }
1095  else {
1096  /* BOOLEAN BINARY OPERATOR */
1097  j = 0;
1098  if (currS == '*') currS = '&'; /* operator '*' is also allowed for conjunction */
1099  if (currS == '+') currS = '|'; /* operator '+' is also allowed for disjunction */
1100  if (currS == '%') currS = '^'; /* operator '%' is also allowed for xor */
1101  for (i = 0; i < 16; i++) { if (boolOperators[i] == currS) { break; } }
1102  if (i == 0) {
1103  /* printf("ERROR:INVALID USE OF UNARY OPERATOR ~\n"); */
1104  break;
1105  }
1106  else if ((i < 16) && (boolOperators[i] != ' ')) {
1107  tree->tnode[currTreePos].op = (char) i;
1108  if (i == 1) { tree->tnode[currTreePos].index = offset + 3; }
1109  else if ((i == 2) || (i == 4)) { tree->tnode[currTreePos].index = offset + 3; }
1110  else if ((i == 6) || (i == 7) || (i == 14)) { tree->tnode[currTreePos].index = offset + 2; }
1111  else { tree->tnode[currTreePos].index = offset + 1; }
1112  oldTreePos = tree->tnode[oldTreePos].parent;
1113  while (tree->tnode[oldTreePos].index >= tree->tnode[currTreePos].index) {
1114  oldTreePos = tree->tnode[oldTreePos].parent;
1115  }
1116  tempPos = tree->tnode[oldTreePos].right;
1117  tree->tnode[oldTreePos].right = currTreePos;
1118  tree->tnode[tempPos].parent = currTreePos;
1119  tree->tnode[currTreePos].parent = oldTreePos;
1120  tree->tnode[currTreePos].left = tempPos;
1121  }
1122  else {
1123  /* printf("ERROR: MISSING OPERATOR OR INVALID BOOLEAN OPERATOR %c\n",currS); */
1124  break;
1125  }
1126  }
1127  }
1128  currStringPos++;
1129  currS = expression[currStringPos];
1130  oldTreePos = currTreePos;
1131  }
1132 
1133  if (j == 0) {
1134  /* printf("ERROR: INCORRECT PARENTHESIS IN THE EXPRESSION\n"); */
1135  return biddyNull;
1136  }
1137 
1138  /*
1139  printBiddyBTreeContainer(tree);
1140  */
1141 
1142  /*
1143  printf("%s\n",expression);
1144  printPrefixFromBTree(tree,tree->tnode[0].right);
1145  printf("\n");
1146  */
1147 
1148  free(expression);
1149 
1150 #ifndef COMPACT
1151 
1152  /* FOR SOME BDD TYPES, IT IS NECESSARY TO CREATE ALL VARIABLES IN ADVANCE */
1153  /* createBddFromBTree DOES NOT STORE TMP RESULTS AS FORMULAE AND THUS */
1154  /* TMP RESULTS BECOME WRONG IF NEW VARIABLES ARE ADDED ON-THE-FLY */
1155 
1156  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
1157  {
1158  createVariablesFromBTree(MNG,tree,NULL);
1159  }
1160 
1161  if (biddyManagerType == BIDDYTYPETZBDD)
1162  {
1163  createVariablesFromBTree(MNG,tree,NULL);
1164  }
1165 
1166 #endif
1167 
1168  fbdd = createBddFromBTree(MNG,tree,tree->tnode[0].right,NULL);
1169 
1170  for (i = EVAL_SIZE-1; i >= 0; i--) {
1171  if (tree->tnode[i].name) free(tree->tnode[i].name);
1172  }
1173  free(tree->tnode);
1174  free(tree);
1175 
1176  return fbdd;
1177 }
1178 
1179 /***************************************************************************/
1189 BiddyManagedReadBddview(Biddy_Manager MNG, const char filename[],
1190  Biddy_String name)
1191 {
1192  FILE *bddfile;
1193  char buffer[65536]; /* line with variables can be very long! */
1194  char code[4];
1195  Biddy_String word,word2,line;
1196  BiddyVariableOrder *tableV;
1197  BiddyNodeList *tableN;
1198  BiddyFormulaList *tableF;
1199  int numV,numN,numF;
1200  int i,n,m; /* this must be signed because they are used in a special "for" loop */
1201  Biddy_Boolean typeOK;
1202  Biddy_String namelist;
1203 
1204 #ifndef COMPACT
1205  char buffer2[256];
1206 #endif
1207 
1208  assert( MNG );
1209 
1210  bddfile = fopen(filename,"r");
1211  if (!bddfile) {
1212  printf("BiddyManagedReadBddview: File error (%s)!\n",filename);
1213  return NULL;
1214  }
1215 
1216  numV = 0;
1217  numN = 0;
1218  numF = 0;
1219  tableV = NULL;
1220  tableN = NULL;
1221  tableF = NULL;
1222  typeOK = FALSE;
1223 
1224  namelist = NULL;
1225  if (name) namelist = strdup(name);
1226 
1227  /* PARSE FILE */
1228 
1229  line = fgets(buffer,65535,bddfile);
1230  while (line) {
1231 
1232  line = trim(line);
1233 
1234  /* DEBUGGING */
1235  /*
1236  printf("<%s>\n",line);
1237  */
1238 
1239  if (line[0] == '#') { /* skip the comment line */
1240  line = fgets(buffer,65535,bddfile);
1241  continue;
1242  }
1243  else if ((line[0] == 'c') && !strncmp(line,"connect",7)) { /* parsing line with a connection */
1244  line = &line[8];
1245  word = word2 = NULL;
1246 #ifdef COMPACT
1247  sscanf(line,"%u %u %s",&n,&m,code);
1248 #else
1249  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
1250  buffer[0] = buffer2[0] = 0;
1251  sscanf(line,"%u %u %s %s",&n,&m,code,buffer);
1252  if ((code[0] == 'e') || (code[0] == 'd'))
1253  {
1254  sscanf(line,"%u %u %s %s %s",&n,&m,code,buffer,buffer2);
1255  }
1256  if (buffer[0] == '"') {
1257  buffer[strlen(buffer)-1] = 0;
1258  word = &buffer[1];
1259  } else {
1260  if (buffer[0]) word = &buffer[0];
1261  }
1262  if (buffer2[0] == '"') {
1263  buffer2[strlen(buffer2)-1] = 0;
1264  word2= &buffer2[1];
1265  } else {
1266  if (buffer2[0]) word2 = &buffer2[0];
1267  }
1268  } else {
1269  sscanf(line,"%u %u %s",&n,&m,code);
1270  }
1271 #endif
1272  if (word2) {
1273  tableN[n].ltag = BiddyManagedGetVariable(MNG,word);
1274  tableN[n].rtag = BiddyManagedGetVariable(MNG,word2);
1275  } else if (word) {
1276  /* if (!strcmp(code,"l") || !strcmp(code,"s") || !strcmp(code,"si")) */
1277  if ((code[0] == 'l') || (code[0] == 's'))
1278  {
1279  tableN[n].ltag = BiddyManagedGetVariable(MNG,word);
1280  }
1281  /* else if (!strcmp(code,"r") || !strcmp(code,"ri")) */
1282  else if (code[0] == 'r')
1283  {
1284  tableN[n].rtag = BiddyManagedGetVariable(MNG,word);
1285  }
1286  /* else if (!strcmp(code,"e") || !strcmp(code,"di")) */
1287  else if ((code[0] == 'e') || (code[0] == 'd'))
1288  {
1289  tableN[n].ltag = tableN[n].rtag = BiddyManagedGetVariable(MNG,word);
1290  }
1291  }
1292  /* if (!strcmp(code,"s")) */
1293  if ((code[0] == 's') && (code[1] == 0))
1294  { /* regular label */
1295  /* this is default type for all bdd types */
1296  tableN[n].l = m;
1297  }
1298  /* else if (!strcmp(code,"si")) */
1299  else if ((code[0] == 's') && (code[1] != 0))
1300  { /* complemented label */
1301  /* for OBDD, this is not allowed */
1302  /* for OBDDC, this is type 3 */
1303  /* for ZBDD, this is not allowed */
1304  /* for ZBDDC, this is type 3 */
1305  /* for TZBDD, this is not allowed */
1306  /* for TZBDDC, this is type 3 */
1307  tableN[n].l = m;
1308  if (biddyManagerType == BIDDYTYPEOBDDC) {
1309  tableN[n].type = 3;
1310  }
1311 #ifndef COMPACT
1312  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1313  tableN[n].type = 3;
1314  }
1315  else if (biddyManagerType == BIDDYTYPETZBDDC) {
1316  tableN[n].type = 3;
1317  } else {
1318  printf("BiddyManagedReadBddview: Problem with connection - wrong code\n");
1319  return NULL;
1320  }
1321 #endif
1322  }
1323  /* else if (!strcmp(code,"l")) */
1324  else if ((code[0] == 'l') && (code[1] == 0))
1325  { /* regular left successor */
1326  /* this is default type for all bdd types, this can be changed by right successor */
1327  tableN[n].l = m;
1328  }
1329  /* else if (!strcmp(code,"li")) */
1330  else if ((code[0] == 'l') && (code[1] != 0))
1331  { /* complemented left successor */
1332  /* for OBDD, this is not allowed */
1333  /* for OBDDC, this is type 5 */
1334  /* for ZBDD, this is not allowed */
1335  /* for ZBDDC, this is not allowed */
1336  /* for TZBDD, this is not allowed */
1337  /* for TZBDDC, this is not allowed */
1338  tableN[n].l = m;
1339  if (biddyManagerType == BIDDYTYPEOBDDC) {
1340  tableN[n].type = 5;
1341  } else {
1342  printf("BiddyManagedReadBddview: Problem with connection - wrong code\n");
1343  return NULL;
1344  }
1345  }
1346  /* else if (!strcmp(code,"r")) */
1347  else if ((code[0] == 'r') && (code[1] == 0))
1348  { /* regular right successor */
1349  /* this is default type for all bdd types, this can be changed by left successor */
1350  tableN[n].r = m;
1351  }
1352  /* else if (!strcmp(code,"ri")) */
1353 #ifndef COMPACT
1354  else if ((code[0] == 'r') && (code[1] != 0))
1355  { /* complemented right successor */
1356  tableN[n].r = m;
1357  /* for OBDD, this is not allowed */
1358  /* for OBDDC, this is not allowed */
1359  /* for ZBDD, this is not allowed */
1360  /* for ZBDDC, this is type 5 */
1361  /* for TZBDD, this is not allowed */
1362  /* for TZBDDC, this is type 5 */
1363  if (biddyManagerType == BIDDYTYPEZBDDC) {
1364  tableN[n].type = 5;
1365  }
1366  else if (biddyManagerType == BIDDYTYPETZBDDC) {
1367  tableN[n].type = 5;
1368  } else {
1369  printf("BiddyManagedReadBddview: Problem with connection - wrong code\n");
1370  return NULL;
1371  }
1372  }
1373 #endif
1374  /* else if (!strcmp(code,"d")) */
1375  else if ((code[0] == 'd') && (code[1] == 0))
1376  { /* double line, type 'd' */
1377  tableN[n].l = tableN[n].r = m;
1378  /* for OBDD, this is not allowed */
1379  /* for OBDDC, this is type 5 */
1380  /* for ZBDD, this is not allowed */
1381  /* for ZBDDC, this is not allowed */
1382  /* for TZBDD, this is not allowed */
1383  /* for TZBDDC, this is not allowed */
1384  if (biddyManagerType == BIDDYTYPEOBDDC) {
1385  tableN[n].type = 5;
1386  } else {
1387  printf("BiddyManagedReadBddview: Problem with connection - wrong code\n");
1388  return NULL;
1389  }
1390  }
1391  /* else if (!strcmp(code,"di")) */
1392 #ifndef COMPACT
1393  else if ((code[0] == 'd') && (code[1] != 0))
1394  { /* double line, type 'di' */
1395  /* for OBDD, this is not allowed */
1396  /* for OBDDC, this is not allowed */
1397  /* for ZBDD, this is not allowed */
1398  /* for ZBDDC, this is type 5 */
1399  /* for TZBDD, this is not allowed */
1400  /* for TZBDDC, this is type 5 */
1401  tableN[n].l = tableN[n].r = m;
1402  if (biddyManagerType == BIDDYTYPEZBDDC) {
1403  tableN[n].type = 5;
1404  }
1405  else if (biddyManagerType == BIDDYTYPETZBDDC) {
1406  tableN[n].type = 5;
1407  } else {
1408  printf("BiddyManagedReadBddview: Problem with connection - wrong code\n");
1409  return NULL;
1410  }
1411  }
1412 #endif
1413  /* else if (!strcmp(code,"e")) */
1414  else if ((code[0] == 'e') && (code[1] == 0))
1415  { /* double line, type 'e' */
1416  /* this is default type for all allowed bdd types */
1417  tableN[n].l = tableN[n].r = m;
1418  }
1419  /* else if (!strcmp(code,"ei")) */
1420 #ifndef COMPACT
1421  else if ((code[0] == 'e') && (code[1] != 0))
1422  { /* double line, type 'ei' */
1423  /* for OBDD, this is not allowed */
1424  /* for OBDDC, this is not allowed */
1425  /* for ZBDD, this is not allowed */
1426  /* for ZBDDC, this is not allowed */
1427  /* for TZBDD, this is not allowed */
1428  /* for TZBDDC, this is not allowed */
1429  tableN[n].l = tableN[n].r = m;
1430  printf("BiddyManagedReadBddview: Problem with connection - wrong code\n");
1431  return NULL;
1432  } else {
1433  printf("BiddyManagedReadBddview: Problem with connection - unknown code\n");
1434  return NULL;
1435  }
1436 #endif
1437  /* printf("CONNECT: <%u><%u><%s><%s><%s>\n",n,m,code,word,word2); */
1438  }
1439  else if ((line[0] == 'n') && !strncmp(line,"node",4)) { /* parsing line with node */
1440  line = &line[5];
1441  word = NULL;
1442  sscanf(line,"%u %s",&n,buffer);
1443  if (buffer[0]=='"') {
1444  buffer[strlen(buffer)-1] = 0;
1445  word = &buffer[1];
1446  } else {
1447  word = &buffer[0];
1448  }
1449  if (!numN) {
1450  tableN = (BiddyNodeList *) malloc(sizeof(BiddyNodeList));
1451  if (!tableN) return NULL;
1452  } else if (numN <= n) {
1453  tableN = (BiddyNodeList *) realloc(tableN,(n+1)*sizeof(BiddyNodeList));
1454  if (!tableN) return NULL;
1455  }
1456  tableN[n].name = strdup(word);
1457  tableN[n].id = n;
1458  tableN[n].type = 4; /* 4 is for regular node, this may change to type 5 later */
1459  tableN[n].l = tableN[n].r = -1;
1460  tableN[n].ltag = tableN[n].rtag = 0;
1461  tableN[n].f = NULL;
1462  tableN[n].created = FALSE;
1463  numN = n+1; // more safe than numN++;
1464  /* printf("NODE: <%u><%s>\n",n,word); */
1465  }
1466  else if ((line[0] == 't') && !strncmp(line,"terminal",8)) { /* parsing line with terminal */
1467  line = &line[9];
1468  word = NULL;
1469  sscanf(line,"%u %s",&n,buffer);
1470  if (buffer[0]=='"') {
1471  buffer[strlen(buffer)-1] = 0;
1472  word = &buffer[1];
1473  } else {
1474  word = &buffer[0];
1475  }
1476  if (!numN) {
1477  tableN = (BiddyNodeList *) malloc(sizeof(BiddyNodeList));
1478  if (!tableN) return NULL;
1479  } else if (numN <= n) {
1480  tableN = (BiddyNodeList *) realloc(tableN,(n+1)*sizeof(BiddyNodeList));
1481  if (!tableN) return NULL;
1482  }
1483  tableN[n].name = strdup(word);
1484  tableN[n].id = n;
1485  if (!strcmp(word,"0")) {
1486  tableN[n].type = 0;
1487  } else if (!strcmp(word,"1")) {
1488  tableN[n].type = 1;
1489  } else {
1490  printf("BiddyManagedReadBddview: Problem with terminal\n");
1491  return NULL;
1492  }
1493  tableN[n].l = tableN[n].r = -1;
1494  tableN[n].ltag = tableN[n].rtag = 0;
1495  tableN[n].f = NULL;
1496  tableN[n].created = FALSE;
1497  numN = n+1; // more safe than numN++;
1498  /* printf("TERMINAL: <%u><%s>\n",n,word); */
1499  }
1500  else if ((line[0] == 'f') && !strncmp(line,"formula",7)) { /* parsing line with formula declaration */
1501  /* TESTING, ONLY */
1502 
1503  line = &line[8];
1504  word = NULL;
1505  sscanf(line,"%s %u %s",buffer,&n,code);
1506  if (buffer[0]=='"') {
1507  buffer[strlen(buffer)-1] = 0;
1508  word = &buffer[1];
1509  } else {
1510  word = &buffer[0];
1511  }
1512  printf("FORMULA: <%s><%u><%s>\n",word,n,code);
1513 
1514  }
1515  else if (!typeOK && (line[0] == 't') && !strncmp(line,"type",4)) { /* parsing line with type */
1516  typeOK = TRUE;
1517  line = &line[5];
1518  /* printf("TYPE: %s\n",line); */
1519  if (((biddyManagerType == BIDDYTYPEOBDD) && strcmp(line,"robdd") && strcmp(line,"ROBDD")) ||
1520  ((biddyManagerType == BIDDYTYPEOBDDC) && strcmp(line,"robddce") && strcmp(line,"ROBDDCE")) ||
1521  ((biddyManagerType == BIDDYTYPEZBDD) && strcmp(line,"zbdd") && strcmp(line,"ZBDD")) ||
1522  ((biddyManagerType == BIDDYTYPEZBDDC) && strcmp(line,"zbddce") && strcmp(line,"ZBDDCE")) ||
1523  ((biddyManagerType == BIDDYTYPETZBDD) && strcmp(line,"tzbdd") && strcmp(line,"TZBDD")) ||
1524  ((biddyManagerType == BIDDYTYPETZBDDC) && strcmp(line,"tzbddce") && strcmp(line,"TZBDDCE")))
1525  {
1526  fprintf(stderr,"BiddyManagedReadBddview: Wrong BDD type!\n");
1527  return NULL;
1528  }
1529  }
1530  /* else if (!varOK && (line[0] == 'v') && !strncmp(line,"var",3)) { */ /* parsing line with variables */
1531  else if ((line[0] == 'v') && !strncmp(line,"var",3)) { /* parsing line with variables, multiple var declarations allowed */
1532  /* varOK = TRUE; */ /* not needed if multiple vars are allowed */
1533  line = &line[4];
1534  word = strtok(line," ");
1535  while (word) {
1536  if (word[0]=='"') {
1537  word[strlen(word)-1] = 0;
1538  word = &word[1];
1539  }
1540  if (!numV) {
1541  tableV = (BiddyVariableOrder *) malloc(sizeof(BiddyVariableOrder));
1542  if (!tableV) return NULL;
1543  } else {
1544  tableV = (BiddyVariableOrder *) realloc(tableV,(numV+1)*sizeof(BiddyVariableOrder));
1545  if (!tableV) return NULL;
1546  }
1547  tableV[numV].name = strdup(word);
1548  tableV[numV].order = numV;
1549  numV++;
1550  /* printf("<%s>\n",word); */
1551  word = strtok(NULL," ");
1552  }
1553  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
1554  {
1555  for (i=0; i<numV; i++) {
1556  /* BiddyManagedAddVariableByName(MNG,tableV[i].name,TRUE); */ /* OLD */
1557  BiddyManagedFoaVariable(MNG,tableV[i].name,TRUE,TRUE); /* add variable and element, repair regarding Boolean functions */
1558  }
1559  }
1560 #ifndef COMPACT
1561  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
1562  {
1563  for (i=numV-1; i>=0; i--) {
1564  /* BiddyManagedAddVariableByName(MNG,tableV[i].name,TRUE); */
1565  BiddyManagedFoaVariable(MNG,tableV[i].name,FALSE,TRUE); /* add variable and element, repair regarding combination sets */
1566  }
1567  }
1568  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
1569  {
1570  for (i=numV-1; i>=0; i--) {
1571  /* BiddyManagedAddVariableByName(MNG,tableV[i].name,TRUE); */
1572  BiddyManagedFoaVariable(MNG,tableV[i].name,TRUE,TRUE); /* add variable and element, repair regarding Boolean functions */
1573  }
1574  }
1575  else {
1576  fprintf(stderr,"BiddyManagedReadBddview: Unknown BDD type!\n");
1577  return NULL;
1578  }
1579 #endif
1580  }
1581  /* else if (!labelOK && (line[0] == 'l') && !strncmp(line,"label",5)) { */ /* parsing line with label */
1582  else if ((line[0] == 'l') && !strncmp(line,"label",5)) { /* parsing line with label, multiple label declarations allowed */
1583  /* labelOK = TRUE; */ /* not needed if multiple var are allowed */
1584  line = &line[6];
1585  word = NULL;
1586  sscanf(line,"%u %s",&n,buffer);
1587  if (buffer[0]=='"') {
1588  buffer[strlen(buffer)-1] = 0;
1589  word = &buffer[1];
1590  } else {
1591  word = &buffer[0];
1592  }
1593  if (!numN) {
1594  tableN = (BiddyNodeList *) malloc(sizeof(BiddyNodeList));
1595  if (!tableN) return NULL;
1596  } else if (numN <= n) {
1597  tableN = (BiddyNodeList *) realloc(tableN,(n+1)*sizeof(BiddyNodeList));
1598  if (!tableN) return NULL;
1599  }
1600  tableN[n].name = strdup(word);
1601  tableN[n].id = n;
1602  tableN[n].type = 2; /* 2 is for regular label, this may change to type 3 later */
1603  tableN[n].l = tableN[n].r = -1;
1604  tableN[n].ltag = tableN[n].rtag = 0;
1605  tableN[n].f = NULL;
1606  tableN[n].created = FALSE;
1607  numN = n+1; // more safe than numN++;
1608  /* add to formula list */
1609  if (!numF) {
1610  tableF = (BiddyFormulaList *) malloc(sizeof(BiddyFormulaList));
1611  if (!tableF) return NULL;
1612  } else {
1613  tableF = (BiddyFormulaList *) realloc(tableF,(numF+1)*sizeof(BiddyFormulaList));
1614  if (!tableF) return NULL;
1615  }
1616  tableF[numF].name = strdup(tableN[n].name);
1617  tableF[numF].id = n;
1618  tableF[numF].f = biddyNull;
1619  numF++;
1620  /* printf("LABEL: <%u><%s>\n",n,word); */
1621  }
1622 
1623  line = fgets(buffer,65535,bddfile);
1624  }
1625 
1626  fclose(bddfile);
1627 
1628  /* CONSTRUCT BDD */
1629 
1630  /* DEBUGGING */
1631  /*
1632  for (i=0; i<numN; i++) {
1633  printf("tableN[%d]: %s, type:%d, l:%d, ltag:%u<%s>, r:%d, rtag:%u<%s>\n",
1634  tableN[i].id,tableN[i].name,tableN[i].type,
1635  tableN[i].l,tableN[i].ltag,BiddyManagedGetVariableName(MNG,tableN[i].ltag),
1636  tableN[i].r,tableN[i].rtag,BiddyManagedGetVariableName(MNG,tableN[i].rtag));
1637  }
1638  */
1639 
1640  BiddyConstructBDD(MNG,numN,tableN,numF,tableF);
1641 
1642  /* all formulae are stored */
1643  if (!numF) {
1644  fprintf(stderr,"WARNING (BiddyManagedReadBddview): no label\n");
1645  } else {
1646  for (i=0; i<numF; ++i) {
1647  BiddyManagedAddFormula(MNG,tableF[i].name,tableF[i].f,-1);
1648  /* printf("BDD %s CONSTRUCTED\n",tableF[i].name); */
1649  }
1650  }
1651 
1652  /* if parameter name is not null then root formula (id = 0) is stored also with this name */
1653  /* TO DO: maybe store only with the given name? */
1654  if (name) {
1655  for (i=0; i<numF; ++i) {
1656  if (tableF[i].id == 0) {
1657  BiddyManagedAddFormula(MNG,name,tableF[i].f,-1);
1658  }
1659  }
1660  }
1661 
1662 
1663  /* create list of all labels */
1664  for (i=0; i<numF; ++i) {
1665  if (!namelist) {
1666  namelist = strdup(tableF[i].name);
1667  } else {
1668  concat(&namelist," ");
1669  concat(&namelist,tableF[i].name);
1670  }
1671  }
1672 
1673  for (i=0; i<numV; ++i) {
1674  free(tableV[i].name);
1675  }
1676  for (i=0; i<numN; ++i) {
1677  free(tableN[i].name);
1678  }
1679  for (i=0; i<numF; ++i) {
1680  free(tableF[i].name);
1681  }
1682 
1683  free(tableV);
1684  free(tableN);
1685  free(tableF);
1686 
1687  /* printf("BiddyManagedReadBddview: return %s\n",namelist); */
1688 
1689  return namelist;
1690 }
1691 
1692 /***************************************************************************/
1701 void
1702 BiddyManagedReadVerilogFile(Biddy_Manager MNG, const char filename[],
1703  Biddy_String prefix)
1704 {
1705  FILE *s;
1706  BiddyVerilogCircuit *c;
1707  unsigned int linecount, modulecount;
1708  BiddyVerilogLine **lt;
1709  BiddyVerilogModule **mt;
1710  BiddyVerilogModule *md;
1711  BiddyVerilogLine *ln;
1712  unsigned int i,j;
1713 
1714  assert( MNG );
1715 
1716  s = fopen(filename,"r");
1717  if (!s) return;
1718 
1719  /* DEBUGGING */
1720  /*
1721  printf("PARSING VERILOG FILE %s\n",filename);
1722  */
1723 
1724  c = (BiddyVerilogCircuit *) calloc(1,sizeof(BiddyVerilogCircuit)); /* declare an instance of a circuit */
1725  c->name = strdup("CIRCUIT"); /* set circuit name */
1726  parseVerilogFile(s,&linecount,&lt,&modulecount,&mt); /* read all modules from the file */
1727 
1728  fclose(s);
1729 
1730  /* DEBUGGING */
1731  /*
1732  printf("TARGET MODULE: %s\n",(mt[0])->name);
1733  */
1734 
1735  /* DEBUGGING */
1736  /*
1737  for (i = 0; i < modulecount; i++) {
1738  printf("MODULE: %s\n",(mt[i])->name);
1739  }
1740  printf("ACCEPTABLE LINES\n");
1741  for (i = 0; i < linecount; i++) {
1742  printf("<%s> %s\n",(lt[i])->keyword,(lt[i])->line);
1743  }
1744  */
1745 
1746  createVerilogCircuit(linecount,lt,modulecount,mt,c); /* create circuit object for the given table of acceptable lines and table of modules */
1747  createBddFromVerilogCircuit(MNG,c,prefix); /* create BDDs for all primary outputs */
1748 
1749  for (i = 0; i < linecount; i++) {
1750  ln = lt[i];
1751  free(ln->keyword);
1752  free(ln->line);
1753  free(ln);
1754  }
1755  free(lt);
1756 
1757  for (i = 0; i < modulecount; i++) {
1758  md = mt[i];
1759  for (j = 0; j < md->outputcount; j++) free (md->outputs[j]);
1760  for (j = 0; j < md->inputcount; j++) free (md->inputs[j]);
1761  for (j = 0; j < md->wirecount; j++) free (md->wires[j]);
1762  for (j = 0; j < md->gatecount; j++) free (md->gates[j]);
1763  free(md->name);
1764  free(md);
1765  }
1766  free(mt);
1767 
1768  for (i=0; i < c->outputcount; i++) free (c->outputs[i]);
1769 
1770  for (i=0; i < c->inputcount; i++) free (c->inputs[i]);
1771 
1772  for (i=0; i < c->nodecount; i++) {
1773  free(c->nodes[i]->type);
1774  free(c->nodes[i]->name);
1775  free(c->nodes[i]);
1776  }
1777  free(c->nodes);
1778 
1779  for (i=0; i < c->wirecount; i++) {
1780  free (c->wires[i]->type);
1781  free (c->wires[i]);
1782  }
1783  free(c->wires);
1784 
1785  free(c->name);
1786  free(c);
1787 }
1788 
1789 /***************************************************************************/
1798 void
1799 BiddyManagedPrintBDD(Biddy_Manager MNG, Biddy_String *var, const char filename[],
1800  Biddy_Edge f, Biddy_String label)
1801 {
1802  unsigned int line;
1803  FILE *s;
1804 
1805  assert( MNG );
1806 
1807  line = 0;
1808  s = NULL;
1809 
1810  if (var) {
1811  }
1812  if (!strcmp(filename,"stdout")) {
1813  s = stdout;
1814  } else if (strcmp(filename,"")) {
1815  s = fopen(filename,"w");
1816  if (!s) return;
1817  fprintf(s,"%s ",label);
1818  }
1819 
1820  if (BiddyIsNull(f)) {
1821 
1822  if (var) {
1823  concat(var,"NULL");
1824  }
1825  if (!strcmp(filename,"stdout")) {
1826  printf("NULL\n");
1827  } else if (strcmp(filename,"")) {
1828  fprintf(s,"NULL\n");
1829  fclose(s);
1830  }
1831 
1832  return;
1833 
1834  } else {
1835 
1836  if (!strcmp(filename,"stdout")) {
1837  WriteBDD(MNG,var,stdout,f,&line);
1838  } else {
1839  WriteBDD(MNG,var,s,f,&line);
1840  }
1841 
1842  if (var) {
1843  }
1844  if (!strcmp(filename,"stdout")) {
1845  printf("\n");
1846  } else if (strcmp(filename,"")) {
1847  if (line != 0) fprintf(s,"\n");
1848  }
1849 
1850  }
1851 
1852  if (var) {
1853  }
1854  if (!strcmp(filename,"stdout")) {
1855  } else if (strcmp(filename,"")) {
1856  fclose(s);
1857  }
1858 }
1859 
1860 /***************************************************************************/
1869 void
1870 BiddyManagedPrintTable(Biddy_Manager MNG, Biddy_String *var, const char filename[],
1871  Biddy_Edge f)
1872 {
1873  unsigned int variableNumber;
1874  Biddy_Variable* variableTable;
1875  unsigned int i;
1876  int j;
1877  Biddy_Variable k,v;
1878  unsigned int numcomb;
1879  FILE *s;
1880 
1881  assert( MNG );
1882 
1883  s = NULL;
1884 
1885  if (var) {
1886  }
1887  if (!strcmp(filename,"stdout")) {
1888  s = NULL; /* s is not needed */
1889  } else if (strcmp(filename,"")) {
1890  s = fopen(filename,"w");
1891  if (!s) return;
1892  }
1893 
1894  if (BiddyIsNull(f)) {
1895 
1896  if (var) {
1897  concat(var,"NULL");
1898  }
1899  if (!strcmp(filename,"stdout")) {
1900  printf("NULL\n");
1901  } else if (strcmp(filename,"")) {
1902  fprintf(s,"NULL\n");
1903  fclose(s);
1904  }
1905 
1906  return;
1907  }
1908 
1909  /* variableNumber is the number of dependent variables in BDD */
1910  variableNumber = BiddyManagedDependentVariableNumber(MNG,f,TRUE);
1911 
1912  /* DEBUGGING */
1913  /*
1914  reportOrdering();
1915  printf("DEPENDENT: %u\n",variableNumber);
1916  printf("TOP VARIABLE: %s\n",BiddyManagedGetVariableName(MNG,BiddyV(f)));
1917  for (k = 1; k < biddyVariableTable.num; k++) {
1918  if (biddyVariableTable.table[k].selected == TRUE) {
1919  printf("SELECTED: %s\n",BiddyManagedGetVariableName(MNG,k));
1920  }
1921  }
1922  */
1923 
1924  if (variableNumber > 6) {
1925 
1926  if (var) {
1927  concat(var,"TO MANY VARIABLES");
1928  }
1929  if (!strcmp(filename,"stdout")) {
1930  printf("Table for %d variables is to large for output.\n",variableNumber);
1931  } else if (strcmp(filename,"")) {
1932  fprintf(s,"Table for %d variables is to large for output.\n",variableNumber);
1933  fclose(s);
1934  }
1935 
1936  for (k = 0; k < biddyVariableTable.num; k++) {
1937  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
1938  }
1939  return;
1940  }
1941 
1942  /* variableTable is a table of all dependent variables in BDD */
1943  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
1944  i = 0;
1945  v = BiddyManagedGetLowestVariable(MNG); /* lowest = topmost */
1946  for (k = 1; k < biddyVariableTable.num; k++) {
1947  if (biddyVariableTable.table[v].selected == TRUE) {
1948  variableTable[i] = v;
1949 
1950  if (var) {
1951  concat(var,"|");
1952  concat(var,BiddyManagedGetVariableName(MNG,v));
1953  }
1954  if (!strcmp(filename,"stdout")) {
1955  printf("|%s",BiddyManagedGetVariableName(MNG,v));
1956  } else if (strcmp(filename,"")) {
1957  fprintf(s,"|%s",BiddyManagedGetVariableName(MNG,v));
1958  }
1959 
1960  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1961  i++;
1962  }
1963  v = biddyVariableTable.table[v].next;
1964  }
1965 
1966  if (var) {
1967  concat(var,"|| value\n");
1968  }
1969  if (!strcmp(filename,"stdout")) {
1970  printf("|| value\n");
1971  } else if (strcmp(filename,"")) {
1972  fprintf(s,"|| value\n");
1973  }
1974 
1975  numcomb = 1;
1976  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
1977  for (i = 0; i < numcomb; i++)
1978  {
1979  for (j = variableNumber - 1; j >= 0; j--) {
1980  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
1981  if (i&(1 << j)) {
1982 
1983  if (var) {
1984  concat(var," 1");
1985  }
1986  if (!strcmp(filename,"stdout")) {
1987  printf("%*c",1+(int)strlen(
1988  BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1])
1989  ),'1');
1990  } else if (strcmp(filename,"")) {
1991  fprintf(s,"%*c",1+(int)strlen(
1992  BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1])
1993  ),'1');
1994  }
1995 
1996 
1997  } else {
1998 
1999  if (var) {
2000  concat(var," 0");
2001  }
2002  if (!strcmp(filename,"stdout")) {
2003  printf("%*c",1+(int)strlen(
2004  BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1])
2005  ),'0');
2006  } else if (strcmp(filename,"")) {
2007  fprintf(s,"%*c",1+(int)strlen(
2008  BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1])
2009  ),'0');
2010  }
2011 
2012  }
2013  }
2014 
2015  if (var) {
2016  concat(var," :");
2017  }
2018  if (!strcmp(filename,"stdout")) {
2019  printf(" :");
2020  } else if (strcmp(filename,"")) {
2021  fprintf(s," :");
2022  }
2023 
2024  if (BiddyManagedEval(MNG,f)) {
2025 
2026  if (var) {
2027  concat(var," 1\n");
2028  }
2029  if (!strcmp(filename,"stdout")) {
2030  printf(" 1\n");
2031  } else if (strcmp(filename,"")) {
2032  fprintf(s," 1\n");
2033  }
2034 
2035  } else {
2036 
2037  if (var) {
2038  concat(var," 0\n");
2039  }
2040  if (!strcmp(filename,"stdout")) {
2041  printf(" 0\n");
2042  } else if (strcmp(filename,"")) {
2043  fprintf(s," 0\n");
2044  }
2045 
2046  }
2047  }
2048 
2049  free(variableTable);
2050 
2051  if (var) {
2052  }
2053  if (!strcmp(filename,"stdout")) {
2054  } else if (strcmp(filename,"")) {
2055  fclose(s);
2056  }
2057 }
2058 
2059 /***************************************************************************/
2068 void
2069 BiddyManagedPrintSOP(Biddy_Manager MNG, Biddy_String *var, const char filename[],
2070  Biddy_Edge f)
2071 {
2072  unsigned int maxsize = 100;
2073  Biddy_Variable top;
2074  FILE *s;
2075 
2076  assert( MNG );
2077 
2078  s = NULL;
2079 
2080  if (var) {
2081  }
2082  if (!strcmp(filename,"stdout")) {
2083  s = stdout;
2084  } else if (strcmp(filename,"")) {
2085  s = fopen(filename,"w");
2086  if (!s) return;
2087  }
2088 
2089  if (BiddyIsNull(f)) {
2090 
2091  if (var) {
2092  concat(var,"NULL\n");
2093  }
2094  if (!strcmp(filename,"stdout")) {
2095  printf(" NULL\n");
2096  } else if (strcmp(filename,"")) {
2097  fprintf(s," NULL\n");
2098  fclose(s);
2099  }
2100 
2101  return;
2102  }
2103 
2104  if (BiddyIsTerminal(f)) {
2105  if (f == biddyZero) {
2106 
2107  if (var) {
2108  concat(var," + 0\n");
2109  }
2110  if (!strcmp(filename,"stdout")) {
2111  printf(" + 0\n");
2112  } else if (strcmp(filename,"")) {
2113  fprintf(s," + 0\n");
2114  fclose(s);
2115  }
2116 
2117  return;
2118 
2119  } else if (f == biddyOne) {
2120 
2121  if (var) {
2122  concat(var," + 1\n");
2123  }
2124  if (!strcmp(filename,"stdout")) {
2125  printf(" + 1\n");
2126  } else if (strcmp(filename,"")) {
2127  fprintf(s," + 1\n");
2128  fclose(s);
2129  }
2130 
2131  return;
2132  }
2133  }
2134 
2135  top = BiddyV(f);
2136  if (biddyManagerType == BIDDYTYPEOBDD) {
2137  }
2138  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2139  }
2140 #ifndef COMPACT
2141  else if (biddyManagerType == BIDDYTYPEZBDD) {
2142  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
2143  top = biddyVariableTable.table[top].prev;
2144  }
2145  }
2146  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2147  while (biddyVariableTable.table[top].prev != biddyVariableTable.num) {
2148  top = biddyVariableTable.table[top].prev;
2149  }
2150  }
2151  else if (biddyManagerType == BIDDYTYPETZBDD) {
2152  top = BiddyGetTag(f);
2153  }
2154 #endif
2155 
2156  WriteSOP(MNG,var,s,f,top,BiddyGetMark(f),NULL,&maxsize,FALSE);
2157 
2158  if (var) {
2159  concat(var,"\n");
2160  }
2161  if (!strcmp(filename,"stdout")) {
2162  printf("\n");
2163  } else if (strcmp(filename,"")) {
2164  fprintf(s,"\n");
2165  fclose(s);
2166  }
2167 
2168 }
2169 
2170 /***************************************************************************/
2179 void
2180 BiddyManagedPrintMinterms(Biddy_Manager MNG, Biddy_String *var, const char filename[],
2181  Biddy_Edge f, Biddy_Boolean negative)
2182 {
2183  FILE *s;
2184 
2185  Biddy_Variable v;
2186  unsigned int maxsize;
2187  Biddy_Boolean OK;
2188 
2189  assert( MNG );
2190 
2191  /* DEBUGGING */
2192  /*
2193  printf("BiddyManagedPrintMinterms STARTED\n");
2194  */
2195 
2196  if (negative) maxsize = 16; else maxsize = 32;
2197 
2198  s = NULL;
2199 
2200  if (var) {
2201  }
2202  if (!strcmp(filename,"stdout")) {
2203  s = stdout;
2204  } else if (strcmp(filename,"")) {
2205  s = fopen(filename,"w");
2206  if (!s) return;
2207  }
2208 
2209  if (BiddyIsNull(f)) {
2210 
2211  if (var) {
2212  concat(var,"NULL\n");
2213  }
2214  if (!strcmp(filename,"stdout")) {
2215  printf(" NULL\n");
2216  } else if (strcmp(filename,"")) {
2217  fprintf(s," NULL\n");
2218  fclose(s);
2219  }
2220 
2221  return;
2222  }
2223 
2224  if (f == biddyZero) {
2225 
2226  if (var) {
2227  concat(var,"EMPTY\n");
2228  }
2229  if (!strcmp(filename,"stdout")) {
2230  printf("EMPTY\n");
2231  } else if (strcmp(filename,"")) {
2232  fprintf(s,"EMPTY\n");
2233  fclose(s);
2234  }
2235 
2236  return;
2237  }
2238 
2239  /* DEBUGGING */
2240  /*
2241  if (biddyManagerType == BIDDYTYPEOBDD) {
2242  Biddy_Managed_WriteBddview(MNG,"minterms.bddview",f,"F",NULL);
2243  }
2244  */
2245 
2246  v = 0;
2247  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2248  v = BiddyV(f);
2249  }
2250 #ifndef COMPACT
2251  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2252  v = BiddyV(f);
2253  }
2254  else if (biddyManagerType == BIDDYTYPETZBDD) {
2255  v = BiddyManagedGetLowestVariable(MNG);
2256  }
2257 #endif
2258 
2259  OK = WriteSOP(MNG,var,s,f,v,BiddyGetMark(f),NULL,&maxsize,!negative);
2260 
2261  if (!OK) { /* output to large */
2262  if (var) {
2263  concat(var,"... (to large)");
2264  }
2265  if (!strcmp(filename,"stdout")) {
2266  printf("... (to large)");
2267  } else if (strcmp(filename,"")) {
2268  fprintf(s,"... (to large)");
2269  }
2270  }
2271 
2272  if (var) {
2273  concat(var,"\n");
2274  }
2275  if (!strcmp(filename,"stdout")) {
2276  printf("\n");
2277  } else if (strcmp(filename,"")) {
2278  fprintf(s,"\n");
2279  }
2280 
2281  if (var) {
2282  }
2283  if (!strcmp(filename,"stdout")) {
2284  } else if (strcmp(filename,"")) {
2285  fclose(s);
2286  }
2287 
2288 }
2289 
2290 /***************************************************************************/
2299 unsigned int
2300 BiddyManagedWriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f,
2301  const char label[], int id, Biddy_Boolean cudd)
2302 {
2303  unsigned int n;
2304  char *label1;
2305  char *hash;
2306  FILE *s;
2307  Biddy_Variable tag;
2308  BiddyLocalInfo *li;
2309  Biddy_Variable v;
2310  Biddy_String name;
2311 
2312  assert( MNG );
2313 
2314  s = NULL;
2315 
2316  /* if (id != -1) use it instead of <...> */
2317 
2318  if (BiddyIsNull(f)) {
2319  printf("WARNING (BiddyManagedWriteDot): Function is null!\n");
2320  return 0;
2321  }
2322 
2323  if (filename) {
2324  s = fopen(filename,"w");
2325  } else {
2326  s = stdout;
2327  }
2328  if (!s) return 0;
2329 
2330  if (BiddyIsTerminal(f)) {
2331  n = 1; /* there is only one terminal node */
2332  } else {
2333  BiddyCreateLocalInfo(MNG,f);
2334  n = enumerateNodes(MNG,f,0); /* this will select all nodes except terminal node */
2335  BiddyManagedDeselectAll(MNG);
2336  }
2337 
2338  label1 = strdup(label);
2339  while ((hash=strchr(label1,'#'))) hash[0]='_'; /* avoid hashes in the name */
2340 
2341  if (cudd) {
2342  fprintf(s,"//GENERATED WITH BIDDY - biddy.meolic.com\n");
2343  if (filename) {
2344  fprintf(s,"//USE 'dot -y -Tpng -O %s' TO VISUALIZE %s\n",filename,biddyManagerName);
2345  }
2346  fprintf(s,"digraph \"DD\" {\n");
2347  /* fprintf(s,"size = \"7.5,10\"\n"); */
2348  fprintf(s,"center=true;\nedge [dir=none];\n");
2349  fprintf(s,"{ node [shape=plaintext];\n");
2350  fprintf(s," edge [style=invis];\n");
2351  fprintf(s," \"CONST NODES\" [style = invis];\n");
2352 
2353  if (!BiddyIsTerminal(f)) {
2354  li = (BiddyLocalInfo *)(BiddyN(f)->list);
2355  BiddyManagedResetVariablesValue(MNG);
2356  while (li->back) {
2357  v = BiddyV(li->back);
2358  if (biddyVariableTable.table[v].value == biddyZero) {
2359  biddyVariableTable.table[v].value = biddyOne;
2360  /* variable names containing # are adpated */
2361  name = strdup(BiddyManagedGetVariableName(MNG,v));
2362  while ((hash = strchr(name,'#'))) hash[0] = '_';
2363  fprintf(s,"\" %s \" -> ",name);
2364  free(name);
2365  }
2366  li = &li[1]; /* next field in the array */
2367  }
2368  BiddyManagedResetVariablesValue(MNG);
2369  }
2370 
2371  fprintf(s,"\"CONST NODES\"; \n}\n");
2372  fprintf(s,"{ rank=same; node [shape=box]; edge [style=invis];\n");
2373  fprintf(s,"\"%s\"",label1);
2374  fprintf(s,"; }\n");
2375  } else {
2376  fprintf(s,"//GENERATED WITH BIDDY - biddy.meolic.com\n");
2377  if (filename) {
2378  fprintf(s,"//USE 'dot -y -Tpng -O %s' TO VISUALIZE %s\n",filename,biddyManagerName);
2379  }
2380  fprintf(s,"digraph ");
2381  if (biddyManagerType == BIDDYTYPEOBDD) fprintf(s,"ROBDD");
2382  else if (biddyManagerType == BIDDYTYPEZBDD) fprintf(s,"ZBDD");
2383  else if (biddyManagerType == BIDDYTYPETZBDD) fprintf(s,"TZBDD");
2384  else if (biddyManagerType == BIDDYTYPEOBDDC) fprintf(s,"ROBDDCE");
2385  else if (biddyManagerType == BIDDYTYPEZBDDC) fprintf(s,"ZBDDCE");
2386  else if (biddyManagerType == BIDDYTYPETZBDDC) fprintf(s,"TZBDDCE");
2387  else fprintf(s,"BDD");
2388  fprintf(s," {\n");
2389  fprintf(s," ordering=out;\n");
2390 #ifdef LEGACY_DOT
2391 #else
2392  fprintf(s," edge [dir=\"both\"];\n");
2393 #endif
2394  fprintf(s," edge [arrowhead=\"none\"]\n");
2395  fprintf(s," node [shape=none, label=\"%s\"] 0;\n",label1);
2396  }
2397 
2398  WriteDotNodes(MNG,s,f,id,cudd);
2399 
2400  if (((biddyManagerType == BIDDYTYPEOBDD) ||
2401  (biddyManagerType == BIDDYTYPEZBDD) ||
2402  (biddyManagerType == BIDDYTYPETZBDD) ||
2403  !(BiddyGetMark(f))))
2404  {
2405  if ((f != biddyZero) && (tag = BiddyGetTag(f))) {
2406  if (cudd) {
2407  fprintf(s,"\"%s\"",label1);
2408  if (BiddyIsTerminal(f)) {
2409  fprintf(s," -> \"1\" [style=solid label=\"%s\"];\n",BiddyManagedGetVariableName(MNG,tag));
2410  } else {
2411  fprintf(s," -> \"%p\" [style=solid label=\"%s\"];\n",BiddyP(f),BiddyManagedGetVariableName(MNG,tag));
2412  }
2413  } else {
2414 #ifdef LEGACY_DOT
2415  fprintf(s," 0 -> 1 [style=solid label=\"%s\"];\n",BiddyManagedGetVariableName(MNG,tag));
2416 #else
2417  fprintf(s," 0 -> 1 [arrowtail=\"none\" label=\"%s\"];\n",BiddyManagedGetVariableName(MNG,tag));
2418 #endif
2419  }
2420  } else {
2421  if (cudd) {
2422  fprintf(s,"\"%s\"",label1);
2423  if (BiddyIsTerminal(f)) {
2424  fprintf(s," -> \"1\" [style=solid];\n");
2425  } else {
2426  fprintf(s," -> \"%p\" [style=solid];\n",BiddyP(f));
2427  }
2428  } else {
2429 #ifdef LEGACY_DOT
2430  fprintf(s," 0 -> 1 [style=solid];\n");
2431 #else
2432  fprintf(s," 0 -> 1 [arrowtail=\"none\"];\n");
2433 #endif
2434  }
2435  }
2436  } else {
2437  if ((f != biddyZero) && (tag = BiddyGetTag(f))) {
2438  if (cudd) {
2439  fprintf(s,"\"%s\"",label1);
2440  if (BiddyIsTerminal(f)) {
2441  fprintf(s," -> \"1\" [style=dotted label=\"%s\"];\n",BiddyManagedGetVariableName(MNG,tag));
2442  } else {
2443  fprintf(s," -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),BiddyManagedGetVariableName(MNG,tag));
2444  }
2445  } else {
2446 #ifdef LEGACY_DOT
2447  fprintf(s," 0 -> 1 [style=dotted label=\"%s\"];\n",BiddyManagedGetVariableName(MNG,tag));
2448 #else
2449  fprintf(s," 0 -> 1 [arrowtail=\"none\" arrowhead=\"dot\" label=\"%s\"];\n",BiddyManagedGetVariableName(MNG,tag));
2450 #endif
2451  }
2452  } else {
2453  if (cudd) {
2454  fprintf(s,"\"%s\"",label1);
2455  if (BiddyIsTerminal(f)) {
2456  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2457  fprintf(s," -> \"1\" [style=dotted];\n");
2458  } else {
2459  fprintf(s," -> \"1\" [style=bold];\n");
2460  }
2461  } else {
2462  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2463  fprintf(s," -> \"%p\" [style=dotted];\n",BiddyP(f));
2464  } else {
2465  fprintf(s," -> \"%p\" [style=bold];\n",BiddyP(f));
2466  }
2467  }
2468  } else {
2469 #ifdef LEGACY_DOT
2470  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2471  fprintf(s," 0 -> 1 [style=dotted];\n");
2472  } else {
2473  fprintf(s," 0 -> 1 [style=bold];\n");
2474  }
2475 #else
2476  fprintf(s," 0 -> 1 [arrowtail=\"none\" arrowhead=\"dot\"];\n");
2477 #endif
2478  }
2479  }
2480  }
2481 
2482  free(label1);
2483 
2484  WriteDotEdges(MNG,s,f,cudd); /* this will select all nodes except terminal node */
2485 
2486  if (!BiddyIsTerminal(f)) {
2487  BiddyDeleteLocalInfo(MNG,f);
2488  }
2489 
2490  fprintf(s,"}\n");
2491 
2492  if (filename) {
2493  fclose(s);
2494  }
2495 
2496  return n;
2497 }
2498 
2499 /***************************************************************************/
2508 unsigned int
2509 BiddyManagedWriteBddview(Biddy_Manager MNG, const char filename[],
2510  Biddy_Edge f, const char label[], void *xytable)
2511 {
2512  FILE *s;
2513  unsigned int i,n;
2514  Biddy_Boolean useCoordinates;
2515  BiddyLocalInfo *li;
2516  Biddy_Variable v,k;
2517  char *hash;
2518  Biddy_String name;
2519  BiddyXY *table;
2520 
2521 #ifndef COMPACT
2522  Biddy_Variable tag;
2523 #endif
2524 
2525  assert( MNG );
2526 
2527  s = NULL;
2528 
2529  if (BiddyIsNull(f)) {
2530  /* printf("ERROR BiddyManagedWriteBddview: Function is null!\n"); */
2531  return 0 ;
2532  }
2533 
2534  if (filename) {
2535  s = fopen(filename,"w");
2536  } else {
2537  s = stdout;
2538  }
2539  if (!s) {
2540  printf("ERROR: s = 0\n");
2541  return(0);
2542  }
2543 
2544  table = (BiddyXY *)xytable;
2545 
2546  fprintf(s,"#GENERATED WITH BIDDY - biddy.meolic.com\n");
2547 
2548  /* WRITE BDD TYPE */
2549 
2550  if (biddyManagerType == BIDDYTYPEOBDD) {
2551  fprintf(s,"type ROBDD\n");
2552  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
2553  fprintf(s,"type ROBDDCE\n");
2554  }
2555 #ifndef COMPACT
2556  else if (biddyManagerType == BIDDYTYPEZBDD) {
2557  fprintf(s,"type ZBDD\n");
2558  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
2559  fprintf(s,"type ZBDDCE\n");
2560  } else if (biddyManagerType == BIDDYTYPETZBDD) {
2561  fprintf(s,"type TZBDD\n");
2562  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
2563  fprintf(s,"type TZBDDCE\n");
2564  } else if (biddyManagerType == BIDDYTYPEOFDD) {
2565  fprintf(s,"type ROFDD\n");
2566  } else if (biddyManagerType == BIDDYTYPEOFDDC) {
2567  fprintf(s,"type ROFDDCE\n");
2568  } else if (biddyManagerType == BIDDYTYPEZFDD) {
2569  fprintf(s,"type ZFDD\n");
2570  } else if (biddyManagerType == BIDDYTYPEZFDDC) {
2571  fprintf(s,"type ZFDDCE\n");
2572  } else if (biddyManagerType == BIDDYTYPETZFDD) {
2573  fprintf(s,"type TZFDD\n");
2574  } else if (biddyManagerType == BIDDYTYPETZFDDC) {
2575  fprintf(s,"type TZFDDCE\n");
2576  }
2577 #endif
2578 
2579  /* WRITE VARIABLES */
2580  /* a conservative approach to list all the existing variables in the manager */
2581  /* (and not only the dependent ones) is used. */
2582 
2583  fprintf(s,"var");
2584  v = BiddyManagedGetLowestVariable(MNG); /* lowest = topmost */
2585  for (k = 1; k < biddyVariableTable.num; k++) {
2586  name = strdup(BiddyManagedGetVariableName(MNG,v));
2587 
2588  /* variable names containing # are adpated */
2589  while ((hash = strchr(name,'#'))) hash[0] = '_';
2590  /* to support EST, also variable names containing <> are adapted */
2591  for (i=0; i<strlen(name); i++) {
2592  if (name[i] == '<') name[i] = '_';
2593  if (name[i] == '>') name[i] = 0;
2594  }
2595 
2596  fprintf(s," \"%s\"",name);
2597  free(name);
2598  v = biddyVariableTable.table[v].next;
2599  }
2600  fprintf(s,"\n");
2601 
2602  /* PREPARE CALCULATION */
2603 
2604  useCoordinates = FALSE;
2605  if (BiddyIsTerminal(f)) {
2606 
2607  n = 1; /* for all BDD types, in memory there is only one terminal node */
2608  if (table) {
2609  /* use table of nodes given by the user */
2610  useCoordinates = TRUE;
2611  } else {
2612  n = 1; /* there is one terminal node */
2613  table = (BiddyXY *) malloc((n+1) * sizeof(BiddyXY)); /* n = nodes, add one label */
2614  if (!table) return 0;
2615  table[0].id = 0;
2616  table[0].label = strdup(label);
2617  table[0].x = 0;
2618  table[0].y = 0;
2619  table[0].isConstant = FALSE;
2620  table[1].id = 1;
2621  table[1].label = getname(MNG,f);
2622  table[1].x = 0;
2623  table[1].y = 0;
2624  table[1].isConstant = TRUE;
2625  }
2626 
2627  } else {
2628 
2629  BiddyCreateLocalInfo(MNG,f);
2630  n = enumerateNodes(MNG,f,0); /* this will select all nodes except terminal node */
2631  BiddyManagedDeselectAll(MNG);
2632 
2633  if (table) {
2634  /* use table of nodes given by the user */
2635  useCoordinates = TRUE;
2636  } else {
2637  /* generate table of nodes */
2638  /* TO DO: coordinates are not calculated, how to do this without graphviz/dot? */
2639  table = (BiddyXY *) malloc((n+1) * sizeof(BiddyXY)); /* n = nodes, add one label */
2640  if (!table) return 0;
2641  table[0].id = 0;
2642  table[0].label = strdup(label);
2643  table[0].x = 0;
2644  table[0].y = 0;
2645  table[0].isConstant = FALSE;
2646  li = (BiddyLocalInfo *)(BiddyN(f)->list);
2647  while (li->back) {
2648 
2649  /* add one node */
2650  table[li->data.enumerator].id = li->data.enumerator;
2651  table[li->data.enumerator].label = getname(MNG,li->back);
2652  table[li->data.enumerator].x = 0;
2653  table[li->data.enumerator].y = 0;
2654  table[li->data.enumerator].isConstant = FALSE;
2655 
2656  /* if one or both successors are terminal node then extra nodes must be added */
2657  if (BiddyIsTerminal(BiddyE(li->back)) || BiddyIsTerminal(BiddyT(li->back))) {
2658  if (((biddyManagerType == BIDDYTYPEOBDD) ||
2659  (biddyManagerType == BIDDYTYPEZBDD) ||
2660  (biddyManagerType == BIDDYTYPETZBDD)
2661  ) && (BiddyGetMark(BiddyE(li->back)) != BiddyGetMark(BiddyT(li->back))))
2662  {
2663  /* two terminal nodes only if complemented edges are not used and they are different */
2664  unsigned int num;
2665  num = 0;
2666  if (BiddyIsTerminal(BiddyE(li->back))) {
2667  num = 1;
2668  table[li->data.enumerator+1].id = li->data.enumerator+1;
2669  if (BiddyE(li->back) == biddyZero) {
2670  table[li->data.enumerator+1].label = strdup("0");
2671  } else {
2672  table[li->data.enumerator+1].label = strdup("1");
2673  }
2674  table[li->data.enumerator+1].x = 0;
2675  table[li->data.enumerator+1].y = 0;
2676  table[li->data.enumerator+1].isConstant = TRUE;
2677  }
2678  if (BiddyIsTerminal(BiddyT(li->back))) {
2679  table[li->data.enumerator+num+1].id = li->data.enumerator+num+1;
2680  if (BiddyT(li->back) == biddyZero) {
2681  table[li->data.enumerator+num+1].label = strdup("0");
2682  } else {
2683  table[li->data.enumerator+num+1].label = strdup("1");
2684  }
2685  table[li->data.enumerator+num+1].x = 0;
2686  table[li->data.enumerator+num+1].y = 0;
2687  table[li->data.enumerator+num+1].isConstant = TRUE;
2688  }
2689  } else {
2690  /* only one terminal node */
2691  table[li->data.enumerator+1].id = li->data.enumerator+1;
2692  table[li->data.enumerator+1].label = strdup("1");
2693  table[li->data.enumerator+1].x = 0;
2694  table[li->data.enumerator+1].y = 0;
2695  table[li->data.enumerator+1].isConstant = TRUE;
2696  }
2697  }
2698 
2699  li = &li[1]; /* next field in the array */
2700  }
2701  }
2702 
2703  }
2704 
2705  /* WRITE bddview NODES */
2706 
2707  if (useCoordinates) {
2708  fprintf(s,"label %d %s %d %d\n",table[0].id,table[0].label,table[0].x,table[0].y);
2709  } else {
2710  fprintf(s,"label %d %s\n",table[0].id,table[0].label);
2711  }
2712  for (i=1;i<(n+1);i++) {
2713  if (table[i].isConstant) {
2714  fprintf(s,"terminal ");
2715  } else {
2716  fprintf(s,"node ");
2717  }
2718  if (useCoordinates) {
2719  fprintf(s,"%d %s %d %d\n",table[i].id,table[i].label,table[i].x,table[i].y);
2720  } else {
2721  fprintf(s,"%d %s\n",table[i].id,table[i].label);
2722  }
2723  }
2724 
2725  if (!useCoordinates) {
2726  for (i=1;i<(n+1);i++) {
2727  free(table[i].label);
2728  }
2729  free(table);
2730  }
2731 
2732  /* WRITE bddview CONNECTIONS */
2733 
2734  fprintf(s,"connect 0 1 ");
2735  if ((biddyManagerType == BIDDYTYPEOBDD) ||
2736  (biddyManagerType == BIDDYTYPEZBDD) ||
2737  (biddyManagerType == BIDDYTYPETZBDD))
2738  {
2739  fprintf(s,"s");
2740  }
2741  else {
2742  if (BiddyGetMark(f)) {
2743  fprintf(s,"si");
2744  } else {
2745  fprintf(s,"s");
2746  }
2747  }
2748 
2749 #ifdef COMPACT
2750  fprintf(s,"\n");
2751 #else
2752  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2753  {
2754  tag = BiddyGetTag(f);
2755  fprintf(s," %s\n",BiddyManagedGetVariableName(MNG,tag));
2756  } else {
2757  fprintf(s,"\n");
2758  }
2759 #endif
2760 
2761  if (!BiddyIsTerminal(f)) {
2762  WriteBddviewConnections(MNG,s,f); /* this will select all nodes except terminal node */
2763  BiddyDeleteLocalInfo(MNG,f);
2764  }
2765 
2766  if (filename) {
2767  fclose(s);
2768  }
2769 
2770  return n;
2771 }
2772 
2773 /*----------------------------------------------------------------------------*/
2774 /* Definition of other internal functions */
2775 /*----------------------------------------------------------------------------*/
2776 
2777 /*----------------------------------------------------------------------------*/
2778 /* Definition of static functions */
2779 /*----------------------------------------------------------------------------*/
2780 
2781 /* Some of these were implemented long time ago (1995). */
2782 
2783 static Biddy_Boolean
2784 charOK(char c)
2785 {
2786  return (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z') || c == '_' ||
2787  (c >= '0' && c <= '9') || c == '[' || c == ']' ||
2788  c == '+' || c == '-' || c == '*' || c == '\'' ||
2789  c == '$' || c == '&' || c == '%' || c == '#' ||
2790  c == '?' || c == '!' || c == ':' || c == '.' ;
2791 }
2792 
2793 static void
2794 nextCh(Biddy_String s, int *i, Biddy_String *ch)
2795 {
2796  char c;
2797  int j;
2798 
2799  while (s[*i] == ' ' || s[*i] == '\t' || s[*i] == '\n') (*i)++;
2800  j = *i;
2801  c = s[*i];
2802 
2803  /* DEBUGGING */
2804  /*
2805  printf("%c",c);
2806  */
2807 
2808  if (c == '(') {
2809  (*i)++;
2810  strcpy(*ch,"(");
2811  }
2812 
2813  else if (c == ')') {
2814  (*i)++;
2815  strcpy(*ch,")");
2816  }
2817 
2818  else if (c == '*') {
2819  (*i)++;
2820  strcpy(*ch,"*");
2821  }
2822 
2823  else if (charOK(c)) {
2824  (*i)++;
2825  while (charOK(s[*i])) (*i)++;
2826  c = s[*i];
2827  if ( (c == ' ') || (c == '\t') || (c == '\n') || (c == '(') || (c == ')') ) {
2828  strncpy(*ch, &(s[j]), *i-j);
2829  (*ch)[*i-j] = 0;
2830  }
2831  }
2832 
2833  else {
2834  strcpy(*ch,"");
2835  }
2836 
2837  /* DEBUGGING */
2838  /*
2839  printf("nextCh: '%s'\n",*ch);
2840  */
2841 }
2842 
2843 static Biddy_Edge
2844 ReadBDD(Biddy_Manager MNG, Biddy_String s, int *i, Biddy_String *ch)
2845 {
2846  Biddy_Boolean inv;
2847  Biddy_String varname;
2848  Biddy_Edge f,n,e,t;
2849 
2850  assert( (biddyManagerType == BIDDYTYPEOBDD) || (biddyManagerType == BIDDYTYPEOBDDC) );
2851 
2852  nextCh(s,i,ch);
2853 
2854  if (strcmp(*ch,"*")) {
2855  inv = FALSE;
2856  } else {
2857  inv = TRUE;
2858  /* printf("<*>\n"); */
2859  nextCh(s,i,ch);
2860  }
2861 
2862  /* printf("<%s>\n",*ch); */
2863 
2864  if (!strcmp(*ch,"0")) {
2865  if (inv) {
2866  f = biddyOne;
2867  } else {
2868  f = biddyZero;
2869  }
2870  } else if (!strcmp(*ch,"1")) {
2871  if (inv) {
2872  f = biddyZero;
2873  } else {
2874  f = biddyOne;
2875  }
2876  } else {
2877  varname = strdup(*ch);
2878  n = BiddyManagedGetVariableEdge(MNG,BiddyManagedGetVariable(MNG,varname)); /* variables should already exist */
2879  if (!n) return biddyNull;
2880  nextCh(s,i,ch);
2881  if (strcmp(*ch,"(")) {
2882  printf("ERROR: <%s>\n",*ch);
2883  return biddyNull;
2884  }
2885  e = ReadBDD(MNG,s,i,ch);
2886  nextCh(s,i,ch);
2887  if (strcmp(*ch,")")) {
2888  printf("ERROR: <%s>\n",*ch);
2889  return biddyNull;
2890  }
2891  nextCh(s,i,ch);
2892  if (strcmp(*ch,"(")) {
2893  printf("ERROR: <%s>\n",*ch);
2894  return biddyNull;
2895  }
2896  t = ReadBDD(MNG,s,i,ch);
2897  nextCh(s,i,ch);
2898  if (strcmp(*ch,")")) {
2899  printf("ERROR: <%s>\n",*ch);
2900  return biddyNull;
2901  }
2902  if (inv) {
2903  f = BiddyManagedNot(MNG,BiddyManagedITE(MNG,n,t,e));
2904  } else {
2905  f = BiddyManagedITE(MNG,n,t,e);
2906  }
2907  free(varname);
2908  }
2909 
2910  return f;
2911 }
2912 
2913 static void
2914 createVariablesFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, Biddy_LookupFunction lf)
2915 {
2916  int i;
2917  unsigned int idx;
2918  Biddy_Edge tmp;
2919 
2920  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
2921  {
2922  for (i = 0; i <= tree->availableNode; i++) {
2923  if (tree->tnode[i].op == 255) {
2924  if (tree->tnode[i].name) {
2925  if (!lf) {
2926  if (!BiddyManagedFindFormula(MNG,tree->tnode[i].name,&idx,&tmp))
2927  {
2928  BiddyManagedAddVariableByName(MNG,tree->tnode[i].name);
2929  }
2930  } else {
2931  if ((!(lf(tree->tnode[i].name,&tmp))) &&
2932  (!BiddyManagedFindFormula(MNG,tree->tnode[i].name,&idx,&tmp)))
2933  {
2934  BiddyManagedAddVariableByName(MNG,tree->tnode[i].name);
2935  }
2936  }
2937  }
2938  }
2939  }
2940  }
2941 
2942 #ifndef COMPACT
2943  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2944  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2945  {
2946  for (i = tree->availableNode; i >= 0; i--) {
2947  if (tree->tnode[i].op == 255) {
2948  if (tree->tnode[i].name) {
2949  if (!lf) {
2950  if (!BiddyManagedFindFormula(MNG,tree->tnode[i].name,&idx,&tmp))
2951  {
2952  BiddyManagedAddVariableByName(MNG,tree->tnode[i].name);
2953  }
2954  } else {
2955  if ((!(lf(tree->tnode[i].name,&tmp))) &&
2956  (!BiddyManagedFindFormula(MNG,tree->tnode[i].name,&idx,&tmp)))
2957  {
2958  BiddyManagedAddVariableByName(MNG,tree->tnode[i].name);
2959  }
2960  }
2961  }
2962  }
2963  }
2964  }
2965 #endif
2966 }
2967 
2968 static Biddy_Edge
2969 createBddFromBTree(Biddy_Manager MNG, BiddyBTreeContainer *tree, int i, Biddy_LookupFunction lf)
2970 {
2971  unsigned int idx;
2972  Biddy_Edge lbdd,rbdd,fbdd;
2973 
2974  if (i == -1) return biddyNull;
2975  if (tree->tnode[i].op == 255) {
2976  if (tree->tnode[i].name) {
2977  if (!strcmp(tree->tnode[i].name,"0")) {
2978  fbdd = biddyZero;
2979  } else if (!strcmp(tree->tnode[i].name,"1")) {
2980  fbdd = biddyOne;
2981  } else {
2982  if (!lf) {
2983  if (!BiddyManagedFindFormula(MNG,tree->tnode[i].name,&idx,&fbdd))
2984  {
2985  fbdd = BiddyManagedGetVariableEdge(MNG,BiddyManagedAddVariableByName(MNG,tree->tnode[i].name));
2986  }
2987  } else {
2988  if ((!(lf(tree->tnode[i].name,&fbdd))) &&
2989  (!BiddyManagedFindFormula(MNG,tree->tnode[i].name,&idx,&fbdd)))
2990  {
2991  fbdd = BiddyManagedGetVariableEdge(MNG,BiddyManagedAddVariableByName(MNG,tree->tnode[i].name));
2992  }
2993  }
2994  assert( fbdd != biddyNull );
2995  }
2996  } else {
2997  fbdd = biddyNull;
2998  }
2999 
3000  /* DEBUGGING */
3001  /*
3002  printf("createBddFromBTree: op == 255\n");
3003  printPrefixFromBTree(tree,i);
3004  printf("\n");
3005  printf("HERE IS fbdd:\n");
3006  BiddyManagedPrintfBDD(MNG,fbdd);
3007  BiddyManagedPrintfSOP(MNG,fbdd);
3008  */
3009 
3010  return fbdd;
3011  }
3012  lbdd = createBddFromBTree(MNG,tree,tree->tnode[i].left,lf);
3013  rbdd = createBddFromBTree(MNG,tree,tree->tnode[i].right,lf);
3014 
3015  /* NOT (~!), AND (&*), BUTNOT (\), NOTBUT (/), XOR (^%), OR (|+), NOR (#), XNOR(-), IMPLIES-LEFT (<), IMPLIES-RIGHT (>), NAND (@) */
3016  /* char boolOperators[] = { '~', '&', '\\', ' ', '/', ' ', '^', '|', '#', '-', ' ', '<', ' ', '>', '@', ' ' }; */
3017  if (tree->tnode[i].op == oNOT) fbdd = BiddyManagedNot(MNG,rbdd); /* NOT */
3018  else if (tree->tnode[i].op == oAND) fbdd = BiddyManagedAnd(MNG,lbdd,rbdd); /* AND */
3019  else if (tree->tnode[i].op == oBUTNOT) fbdd = BiddyManagedGt(MNG,lbdd,rbdd); /* BUTNOT */
3020  else if (tree->tnode[i].op == oNOTBUT) fbdd = BiddyManagedGt(MNG,rbdd,lbdd); /* NOTBUT */
3021  else if (tree->tnode[i].op == oXOR) fbdd = BiddyManagedXor(MNG,lbdd,rbdd); /* XOR */
3022  else if (tree->tnode[i].op == oOR) fbdd = BiddyManagedOr(MNG,lbdd,rbdd); /* OR */
3023  else if (tree->tnode[i].op == oNOR) fbdd = Biddy_Managed_Nor(MNG,lbdd,rbdd); /* NOR is not directly implemented for all BDD types */
3024  else if (tree->tnode[i].op == oXNOR) fbdd = Biddy_Managed_Xnor(MNG,lbdd,rbdd); /* XNOR is not directly implemented for all BDD types */
3025  else if (tree->tnode[i].op == oIMPLEFT) fbdd = BiddyManagedLeq(MNG,rbdd,lbdd); /* IMPLIES <= */
3026  else if (tree->tnode[i].op == oIMPRIGHT) fbdd = BiddyManagedLeq(MNG,lbdd,rbdd); /* IMPLIES => */
3027  else if (tree->tnode[i].op == oNAND) fbdd = Biddy_Managed_Nand(MNG,lbdd,rbdd); /* NAND is not directly implemented for all BDD types */
3028  else fbdd = biddyNull;
3029 
3030  /* DEBUGGING */
3031  /*
3032  printf("createBddFromBTree: op == %u\n",tree->tnode[i].op);
3033  printPrefixFromBTree(tree,i);
3034  printf("\n");
3035  printf("HERE IS lbdd:\n");
3036  BiddyManagedPrintfBDD(MNG,lbdd);
3037  BiddyManagedPrintfSOP(MNG,lbdd);
3038  printf("HERE IS rbdd:\n");
3039  BiddyManagedPrintfBDD(MNG,rbdd);
3040  BiddyManagedPrintfSOP(MNG,rbdd);
3041  printf("HERE IS fbdd:\n");
3042  BiddyManagedPrintfBDD(MNG,fbdd);
3043  BiddyManagedPrintfSOP(MNG,fbdd);
3044  */
3045 
3046  return fbdd;
3047 }
3048 
3049 static void
3050 evaluate1(Biddy_Manager MNG, BiddyBTreeContainer *tree, Biddy_String s,
3051  int *i, Biddy_String *ch, Biddy_LookupFunction lf)
3052 {
3053  int op;
3054  int current,left,right;
3055 
3056  /* DEBUGGING */
3057  /*
3058  printf("evaluate1: i = %d, ch = '%s', s = '%s'\n",*i,*ch,s);
3059  */
3060 
3061  if (!strcmp(*ch,"(")) {
3062  nextCh(s,i,ch);
3063  op = Op(s,i,ch); /* this performs nextCh() */
3064 
3065  if (op == 0) {
3066  /* operator NOT */
3067  left = -1;
3068  evaluate1(MNG,tree,s,i,ch,lf);
3069  right = tree->availableNode;
3070 
3071  current = tree->tnode[tree->availableNode].parent;
3072  if (current == -1) {
3073  printf("evaluate1: BiddyBTreeContainer out of space!\n");
3074  exit(1);
3075  }
3076 
3077  if (left != -1) tree->tnode[left].parent = current;
3078  if (right != -1) tree->tnode[right].parent = current;
3079  tree->tnode[current].op = op;
3080  tree->tnode[current].left = left;
3081  tree->tnode[current].right = right;
3082  tree->availableNode = current;
3083 
3084  } else if (op > 0) {
3085  /* operators AND, OR, XOR */
3086  evaluate1(MNG,tree,s,i,ch,lf);
3087  evaluateN(MNG,tree,s,i,ch,op,lf);
3088  } else {
3089  /* variable or extra open parenthesis */
3090  evaluate1(MNG,tree,s,i,ch,lf);
3091  }
3092 
3093  if (!strcmp(*ch,")")) {
3094  nextCh(s,i,ch);
3095  } else {
3096  printf("evaluate1: missing closing paranthesis\n");
3097  }
3098 
3099  return;
3100  }
3101 
3102  if (charOK(*ch[0])) {
3103  left = right = -1;
3104  current = tree->tnode[tree->availableNode].parent;
3105  if (current == -1) {
3106  printf("evaluate1: BiddyBTreeContainer out of space!\n");
3107  exit(1);
3108  }
3109 
3110  tree->tnode[current].op = 255;
3111  tree->tnode[current].name = strdup(*ch);
3112  tree->tnode[current].left = left;
3113  tree->tnode[current].right = right;
3114  tree->availableNode = current;
3115 
3116  nextCh(s,i,ch);
3117  return;
3118  }
3119 }
3120 
3121 static void
3122 evaluateN(Biddy_Manager MNG, BiddyBTreeContainer *tree, Biddy_String s,
3123  int *i, Biddy_String *ch, int op, Biddy_LookupFunction lf)
3124 {
3125  int current,left,right;
3126 
3127  /* DEBUGGING */
3128  /*
3129  printf("evaluateN: i = %d, ch = '%s', s = '%s'\n",*i,*ch,s);
3130  */
3131 
3132  left = tree->availableNode;
3133  evaluate1(MNG,tree,s,i,ch,lf);
3134  right = tree->availableNode;
3135  if (right != left) {
3136  current = tree->tnode[tree->availableNode].parent;
3137  if (current == -1) {
3138  printf("evaluateN: BiddyBTreeContainer out of space!\n");
3139  exit(1);
3140  }
3141 
3142  if (left != -1) tree->tnode[left].parent = current;
3143  if (right != -1) tree->tnode[right].parent = current;
3144  tree->tnode[current].op = op;
3145  tree->tnode[current].left = left;
3146  tree->tnode[current].right = right;
3147  tree->availableNode = current;
3148 
3149  evaluateN(MNG,tree,s,i,ch,op,lf);
3150  }
3151 }
3152 
3153 /*
3154 This must be compatible with defined global macros:
3155 #define oNOT 0
3156 #define oAND 1
3157 #define oBUTNOT 2
3158 #define oNOTBUT 4
3159 #define oXOR 6
3160 #define oOR 7
3161 #define oNOR 8
3162 #define oXNOR 9
3163 #define oIMPLEFT 11
3164 #define oIMPRIGHT 13
3165 #define oNAND 14
3166 */
3167 
3168 static int
3169 Op(Biddy_String s, int *i, Biddy_String *ch)
3170 {
3171 
3172  /* DEBUGGING */
3173  /*
3174  printf("Op ch = %s\n",*ch);
3175  */
3176 
3177  if (!strcasecmp(*ch, "NOT")) {
3178  nextCh(s,i,ch);
3179  return oNOT;
3180  }
3181 
3182  else if (!strcasecmp(*ch, "AND")) {
3183  nextCh(s,i,ch);
3184  return oAND;
3185  }
3186 
3187  else if (!strcasecmp(*ch, "XOR")) {
3188  nextCh(s,i,ch);
3189  return oXOR;
3190  }
3191 
3192  else if (!strcasecmp(*ch, "EXOR")) {
3193  nextCh(s,i,ch);
3194  return oXOR;
3195  }
3196 
3197  else if (!strcasecmp(*ch, "OR")) {
3198  nextCh(s,i,ch);
3199  return oOR;
3200  }
3201 
3202  else if (!strcasecmp(*ch, "NOR")) {
3203  nextCh(s,i,ch);
3204  return oNOR;
3205  }
3206 
3207  else if (!strcasecmp(*ch, "XNOR")) {
3208  nextCh(s,i,ch);
3209  return oXNOR;
3210  }
3211 
3212  else if (!strcasecmp(*ch, "NAND")) {
3213  nextCh(s,i,ch);
3214  return oNAND;
3215  }
3216 
3217  return -1;
3218 }
3219 
3220 static void
3221 parseVerilogFile(FILE *verilogfile, unsigned int *l, BiddyVerilogLine ***lt, unsigned int *n, BiddyVerilogModule ***mt)
3222 {
3223  unsigned int activemodule=0;
3224  BiddyVerilogLine *ln;
3225  BiddyVerilogModule *md;
3226  unsigned int i=0, j=0, k=0; /* indexes */
3227  char ch, linebuf[LINESIZE]; /* buffer for single line from the verilog file */
3228  Biddy_String buffer; /* buffer for complete verilog statements */
3229  Biddy_String token[TOKENNUM]; /* array to hold tokens for the line */
3230  Biddy_String keyword; /* keyword from verilog line */
3231  Biddy_Boolean comment, noname, ok, acceptable;
3232  Biddy_String t,tc;
3233  unsigned int tn;
3234 
3235  (*l) = 0;
3236  (*lt) = NULL;
3237  (*n) = 0;
3238  (*mt) = NULL;
3239 
3240  keyword = NULL;
3241  buffer = NULL;
3242  md = NULL;
3243  while (fgets(linebuf,LINESIZE,verilogfile) != NULL) {
3244 
3245  if (keyword) free(keyword);
3246  tn = (unsigned int) strspn(linebuf," ");
3247 
3248  if (tn == strlen(linebuf)) {
3249  continue; /* skip empty lines and white space */
3250  }
3251 
3252  /* get 1st word from the line */
3253  tn += (unsigned int) strcspn(&linebuf[tn]," ");
3254  ch = 0;
3255  if (tn < strlen(linebuf)) {
3256  ch = linebuf[tn];
3257  linebuf[tn] = 0;
3258  }
3259  tn = (unsigned int) strspn(linebuf," ");
3260  keyword = strdup(&linebuf[tn]);
3261  if (ch) {
3262  tn += (unsigned int) strcspn(&linebuf[tn]," ");
3263  linebuf[tn] = ch;
3264  }
3265  keyword = trim(keyword);
3266 
3267  if (!strlen(keyword)) {
3268  continue; /* skip white space not recognised before */
3269  }
3270 
3271  if (!strcmp(keyword,"//")) {
3272  continue; /* skip comment lines */
3273  }
3274 
3275  if (buffer) free(buffer);
3276  buffer = strdup("");
3277  if (!strcmp(keyword,"endmodule")) { /* endmodule keyword does not use ';' */
3278  concat(&buffer," ");
3279  concat(&buffer,keyword);
3280  } else {
3281  concat(&buffer," ");
3282  concat(&buffer,linebuf);
3283  while (!isEndOfLine(linebuf)) { /* check if the line ends with a ';' character (multiple lines statement) */
3284  if (fgets(linebuf,LINESIZE,verilogfile) != NULL) {/* otherwise, append all the following lines */
3285  concat(&buffer," ");
3286  concat(&buffer,linebuf);
3287  if ((strlen(buffer) + LINESIZE) > BUFSIZE) printf("ERROR (parseVerilogFile): BUFFER TO SMALL\n");
3288  }
3289  }
3290  }
3291 
3292  /* tokenize the line to extract data */
3293  noname = FALSE;
3294  if (strcmp(keyword,"module") && strcmp(keyword,"endmodule") &&
3295  strcmp(keyword,"input") && strcmp(keyword,"output") &&
3296  strcmp(keyword,"wire") && strcmp(keyword,"reg") &&
3297  strcmp(keyword,"assign"))
3298  {
3299  tn = (unsigned int) strspn(buffer," ");
3300  tn += (unsigned int) strcspn(&buffer[tn]," ");
3301  tn += (unsigned int) strspn(&buffer[tn]," ");
3302  if (buffer[tn] == '(') noname = TRUE;
3303  }
3304  i=0;
3305  comment = FALSE;
3306  t = strtok(buffer," ");
3307  token[i++] = strdup(t); /* full keyword */
3308  if (noname) {
3309  sprintf(linebuf,"NONAME%d",(*l));
3310  token[i++] = strdup(linebuf); /* add NONAME */
3311  }
3312  while ((t = strtok(NULL," (),;\r\n")) && (strcmp(t,"//"))) {
3313  if (!strcmp(t,"/*")) comment = TRUE;
3314  if (!comment) {
3315  if (strlen(t)>1) {
3316  tn = (unsigned int) strcspn(t,"{}");
3317  while (tn != strlen(t)) {
3318  tc = NULL;
3319  if (t[tn] == '{') tc = strdup("{");
3320  if (t[tn] == '}') tc = strdup("}");
3321  if (tn) {
3322  t[tn] = 0;
3323  token[i++] = strdup(t);
3324  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
3325  }
3326  token[i++] = tc;
3327  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
3328  t = &t[tn+1];
3329  tn = (unsigned int) strcspn(t,"{}");
3330  }
3331  }
3332  if (strlen(t)) {
3333  token[i++] = strdup(t);
3334  if (i >= TOKENNUM) printf("ERROR (parseVerilogFile): TOKENNUM TO SMALL\n");
3335  }
3336  }
3337  if (comment && !strcmp(t,"*/")) comment = FALSE;
3338  }
3339  token[i] = NULL;
3340 
3341  if (!strcmp(keyword,"module")) { /* START OF MODULE */
3342  (*n)++;
3343  (*mt) = (BiddyVerilogModule **) realloc((*mt), (*n) * sizeof(BiddyVerilogModule *)); /* create or enlarge table of modules */
3344  md = (BiddyVerilogModule *) calloc(1, sizeof(BiddyVerilogModule)); /* declare an instance of a module */
3345  (*mt)[(*n)-1] = md;
3346  md->name = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for module name string */
3347  strcpy(md->name,token[1]); /* set module name */
3348  activemodule = (*n);
3349  /* DEBUGGING */
3350  /*
3351  printf("MODULE: %s (#%d)\n",token[1],activemodule);
3352  */
3353  md->outputFirst = TRUE; /* TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3), FALSE iff N3 = NAND(N1,N2) */
3354  }
3355 
3356  if (!strcmp(keyword,"endmodule")) { /* END OF MODULE */
3357  /* DEBUGGING */
3358  /*
3359  printf("ENDMODULE: #%d\n",activemodule);
3360  */
3361  activemodule = 0;
3362  md = NULL;
3363  } else {
3364  if (!activemodule) {
3365  printf("ERROR (parseVerilogFile): statement <%s> is outside of module\n",keyword);
3366  continue;
3367  }
3368  }
3369 
3370  acceptable = FALSE;
3371  if ((activemodule == 1) || !strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
3372  /* TO DO: MULTIPLE MODULES ARE NOT SUPPORTED, YET */
3373 
3374  if (!strcmp(keyword,"module") || !strcmp(keyword,"endmodule")) {
3375  acceptable = TRUE;
3376  }
3377 
3378  else if (!strcmp(keyword,"input")) { /* PRIMARY INPUTS */
3379  acceptable = TRUE;
3380  for (j = 1; j < i; j++) { /* parse all the words in the line */
3381  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
3382  parseSignalVector(md->inputs, token, &j, &md->inputcount);
3383  else { /* not a vector of signal */
3384  md->inputs[md->inputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for input string */
3385  strcpy(md->inputs[md->inputcount],token[j]); /* add the input name to the array of inputs */
3386  (md->inputcount)++; /* update the number of inputs in the circuit */
3387  if (md->inputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
3388  }
3389  }
3390  }
3391 
3392  else if (!strcmp(keyword,"output")) { /* PRIMARY OUTPUTS */
3393  acceptable = TRUE;
3394  for (j = 1; j < i; j++) { /* parse all the words in the line */
3395  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
3396  parseSignalVector(md->outputs, token, &j, &md->outputcount);
3397  else { /* not a vector of signal */
3398  md->outputs[md->outputcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for output string */
3399  strcpy(md->outputs[md->outputcount],token[j]); /* add the output name to the array of outputs */
3400  (md->outputcount)++; /* update the number of outputs in the circuit */
3401  if (md->outputcount >= INOUTNUM) printf("ERROR (parseVerilogFile): INOUTNUM TO SMALL\n");
3402  }
3403  }
3404  }
3405 
3406  else if (!strcmp(keyword,"wire")) { /* WIRES */
3407  for (j = 1; j < i; j++) { /* parse all the words in the line */
3408  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
3409  parseSignalVector(md->wires, token, &j, &md->wirecount);
3410  else { /* not a vector of signal */
3411  /* check if this wire has not already been stated as input or output */
3412  ok = TRUE;
3413  for (k=0; k < md->inputcount; k++) {
3414  if (!strcmp(md->inputs[k],token[j])) ok = FALSE;
3415  }
3416  for (k=0; k < md->outputcount; k++) {
3417  if (!strcmp(md->outputs[k],token[j])) ok = FALSE;
3418  }
3419  if (ok) {
3420  acceptable = TRUE;
3421  md->wires[md->wirecount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for wire string */
3422  strcpy(md->wires[md->wirecount],token[j]); /* add the wire name to the array of wires */
3423  (md->wirecount)++; /* update the number of wires in the circuit */
3424  if (md->wirecount >= WIRENUM) printf("ERROR (parseVerilogFile): WIRENUM TO SMALL\n");
3425  } else {
3426  /* DEBUGGING */
3427  /*
3428  printf("WARNING (parseVerilogFile): wire %s already defined as input/output\n",token[j]);
3429  */
3430  }
3431  }
3432  }
3433  }
3434 
3435  else if (!strcmp(keyword,"reg")) { /* REGS */
3436  acceptable = TRUE;
3437  for (j = 1; j < i; j++) { /* parse all the words in the line */
3438  if (isSignalVector(token[j])) /* handle a vector of signals, this is not implemented correctly! */
3439  parseSignalVector (md->regs, token, &j, &md->regcount);
3440  else { /* not a vector of signal */
3441  md->regs[md->regcount] = (Biddy_String) calloc(strlen(token[j]) + 1, sizeof(char)); /* allocating memory for reg string */
3442  strcpy(md->regs [md->regcount],token[j]); /* add the reg name to the array of regs */
3443  (md->regcount)++; /* update the number of regs in the circuit */
3444  if (md->regcount >= REGNUM) printf("ERROR (parseVerilogFile): REGNUM TO SMALL\n");
3445  }
3446  }
3447  }
3448 
3449  else if (isGate(keyword)) { /* BASIC GATES */
3450  acceptable = TRUE;
3451  md->gates[md->gatecount] = (Biddy_String) calloc(strlen(token[1]) + 1, sizeof(char)); /* allocating memory for gate name string */
3452  strcpy(md->gates[md->gatecount],token[1]); /* add the gate name to the array of gates */
3453  if (!md->gatecount) { /* use the first gate to determine md->outputFirst */
3454  for (j=0; md->inputs[j] != NULL; j++) if (!strcmp(md->inputs[j],token[2])) md->outputFirst = FALSE;
3455  }
3456  (md->gatecount)++; /* update the number of gates in the circuit */
3457  if (md->gatecount >= GATENUM) printf("ERROR (parseVerilogFile): GATENUM TO SMALL\n");
3458  }
3459 
3460  else {
3461  /* AN UNIMPLEMENTED KEYWORD */
3462  /* GATES DEFINED BY OTHER MODULES ARE NOT RESOLVED */
3463  }
3464 
3465  }
3466 
3467  /* add this line to the table of acceptable lines */
3468  if (acceptable) {
3469  (*l)++;
3470  (*lt) = (BiddyVerilogLine **) realloc((*lt), (*l) * sizeof(BiddyVerilogLine *)); /* create or enlarge table of lines */
3471  ln = (BiddyVerilogLine *) calloc(1, sizeof(BiddyVerilogLine)); /* declare an instance of a line */
3472  ln->keyword = strdup(keyword);
3473  ln->line = strdup(token[0]);
3474  for (j=1; j<i; j++) {
3475  concat(&(ln->line)," ");
3476  concat(&(ln->line),token[j]);
3477  }
3478  (*lt)[(*l)-1] = ln;
3479  }
3480 
3481  }
3482 
3483  if (keyword) free(keyword);
3484  if (buffer) free(buffer);
3485 
3486  /* DEBUGGING - print summary of the module */
3487  /*
3488  printModuleSummary(m);
3489  */
3490 }
3491 
3496 static void
3497 createVerilogCircuit(unsigned int linecount, BiddyVerilogLine **lt, unsigned int modulecount, BiddyVerilogModule **mt, BiddyVerilogCircuit *c)
3498 {
3499  BiddyVerilogModule *m;
3500  unsigned int i=0, j=0, k=0, l=0;
3501  int in=0, id=0, index=0;
3502  unsigned int activemodule=0;
3503  Biddy_String keyword, buffer;
3504  Biddy_String token[TOKENNUM]; /* array to hold tokens for one line */
3505  Biddy_Boolean ok;
3506  Biddy_String tmptoken;
3507 
3508  memset(token, 0, sizeof(char*) * TOKENNUM);
3509 
3510  m = mt[0]; /* target module is the first one in the table */
3511 
3512  /* initialization of the circuit */
3513  c->inputcount = m->inputcount; /* set the number of inputs for the ciruit */
3514  c->outputcount = m->outputcount; /* set the number of outputs for the circuit */
3515  c->wirecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of wires for the circuit */
3516  c->nodecount = m->inputcount + m->outputcount + m->wirecount + m->gatecount; /* set the number of nodes for the circuit */
3517  c->wires = (BiddyVerilogWire **) calloc(c->wirecount,sizeof(BiddyVerilogWire *)); /* allocate a contiguous array to index every wire */
3518  c->nodes = (BiddyVerilogNode **) calloc(c->nodecount,sizeof(BiddyVerilogNode *)); /* allocate a contiguous array to index every node */
3519 
3520  id = 0 * modulecount; // to avoif unused warning for modulecount
3521  for (i=0; i < m->inputcount; i++) { /* store the names of primary inputs */
3522  c->inputs[i] = (Biddy_String) calloc(strlen(m->inputs[i]) + 1, sizeof (char));
3523  strcpy(c->inputs[i],m->inputs[i]);
3524  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
3525  buildNode(c->nodes[id],(Biddy_String)"input", m->inputs[i]);
3526  id++;
3527  }
3528  for (i=0; i < m->outputcount; i++) { /* store the names of primary outputs */
3529  c->outputs[i] = (Biddy_String) calloc(strlen(m->outputs[i]) + 1, sizeof(char));
3530  strcpy(c->outputs[i],m->outputs[i]);
3531  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
3532  buildNode(c->nodes[id],(Biddy_String)"output",m->outputs[i]);
3533  id++;
3534  }
3535  for (i=0; i < m->wirecount; i++) { /* store the names of wires */
3536  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
3537  buildNode(c->nodes[id],(Biddy_String)"wire",m->wires[i]);
3538  id++;
3539  }
3540  for (i=0; i < m->gatecount; i++) { /* store the names of gates */
3541  c->nodes[id] = (BiddyVerilogNode *) calloc(1,sizeof(BiddyVerilogNode));
3542  buildNode(c->nodes[id],(Biddy_String)"gate",m->gates[i]);
3543  id++;
3544  }
3545 
3546  index = 0;
3547  for (l=0; l<linecount;l++) {
3548  keyword = lt[l]->keyword;
3549  buffer = lt[l]->line;
3550 
3551  if (!strcmp(keyword,"module")) {
3552  activemodule++;
3553  continue;
3554  }
3555 
3556  if (!strcmp(keyword,"endmodule")) {
3557  continue;
3558  }
3559 
3560  if (activemodule > 1) {
3561  /* TO DO: MULTIPLE MODULES ARE NOT FULLY SUPPORTED, YET */
3562  continue;
3563  }
3564 
3565  if (!strcmp(keyword,"input")) {
3566  continue;
3567  }
3568  if (!strcmp(keyword,"output")) {
3569  continue;
3570  }
3571  if (!strcmp(keyword,"wire")) {
3572  continue;
3573  }
3574  if (!strcmp(keyword,"reg")) {
3575  continue;
3576  }
3577  if (!strcmp(keyword,"assign")) {
3578  continue;
3579  }
3580 
3581  /* tokenize the line to extract data */
3582  i=0;
3583  token[0] = strtok(buffer," ");
3584  while(token[i]!= NULL) {
3585  /* DEBUGGING */
3586  /*
3587  printf("(#%d) TOKENIZE: <%s>\n",i,token[i]);
3588  */
3589  i++;
3590  token[i] = strtok(NULL," ");
3591  }
3592 
3593  if (!isGate(keyword)) {
3594  printf("WARNING (createVerilogCircuit): SKIP <%s>\n",buffer);
3595  continue;
3596  }
3597 
3598  if (!m->outputFirst) {
3599  /* m->outputFirst == FALSE iff "nand NAND2_1 (N1, N2, N3);" defines N3 = NAND(N1,N2) */
3600  /* m->outputFirst == TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3) */
3601  /* exchange token[2] and token[i-1] */
3602  tmptoken = token[2];
3603  token[2] = token[i-1];
3604  token[i-1] = tmptoken;
3605  }
3606 
3607  /* A. Check or create wires for all the gate inputs */
3608  /* if wire is not known it will be treated as a primary input */
3609  for (j = 3; j < i; j++) {
3610  if (!isDefined(c,token[j])) {
3611  ok = FALSE;
3612  for (k=0; k < m->wirecount; k++) { /* check the names of wires */
3613  if (!strcmp(m->wires[k],token[j])) {
3614  printf("ERROR (createVerilogCircuit): wire %s used before defined!\n",token[j]);
3615  exit(1);
3616  }
3617  }
3618  for (k=0; !ok && k < m->inputcount; k++) { /* check the names of primary inputs */
3619  if (!strcmp(m->inputs[k],token[j])) ok = TRUE;
3620  }
3621  if (!ok) {
3622  printf("WARNING (createVerilogCircuit): wire %s treated as primary input!\n",token[j]);
3623  }
3624  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
3625  buildWire(c,c->wires[index],(Biddy_String)"I",token[j]);
3626  /* assign inputs to the wires representing gate inputs */
3627  /* NOT NEEDED */
3628  /* assign outputs to the wires representing gate inputs */
3629  /* NOT USED */
3630  index++;
3631  }
3632  }
3633 
3634  /* B. Create a wire for the gate */
3635  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
3636  buildWire(c,c->wires[index],keyword,token[1]);
3637  /* assign inputs to the wire representing gate */
3638  in = 0;
3639  for (j = 3; j < i; j++) {
3640  c->wires[index]->inputs[in] = getNodeIdByName(c,token[j]);
3641  c->wires[index]->inputcount++;
3642  in++;
3643  }
3644  /* assign outputs to the wire representing gate */
3645  /* NOT USED */
3646  index++;
3647 
3648  /* C. Check or create a wire for the gate output */
3649  if (!isDefined(c,token[2])) { /* if wire is not already defined */
3650  c->wires[index] = (BiddyVerilogWire *) calloc(1,sizeof(BiddyVerilogWire));
3651  buildWire(c,c->wires[index],(Biddy_String)"W",token[2]);
3652  /* assign inputs to the wire representing gate ouput */
3653  c->wires[index]->inputs[0] = getNodeIdByName(c,token[1]);
3654  c->wires[index]->inputcount = 1;
3655  /* assign outputs to the wire representing gate ouput */
3656  /* NOT USED */
3657  index++;
3658  } else { /* if wire is already defined */
3659  getWireByName(c,token[2])->inputs[0] = getNodeIdByName(c,token[1]); /* find the wire and attach an input to it */
3660  getWireByName(c,token[2])->inputcount = 1;
3661  }
3662 
3663  }
3664 
3665  c->wirecount = index;
3666 
3667  /* c->wires[i]->fanout is the count of gates (and wires), where */
3668  /* this wire is used as an input */
3669  i=0;
3670  while (i<c->wirecount && c->wires[i] != NULL) {
3671  for (j=0; j<c->wires[i]->inputcount; j++) {
3672  (getWireById(c,c->wires[i]->inputs[j])->fanout)++;
3673  /* DEBUGGING */
3674  /*
3675  printf("Increment TTL for wire %d\n",c->wires[i]->inputs[j]);
3676  */
3677  }
3678  i++;
3679  }
3680 
3681  /* DEBUGGING - print summary of the circuit */
3682  /*
3683  printCircuitSummary(c);
3684  */
3685 }
3686 
3695 static void
3696 createBddFromVerilogCircuit(Biddy_Manager MNG, BiddyVerilogCircuit *c, Biddy_String prefix)
3697 {
3698  unsigned int i,j;
3699  BiddyVerilogWire *w;
3700  Biddy_Edge f;
3701 
3702  /* DEBUGGING */
3703  /*
3704  printf("Creating %d primary inputs\n",c->inputcount);
3705  */
3706 
3707  /* DEBUGGING */
3708  /*
3709  for (i = 0; i < c->inputcount; i++) {
3710  printf("%s ",c->inputs[i]);
3711  }
3712  if (c->inputcount) printf("\n");
3713  */
3714 
3715  /* DEBUGGING */
3716  /*
3717  printf("Creating %d primary outputs\n",c->outputcount);
3718  */
3719 
3720  /* DEBUGGING */
3721  /*
3722  for (i = 0; i < c->outputcount; i++) {
3723  printf("%s ",c->outputs[i]);
3724  }
3725  if (c->outputcount) printf("\n");
3726  */
3727 
3728  /* DEBUGGING */
3729  /*
3730  printf("Creating %d wires\n",c->wirecount);
3731  */
3732 
3733  if (prefix) {
3734  printf("WARNING: prefix is not supported, yet");
3735  }
3736 
3737  /* create all BDD variables - important for ZBDD and TZBDD */
3738  for (i = 0; i < c->nodecount; i++) {
3739  if (!strcmp(c->nodes[i]->type,"input")) {
3740  BiddyManagedAddVariableByName(MNG,c->nodes[i]->name); /* TO DO: add prefix */
3741  }
3742  if (!strcmp(c->nodes[i]->type,"extern")) {
3743  BiddyManagedAddVariableByName(MNG,c->nodes[i]->name); /* TO DO: add prefix */
3744  }
3745  }
3746 
3747  /* prepare c->wires[i]->ttl which will be used to guide GC */
3748  for (i = 0; i < c->wirecount; i++) {
3749  c->wires[i]->ttl = 0;
3750  }
3751  for (i = 0; i < c->wirecount; i++) {
3752  for (j = 0; j < c->wires[i]->inputcount; j++) {
3753  w = getWireById(c,c->wires[i]->inputs[j]);
3754  (w->ttl)++;
3755  if (w->ttl == w->fanout) {
3756  w->ttl = i;
3757  }
3758  }
3759  }
3760  for (i = 0; i < c->outputcount; i++) {
3761  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3762  if (w) {
3763  w->ttl = c->wirecount - 1;
3764  }
3765  }
3766  for (i = 0; i < c->wirecount; i++) {
3767  if (c->wires[i]->ttl) c->wires[i]->ttl = c->wires[i]->ttl - i;
3768  }
3769 
3770  for (i = 0; i < c->wirecount; i++) {
3771 
3772  /* REPORT PROGRESS */
3773  /*
3774  printf("#%d",i);
3775  if (i == c->wirecount-1) printf("\n");
3776  */
3777 
3778  /* DEBUGGING */
3779  /*
3780  printf("Creating c->wire[%d], ",i);
3781  printf("ID: %d, ",c->wires[i]->id);
3782  printf("name: %s, ",c->nodes[c->wires[i]->id]->name);
3783  printf("type: %s, ",c->wires[i]->type);
3784  printf("fanout: %d, ",c->wires[i]->fanout);
3785  printf("ttl: %d, ",c->wires[i]->ttl);
3786  printf("Inputs (%d): ",c->wires[i]->inputcount);
3787  if (strcmp(c->wires[i]->type,"I")) {
3788  if (c->wires[i]->inputcount) {
3789  for (j=0;j<c->wires[i]->inputcount;j++) {
3790  printf("%d ",c->wires[i]->inputs[j]);
3791  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3792  printf("ERROR (gate ordering is wrong)");
3793  }
3794  }
3795  } else {
3796  printf("ERROR (wire must be a primary input or it must have some inputs)");
3797  }
3798  } else {
3799  if (c->wires[i]->inputcount) {
3800  printf("ERROR (primary input cannot have additional inputs)");
3801  } else {
3802  printf("/");
3803  }
3804  }
3805  printf("\n");
3806  */
3807 
3808  f = biddyNull;
3809 
3810  if (!strcmp(c->wires[i]->type,"I")) {
3811  if (c->wires[i]->inputcount) {
3812  printf("ERROR (primary input cannot have additional inputs)\n");
3813  } else {
3814  f = BiddyManagedGetVariableEdge(MNG,BiddyManagedGetVariable(MNG,c->nodes[c->wires[i]->id]->name)); /* TO DO: add prefix */
3815  }
3816  }
3817  else if (!strcmp(c->wires[i]->type,"M")) {
3818  /* TO DO: this will be used for gates defined by other modules */
3819  }
3820  else {
3821  if (c->wires[i]->inputcount) {
3822  for (j=0; j<c->wires[i]->inputcount; j++) {
3823  if (getWireById(c,c->wires[i]->inputs[j])->bdd == biddyNull) {
3824  printf("ERROR (gate ordering is wrong)\n");
3825  }
3826  }
3827 
3828  if (!strcmp(c->wires[i]->type,"W")) {
3829  if (c->wires[i]->inputcount == 1) {
3830  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3831  } else {
3832  printf("ERROR (internal wire must have exactly one input)\n");
3833  }
3834  }
3835 
3836  else if (!strcmp(c->wires[i]->type,"buf"))
3837  {
3838  if (c->wires[i]->inputcount != 1) {
3839  printf("ERROR (buf gate must have exactly 1 input)\n");
3840  } else {
3841  f = getWireById(c,c->wires[i]->inputs[0])->bdd;
3842  }
3843  }
3844 
3845  else if (!strcmp(c->wires[i]->type,"and"))
3846  {
3847  f = biddyOne;
3848  for (j=0; j<c->wires[i]->inputcount; j++) {
3849  f = BiddyManagedAnd(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3850  }
3851  }
3852 
3853  else if (!strcmp(c->wires[i]->type,"nand"))
3854  {
3855  f = biddyOne;
3856  for (j=0; j<c->wires[i]->inputcount; j++) {
3857  f = BiddyManagedAnd(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3858  }
3859  f = BiddyManagedNot(MNG,f);
3860  }
3861 
3862  else if (!strcmp(c->wires[i]->type,"or"))
3863  {
3864  f = biddyZero;
3865  for (j=0; j<c->wires[i]->inputcount; j++) {
3866  f = BiddyManagedOr(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3867  }
3868  }
3869 
3870  else if (!strcmp(c->wires[i]->type,"nor"))
3871  {
3872  f = biddyZero;
3873  for (j=0; j<c->wires[i]->inputcount; j++) {
3874  f = BiddyManagedOr(MNG,f,getWireById(c,c->wires[i]->inputs[j])->bdd);
3875  }
3876  f = BiddyManagedNot(MNG,f);
3877  }
3878 
3879  else if (!strcmp(c->wires[i]->type,"xor"))
3880  {
3881  if (c->wires[i]->inputcount != 2) {
3882  printf("ERROR (xor gate not having exactly 2 inputs is not supported)\n");
3883  } else {
3884  f = BiddyManagedXor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3885  getWireById(c,c->wires[i]->inputs[1])->bdd);
3886  }
3887  }
3888 
3889  else if (!strcmp(c->wires[i]->type,"xnor"))
3890  {
3891  if (c->wires[i]->inputcount != 2) {
3892  printf("ERROR (xnor gate not having exactly 2 inputs is not supported)\n");
3893  } else {
3894  f = BiddyManagedXor(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd,
3895  getWireById(c,c->wires[i]->inputs[1])->bdd);
3896  f = BiddyManagedNot(MNG,f);
3897  }
3898  }
3899 
3900  else if (!strcmp(c->wires[i]->type,"not") ||
3901  !strcmp(c->wires[i]->type,"inv"))
3902  {
3903  if (c->wires[i]->inputcount != 1) {
3904  printf("ERROR (not gate must have exactly 1 input)\n");
3905  } else {
3906  f = BiddyManagedNot(MNG,getWireById(c,c->wires[i]->inputs[0])->bdd);
3907  }
3908  }
3909 
3910  else {
3911  printf("ERROR (unimplemented type: %s)\n",c->wires[i]->type);
3912  }
3913 
3914  } else {
3915  printf("ERROR (wire must be a primary input or it must have some inputs)\n");
3916  }
3917  }
3918 
3919  c->wires[i]->bdd = f;
3920 
3921  BiddyManagedKeepFormulaProlonged(MNG,f,c->wires[i]->ttl);
3922  BiddyManagedClean(MNG);
3923  }
3924 
3925  for (i = 0; i < c->outputcount; i++) {
3926  w = getWireByName(c,c->outputs[i]); /* if NULL then this output is undefined! */
3927  if (w) {
3928  f = w->bdd;
3929  } else {
3930  f = biddyZero; /* undefined outputs are represented with biddyZero */
3931  }
3932  BiddyManagedAddFormula(MNG,c->outputs[i],f,1); /* TO DO: add prefix */
3933  }
3934  BiddyManagedClean(MNG);
3935 
3936  /*
3937  printf("Report on primary outputs\n");
3938  for (i = 0; i < c->outputcount; i++) {
3939  f = getWireByName(c,c->outputs[i])->bdd;
3940  printf("%s - %d nodes / %d nodes without complement edge\n",
3941  c->outputs[i],
3942  BiddyManagedCountNodes(MNG,f),
3943  BiddyManagedCountNodesPlain(MNG,f)
3944  );
3945  }
3946  */
3947 
3948  /* DEBUGGING */
3949  /*
3950  j = 0;
3951  for (i = 0; i < c->outputcount; i++) {
3952  f = getWireByName(c,c->outputs[i])->bdd;
3953  j = j + BiddyManagedCountNodes(MNG,f);
3954  }
3955  printf("The sum of BDD sizes for all outputs: %u\n",j);
3956  */
3957 
3958 }
3959 
3964 static void
3965 parseSignalVector(Biddy_String signal_arr[], Biddy_String token[], unsigned int *index, unsigned int *count)
3966 {
3967  int v,v1,v2;
3968  char *sig_vector; /* array to hold tokens for the line */
3969 
3970  sig_vector = strtok(token[*index],":"); /* tokenize the vector to extract vector width */
3971  v1 = atoi(sig_vector); /* starting index for the vector */
3972  sig_vector = strtok(NULL, ":");
3973  v2 = atoi(sig_vector); /* ending index for the vector */
3974  (*index)++; /* get vector name from the next token */
3975  for (v = v2; v <= v1; v++) { /* add the vector signals to the array of signals */
3976  int wordsize = (int) strlen(token[*index]); /* size of the string read from the line */
3977  signal_arr [*count] = (Biddy_String) calloc(wordsize + 1, sizeof(char)); /* allocating memory for signal string */
3978  strcpy(signal_arr [*count], token[*index]); /* add the signal name to the array of signals */
3979  (*count)++; /* update the number of signals in the circuit */
3980  }
3981 }
3982 
3986 /*
3987 static void
3988 printModuleSummary(BiddyVerilogModule *m)
3989 {
3990  unsigned int i;
3991 
3992  printf("************** Module %s statistical results *************\n", m->name);
3993 
3994  printf("Number of primary inputs: %d\n", m->inputcount);
3995  for (i = 0; i < m->inputcount; i++)
3996  printf("%s ", m->inputs[i]);
3997  if (m->inputcount) printf("\n");
3998 
3999  printf("Number of primary outputs: %d\n", m->outputcount);
4000  for (i = 0; i < m->outputcount; i++)
4001  printf("%s ", m->outputs[i]);
4002  if ( m->outputcount) printf("\n");
4003 
4004  printf("Number of gates: %d\n", m->gatecount);
4005  for (i = 0; i < m->gatecount; i++)
4006  printf("%s ", m->gates[i]);
4007  if (m->gatecount) printf("\n");
4008 
4009  printf("Number of wires: %d\n", m->wirecount);
4010  for (i = 0; i < m->wirecount; i++)
4011  printf("%s ", m->wires[i]);
4012  if (m->wirecount) printf("\n");
4013 
4014  printf("Number of regs: %d\n", m->regcount);
4015  for (i = 0; i < m->regcount; i++)
4016  printf("%s ", m->regs[i]);
4017  if (m->regcount) printf("\n");
4018 
4019  printf("*************************** END **************************\n");
4020 }
4021 */
4022 
4028 /*
4029 static void
4030 printCircuitSummary(BiddyVerilogCircuit *c)
4031 {
4032  unsigned int i,j;
4033 
4034  printf("************** Circuit %s statistical results *************\n", c->name);
4035 
4036  printf("Circuit size: %d\n", c->nodecount);
4037 
4038  printf("Number of primary inputs: %d\n", c->inputcount);
4039  for (i = 0; i < c->inputcount; i++)
4040  printf("%s ", c->inputs[i]);
4041  if (c->inputcount) printf("\n");
4042 
4043  printf("Number of primary outputs: %d\n", c->outputcount);
4044  for (i = 0; i < c->outputcount; i++)
4045  printf("%s ", c->outputs[i]);
4046  if (c->outputcount) printf("\n");
4047 
4048  i=0;
4049  while (i<c->wirecount && c->wires[i] != NULL) {
4050  printf ("c->wire[%d]->type: %s, ",i, c->wires[i]->type);
4051  printf ("ID: %d, ", c->wires[i]->id);
4052  printf ("name: %s, ", c->nodes[c->wires[i]->id]->name);
4053 
4054  printf ("\nInputs (%d): ", c->wires[i]->inputcount); / * wire inputs * /
4055  for (j=0; j<c->wires[i]->inputcount; j++)
4056  printf ("%d ",c->wires[i]->inputs[j]);
4057 
4058  printf ("\nOutputs (%d): ", c->wires[i]->outputcount); / * wire outputs * /
4059  for (j=0; j<c->wires[i]->outputcount; j++)
4060  printf ("%d ",c->wires[i]->outputs[j]);
4061 
4062  i++;
4063  printf ("\n");
4064  }
4065 
4066  printf("*************************** END **************************\n");
4067 }
4068 */
4069 
4075 static Biddy_Boolean
4076 isGate(Biddy_String word)
4077 {
4078  int i;
4079  for (i = 0; i < GATESNUM; i++)
4080  if (strcmp(word,VerilogFileGateName[i]) == 0)
4081  return TRUE;
4082  return FALSE;
4083 }
4084 
4090 static Biddy_Boolean
4091 isSignalVector(Biddy_String word)
4092 {
4093  unsigned int i;
4094  for (i = 0; i < strlen(word); i++)
4095  if (word[i] == ':')
4096  return TRUE;
4097  return FALSE;
4098 }
4099 
4105 static Biddy_Boolean
4106 isEndOfLine(Biddy_String source)
4107 {
4108  Biddy_String pchar = strchr(source, ';');
4109  return (pchar == NULL) ? FALSE : TRUE;
4110 }
4111 
4117 static Biddy_Boolean
4118 isDefined(BiddyVerilogCircuit *c, Biddy_String name)
4119 {
4120  unsigned int i;
4121  for (i=0; (i < c->wirecount) && c->wires[i]; i++) {
4122  if (strcmp(c->nodes[c->wires[i]->id]->name, name) == 0) return TRUE;
4123  }
4124  return FALSE;
4125 }
4126 
4131 static void
4132 buildNode(BiddyVerilogNode *n, Biddy_String type, Biddy_String name)
4133 {
4134  n->type = strdup(type);
4135  n->name = strdup(name);
4136 }
4137 
4142 static void
4143 buildWire(BiddyVerilogCircuit *c, BiddyVerilogWire *w, Biddy_String type, Biddy_String name)
4144 {
4145  int id;
4146 
4147  /* TO DO: check if wire with the same name does not already exists */
4148 
4149  if ((id = getNodeIdByName(c,name)) == -1) {
4150  printf("ERROR (buildWire): node %s does not exists!\n",name);
4151  exit(1);
4152  }
4153  w->id = id; /* wire ID */
4154  w->type = strdup(type); /* wire type */
4155  w->inputcount = 0; /* initial number of inputs */
4156  w->outputcount = 0; /* initial number of outputs */
4157  w->fanout = 0;
4158  w->ttl = 0;
4159  w->bdd = biddyNull;
4160 
4161  /* DEBUGGING */
4162  /*
4163  printf("Creating wire: id: %d, type: %s\n", w->id, w->type);
4164  */
4165 }
4166 
4172 static int
4173 getNodeIdByName(BiddyVerilogCircuit *c, Biddy_String name)
4174 {
4175  unsigned int i;
4176  if (strcmp(name,c->nodes[c->nodecount-1]->name) == 0) return (int) c->nodecount-1;
4177  for (i=0; i < c->nodecount; i++) {
4178  if (strcmp(name,c->nodes[i]->name) == 0) return (int) i;
4179  }
4180  return -1;
4181 }
4182 
4188 static BiddyVerilogWire *
4189 getWireById(BiddyVerilogCircuit *c, int id)
4190 {
4191  unsigned int i;
4192  for (i=0; i < c->wirecount; i++) {
4193  if (c->wires[i]->id == id) return c->wires[i];
4194  }
4195  return NULL;
4196 }
4197 
4203 static BiddyVerilogWire *
4204 getWireByName(BiddyVerilogCircuit *c, Biddy_String name)
4205 {
4206  unsigned int i;
4207  for (i=0; i < c->wirecount; i++) {
4208  if (strcmp(name, c->nodes[c->wires[i]->id]->name) == 0) return c->wires[i];
4209  }
4210  return NULL;
4211 }
4212 
4217 static Biddy_String
4218 trim(Biddy_String source)
4219 {
4220  unsigned int sr_length;
4221 
4222  sr_length = (unsigned int) strlen(source);
4223  while (sr_length && ((source[sr_length-1] == ' ') ||
4224  (source[sr_length-1] == '\t') ||
4225  (source[sr_length-1] == 10) ||
4226  (source[sr_length-1] == 13)))
4227  {
4228  source[sr_length-1] = 0;
4229  sr_length = (unsigned int) strlen(source);
4230  }
4231 
4232  return source;
4233 }
4234 
4235 static void
4236 concat(char **s1, const char *s2)
4237 {
4238  if (s2) {
4239  *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1+1);
4240  strcat(*s1,s2);
4241  }
4242 }
4243 
4244 static void
4245 WriteBDD(Biddy_Manager MNG, Biddy_String *var, FILE *s, Biddy_Edge f, unsigned int *line)
4246 {
4247  Biddy_Variable v;
4248  Biddy_String varname;
4249 
4250  if (BiddyGetMark(f)) {
4251 
4252  if (var) {
4253  concat(var,"*");
4254  }
4255  if (s == stdout) {
4256  printf("*");
4257  } else if (s) {
4258  fprintf(s,"*");
4259  }
4260 
4261  }
4262 
4263  if ((v = BiddyGetTag(f))) {
4264 
4265  if (var) {
4266  concat(var,"<");
4267  concat(var,BiddyManagedGetVariableName(MNG,v));
4268  concat(var,">");
4269  }
4270  if (s == stdout) {
4271  printf("<%s>",BiddyManagedGetVariableName(MNG,v));
4272  } else if (s) {
4273  fprintf(s,"<%s>",BiddyManagedGetVariableName(MNG,v));
4274  }
4275 
4276  }
4277 
4278  varname = BiddyManagedGetTopVariableName(MNG,f);
4279 
4280  if (var) {
4281  concat(var,varname);
4282  }
4283  if (s == stdout) {
4284  printf("%s",varname);
4285  } else if (s) {
4286  fprintf(s,"%s",varname);
4287  }
4288 
4289  if (!BiddyIsTerminal(f)) {
4290 
4291  if (var) {
4292  concat(var,"(");
4293  }
4294  if (s == stdout) {
4295  printf("(");
4296  } else if (s) {
4297  fprintf(s,"(");
4298  }
4299 
4300 
4301  WriteBDD(MNG,var,s,BiddyE(f),line);
4302 
4303  if (var) {
4304  concat(var,")(");
4305  }
4306  if (s == stdout) {
4307  printf(")(");
4308  } else if (s) {
4309  fprintf(s,")(");
4310  }
4311 
4312 
4313  WriteBDD(MNG,var,s,BiddyT(f),line);
4314 
4315  if (var) {
4316  concat(var,")");
4317  }
4318  if (s == stdout) {
4319  printf(")");
4320  } else if (s) {
4321  fprintf(s,")");
4322  }
4323 
4324  }
4325 }
4326 
4327 static Biddy_Boolean
4328 WriteProduct(Biddy_Manager MNG, Biddy_String *var, FILE *s, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
4329 {
4330  /* DEBUGGING */
4331  /*
4332  typedef struct LIMIT {
4333  unsigned int part;
4334  unsigned int w;
4335  } LIMIT;
4336  void *data;
4337  */
4338 
4339  /* ITERATIVE VARIANT - NOT FULLY IMPLEMENTED */
4340  /* LITERALS ARE ADDED IN REVERSE ORDERING */
4341  /*
4342  while (l) {
4343  if (combinationset) {
4344  if (!l->negative) {
4345  if (first) first = FALSE; else printf(",");
4346  printf("%s",BiddyManagedGetVariableName(MNG,l->v));
4347  } else {
4348  printf(" ");
4349  if (l->negative) {
4350  printf("*");
4351  }
4352  printf("%s",BiddyManagedGetVariableName(MNG,l->v));
4353  }
4354  l = l->next;
4355  }
4356  */
4357 
4358  /* RECURSIVE VARIANT */
4359  /* LITERALS ARE ADDED IN REVERSE ORDERING BUT THE RESULT WILL BE REVERSED */
4360 
4361  if (l) {
4362  if (combinationset) {
4363  first = WriteProduct(MNG,var,s,l->next,combinationset,first);
4364  if (!l->negative) {
4365  if (first) {
4366  first = FALSE;
4367  } else {
4368 
4369  if (var) {
4370  concat(var," ");
4371  }
4372  if (s == stdout) {
4373  printf(" ");
4374  } else if (s) {
4375  fprintf(s," ");
4376  }
4377 
4378  }
4379 
4380  if (var) {
4381  concat(var,BiddyManagedGetVariableName(MNG,l->v));
4382  }
4383  if (s == stdout) {
4384  printf("%s",BiddyManagedGetVariableName(MNG,l->v));
4385  } else if (s) {
4386  fprintf(s,"%s",BiddyManagedGetVariableName(MNG,l->v));
4387  }
4388 
4389  /* DEBUGGING */
4390  /*
4391  if ((data = BiddyManagedGetVariableData(MNG,l->v))) {
4392  printf("<%u>",((LIMIT *) data)->w);
4393  }
4394  */
4395 
4396  }
4397  } else {
4398  WriteProduct(MNG,var,s,l->next,combinationset,first);
4399 
4400  if (var) {
4401  concat(var," ");
4402  }
4403  if (s == stdout) {
4404  printf(" ");
4405  } else if (s) {
4406  fprintf(s," ");
4407  }
4408 
4409  if (l->negative) {
4410 
4411  if (var) {
4412  concat(var,"*");
4413  }
4414  if (s == stdout) {
4415  printf("*");
4416  } else if (s) {
4417  fprintf(s,"*");
4418  }
4419  }
4420 
4421  if (var) {
4422  concat(var,BiddyManagedGetVariableName(MNG,l->v));
4423  }
4424  if (s == stdout) {
4425  printf("%s",BiddyManagedGetVariableName(MNG,l->v));
4426  } else if (s) {
4427  fprintf(s,"%s",BiddyManagedGetVariableName(MNG,l->v));
4428  }
4429 
4430  }
4431  }
4432 
4433 
4434  return first;
4435 }
4436 
4437 /* Currently, not used */
4438 /*
4439 static void
4440 WriteProductAlphabetic(Biddy_Manager MNG, BiddyVarList *l, Biddy_Boolean combinationset, Biddy_Boolean first)
4441 {
4442  BiddyVarList *tmp;
4443  Biddy_String tmpname,minname,prevname;
4444 
4445  if (l) {
4446  if (combinationset) {
4447  prevname = NULL;
4448  do {
4449  tmp = l;
4450  minname = NULL;
4451  while (tmp) {
4452  if (!tmp->negative) {
4453  tmpname = BiddyManagedGetVariableName(MNG,tmp->v);
4454  if ((!minname || (strcmp(tmpname,minname)<0)) && (!prevname || (strcmp(tmpname,prevname)>0))) {
4455  minname = tmpname;
4456  }
4457  }
4458  tmp = tmp->next;
4459  }
4460  if (minname) {
4461  if (!first) printf(","); else first = FALSE;
4462  printf("%s",minname);
4463  prevname = minname;
4464  }
4465  } while (minname);
4466  } else {
4467  / * NOT IMPLEMENTED, YET * /
4468  }
4469  }
4470 }
4471 */
4472 
4473 static Biddy_Boolean
4474 WriteSOP(Biddy_Manager MNG, Biddy_String *var, FILE *s, Biddy_Edge f,
4475  Biddy_Variable top, Biddy_Boolean mark, BiddyVarList *l,
4476  unsigned int *maxsize, Biddy_Boolean combinationset)
4477 {
4478  BiddyVarList tmp;
4479  Biddy_Variable v;
4480  Biddy_Boolean OK = TRUE;
4481 
4482  /* if ((!combinationset) && (*maxsize == 0)) return; */ /* output to large, Boolean functions only */
4483  if (*maxsize == 0) { /* output to large */
4484  return FALSE;
4485  }
4486 
4487  v = BiddyV(f);
4488 
4489  /* DEBUGGING */
4490  /*
4491  printf("WriteSOP: top = %u (%s), v = %u (%s)\n",top,BiddyManagedGetVariableName(MNG,top),v,BiddyManagedGetVariableName(MNG,v));
4492  */
4493 
4494  /* DEBUGGING */
4495  /*
4496  printf("WriteSOP DEBUG:");
4497  WriteProduct(MNG,var,s,l,combinationset,TRUE);
4498  printf("\n");
4499  */
4500 
4501  assert( !(BiddyIsSmaller(biddyOrderingTable,BiddyV(f),top)) );
4502 
4503  if ((top != v) && ((f != biddyZero) || (biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEZBDDC)))
4504  {
4505 
4506  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
4507  if (combinationset) {
4508  /* for Boolean functions, don't care variables are not reported */
4509  tmp.next = l;
4510  tmp.v = top;
4511  tmp.negative = FALSE; /* positive literal */
4512  OK = OK && WriteSOP(MNG,var,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
4513  tmp.negative = TRUE; /* negative literal */
4514  OK = OK && WriteSOP(MNG,var,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
4515  }
4516  }
4517 #ifndef COMPACT
4518  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
4519  tmp.next = l;
4520  tmp.v = top;
4521  tmp.negative = TRUE; /* negative literal */
4522  OK = OK && WriteSOP(MNG,var,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
4523  } else if (biddyManagerType == BIDDYTYPETZBDD) {
4524  if (BiddyIsSmaller(biddyOrderingTable,top,BiddyGetTag(f))) {
4525  if (combinationset) {
4526  /* for Boolean functions, don't care variables are not reported */
4527  tmp.next = l;
4528  tmp.v = top;
4529  tmp.negative = FALSE; /* positive literal */
4530  OK = OK && WriteSOP(MNG,var,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
4531  tmp.negative = TRUE; /* negative literal */
4532  OK = OK && WriteSOP(MNG,var,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
4533  }
4534  } else {
4535  tmp.next = l;
4536  tmp.v = top;
4537  tmp.negative = TRUE; /* negative literal */
4538  OK = OK && WriteSOP(MNG,var,s,f,biddyVariableTable.table[top].next,mark,&tmp,maxsize,combinationset);
4539  }
4540  }
4541 #endif
4542 
4543  } else if (v == 0) {
4544 
4545  if (combinationset) {
4546  /* write one combination */
4547  if (!mark) {
4548 
4549  if (l) {
4550  /* printf("{"); */
4551  /* WriteProductAlphabetic(MNG,l,combinationset,TRUE); */
4552  WriteProduct(MNG,var,s,l,combinationset,TRUE);
4553  /* printf("}"); */
4554 
4555  if (var) {
4556  concat(var," ; ");
4557  }
4558  if (s == stdout) {
4559  printf(" ; ");
4560  } else if (s) {
4561  fprintf(s," ; ");
4562  }
4563 
4564  (*maxsize)--;
4565  } else {
4566  /* printf("{}"); */
4567 
4568  if (var) {
4569  concat(var,",");
4570  }
4571  if (s == stdout) {
4572  printf(",");
4573  } else if (s) {
4574  fprintf(s,",");
4575  }
4576 
4577  }
4578  } else {
4579  if (!l) {
4580 
4581  if (var) {
4582  concat(var,"EMPTY");
4583  }
4584  if (s == stdout) {
4585  printf("EMPTY");
4586  } else if (s) {
4587  fprintf(s,"EMPTY");
4588  }
4589 
4590  }
4591  }
4592  } else {
4593  /* write one minterm */
4594  if (!mark) {
4595 
4596  if (var) {
4597  concat(var," + ");
4598  }
4599  if (s == stdout) {
4600  printf(" + ");
4601  } else if (s) {
4602  fprintf(s," + ");
4603  }
4604 
4605  if (l) {
4606  WriteProduct(MNG,var,s,l,combinationset,TRUE);
4607 
4608  if (var) {
4609  concat(var,"\n");
4610  }
4611  if (s == stdout) {
4612  printf("\n");
4613  } else if (s) {
4614  fprintf(s,"\n");
4615  }
4616 
4617  (*maxsize)--;
4618  } else {
4619 
4620  if (var) {
4621  concat(var," 1");
4622  }
4623  if (s == stdout) {
4624  printf(" 1");
4625  } else if (s) {
4626  fprintf(s," 1");
4627  }
4628 
4629  }
4630  } else {
4631  if (!l) {
4632 
4633  if (var) {
4634  concat(var," + 0");
4635  }
4636  if (s == stdout) {
4637  printf(" + 0");
4638  } else if (s) {
4639  fprintf(s," + 0");
4640  }
4641 
4642  }
4643  }
4644  }
4645 
4646  } else {
4647 
4648  tmp.next = l;
4649  tmp.v = v;
4650 
4651  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
4652  if (combinationset) {
4653  tmp.negative = FALSE; /* for combination sets, right successor go first for better ordering */
4654  OK = OK && WriteSOP(MNG,var,s,BiddyT(f),biddyVariableTable.table[v].next,(mark ^ BiddyGetMark(BiddyT(f))),&tmp,maxsize,combinationset);
4655  } else {
4656  tmp.negative = TRUE; /* for Boolean function, left successor go first for better ordering */
4657  OK = OK && WriteSOP(MNG,var,s,BiddyE(f),BiddyV(BiddyE(f)),(mark ^ BiddyGetMark(BiddyE(f))),&tmp,maxsize,combinationset);
4658  }
4659  }
4660 #ifndef COMPACT
4661  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
4662  if (combinationset) {
4663  tmp.negative = FALSE; /* for combination sets, right successor go first for better ordering */
4664  OK = OK && WriteSOP(MNG,var,s,BiddyT(f),biddyVariableTable.table[v].next,BiddyGetMark(BiddyT(f)),&tmp,maxsize,combinationset);
4665  } else {
4666  tmp.negative = TRUE; /* for Boolean function, left successor go first for better ordering */
4667  OK = OK && WriteSOP(MNG,var,s,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ BiddyGetMark(BiddyE(f))),&tmp,maxsize,combinationset);
4668  }
4669  }
4670  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
4671  if (combinationset) {
4672  tmp.negative = FALSE; /* for combination sets, right successor go first for better ordering */
4673  OK = OK && WriteSOP(MNG,var,s,BiddyT(f),biddyVariableTable.table[v].next,BiddyGetMark(BiddyT(f)),&tmp,maxsize,combinationset);
4674  } else {
4675  tmp.negative = TRUE; /* for Boolean function, left successor go first for better ordering */
4676  OK = OK && WriteSOP(MNG,var,s,BiddyE(f),BiddyGetTag(BiddyE(f)),(mark ^ BiddyGetMark(BiddyE(f))),&tmp,maxsize,combinationset);
4677  }
4678  }
4679 #endif
4680 
4681  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
4682  if (combinationset) {
4683  tmp.negative = TRUE; /* for combination sets, left successor is second for better ordering */
4684  OK = OK && WriteSOP(MNG,var,s,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ BiddyGetMark(BiddyE(f))),&tmp,maxsize,combinationset);
4685  } else {
4686  tmp.negative = FALSE; /* for Boolean function, right successor is second for better ordering */
4687  OK = OK && WriteSOP(MNG,var,s,BiddyT(f),BiddyV(BiddyT(f)),(mark ^ BiddyGetMark(BiddyT(f))),&tmp,maxsize,combinationset);
4688  }
4689  }
4690 #ifndef COMPACT
4691  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
4692  if (combinationset) {
4693  tmp.negative = TRUE; /* for combination sets, left successor is second for better ordering */
4694  OK = OK && WriteSOP(MNG,var,s,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ BiddyGetMark(BiddyE(f))),&tmp,maxsize,combinationset);
4695  } else {
4696  tmp.negative = FALSE; /* for Boolean function, right successor is second for better ordering */
4697  OK = OK && WriteSOP(MNG,var,s,BiddyT(f),biddyVariableTable.table[v].next,BiddyGetMark(BiddyT(f)),&tmp,maxsize,combinationset);
4698  }
4699  }
4700  else if (biddyManagerType == BIDDYTYPETZBDD) {
4701  if (combinationset) {
4702  tmp.negative = TRUE; /* for combination sets, left successor is second for better ordering */
4703  OK = OK && WriteSOP(MNG,var,s,BiddyE(f),biddyVariableTable.table[v].next,(mark ^ BiddyGetMark(BiddyE(f))),&tmp,maxsize,combinationset);
4704  } else {
4705  tmp.negative = FALSE; /* for Boolean function, right successor is second for better ordering */
4706  OK = OK && WriteSOP(MNG,var,s,BiddyT(f),BiddyGetTag(BiddyT(f)),BiddyGetMark(BiddyT(f)),&tmp,maxsize,combinationset);
4707  }
4708  }
4709 #endif
4710 
4711  }
4712 
4713  return OK;
4714 }
4715 
4716 static unsigned int
4717 enumerateNodes(Biddy_Manager MNG, Biddy_Edge f, unsigned int n)
4718 {
4719  if (!BiddyManagedIsSelected(MNG,f)) {
4720  if (BiddyIsTerminal(f)) {
4721  } else {
4722  BiddyManagedSelectNode(MNG,f);
4723  n++;
4724  BiddySetEnumerator(f,n);
4725 
4726  /* one or both are terminal node */
4727  /* every instance of terminal node is enumerated */
4728  if (BiddyIsTerminal(BiddyE(f)) || BiddyIsTerminal(BiddyT(f))) {
4729 
4730  if (((biddyManagerType == BIDDYTYPEOBDD) ||
4731  (biddyManagerType == BIDDYTYPEZBDD) ||
4732  (biddyManagerType == BIDDYTYPETZBDD)
4733  ) && (BiddyGetMark(BiddyE(f)) != BiddyGetMark(BiddyT(f))))
4734  {
4735  /* two terminal nodes only if complemented edges are not used and they are different */
4736  if (BiddyIsTerminal(BiddyE(f))) {
4737  n++;
4738  }
4739  if (BiddyIsTerminal(BiddyT(f))) {
4740  n++;
4741  }
4742  }
4743  else {
4744  /* only one terminal node */
4745  n++;
4746  }
4747 
4748  }
4749 
4750  if (!BiddyIsTerminal(BiddyE(f))) {
4751  n = enumerateNodes(MNG,BiddyE(f),n);
4752  }
4753  if (!BiddyIsTerminal(BiddyT(f))) {
4754  n = enumerateNodes(MNG,BiddyT(f),n);
4755  }
4756  }
4757  }
4758  return n;
4759 }
4760 
4761 static void
4762 WriteDotNodes(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, int id, Biddy_Boolean cudd)
4763 {
4764  BiddyLocalInfo *li;
4765  Biddy_String name,hash;
4766  Biddy_Variable v;
4767  BiddyLocalInfo *li2;
4768 
4769  if (BiddyIsTerminal(f)) {
4770  if (cudd) {
4771 
4772  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
4773  /*
4774  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
4775  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
4776  fprintf(dotfile,"\"%p\";\n",biddyOne);
4777  */
4778 
4779  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
4780 
4781  fprintf(dotfile,"{ \"CONST NODES\";\n");
4782  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
4783  fprintf(dotfile,"\"1\";\n");
4784 
4785 
4786  fprintf(dotfile,"}\n}\n");
4787  } else {
4788  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4789  (biddyManagerType == BIDDYTYPEZBDD) ||
4790  (biddyManagerType == BIDDYTYPETZBDD))
4791  {
4792  if (f == biddyZero) {
4793  fprintf(dotfile, " node [shape = none, label = \"0\"] %u;\n",1);
4794  } else {
4795  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
4796  }
4797  }
4798  else {
4799  fprintf(dotfile, " node [shape = none, label = \"1\"] %u;\n",1);
4800  }
4801  }
4802  return;
4803  }
4804  if (cudd) {
4805  BiddyManagedResetVariablesValue(MNG);
4806  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4807  while (li->back) {
4808  v = BiddyV(li->back);
4809  if (biddyVariableTable.table[v].value == biddyZero) {
4810  biddyVariableTable.table[v].value = biddyOne;
4811  name = strdup(BiddyManagedGetVariableName(MNG,v));
4812  while ((hash = strchr(name,'#'))) hash[0] = '_';
4813  fprintf(dotfile,"{ rank = same; ");
4814  fprintf(dotfile,"\" %s \";\n",name);
4815  free(name);
4816  li2 = li;
4817  while (li2->back) {
4818  if (BiddyV(li2->back) == v) {
4819  fprintf(dotfile,"\"%p\";\n",li2->back);
4820  }
4821  li2 = &li2[1]; /* next field in the array */
4822  }
4823  fprintf(dotfile,"}\n");
4824  }
4825  li = &li[1]; /* next field in the array */
4826  }
4827  BiddyManagedResetVariablesValue(MNG);
4828 
4829  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotEdges */
4830  /*
4831  fprintf(dotfile,"{ rank = same; \"CONST NODES\";\n");
4832  fprintf(dotfile,"{ node [shape = box label = \"1\"]; ");
4833  fprintf(dotfile,"\"%p\";\n",biddyOne);
4834  */
4835 
4836  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotEdges */
4837 
4838  fprintf(dotfile,"{ \"CONST NODES\";\n");
4839  fprintf(dotfile,"{ node [shape = none label = \"1\"];\n");
4840  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4841  while (li->back) {
4842  if (BiddyIsTerminal(BiddyE(li->back)) || BiddyIsTerminal(BiddyT(li->back))) {
4843  fprintf(dotfile,"\"%u\";\n",li->data.enumerator+1);
4844  }
4845  li = &li[1];
4846  }
4847 
4848 
4849  fprintf(dotfile,"}\n}\n");
4850  } else {
4851  li = (BiddyLocalInfo *)(BiddyN(f)->list);
4852  while (li->back) {
4853  if (id == -1) {
4854  name = getname(MNG,li->back);
4855  } else {
4856  name = getshortname(MNG,li->back,id);
4857  }
4858  while ((hash = strchr(name,'#'))) hash[0] = '_';
4859  fprintf(dotfile," node [shape = circle, label = \"%s\"] %u;\n",name,li->data.enumerator);
4860  free(name);
4861  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4862  (biddyManagerType == BIDDYTYPEZBDD) ||
4863  (biddyManagerType == BIDDYTYPETZBDD))
4864  {
4865  if (BiddyE(li->back) == biddyZero) {
4866  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
4867  }
4868  else if (BiddyIsTerminal(BiddyE(li->back))) {
4869  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4870  }
4871  if (BiddyT(li->back) == biddyZero) {
4872  if (BiddyIsTerminal(BiddyE(li->back)) && (BiddyGetMark(BiddyE(li->back)) != BiddyGetMark(BiddyT(li->back)))) {
4873  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+2);
4874  } else {
4875  fprintf(dotfile," node [shape = none, label = \"0\"] %u;\n",li->data.enumerator+1);
4876  }
4877  }
4878  else if (BiddyIsTerminal(BiddyT(li->back))) {
4879  if (BiddyIsTerminal(BiddyE(li->back)) && (BiddyGetMark(BiddyE(li->back)) != BiddyGetMark(BiddyT(li->back)))) {
4880  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+2);
4881  } else {
4882  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4883  }
4884  }
4885  }
4886  else {
4887  if (BiddyIsTerminal(BiddyE(li->back)) || BiddyIsTerminal(BiddyT(li->back))) {
4888  fprintf(dotfile," node [shape = none, label = \"1\"] %u;\n",li->data.enumerator+1);
4889  }
4890  }
4891  li = &li[1]; /* next field in the array */
4892  }
4893  }
4894 }
4895 
4896 static void
4897 WriteDotEdges(Biddy_Manager MNG, FILE *dotfile, Biddy_Edge f, Biddy_Boolean cudd)
4898 {
4899  unsigned int n1,n2;
4900  Biddy_Variable tag;
4901 
4902  if (!BiddyIsTerminal(f) && !BiddyManagedIsSelected(MNG,f)) {
4903  BiddyManagedSelectNode(MNG,f);
4904  n1 = BiddyGetEnumerator(f);
4905 
4906  if (BiddyIsTerminal(BiddyE(f))) {
4907  n2 = n1 + 1;
4908  } else {
4909  n2 = BiddyGetEnumerator(BiddyE(f));
4910  }
4911  if (BiddyGetMark(BiddyE(f))) {
4912  if ((BiddyE(f) != biddyZero) && (tag = BiddyGetTag(BiddyE(f)))) {
4913  if (cudd) {
4914 
4915  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4916  /*
4917  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),BiddyManagedGetVariableName(MNG,tag));
4918  */
4919 
4920  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4921 
4922  if (BiddyIsTerminal(BiddyE(f))) {
4923  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted label=\"%s\"];\n",BiddyP(f),n2,BiddyManagedGetVariableName(MNG,tag));
4924  } else {
4925  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),BiddyManagedGetVariableName(MNG,tag));
4926  }
4927 
4928 
4929  } else {
4930 #ifdef LEGACY_DOT
4931  fprintf(dotfile," %u -> %u [style=dotted label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
4932 #else
4933  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
4934 #endif
4935  }
4936  } else {
4937  if (cudd) {
4938 
4939  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4940  /*
4941  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
4942  */
4943 
4944  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4945 
4946  if (BiddyIsTerminal(BiddyE(f))) {
4947  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dotted];\n",BiddyP(f),n2);
4948  } else {
4949  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dotted];\n",BiddyP(f),BiddyP(BiddyE(f)));
4950  }
4951 
4952 
4953  } else {
4954  if ((biddyManagerType == BIDDYTYPEOBDD) ||
4955  (biddyManagerType == BIDDYTYPEZBDD) ||
4956  (biddyManagerType == BIDDYTYPETZBDD))
4957  {
4958 #ifdef LEGACY_DOT
4959  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
4960 #else
4961  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
4962 #endif
4963  }
4964  else {
4965 #ifdef LEGACY_DOT
4966  fprintf(dotfile," %u -> %u [style=dotted];\n",n1,n2);
4967 #else
4968  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" arrowhead=\"dot\"];\n",n1,n2);
4969 #endif
4970  }
4971  }
4972  }
4973  } else {
4974  if ((BiddyE(f) != biddyZero) && (tag = BiddyGetTag(BiddyE(f)))) {
4975  if (cudd) {
4976 
4977  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
4978  /*
4979  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),BiddyManagedGetVariableName(MNG,tag));
4980  */
4981 
4982  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
4983 
4984  if (BiddyIsTerminal(BiddyE(f))) {
4985  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed label=\"%s\"];\n",BiddyP(f),n2,BiddyManagedGetVariableName(MNG,tag));
4986  } else {
4987  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyE(f)),BiddyManagedGetVariableName(MNG,tag));
4988  }
4989 
4990 
4991  } else {
4992 #ifdef LEGACY_DOT
4993  fprintf(dotfile," %u -> %u [style=dashed label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
4994 #else
4995  fprintf(dotfile," %u -> %u [arrowtail=\"odot\" label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
4996 #endif
4997  }
4998  } else {
4999  if (cudd) {
5000 
5001  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
5002  /*
5003  fprintf(dotfile,"\"%p\" -> \"%p\" [style = dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
5004  */
5005 
5006  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
5007 
5008  if (BiddyIsTerminal(BiddyE(f))) {
5009  fprintf(dotfile,"\"%p\" -> \"%u\" [style=dashed];\n",BiddyP(f),n2);
5010  } else {
5011  fprintf(dotfile,"\"%p\" -> \"%p\" [style=dashed];\n",BiddyP(f),BiddyP(BiddyE(f)));
5012  }
5013 
5014 
5015  } else {
5016 #ifdef LEGACY_DOT
5017  fprintf(dotfile," %u -> %u [style=dashed];\n",n1,n2);
5018 #else
5019  fprintf(dotfile," %u -> %u [arrowtail=\"odot\"];\n",n1,n2);
5020 #endif
5021  }
5022  }
5023  }
5024 
5025  if (BiddyIsTerminal(BiddyT(f))) {
5026  if (((biddyManagerType == BIDDYTYPEOBDD) ||
5027  (biddyManagerType == BIDDYTYPEZBDD) ||
5028  (biddyManagerType == BIDDYTYPETZBDD))
5029  && (BiddyIsTerminal(BiddyE(f)))
5030  && (BiddyGetMark(BiddyE(f)) != BiddyGetMark(BiddyT(f))))
5031  {
5032  n2 = n1 + 2;
5033  }
5034  else {
5035  n2 = n1 + 1;
5036  }
5037  } else {
5038  n2 = BiddyGetEnumerator(BiddyT(f));
5039  }
5040  if (BiddyGetMark(BiddyT(f))) {
5041  if ((BiddyT(f) != biddyZero) && (tag = BiddyGetTag(BiddyT(f)))) {
5042  if (cudd) {
5043 
5044  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
5045  /*
5046  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),BiddyManagedGetVariableName(MNG,tag));
5047  */
5048 
5049  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
5050 
5051  if (BiddyIsTerminal(BiddyT(f))) {
5052  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold label=\"%s\"];\n",BiddyP(f),n2,BiddyManagedGetVariableName(MNG,tag));
5053  } else {
5054  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),BiddyManagedGetVariableName(MNG,tag));
5055  }
5056 
5057 
5058  } else {
5059 #ifdef LEGACY_DOT
5060  fprintf(dotfile," %d -> %d [style=bold label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
5061 #else
5062  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\" label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
5063 #endif
5064  }
5065  } else {
5066  if (cudd) {
5067 
5068  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
5069  /*
5070  fprintf(dotfile,"\"%p\" -> \"%p\" [style = bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
5071  */
5072 
5073  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
5074 
5075  if (BiddyIsTerminal(BiddyT(f))) {
5076  fprintf(dotfile,"\"%p\" -> \"%u\" [style=bold];\n",BiddyP(f),n2);
5077  } else {
5078  fprintf(dotfile,"\"%p\" -> \"%p\" [style=bold];\n",BiddyP(f),BiddyP(BiddyT(f)));
5079  }
5080 
5081 
5082  } else {
5083  if ((biddyManagerType == BIDDYTYPEOBDD) ||
5084  (biddyManagerType == BIDDYTYPEZBDD) ||
5085  (biddyManagerType == BIDDYTYPETZBDD))
5086  {
5087 #ifdef LEGACY_DOT
5088  fprintf(dotfile," %d -> %d;\n",n1,n2);
5089 #else
5090  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
5091 #endif
5092  }
5093  else {
5094 #ifdef LEGACY_DOT
5095  fprintf(dotfile," %d -> %d [style=bold];\n",n1,n2);
5096 #else
5097  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" arrowhead=\"dot\"];\n",n1,n2);
5098 #endif
5099  }
5100  }
5101  }
5102  } else {
5103  if ((BiddyT(f) != biddyZero) && (tag = BiddyGetTag(BiddyT(f)))) {
5104  if (cudd) {
5105 
5106  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
5107  /*
5108  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),BiddyManagedGetVariableName(MNG,tag));
5109  */
5110 
5111  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
5112 
5113  if (BiddyIsTerminal(BiddyT(f))) {
5114  fprintf(dotfile,"\"%p\" -> \"%u\" [label=\"%s\"];\n",BiddyP(f),n2,BiddyManagedGetVariableName(MNG,tag));
5115  } else {
5116  fprintf(dotfile,"\"%p\" -> \"%p\" [label=\"%s\"];\n",BiddyP(f),BiddyP(BiddyT(f)),BiddyManagedGetVariableName(MNG,tag));
5117  }
5118 
5119 
5120  } else {
5121 #ifdef LEGACY_DOT
5122  fprintf(dotfile," %d -> %d [label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
5123 #else
5124  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\" label=\"%s\"];\n",n1,n2,BiddyManagedGetVariableName(MNG,tag));
5125 #endif
5126  }
5127  } else {
5128  if (cudd) {
5129 
5130  /* VARIANT 1 - THIS SHOULD BE COMBINED WITH VARIANT 1 IN WriteDotNodes */
5131  /*
5132  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
5133  */
5134  /* VARIANT 2 - THIS SHOULD BE COMBINED WITH VARIANT 2 IN WriteDotNodes */
5135 
5136 
5137  if (BiddyIsTerminal(BiddyT(f))) {
5138  fprintf(dotfile,"\"%p\" -> \"%u\";\n",BiddyP(f),n2);
5139  } else {
5140  fprintf(dotfile,"\"%p\" -> \"%p\";\n",BiddyP(f),BiddyP(BiddyT(f)));
5141  }
5142 
5143 
5144  } else {
5145 #ifdef LEGACY_DOT
5146  fprintf(dotfile," %d -> %d [style=solid];\n",n1,n2);
5147 #else
5148  fprintf(dotfile," %d -> %d [arrowtail=\"invempty\"];\n",n1,n2);
5149 #endif
5150  }
5151  }
5152  }
5153 
5154  WriteDotEdges(MNG,dotfile,BiddyE(f),cudd);
5155  WriteDotEdges(MNG,dotfile,BiddyT(f),cudd);
5156  }
5157 }
5158 
5159 static void
5160 WriteBddviewConnections(Biddy_Manager MNG, FILE *funfile, Biddy_Edge f)
5161 {
5162  int n1,n2;
5163  Biddy_Variable tag1,tag2;
5164 
5165  if (!BiddyIsTerminal(f) && !BiddyManagedIsSelected(MNG,f)) {
5166  BiddyManagedSelectNode(MNG,f);
5167  n1 = BiddyGetEnumerator(f);
5168 
5169  /* if successors are equal then double line is possible */
5170  if ((BiddyP(BiddyE(f)) != BiddyP(BiddyT(f))) ||
5171  (((biddyManagerType == BIDDYTYPEOBDD) ||
5172  (biddyManagerType == BIDDYTYPEZBDD) ||
5173  (biddyManagerType == BIDDYTYPETZBDD))
5174  &&
5175  (BiddyGetMark((BiddyE(f))) != BiddyGetMark((BiddyT(f)))))
5176  )
5177  {
5178 
5179  unsigned int num;
5180 
5181  /* SINGLE LINE */
5182 
5183  num = 0;
5184  if (BiddyIsTerminal(BiddyE(f))) {
5185  n2 = n1 + 1;
5186  num = 1;
5187  } else {
5188  n2 = BiddyGetEnumerator(BiddyE(f));
5189  }
5190  fprintf(funfile,"connect %d %d ",n1,n2);
5191  if ((biddyManagerType == BIDDYTYPEOBDD) ||
5192  (biddyManagerType == BIDDYTYPEZBDD) ||
5193  (biddyManagerType == BIDDYTYPETZBDD))
5194  {
5195  fprintf(funfile,"l");
5196  }
5197  else {
5198  if (BiddyGetMark((BiddyE(f)))) {
5199  fprintf(funfile,"li");
5200  } else {
5201  fprintf(funfile,"l");
5202  }
5203  }
5204  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
5205  {
5206  if (BiddyE(f) == biddyZero) {
5207  fprintf(funfile," 0\n");
5208  } else {
5209  tag1 = BiddyGetTag(BiddyE(f));
5210  fprintf(funfile," %s\n",BiddyManagedGetVariableName(MNG,tag1));
5211  }
5212  } else {
5213  fprintf(funfile,"\n");
5214  }
5215 
5216  if (BiddyIsTerminal(BiddyT(f))) {
5217  n2 = n1 + num + 1;
5218  } else {
5219  n2 = BiddyGetEnumerator(BiddyT(f));
5220  }
5221  fprintf(funfile,"connect %d %d ",n1,n2);
5222  if ((biddyManagerType == BIDDYTYPEOBDD) ||
5223  (biddyManagerType == BIDDYTYPEZBDD) ||
5224  (biddyManagerType == BIDDYTYPETZBDD))
5225  {
5226  fprintf(funfile,"r");
5227  }
5228  else {
5229  if (BiddyGetMark((BiddyT(f)))) {
5230  fprintf(funfile,"ri");
5231  } else {
5232  fprintf(funfile,"r");
5233  }
5234  }
5235  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
5236  {
5237  if (BiddyT(f) == biddyZero) {
5238  fprintf(funfile," 0\n");
5239  } else {
5240  tag2 = BiddyGetTag(BiddyT(f));
5241  fprintf(funfile," %s\n",BiddyManagedGetVariableName(MNG,tag2));
5242  }
5243  } else {
5244  fprintf(funfile,"\n");
5245  }
5246 
5247  } else {
5248 
5249  /* DOUBLE LINE */
5250 
5251  if (BiddyIsTerminal(BiddyE(f))) {
5252  n2 = n1 + 1;
5253  } else {
5254  n2 = BiddyGetEnumerator(BiddyE(f));
5255  }
5256 
5257  fprintf(funfile,"connect %d %d ",n1,n2);
5258  if (BiddyGetMark((BiddyE(f)))) {
5259  if (BiddyGetMark((BiddyT(f)))) {
5260  fprintf(funfile,"ei");
5261  } else {
5262  fprintf(funfile,"d");
5263  }
5264  } else {
5265  if (BiddyGetMark((BiddyT(f)))) {
5266  fprintf(funfile,"di");
5267  } else {
5268  fprintf(funfile,"e");
5269  }
5270  }
5271  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
5272  {
5273  tag1 = BiddyGetTag(BiddyE(f));
5274  tag2 = BiddyGetTag(BiddyT(f));
5275  fprintf(funfile," %s %s\n",BiddyManagedGetVariableName(MNG,tag1),BiddyManagedGetVariableName(MNG,tag2));
5276  } else {
5277  fprintf(funfile,"\n");
5278  }
5279 
5280  }
5281 
5282  WriteBddviewConnections(MNG,funfile,BiddyE(f));
5283  WriteBddviewConnections(MNG,funfile,BiddyT(f));
5284  }
5285 }
5286 
5287 static Biddy_String
5288 getname(Biddy_Manager MNG, void *p)
5289 {
5290  unsigned int i;
5291  Biddy_String newname;
5292 
5293  if ((p == biddyZero) &&
5294  ((biddyManagerType == BIDDYTYPEOBDD) ||
5295  (biddyManagerType == BIDDYTYPEZBDD) ||
5296  (biddyManagerType == BIDDYTYPETZBDD)))
5297  {
5298  newname = strdup("0");
5299  return (newname);
5300  }
5301 
5302  newname = strdup(BiddyManagedGetTopVariableName(MNG,(Biddy_Edge) p));
5303  for (i=0; i<strlen(newname); ++i) {
5304  if (newname[i] == '<') newname[i] = '_';
5305  if (newname[i] == '>') newname[i] = 0;
5306  }
5307 
5308  return (newname);
5309 }
5310 
5311 static Biddy_String
5312 getshortname(Biddy_Manager MNG, void *p, int n)
5313 {
5314  unsigned int i;
5315  Biddy_String name;
5316  Biddy_String shortname;
5317 
5318  if (n != -1) {
5319  printf("WARNING: shortname with n is not supported, yet");
5320  }
5321 
5322  name = strdup(BiddyManagedGetTopVariableName(MNG,(Biddy_Edge) p));
5323  i = (unsigned int)strcspn(name,"<");
5324  name[i]=0;
5325  shortname = strdup(name);
5326  free(name);
5327 
5328  return (shortname);
5329 }
5330 
5331 /*----------------------------------------------------------------------------*/
5332 /* Unused static functions */
5333 /*----------------------------------------------------------------------------*/
5334 
5335 static void
5336 reportOrdering(Biddy_Manager MNG)
5337 {
5338  Biddy_Variable var;
5339 
5340  printf("Variable ordering:\n");
5341  var = BiddyManagedGetLowestVariable(MNG);
5342  while (var != 0) {
5343  printf("(%s)",BiddyManagedGetVariableName(MNG,var));
5344  var = BiddyManagedGetNextVariable(MNG,var);
5345  }
5346  printf("\n");
5347 }
5348 
5349 static void
5350 PrintMintermsOBDD(Biddy_Manager MNG, Biddy_String *var, FILE *s, Biddy_Edge f, Biddy_Boolean negative)
5351 {
5352  unsigned int variableNumber;
5353  Biddy_Variable* variableTable;
5354  unsigned int i;
5355  int j;
5356  Biddy_Variable k,v;
5357  unsigned int numcomb;
5358  Biddy_Boolean first;
5359 
5360  /* all variables are included into minterms! */
5361  variableNumber = biddyVariableTable.num - 1;
5362 
5363  /* DEBUGGING */
5364  /*
5365  printf("variableNumber = %u\n",variableNumber);
5366  */
5367 
5368  /* variableNumber must be small because a loop over 2^variableNumber is used in the algorithm */
5369  if (variableNumber > 16) {
5370 
5371  if (var) {
5372  concat(var,"TO MANY VARIABLES\n");
5373  }
5374  if (s == stdout) {
5375  printf("PrintMintermsOBDD: to many variables, variableNumber = %d, max = 16\n",variableNumber);
5376  } else if (s) {
5377  fprintf(s,"PrintMintermsOBDD: to many variables, variableNumber = %d, max = 16\n",variableNumber);
5378  }
5379 
5380  return;
5381  }
5382 
5383  /* variableTable is a table of all variables - the active ordering is considered */
5384  if (!(variableTable = (Biddy_Variable *) malloc((variableNumber) * sizeof(Biddy_Variable)))) return;
5385  i = 0;
5386  v = BiddyManagedGetLowestVariable(MNG); /* lowest = topmost */
5387  for (k = 1; k < biddyVariableTable.num; k++) {
5388  variableTable[i] = v;
5389  i++;
5390  v = biddyVariableTable.table[v].next;
5391  }
5392 
5393  numcomb = 1;
5394  for (i = 0; i < variableNumber; i++) numcomb = 2 * numcomb;
5395  /* for (i = numcomb - 1; i >= 0; i--) */
5396  for (i = 0; i < numcomb; i++)
5397  {
5398  for (j = variableNumber - 1; j >= 0; j--) {
5399  biddyVariableTable.table[variableTable[variableNumber-j-1]].value = (i&(1 << j))?biddyOne:biddyZero;
5400  }
5401  if (BiddyManagedEval(MNG,f)) {
5402 
5403  if (var) {
5404  concat(var,"{");
5405  }
5406  if (s == stdout) {
5407  printf("{");
5408  } else if (s) {
5409  fprintf(s,"{");
5410  }
5411 
5412  first = TRUE;
5413  for (j = variableNumber - 1; j >= 0; j--) {
5414  if (i&(1 << j)) {
5415  if (first) {
5416  first = FALSE;
5417  } else {
5418 
5419  if (var) {
5420  concat(var,",");
5421  }
5422  if (s == stdout) {
5423  printf(",");
5424  } else if (s) {
5425  fprintf(s,",");
5426  }
5427 
5428  }
5429 
5430  if (var) {
5431  concat(var,BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1]));
5432  }
5433  if (s == stdout) {
5434  printf("%s",BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1]));
5435  } else if (s) {
5436  fprintf(s,"%s",BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1]));
5437  }
5438 
5439  } else {
5440  if (negative) {
5441  if (first) {
5442  first = FALSE;
5443  } else {
5444 
5445  if (var) {
5446  concat(var,",");
5447  }
5448  if (s == stdout) {
5449  printf(",");
5450  } else if (s) {
5451  fprintf(s,",");
5452  }
5453 
5454  }
5455 
5456  if (var) {
5457  concat(var,"*");
5458  concat(var,BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1]));
5459  }
5460  if (s == stdout) {
5461  printf("*%s",BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1]));
5462  } else if (s) {
5463  fprintf(s,"*%s",BiddyManagedGetVariableName(MNG,variableTable[variableNumber-j-1]));
5464  }
5465 
5466  }
5467  }
5468  }
5469 
5470  if (var) {
5471  concat(var,"}");
5472  }
5473  if (s == stdout) {
5474  printf("}");
5475  } else if (s) {
5476  fprintf(s,"}");
5477  }
5478 
5479  }
5480  }
5481 
5482  if (var) {
5483  concat(var,"\n");
5484  }
5485  if (s == stdout) {
5486  printf("\n");
5487  } else if (s) {
5488  fprintf(s,"\n");
5489  }
5490 
5491  free(variableTable);
5492 }
Biddy_Managed_Eval1x
Biddy_Edge Biddy_Managed_Eval1x(Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format.
Definition: biddyInOut.c:296
Biddy_Managed_Nor
EXTERN Biddy_Edge Biddy_Managed_Nor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce).
Definition: biddyOp.c:553
Biddy_Managed_Nand
EXTERN Biddy_Edge Biddy_Managed_Nand(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer).
Definition: biddyOp.c:474
Biddy_Managed_Eval0
Biddy_String Biddy_Managed_Eval0(Biddy_Manager MNG, Biddy_String s)
Function Biddy_Managed_Eval0 evaluates raw format.
Definition: biddyInOut.c:240
Biddy_Managed_PrintTable
void Biddy_Managed_PrintTable(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f)
Function Biddy_Managed_PrintTable writes truth table.
Definition: biddyInOut.c:570
Biddy_Variable
Biddy_Variable is used for indices in variable table.
Biddy_String
Biddy_String is used for strings.
Biddy_Managed_WriteBddview
unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], void *xytable)
Function Biddy_Managed_WriteBDDView writes bddview format using fprintf.
Definition: biddyInOut.c:792
Biddy_LookupFunction
Biddy_LookupFunction is used in Biddy_Eval1x to specify user's function which will lookups in a user'...
Biddy_Edge
Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
Biddy_Managed_PrintSOP
void Biddy_Managed_PrintSOP(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f)
Function Biddy_Managed_PrintSOP writes (non-minimal) SOP.
Definition: biddyInOut.c:623
Biddy_Manager
Biddy_Manager is used to specify manager.
Biddy_Boolean
Biddy_Boolean is used for boolean values.
Biddy_Managed_ReadBddview
Biddy_String Biddy_Managed_ReadBddview(Biddy_Manager MNG, const char filename[], Biddy_String name)
Function Biddy_Managed_ReadBddview reads bddview file and creates all Boolean functions specified by ...
Definition: biddyInOut.c:408
Biddy_Managed_Eval2
Biddy_Edge Biddy_Managed_Eval2(Biddy_Manager MNG, Biddy_String boolFunc)
Function Biddy_Managed_Eval2 evaluates infix format.
Definition: biddyInOut.c:352
Biddy_Managed_Xnor
EXTERN Biddy_Edge Biddy_Managed_Xnor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xnor calculates Boolean function XNOR.
Definition: biddyOp.c:711
Biddy_Managed_WriteDot
unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf.
Definition: biddyInOut.c:736
Biddy_Managed_PrintMinterms
void Biddy_Managed_PrintMinterms(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_Boolean negative)
Function Biddy_Managed_PrintMinterms writes minterms.
Definition: biddyInOut.c:680
Biddy_Managed_PrintBDD
void Biddy_Managed_PrintBDD(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_String label)
Function Biddy_Managed_PrintBDD writes raw format.
Definition: biddyInOut.c:516
Biddy_Managed_ReadVerilogFile
void Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[], Biddy_String prefix)
Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary input...
Definition: biddyInOut.c:463
biddyInt.h
File biddyInt.h contains declaration of internal data structures.