Biddy  1.7.3
An academic Binary Decision Diagrams package
biddy-example-dictionary.c
1 /* $Revision: 305 $ */
2 /* $Date: 2017-09-13 10:47:03 +0200 (sre, 13 sep 2017) $ */
3 /* This file (biddy-example-dictionary.c) is a C file */
4 /* Author: Robert Meolic (robert.meolic@um.si) */
5 /* This file has been released into the public domain by the author. */
6 
7 /* This example is compatible with Biddy v1.7 and CUDD v3.0.0 */
8 
9 /* COMPILE WITH: */
10 /* gcc -DREPORT -DUNIX -DUSE_BIDDY -O2 -o biddy-example-dictionary biddy-example-dictionary.c -I. -L./bin -lbiddy -lgmp */
11 /* gcc -DREPORT -DUSE_CUDD -O2 -o cudd-example-dictionary biddy-example-dictionary.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
12 
13 /* Some notes */
14 /*
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
16 A B C Č D E F G H I J K L M N O P Q R S Š T U V W X Y Z Ž
17 */
18 
19 #define WORDSIZE 5
20 #define ALPHABETSIZE 26
21 #define ALPHABET {'A','B','C','D','E','F','G','H','I','J','K','L','M','N','O','P','Q','R','S','T','U','V','W','X','Y','Z'}
22 /*
23 #define ALPHABET {'A','B','C','Č','D','E','F','G','H','I','J','K','L','M','N','O','P','R','S','Š','T','U','V','Z','Ž'}
24 #define ALPHABET {'A','B','C','Č','D','E','F','G','H','I','J','K','L','M','N','O','P','Q','R','S','Š','T','U','V','W','X','Y','Z','Ž'}
25 */
26 
27 #include <stdio.h>
28 #include <string.h>
29 #include <ctype.h>
30 
31 #ifdef USE_BIDDY
32 # include "biddy.h"
33 # define BDDNULL NULL
34 #endif
35 
36 #ifdef USE_CUDD
37 # include <stdlib.h>
38 # include <stdint.h>
39 # include <stdarg.h>
40 # include <math.h>
41 # include "cudd.h"
42 # define BDDNULL NULL
43 # ifndef TRUE
44 # define TRUE (0 == 0)
45 # endif
46 # ifndef FALSE
47 # define FALSE !TRUE
48 # endif
49 typedef char *Biddy_String;
50 typedef char Biddy_Boolean;
51 typedef DdNode *Biddy_Edge;
52 DdManager * manager; /* BDD Manager */
53 #endif
54 
55 #include <time.h>
56 
57 #ifdef USE_CUDD
58 #define BIDDYTYPEOBDD 1
59 #define BIDDYTYPEOBDDC 2
60 #define BIDDYTYPEZBDD 3
61 #define BIDDYTYPEZBDDC 4
62 #define BIDDYTYPETZBDD 5
63 #define BIDDYTYPETZBDDC 6
64 #define Biddy_GetManagerType() BIDDYTYPEOBDDC
65 #define Biddy_GetConstantZero() Cudd_ReadLogicZero(manager)
66 #define Biddy_GetConstantOne() Cudd_ReadOne(manager)
67 #define Biddy_AddVariable() Cudd_bddNewVar(manager)
68 #define Biddy_Inv(f) Cudd_Not(f)
69 #define Biddy_Not(f) Cudd_Not(f)
70 #define Biddy_And(f,g) Cudd_bddAnd(manager,f,g)
71 #define Biddy_Or(f,g) Cudd_bddOr(manager,f,g)
72 #define Biddy_Xor(f,g) Cudd_bddXor(manager,f,g)
73 #define Biddy_Xnor(f,g) Cudd_bddXnor(manager,f,g)
74 #define Biddy_Support(f) Cudd_Support(manager,f)
75 #define Biddy_DependentVariableNumber(f) Cudd_SupportSize(manager,f)
76 #define Biddy_CountMinterm(f,n) Cudd_CountMinterm(manager,f,n)
77 #define Biddy_ChangeVariableName(v,name) 0
78 #define Biddy_NodeNumber(f) Cudd_DagSize(f)
79 #define Biddy_NodeTableNum() Cudd_ReadKeys(manager)
80 #define Biddy_NodeTableSize() Cudd_ReadSlots(manager)
81 #define Biddy_PrintInfo(s) Cudd_PrintInfo(manager,s)
82 #endif
83 
84 int main(int argv, char ** argc) {
85  clock_t elapsedtime;
86  FILE *f;
87  char alphabet[ALPHABETSIZE] = ALPHABET;
88  Biddy_Edge code[WORDSIZE][ALPHABETSIZE]; /* BDD variables */
89  Biddy_Edge dictionary;
90  Biddy_Edge tmp1;
91  unsigned int i,j;
92  unsigned int letter;
93  Biddy_String name;
94  char word5[6]; /* 5-letter word + \0 */
95  Biddy_Boolean eof;
96 
97  setbuf(stdout,NULL);
98 
99  /* initialize the BDD manager with default options */
100 
101 #ifdef USE_BIDDY
102  printf("Using Biddy");
103  /* DEFAULT INIT CALL: Biddy_InitAnonymous(BIDDYTYPEOBDDC) */
104  Biddy_InitAnonymous(BIDDYTYPEOBDDC);
105 #endif
106 
107 #ifdef USE_CUDD
108  printf("Using CUDD");
109  /* DEFAULT INIT CALL: Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0) */
110  manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
111  /* Cudd_SetMaxCacheHard(manager,262144); */
112  /* Cudd_AutodynEnable(manager,CUDD_REORDER_SAME); */
113 #endif
114 
115  printf(" (%s)...\n",Biddy_GetManagerName());
116 
117  /* check alphabet */
118  for (i=0; i<ALPHABETSIZE; i++) {
119  printf("(%c)",alphabet[i]);
120  }
121  printf("\n");
122 
123  elapsedtime = clock();
124 
125  /* create BDD variables */
126 #ifdef USE_BIDDY
127  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
128  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDD))
129  {
130  char name[3];
131  name[0] = name[1] = name[2] = 0;
132  for (i=0; i<WORDSIZE; i++) {
133  name[1] = '1' + i;
134  for (j=0; j<ALPHABETSIZE; j++) {
135  name[0] = alphabet[j];
136  code[i][j] = Biddy_AddVariable();
137  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
138  }
139  }
140  }
141 #endif
142 
143  /* for ZBDDs, by adding new variables all the existing ones are changed */
144  /* after adding the last variable we have to refresh the array of variables */
145  /* NOTE: for Biddy, variables are added in the reverse order to make results comparable with Knuth */
146  /* NOTE: for Biddy, code[0][0] = "A1" and it is last added, it can be retrieved by Biddy_GetVariableEdge(WORDSIZE*ALPHABETSIZE) */
147  /* NOTE: for Biddy, user variables start with index 1 */
148 #ifdef USE_BIDDY
149  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
150  {
151  char name[3];
152  name[0] = name[1] = name[2] = 0;
153  for (i=0; i<WORDSIZE; i++) {
154  name[1] = '1' + (WORDSIZE-i-1);
155  for (j=0; j<ALPHABETSIZE; j++) {
156  name[0] = alphabet[ALPHABETSIZE-j-1];
157  code[WORDSIZE-i-1][ALPHABETSIZE-j-1] = Biddy_AddVariable();
158  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
159  }
160  }
161  for (i=0; i<WORDSIZE; i++) {
162  for (j=0; j<ALPHABETSIZE; j++) {
163  code[i][j] = Biddy_GetVariableEdge(WORDSIZE*ALPHABETSIZE-(i*ALPHABETSIZE+j));
164  }
165  }
166  }
167 #endif
168 
169  dictionary = Biddy_GetConstantZero();
170 
171  f = fopen("./test/sgb-words.txt","r");
172  eof = FALSE;
173  while (!eof) {
174  eof = ( fscanf(f,"%s",word5) == EOF );
175  if (!eof) {
176 
177  tmp1 = Biddy_GetConstantOne();
178  for (i=0; i<WORDSIZE; i++) {
179  letter = toupper(word5[i]);
180  for (j=0; j<ALPHABETSIZE; j++) {
181  if (letter == alphabet[j]) {
182  tmp1 = Biddy_And(tmp1,code[i][j]);
183  } else {
184  tmp1 = Biddy_And(tmp1,Biddy_Not(code[i][j]));
185  }
186  }
187  }
188  dictionary = Biddy_Or(dictionary,tmp1);
189 
190 #ifdef USE_BIDDY
191  Biddy_AddTmpFormula(dictionary,1);
192  Biddy_Clean();
193 #endif
194 
195  /* DEBUGGING */
196  /*
197  printf("<%s,%u>",word5,Biddy_NodeNumber(dictionary));
198  */
199 
200  }
201  eof = (fgetc(f) == EOF);
202  }
203  fclose(f);
204 
205  elapsedtime = clock()-elapsedtime;
206 
207  printf("\n");
208  printf("Resulting dictionary depends on %u variables.\n",Biddy_DependentVariableNumber(dictionary));
209  printf("Resulting dictionary has %.0f minterms.\n",Biddy_CountMinterm(dictionary,WORDSIZE*ALPHABETSIZE));
210  printf("System has %u nodes.\n",Biddy_NodeTableNum());
211 
212 #ifdef USE_BIDDY
213 #ifdef MINGW
214  printf("Memory in use: %I64u B\n",Biddy_ReadMemoryInUse());
215 #else
216  printf("Memory in use: %llu B\n",Biddy_ReadMemoryInUse());
217 #endif
218 #endif
219 
220  printf("TIME: %.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
221 
222 #ifdef USE_BIDDY
223  if (Biddy_GetManagerType() == BIDDYTYPEOBDD) {
224  printf("OBDD for resulting dictionary has %u nodes.\n",
225  Biddy_NodeNumber(dictionary));
226  } else if (Biddy_GetManagerType() == BIDDYTYPEOBDDC) {
227  printf("OBDD for resulting dictionary has %u nodes (%u nodes if using complement edges).\n",
228  Biddy_NodeNumberPlain(dictionary),Biddy_NodeNumber(dictionary));
229  } else if (Biddy_GetManagerType() == BIDDYTYPEZBDD) {
230  printf("ZBDD for resulting dictionary has %u nodes.\n",
231  Biddy_NodeNumber(dictionary));
232  } else if (Biddy_GetManagerType() == BIDDYTYPEZBDDC) {
233  printf("ZBDD for resulting dictionary has %u nodes (%u nodes if using complement edges).\n",
234  Biddy_NodeNumberPlain(dictionary),Biddy_NodeNumber(dictionary));
235  } else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
236  printf("TZBDD for resulting dictionary has %u nodes.\n",
237  Biddy_NodeNumber(dictionary));
238  } else if (Biddy_GetManagerType() == BIDDYTYPETZBDDC) {
239  printf("TZBDD for resulting dictionary has %u nodes (%u nodes if using complement edges).\n",
240  Biddy_NodeNumberPlain(dictionary),Biddy_NodeNumber(dictionary));
241  }
242 #endif
243 
244  printf("\n");
245  Biddy_PrintInfo(stdout);
246 
247  /* DEBUGGING */
248  /*
249  printf("\n");
250  Biddy_WriteDot("dictionary.dot",dictionary,"DICT",-1,FALSE);
251  printf("USE 'dot -y -Tpng -O dictionary.dot' to visualize BDD for dictionary.\n");
252  */
253 
254  /* DEBUGGING */
255  /*
256  printf("\n");
257  Biddy_WriteBddview("dictionary.bddview",dictionary,"DICT",NULL);
258  */
259 }
#define Biddy_CountMinterm(f, nvars)
Definition: biddy.h:982
void * Biddy_Edge
Definition: biddy.h:250
#define Biddy_GetManagerType()
Definition: biddy.h:309
#define Biddy_And(f, g)
Definition: biddy.h:517
#define Biddy_Clean()
Definition: biddy.h:663
#define Biddy_NodeTableNum()
Definition: biddy.h:821
#define Biddy_ChangeVariableName(v, x)
Definition: biddy.h:458
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:961
#define Biddy_NodeNumberPlain(f)
Definition: biddy.h:956
#define Biddy_GetConstantOne()
Definition: biddy.h:381
#define Biddy_PrintInfo(f)
Definition: biddy.h:1004
#define Biddy_Or(f, g)
Definition: biddy.h:525
#define Biddy_NodeNumber(f)
Definition: biddy.h:781
#define Biddy_VariableTableNum()
Definition: biddy.h:796
#define Biddy_Not(f)
Definition: biddy.h:506
#define Biddy_GetConstantZero()
Definition: biddy.h:374
File biddy.h contains declaration of all external data structures.
char Biddy_Boolean
Definition: biddy.h:220
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:408
#define Biddy_ReadMemoryInUse()
Definition: biddy.h:999
#define Biddy_GetManagerName()
Definition: biddy.h:314
char * Biddy_String
Definition: biddy.h:223