source: vis_dev/glu-2.3/src/cmuBdd/testbdd.c @ 91

Last change on this file since 91 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 27.3 KB
Line 
1/* Basic operation tests */
2
3
4#include <stdio.h>
5#if HAVE_STDARG_H
6#  include <stdarg.h>
7#else
8#  if HAVE_VARARGS_H
9#    include <varargs.h>
10#  else
11#    error "Need to have HAVE_STDARG_H or HAVE_VARARGS_H defined for variable arguments"
12#  endif
13#endif
14#if STDC_HEADERS
15#  include <stdlib.h>
16#endif
17
18#include "bddint.h"
19
20
21#define VARS 500
22
23
24#define TT_BITS 32              /* Size of tt in bits */
25#define TT_VARS 5               /* log2 of BITS */
26/* Also see cofactor_masks below. */
27
28        /* Number of trials to run */
29/* #define ITERATIONS 20000 */
30#define ITERATIONS 200
31
32
33#if defined(__STDC__)
34#if STDC_HEADERS
35#include <stdlib.h>
36#else
37extern void srandom(unsigned int);
38extern long random(void);
39#endif
40#if HAVE_UNISTD_H
41#include <unistd.h>
42#else
43extern int unlink(char *);
44#endif
45#else
46extern void srandom();
47extern long random();
48extern int unlink();
49#endif
50
51
52typedef unsigned long tt;       /* "Truth table" */
53
54
55static cmu_bdd_manager bddm;
56
57
58static bdd vars[VARS];
59static bdd aux_vars[VARS];
60
61
62static tt cofactor_masks[]=
63{
64  0xffff0000,
65  0xff00ff00,
66  0xf0f0f0f0,
67  0xcccccccc,
68  0xaaaaaaaa,
69};
70
71
72static
73bdd
74#if defined(__STDC__)
75decode(int var, tt table)
76#else
77decode(var, table)
78     int var;
79     tt table;
80#endif
81{
82  bdd temp1, temp2;
83  bdd result;
84
85  if (var == TT_VARS)
86    return ((table & 1) ? cmu_bdd_one(bddm) : cmu_bdd_zero(bddm));
87  temp1=decode(var+1, table >> (1 << (TT_VARS-var-1)));
88  temp2=decode(var+1, table);
89  result=cmu_bdd_ite(bddm, vars[var], temp1, temp2);
90  cmu_bdd_free(bddm, temp1);
91  cmu_bdd_free(bddm, temp2);
92  return (result);
93}
94
95
96#define encoding_to_bdd(table) (decode(0, (table)))
97
98
99static union hack_u {
100  INT_PTR as_double_space[2];
101  double  double_value;
102} hack;
103
104static
105double
106#if defined(__STDC__)
107as_double(INT_PTR v1, INT_PTR v2)
108#else
109as_double(v1, v2)
110     INT_PTR v1;
111     INT_PTR v2;
112#endif
113{
114  hack.as_double_space[0]=v1;
115  hack.as_double_space[1]=v2;
116  return (hack.double_value);
117}
118
119
120static
121void
122#if defined(__STDC__)
123as_INT_PTRs(double n, INT_PTR *r1, INT_PTR *r2)
124#else
125as_INT_PTRs(n, r1, r2)
126     double n;
127     INT_PTR *r1;
128     INT_PTR *r2;
129#endif
130{
131  hack.double_value=n;
132  *r1=hack.as_double_space[0];
133  *r2=hack.as_double_space[1];
134}
135
136
137static
138char *
139#if defined(__STDC__)
140terminal_id_fn(cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, pointer junk)
141#else
142terminal_id_fn(bddm, v1, v2, junk)
143     cmu_bdd_manager bddm;
144     INT_PTR v1;
145     INT_PTR v2;
146     pointer junk;
147#endif
148{
149  static char result[100];
150
151  sprintf(result, "%g", as_double(v1, v2));
152  return (result);
153}
154
155
156static
157void
158#if defined(__STDC__)
159print_bdd(bdd f)
160#else
161print_bdd(f)
162     bdd f;
163#endif
164{
165  cmu_bdd_print_bdd(bddm, f, bdd_naming_fn_none, terminal_id_fn, (pointer)0, stderr);
166}
167
168
169#if defined(__STDC__)
170static
171void
172error(char *op, bdd result, bdd expected, ...)
173{
174  int i;
175  va_list ap;
176  bdd f;
177
178  va_start(ap, expected);
179  fprintf(stderr, "\nError: operation %s:\n", op);
180  i=0;
181  while (1)
182    {
183      f=va_arg(ap, bdd);
184      if (f)
185        {
186          ++i;
187          fprintf(stderr, "Argument %d:\n", i);
188          print_bdd(f);
189        }
190      else
191        break;
192    }
193  fprintf(stderr, "Result:\n");
194  print_bdd(result);
195  fprintf(stderr, "Expected result:\n");
196  print_bdd(expected);
197  va_end(ap);
198}
199#else
200static
201void
202error(va_alist)
203     va_dcl
204{
205  int i;
206  va_list ap;
207  char *op;
208  bdd result;
209  bdd expected;
210  bdd f;
211
212  va_start(ap);
213  op=va_arg(ap, char *);
214  result=va_arg(ap, bdd);
215  expected=va_arg(ap, bdd);
216  fprintf(stderr, "\nError: operation %s:\n", op);
217  i=0;
218  while (1)
219    {
220      f=va_arg(ap, bdd);
221      if (f)
222        {
223          ++i;
224          fprintf(stderr, "Argument %d:\n", i);
225          print_bdd(f);
226        }
227      else
228        break;
229    }
230  fprintf(stderr, "Result:\n");
231  print_bdd(result);
232  fprintf(stderr, "Expected result:\n");
233  print_bdd(expected);
234  va_end(ap);
235}
236#endif
237
238
239static
240tt
241#if defined(__STDC__)
242cofactor(tt table, int var, int value)
243#else
244cofactor(table, var, value)
245     tt table;
246     int var;
247     int value;
248#endif
249{
250  int shift;
251
252  shift=1 << (TT_VARS-var-1);
253  if (value)
254    {
255      table&=cofactor_masks[var];
256      table|=table >> shift;
257    }
258  else
259    {
260      table&=~cofactor_masks[var];
261      table|=table << shift;
262    }
263  return (table);
264}
265
266
267static
268void
269#if defined(__STDC__)
270test_ite(bdd f1, tt table1, bdd f2, tt table2, bdd f3, tt table3)
271#else
272test_ite(f1, table1, f2, table2, f3, table3)
273     bdd f1;
274     tt table1;
275     bdd f2;
276     tt table2;
277     bdd f3;
278     tt table3;
279#endif
280{
281  bdd result;
282  tt resulttable;
283  bdd expected;
284
285  result=cmu_bdd_ite(bddm, f1, f2, f3);
286  resulttable=(table1 & table2) | (~table1 & table3);
287  expected=encoding_to_bdd(resulttable);
288  if (result != expected)
289    error("ITE", result, expected, f1, f2, f3, (bdd)0);
290  cmu_bdd_free(bddm, result);
291  cmu_bdd_free(bddm, expected);
292}
293
294
295static
296void
297#if defined(__STDC__)
298test_and(bdd f1, tt table1, bdd f2, tt table2)
299#else
300test_and(f1, table1, f2, table2)
301     bdd f1;
302     tt table1;
303     bdd f2;
304     tt table2;
305#endif
306{
307  bdd result;
308  tt resulttable;
309  bdd expected;
310
311  result=cmu_bdd_and(bddm, f1, f2);
312  resulttable=table1 & table2;
313  expected=encoding_to_bdd(resulttable);
314  if (result != expected)
315    error("and", result, expected, f1, f2, (bdd)0);
316  cmu_bdd_free(bddm, result);
317  cmu_bdd_free(bddm, expected);
318}
319
320
321static
322void
323#if defined(__STDC__)
324test_or(bdd f1, tt table1, bdd f2, tt table2)
325#else
326test_or(f1, table1, f2, table2)
327     bdd f1;
328     tt table1;
329     bdd f2;
330     tt table2;
331#endif
332{
333  bdd result;
334  tt resulttable;
335  bdd expected;
336
337  result=cmu_bdd_or(bddm, f1, f2);
338  resulttable=table1 | table2;
339  expected=encoding_to_bdd(resulttable);
340  if (result != expected)
341    error("or", result, expected, f1, f2, (bdd)0);
342  cmu_bdd_free(bddm, result);
343  cmu_bdd_free(bddm, expected);
344}
345
346
347static
348void
349#if defined(__STDC__)
350test_xor(bdd f1, tt table1, bdd f2, tt table2)
351#else
352test_xor(f1, table1, f2, table2)
353     bdd f1;
354     tt table1;
355     bdd f2;
356     tt table2;
357#endif
358{
359  bdd result;
360  tt resulttable;
361  bdd expected;
362
363  result=cmu_bdd_xor(bddm, f1, f2);
364  resulttable=table1 ^ table2;
365  expected=encoding_to_bdd(resulttable);
366  if (result != expected)
367    error("xor", result, expected, f1, f2, (bdd)0);
368  cmu_bdd_free(bddm, result);
369  cmu_bdd_free(bddm, expected);
370}
371
372
373static
374void
375#if defined(__STDC__)
376test_id_not(bdd f, tt table)
377#else
378test_id_not(f, table)
379     bdd f;
380     tt table;
381#endif
382{
383  bdd result;
384  tt resulttable;
385  bdd expected;
386
387  result=cmu_bdd_not(bddm, f);
388  resulttable= ~table;
389  expected=encoding_to_bdd(resulttable);
390  if (result != expected)
391    error("not", result, expected, f, (bdd)0);
392  cmu_bdd_free(bddm, result);
393  cmu_bdd_free(bddm, expected);
394  result=cmu_bdd_identity(bddm, f);
395  resulttable=table;
396  expected=encoding_to_bdd(resulttable);
397  if (result != expected)
398    error("identity", result, expected, f, (bdd)0);
399  cmu_bdd_free(bddm, result);
400  cmu_bdd_free(bddm, expected);
401}
402
403
404static
405void
406#if defined(__STDC__)
407test_compose(bdd f1, tt table1, bdd f2, tt table2)
408#else
409test_compose(f1, table1, f2, table2)
410     bdd f1;
411     tt table1;
412     bdd f2;
413     tt table2;
414#endif
415{
416  int var;
417  bdd result;
418  tt resulttable;
419  bdd expected;
420
421  var=((unsigned long)random())%TT_VARS;
422  result=cmu_bdd_compose(bddm, f1, vars[var], cmu_bdd_one(bddm));
423  resulttable=cofactor(table1, var, 1);
424  expected=encoding_to_bdd(resulttable);
425  if (result != expected)
426    error("restrict1", result, expected, f1, vars[var], (bdd)0);
427  cmu_bdd_free(bddm, result);
428  cmu_bdd_free(bddm, expected);
429  result=cmu_bdd_compose(bddm, f1, vars[var], cmu_bdd_zero(bddm));
430  resulttable=cofactor(table1, var, 0);
431  expected=encoding_to_bdd(resulttable);
432  if (result != expected)
433    error("restrict0", result, expected, f1, vars[var], (bdd)0);
434  cmu_bdd_free(bddm, result);
435  cmu_bdd_free(bddm, expected);
436  result=cmu_bdd_compose(bddm, f1, vars[var], f2);
437  resulttable=(table2 & cofactor(table1, var, 1)) | (~table2 & cofactor(table1, var, 0));
438  expected=encoding_to_bdd(resulttable);
439  if (result != expected)
440    error("compose", result, expected, f1, vars[var], f2, (bdd)0);
441  cmu_bdd_free(bddm, result);
442  cmu_bdd_free(bddm, expected);
443}
444
445
446static
447void
448#if defined(__STDC__)
449test_qnt(bdd f, tt table)
450#else
451test_qnt(f, table)
452     bdd f;
453     tt table;
454#endif
455{
456  int var1, var2;
457  bdd assoc[3];
458  bdd temp;
459  bdd result;
460  tt resulttable;
461  bdd expected;
462
463  var1=((unsigned long)random())%TT_VARS;
464  do
465    var2=((unsigned long)random())%TT_VARS;
466  while (var1 == var2);
467  assoc[0]=vars[var1];
468  assoc[1]=vars[var2];
469  assoc[2]=0;
470  cmu_bdd_temp_assoc(bddm, assoc, 0);
471  cmu_bdd_assoc(bddm, -1);
472  if (random()%2)
473    result=cmu_bdd_exists(bddm, f);
474  else
475    {
476      temp=cmu_bdd_not(bddm, f);
477      result=cmu_bdd_forall(bddm, temp);
478      cmu_bdd_free(bddm, temp);
479      temp=result;
480      result=cmu_bdd_not(bddm, temp);
481      cmu_bdd_free(bddm, temp);
482    }
483  resulttable=cofactor(table, var1, 1) | cofactor(table, var1, 0);
484  resulttable=cofactor(resulttable, var2, 1) | cofactor(resulttable, var2, 0);
485  expected=encoding_to_bdd(resulttable);
486  if (result != expected)
487    error("quantification", result, expected, f, vars[var1], vars[var2], (bdd)0);
488  cmu_bdd_free(bddm, result);
489  cmu_bdd_free(bddm, expected);
490}
491
492
493static
494void
495#if defined(__STDC__)
496test_rel_prod(bdd f1, tt table1, bdd f2, tt table2)
497#else
498test_rel_prod(f1, table1, f2, table2)
499     bdd f1;
500     tt table1;
501     bdd f2;
502     tt table2;
503#endif
504{
505  int var1, var2;
506  bdd assoc[3];
507  bdd result;
508  tt resulttable;
509  bdd expected;
510
511  var1=((unsigned long)random())%TT_VARS;
512  do
513    var2=((unsigned long)random())%TT_VARS;
514  while (var1 == var2);
515  assoc[0]=vars[var1];
516  assoc[1]=vars[var2];
517  assoc[2]=0;
518  cmu_bdd_temp_assoc(bddm, assoc, 0);
519  cmu_bdd_assoc(bddm, -1);
520  result=cmu_bdd_rel_prod(bddm, f1, f2);
521  table1&=table2;
522  resulttable=cofactor(table1, var1, 1) | cofactor(table1, var1, 0);
523  resulttable=cofactor(resulttable, var2, 1) | cofactor(resulttable, var2, 0);
524  expected=encoding_to_bdd(resulttable);
525  if (result != expected)
526    error("relational product", result, expected, f1, f2, vars[var1], vars[var2], (bdd)0);
527  cmu_bdd_free(bddm, result);
528  cmu_bdd_free(bddm, expected);
529}
530
531
532static
533void
534#if defined(__STDC__)
535test_subst(bdd f1, tt table1, bdd f2, tt table2, bdd f3, tt table3)
536#else
537test_subst(f1, table1, f2, table2, f3, table3)
538     bdd f1;
539     tt table1;
540     bdd f2;
541     tt table2;
542     bdd f3;
543     tt table3;
544#endif
545{
546  int var1, var2;
547  bdd assoc[6];
548  bdd result;
549  tt resulttable;
550  tt temp1, temp2, temp3, temp4;
551  bdd expected;
552
553  var1=((unsigned long)random())%TT_VARS;
554  do
555    var2=((unsigned long)random())%TT_VARS;
556  while (var1 == var2);
557  assoc[0]=vars[var1];
558  assoc[1]=f2;
559  assoc[2]=vars[var2];
560  assoc[3]=f3;
561  assoc[4]=0;
562  assoc[5]=0;
563  cmu_bdd_temp_assoc(bddm, assoc, 1);
564  cmu_bdd_assoc(bddm, -1);
565  result=cmu_bdd_substitute(bddm, f1);
566  temp1=cofactor(cofactor(table1, var1, 1), var2, 1);
567  temp2=cofactor(cofactor(table1, var1, 1), var2, 0);
568  temp3=cofactor(cofactor(table1, var1, 0), var2, 1);
569  temp4=cofactor(cofactor(table1, var1, 0), var2, 0);
570  resulttable=table2 & table3 & temp1;
571  resulttable|=table2 & ~table3 & temp2;
572  resulttable|=~table2 & table3 & temp3;
573  resulttable|=~table2 & ~table3 & temp4;
574  expected=encoding_to_bdd(resulttable);
575  if (result != expected)
576    error("substitute", result, expected, f1, vars[var1], f2, vars[var2], f3, (bdd)0);
577  cmu_bdd_free(bddm, result);
578  cmu_bdd_free(bddm, expected);
579}
580
581
582static
583void
584#if defined(__STDC__)
585test_inter_impl(bdd f1, tt table1, bdd f2, tt table2)
586#else
587test_inter_impl(f1, table1, f2, table2)
588     bdd f1;
589     tt table1;
590     bdd f2;
591     tt table2;
592#endif
593{
594  bdd result;
595  tt resulttable;
596  bdd expected;
597  bdd implies_result;
598
599  result=cmu_bdd_intersects(bddm, f1, f2);
600  resulttable=table1 & table2;
601  expected=encoding_to_bdd(resulttable);
602  implies_result=cmu_bdd_implies(bddm, result, expected);
603  if (implies_result != cmu_bdd_zero(bddm))
604    {
605      error("intersection test", result, expected, f1, f2, (bdd)0);
606      cmu_bdd_free(bddm, implies_result);
607    }
608  cmu_bdd_free(bddm, result);
609  cmu_bdd_free(bddm, expected);
610}
611
612
613static
614void
615#if defined(__STDC__)
616test_sat(bdd f, tt table)
617#else
618test_sat(f, table)
619     bdd f;
620     tt table;
621#endif
622{
623  int var1, var2;
624  bdd assoc[TT_VARS+1];
625  bdd result;
626  bdd temp1, temp2, temp3;
627
628  if (f == cmu_bdd_zero(bddm))
629    return;
630  result=cmu_bdd_satisfy(bddm, f);
631  temp1=cmu_bdd_not(bddm, f);
632  temp2=cmu_bdd_intersects(bddm, temp1, result);
633  if (temp2 != cmu_bdd_zero(bddm))
634    error("intersection of satisfy result with negated argument", temp2, cmu_bdd_zero(bddm), f, (bdd)0);
635  cmu_bdd_free(bddm, temp1);
636  cmu_bdd_free(bddm, temp2);
637  var1=((unsigned long)random())%TT_VARS;
638  do
639    var2=((unsigned long)random())%TT_VARS;
640  while (var1 == var2);
641  assoc[0]=vars[var1];
642  assoc[1]=vars[var2];
643  assoc[2]=0;
644  cmu_bdd_temp_assoc(bddm, assoc, 0);
645  cmu_bdd_assoc(bddm, -1);
646  temp1=cmu_bdd_satisfy_support(bddm, result);
647  temp2=cmu_bdd_not(bddm, result);
648  temp3=cmu_bdd_intersects(bddm, temp2, temp1);
649  if (temp3 != cmu_bdd_zero(bddm))
650    error("intersection of satisfy support result with negated argument", temp3, cmu_bdd_zero(bddm), result, (bdd)0);
651  cmu_bdd_free(bddm, result);
652  cmu_bdd_free(bddm, temp1);
653  cmu_bdd_free(bddm, temp2);
654  cmu_bdd_free(bddm, temp3);
655  temp1=cmu_bdd_compose(bddm, f, vars[var1], cmu_bdd_zero(bddm));
656  temp2=cmu_bdd_compose(bddm, f, vars[var1], cmu_bdd_one(bddm));
657  if (cmu_bdd_satisfying_fraction(bddm, temp1)+cmu_bdd_satisfying_fraction(bddm, temp2) !=
658      2.0*cmu_bdd_satisfying_fraction(bddm, f))
659    {
660      fprintf(stderr, "\nError: operation satisfying fraction:\n");
661      fprintf(stderr, "Argument:\n");
662      print_bdd(f);
663      fprintf(stderr, "Cofactor on:\n");
664      print_bdd(vars[var1]);
665    }
666  cmu_bdd_free(bddm, temp1);
667  cmu_bdd_free(bddm, temp2);
668}
669
670
671static
672void
673#if defined(__STDC__)
674test_gen_cof(bdd f1, tt table1, bdd f2, tt table2)
675#else
676test_gen_cof(f1, table1, f2, table2)
677     bdd f1;
678     tt table1;
679     bdd f2;
680     tt table2;
681#endif
682{
683  int var1, var2;
684  bdd result;
685  bdd temp1, temp2, temp3;
686  tt resulttable;
687  bdd expected;
688
689  result=cmu_bdd_cofactor(bddm, f1, f2);
690  temp1=cmu_bdd_xnor(bddm, result, f1);
691  temp2=cmu_bdd_not(bddm, f2);
692  temp3=cmu_bdd_or(bddm, temp1, temp2);
693  if (temp3 != cmu_bdd_one(bddm))
694    error("d.c. comparison of generalized cofactor", temp3, cmu_bdd_one(bddm), f1, f2, (bdd)0);
695  cmu_bdd_free(bddm, result);
696  cmu_bdd_free(bddm, temp1);
697  cmu_bdd_free(bddm, temp2);
698  cmu_bdd_free(bddm, temp3);
699  var1=((unsigned long)random())%TT_VARS;
700  do
701    var2=((unsigned long)random())%TT_VARS;
702  while (var1 == var2);
703  temp1=cmu_bdd_not(bddm, vars[var2]);
704  temp2=cmu_bdd_and(bddm, vars[var1], temp1);
705  cmu_bdd_free(bddm, temp1);
706  result=cmu_bdd_cofactor(bddm, f1, temp2);
707  resulttable=cofactor(cofactor(table1, var1, 1), var2, 0);
708  expected=encoding_to_bdd(resulttable);
709  if (result != expected)
710    error("generalized cofactor", result, expected, f1, temp2, (bdd)0);
711  cmu_bdd_free(bddm, result);
712  cmu_bdd_free(bddm, expected);
713  cmu_bdd_free(bddm, temp2);
714}
715
716
717static
718void
719#if defined(__STDC__)
720test_reduce(bdd f1, tt table1, bdd f2, tt table2)
721#else
722test_reduce(f1, table1, f2, table2)
723     bdd f1;
724     tt table1;
725     bdd f2;
726     tt table2;
727#endif
728{
729  bdd result;
730  bdd temp1, temp2, temp3;
731
732  result=cmu_bdd_reduce(bddm, f1, f2);
733  temp1=cmu_bdd_xnor(bddm, result, f1);
734  temp2=cmu_bdd_not(bddm, f2);
735  temp3=cmu_bdd_or(bddm, temp1, temp2);
736  if (temp3 != cmu_bdd_one(bddm))
737    error("d.c. comparison of reduce", temp3, cmu_bdd_one(bddm), f1, f2, (bdd)0);
738  cmu_bdd_free(bddm, result);
739  cmu_bdd_free(bddm, temp1);
740  cmu_bdd_free(bddm, temp2);
741  cmu_bdd_free(bddm, temp3);
742}
743
744
745static
746bdd
747#if defined(__STDC__)
748apply_and(cmu_bdd_manager bddm, bdd *f, bdd *g, pointer env)
749#else
750apply_and(bddm, f, g, env)
751     cmu_bdd_manager bddm;
752     bdd *f;
753     bdd *g;
754     pointer env;
755#endif
756{
757  bdd f1, g1;
758
759  f1= *f;
760  g1= *g;
761  {
762    if (f1 == BDD_ZERO(bddm))
763      return (f1);
764    if (g1 == BDD_ZERO(bddm))
765      return (g1);
766    if (f1 == BDD_ONE(bddm))
767      return (g1);
768    if (g1 == BDD_ONE(bddm))
769      return (f1);
770    if ((INT_PTR)f1 < (INT_PTR)g1)
771      {
772        *f=g1;
773        *g=f1;
774      }
775    return ((bdd)0);
776  }
777}
778
779
780static
781void
782#if defined(__STDC__)
783test_apply(bdd f1, tt table1, bdd f2, tt table2)
784#else
785test_apply(f1, table1, f2, table2)
786     bdd f1;
787     tt table1;
788     bdd f2;
789     tt table2;
790#endif
791{
792  bdd result;
793  tt resulttable;
794  bdd expected;
795
796  result=bdd_apply2(bddm, apply_and, f1, f2, (pointer)0);
797  resulttable=table1 & table2;
798  expected=encoding_to_bdd(resulttable);
799  if (result != expected)
800    error("apply2", result, expected, f1, f2, (bdd)0);
801  cmu_bdd_free(bddm, result);
802  cmu_bdd_free(bddm, expected);
803}
804
805
806static
807void
808#if defined(__STDC__)
809test_size(bdd f1, tt table1, bdd f2, tt table2)
810#else
811test_size(f1, table1, f2, table2)
812     bdd f1;
813     tt table1;
814     bdd f2;
815     tt table2;
816#endif
817{
818  int i;
819  long size;
820  long profile[2*TT_VARS+1];
821  bdd fs[3];
822
823  size=cmu_bdd_size(bddm, f1, 1);
824  cmu_bdd_profile(bddm, f1, profile, 1);
825  for (i=0; i < 2*TT_VARS+1; ++i)
826    size-=profile[i];
827  if (size)
828    {
829      fprintf(stderr, "\nError: size count vs. profile sum:\n");
830      fprintf(stderr, "Argument:\n");
831      print_bdd(f1);
832    }
833  size=cmu_bdd_size(bddm, f1, 0);
834  cmu_bdd_profile(bddm, f1, profile, 0);
835  for (i=0; i < 2*TT_VARS+1; ++i)
836    size-=profile[i];
837  if (size)
838    {
839      fprintf(stderr, "\nError: no negout size count vs. profile sum:\n");
840      fprintf(stderr, "Argument:\n");
841      print_bdd(f1);
842    }
843  fs[0]=f1;
844  fs[1]=f2;
845  fs[2]=0;
846  size=cmu_bdd_size_multiple(bddm, fs, 1);
847  cmu_bdd_profile_multiple(bddm, fs, profile, 1);
848  for (i=0; i < 2*TT_VARS+1; ++i)
849    size-=profile[i];
850  if (size)
851    {
852      fprintf(stderr, "\nError: multiple size count vs. multiple profile sum:\n");
853      fprintf(stderr, "Argument 1:\n");
854      print_bdd(f1);
855      fprintf(stderr, "Argument 2:\n");
856      print_bdd(f2);
857    }
858}
859
860
861static
862int
863#if defined(__STDC__)
864canonical_fn(cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, pointer env)
865#else
866canonical_fn(bddm, v1, v2, env)
867     cmu_bdd_manager bddm;
868     INT_PTR v1;
869     INT_PTR v2;
870     pointer env;
871#endif
872{
873  return (as_double(v1, v2) > 0);
874}
875
876
877static
878void
879#if defined(__STDC__)
880transform_fn(cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, INT_PTR *r1, INT_PTR *r2, pointer env)
881#else
882transform_fn(bddm, v1, v2, r1, r2, env)
883     cmu_bdd_manager bddm;
884     INT_PTR v1;
885     INT_PTR v2;
886     INT_PTR *r1;
887     INT_PTR *r2;
888     pointer env;
889#endif
890{
891  as_INT_PTRs(-as_double(v1, v2), r1, r2);
892}
893
894
895static
896bdd
897#if defined(__STDC__)
898terminal(double n)
899#else
900terminal(n)
901     double n;
902#endif
903{
904  INT_PTR v1, v2;
905
906  as_INT_PTRs(n, &v1, &v2);
907  return (cmu_mtbdd_get_terminal(bddm, v1, v2));
908}
909
910
911static
912bdd
913#if defined(__STDC__)
914walsh_matrix(int n)
915#else
916walsh_matrix(n)
917     int n;
918#endif
919{
920  bdd temp1, temp2, temp3;
921  bdd result;
922
923  if (n == TT_VARS)
924    return (terminal(1.0));
925  temp1=walsh_matrix(n+1);
926  temp2=mtbdd_transform(bddm, temp1);
927  temp3=temp2;
928  temp2=mtcmu_bdd_ite(bddm, aux_vars[n], temp3, temp1);
929  cmu_bdd_free(bddm, temp3);
930  result=mtcmu_bdd_ite(bddm, vars[n], temp2, temp1);
931  cmu_bdd_free(bddm, temp1);
932  cmu_bdd_free(bddm, temp2);
933  return (result);
934}
935
936
937#define OP_MULT 1000l
938#define OP_ADD 1100l
939
940
941static
942bdd
943#if defined(__STDC__)
944mtbdd_mult_step(cmu_bdd_manager bddm, bdd f, bdd g)
945#else
946mtbdd_mult_step(bddm, f, g)
947     cmu_bdd_manager bddm;
948     bdd f;
949     bdd g;
950#endif
951{
952  bdd_indexindex_type top_indexindex;
953  bdd f1, f2;
954  bdd g1, g2;
955  bdd temp1, temp2;
956  bdd result;
957  INT_PTR u1, u2;
958  INT_PTR v1, v2;
959 
960  BDD_SETUP(f);
961  BDD_SETUP(g);
962  if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
963    {
964      cmu_mtbdd_terminal_value_aux(bddm, f, &u1, &u2);
965      cmu_mtbdd_terminal_value_aux(bddm, g, &v1, &v2);
966      as_INT_PTRs(as_double(u1, u2)*as_double(v1, v2), &u1, &u2);
967      return (bdd_find_terminal(bddm, u1, u2));
968    }
969  if (BDD_OUT_OF_ORDER(f, g))
970    BDD_SWAP(f, g);
971  if (bdd_lookup_in_cache2(bddm, OP_MULT, f, g, &result))
972    return (result);
973  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
974  BDD_COFACTOR(top_indexindex, f, f1, f2);
975  BDD_COFACTOR(top_indexindex, g, g1, g2);
976  temp1=mtbdd_mult_step(bddm, f1, g1);
977  temp2=mtbdd_mult_step(bddm, f2, g2);
978  result=bdd_find(bddm, top_indexindex, temp1, temp2);
979  bdd_insert_in_cache2(bddm, OP_MULT, f, g, result);
980  return (result);
981}
982
983
984static
985bdd
986#if defined(__STDC__)
987mtbdd_mult(cmu_bdd_manager bddm, bdd f, bdd g)
988#else
989mtbdd_mult(bddm, f, g)
990     cmu_bdd_manager bddm;
991     bdd f;
992     bdd g;
993#endif
994{
995  if (bdd_check_arguments(2, f, g))
996    {
997      FIREWALL(bddm);
998      RETURN_BDD(mtbdd_mult_step(bddm, f, g));
999    }
1000  return ((bdd)0);
1001}
1002
1003
1004static
1005bdd
1006#if defined(__STDC__)
1007mtbdd_add_step(cmu_bdd_manager bddm, bdd f, bdd g)
1008#else
1009mtbdd_add_step(bddm, f, g)
1010     cmu_bdd_manager bddm;
1011     bdd f;
1012     bdd g;
1013#endif
1014{
1015  bdd_indexindex_type top_indexindex;
1016  bdd f1, f2;
1017  bdd g1, g2;
1018  bdd temp1, temp2;
1019  bdd result;
1020  INT_PTR u1, u2;
1021  INT_PTR v1, v2;
1022 
1023  BDD_SETUP(f);
1024  BDD_SETUP(g);
1025  if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
1026    {
1027      cmu_mtbdd_terminal_value_aux(bddm, f, &u1, &u2);
1028      cmu_mtbdd_terminal_value_aux(bddm, g, &v1, &v2);
1029      as_INT_PTRs(as_double(u1, u2)+as_double(v1, v2), &u1, &u2);
1030      return (bdd_find_terminal(bddm, u1, u2));
1031    }
1032  if (BDD_OUT_OF_ORDER(f, g))
1033    BDD_SWAP(f, g);
1034  if (bdd_lookup_in_cache2(bddm, OP_ADD, f, g, &result))
1035    return (result);
1036  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
1037  BDD_COFACTOR(top_indexindex, f, f1, f2);
1038  BDD_COFACTOR(top_indexindex, g, g1, g2);
1039  temp1=mtbdd_add_step(bddm, f1, g1);
1040  temp2=mtbdd_add_step(bddm, f2, g2);
1041  result=bdd_find(bddm, top_indexindex, temp1, temp2);
1042  bdd_insert_in_cache2(bddm, OP_ADD, f, g, result);
1043  return (result);
1044}
1045
1046
1047static
1048bdd
1049#if defined(__STDC__)
1050mtbdd_add(cmu_bdd_manager bddm, bdd f, bdd g)
1051#else
1052mtbdd_add(bddm, f, g)
1053     cmu_bdd_manager bddm;
1054     bdd f;
1055     bdd g;
1056#endif
1057{
1058  if (bdd_check_arguments(2, f, g))
1059    {
1060      FIREWALL(bddm);
1061      RETURN_BDD(mtbdd_add_step(bddm, f, g));
1062    }
1063  return ((bdd)0);
1064}
1065
1066
1067static
1068bdd
1069#if defined(__STDC__)
1070transform(bdd f, bdd g, bdd *elim_vars)
1071#else
1072transform(f, g, elim_vars)
1073     bdd f;
1074     bdd g;
1075     bdd *elim_vars;
1076#endif
1077{
1078  int i;
1079  bdd temp1, temp2;
1080  bdd result;
1081
1082  result=mtbdd_mult(bddm, f, g);
1083  for (i=0; i < TT_VARS; ++i)
1084    {
1085      temp1=cmu_bdd_compose(bddm, result, elim_vars[i], cmu_bdd_one(bddm));
1086      temp2=cmu_bdd_compose(bddm, result, elim_vars[i], cmu_bdd_zero(bddm));
1087      cmu_bdd_free(bddm, result);
1088      result=mtbdd_add(bddm, temp1, temp2);
1089      cmu_bdd_free(bddm, temp1);
1090      cmu_bdd_free(bddm, temp2);
1091    }
1092  return (result);
1093}
1094
1095
1096static
1097void
1098#if defined(__STDC__)
1099test_mtbdd(bdd f1, tt table1)
1100#else
1101test_mtbdd(f1, table1)
1102     bdd f1;
1103     tt table1;
1104#endif
1105{
1106  bdd wm;
1107  bdd temp1, temp2;
1108  bdd result;
1109
1110  wm=walsh_matrix(0);
1111  temp1=transform(wm, f1, vars);
1112  temp2=temp1;
1113  temp1=transform(wm, temp2, aux_vars);
1114  cmu_bdd_free(bddm, wm);
1115  cmu_bdd_free(bddm, temp2);
1116  temp2=terminal(1.0/TT_BITS);
1117  result=mtbdd_mult(bddm, temp1, temp2);
1118  cmu_bdd_free(bddm, temp1);
1119  cmu_bdd_free(bddm, temp2);
1120  if (f1 != result)
1121    error("Walsh transformation and inverse", result, f1, (bdd)0);
1122  cmu_bdd_free(bddm, result);
1123}
1124
1125
1126static
1127void
1128#if defined(__STDC__)
1129test_swap(bdd f, tt table)
1130#else
1131test_swap(f, table)
1132     bdd f;
1133     tt table;
1134#endif
1135{
1136  int var1, var2;
1137  bdd result;
1138  tt resulttable;
1139  tt temp1, temp2, temp3, temp4;
1140  bdd expected;
1141
1142  var1=((unsigned long)random())%TT_VARS;
1143  var2=((unsigned long)random())%TT_VARS;
1144  result=cmu_bdd_swap_vars(bddm, f, vars[var1], vars[var2]);
1145  temp1=cofactor(cofactor(table, var1, 1), var2, 1);
1146  temp2=cofactor(cofactor(table, var1, 1), var2, 0);
1147  temp3=cofactor(cofactor(table, var1, 0), var2, 1);
1148  temp4=cofactor(cofactor(table, var1, 0), var2, 0);
1149  resulttable=cofactor_masks[var2] & cofactor_masks[var1] & temp1;
1150  resulttable|=cofactor_masks[var2] & ~cofactor_masks[var1] & temp2;
1151  resulttable|=~cofactor_masks[var2] & cofactor_masks[var1] & temp3;
1152  resulttable|=~cofactor_masks[var2] & ~cofactor_masks[var1] & temp4;
1153  expected=encoding_to_bdd(resulttable);
1154  if (result != expected)
1155    error("swap variables", result, expected, f, vars[var1], vars[var2], (bdd)0);
1156  cmu_bdd_free(bddm, result);
1157  cmu_bdd_free(bddm, expected);
1158}
1159
1160
1161static void
1162#if defined(__STDC__)
1163test_dump(bdd f, tt table)
1164#else
1165test_dump(f, table)
1166     bdd f;
1167     tt table;
1168#endif
1169{
1170  FILE *fp;
1171  int i, j;
1172  bdd dump_vars[TT_VARS+1];
1173  bdd temp;
1174  bdd result;
1175  int err;
1176
1177  if (!(fp=tmpfile()))
1178    {
1179      fprintf(stderr, "could not open temporary file\n");
1180      exit(1);
1181    }
1182  for (i=0; i < TT_VARS; ++i)
1183    dump_vars[i]=vars[i];
1184  dump_vars[i]=0;
1185  for (i=0; i < TT_VARS-1; ++i)
1186    {
1187      j=i+((unsigned long)random())%(TT_VARS-i);
1188      temp=dump_vars[i];
1189      dump_vars[i]=dump_vars[j];
1190      dump_vars[j]=temp;
1191    }
1192  if (!cmu_bdd_dump_bdd(bddm, f, dump_vars, fp))
1193    {
1194      fprintf(stderr, "Error: dump failure:\n");
1195      fprintf(stderr, "Argument:\n");
1196      print_bdd(f);
1197      fclose(fp);
1198      return;
1199    }
1200  rewind(fp);
1201  if (!(result=cmu_bdd_undump_bdd(bddm, dump_vars, fp, &err)) || err)
1202    {
1203      fprintf(stderr, "Error: undump failure: code %d:\n", err);
1204      fprintf(stderr, "Argument:\n");
1205      print_bdd(f);
1206      fclose(fp);
1207      return;
1208    }
1209  fclose(fp);
1210  if (result != f)
1211    error("dump/undump", result, f, f, (bdd)0);
1212  cmu_bdd_free(bddm, result);
1213}
1214
1215
1216static
1217void
1218#if defined(__STDC__)
1219check_leak(void)
1220#else
1221check_leak()
1222#endif
1223{
1224  bdd assoc[1];
1225
1226  assoc[0]=0;
1227  cmu_bdd_temp_assoc(bddm, assoc, 0);
1228  cmu_bdd_gc(bddm);
1229  if (cmu_bdd_total_size(bddm) != 2*TT_VARS+1l)
1230    fprintf(stderr, "Memory leak somewhere...\n");
1231}
1232
1233
1234static
1235void
1236#if defined(__STDC__)
1237random_tests(int iterations)
1238#else
1239random_tests(iterations)
1240     int iterations;
1241#endif
1242{
1243  int i;
1244  tt table1, table2, table3;
1245  bdd f1, f2, f3;
1246  INT_PTR v1, v2;
1247
1248  printf("Random operation tests...\n");
1249  bddm=cmu_bdd_init();
1250  cmu_bdd_node_limit(bddm, 5000);
1251  mtbdd_transform_closure(bddm, canonical_fn, transform_fn, (pointer)0);
1252  as_INT_PTRs(-1.0, &v1, &v2);
1253  mtcmu_bdd_one_data(bddm, v1, v2);
1254  vars[1]=cmu_bdd_new_var_last(bddm);
1255  vars[0]=cmu_bdd_new_var_first(bddm);
1256  vars[4]=cmu_bdd_new_var_after(bddm, vars[1]);
1257  vars[3]=cmu_bdd_new_var_before(bddm, vars[4]);
1258  vars[2]=cmu_bdd_new_var_after(bddm, vars[1]);
1259  for (i=0; i < 5; ++i)
1260    aux_vars[i]=cmu_bdd_new_var_after(bddm, vars[i]);
1261  for (i=0; i < iterations; ++i)
1262    {
1263      if ((i & 0xf) == 0)
1264        {
1265          putchar('.');
1266          fflush(stdout);
1267        }
1268      if ((i & 0x3ff) == 0x3ff)
1269        {
1270          putchar('\n');
1271          fflush(stdout);
1272          check_leak();
1273        }
1274      table1=random();
1275      table2=random();
1276      table3=random();
1277      f1=encoding_to_bdd(table1);
1278      f2=encoding_to_bdd(table2);
1279      f3=encoding_to_bdd(table3);
1280      test_ite(f1, table1, f2, table2, f3, table3);
1281      test_and(f1, table1, f2, table2);
1282      test_or(f1, table1, f2, table2);
1283      test_xor(f1, table1, f2, table2);
1284      test_id_not(f1, table1);
1285      test_compose(f1, table1, f2, table2);
1286      test_qnt(f1, table1);
1287      test_rel_prod(f1, table1, f2, table2);
1288      test_subst(f1, table1, f2, table2, f3, table3);
1289      test_inter_impl(f1, table1, f2, table2);
1290      test_sat(f1, table1);
1291      test_gen_cof(f1, table1, f2, table2);
1292      test_reduce(f1, table1, f2, table2);
1293      test_apply(f1, table1, f2, table2);
1294      test_size(f1, table1, f2, table2);
1295      test_mtbdd(f1, table1);
1296      test_swap(f1, table1);
1297      if (i < 100)
1298        test_dump(f1, table1);
1299      cmu_bdd_free(bddm, f1);
1300      cmu_bdd_free(bddm, f2);
1301      cmu_bdd_free(bddm, f3);
1302    }
1303  putchar('\n');
1304  cmu_bdd_stats(bddm, stdout);
1305  cmu_bdd_quit(bddm);
1306}
1307
1308
1309int
1310#if defined(__STDC__)
1311main(void)
1312#else
1313main()
1314#endif
1315{
1316  (void) srandom((unsigned) 1);
1317  random_tests(ITERATIONS);
1318  exit(0);
1319}
Note: See TracBrowser for help on using the repository browser.