src/cmuBdd/testbdd.c File Reference

#include <stdio.h>
#include "bddint.h"
Include dependency graph for testbdd.c:

Go to the source code of this file.

Data Structures

union  hack_u

Defines

#define VARS   500
#define TT_BITS   32
#define TT_VARS   5
#define ITERATIONS   200
#define encoding_to_bdd(table)   (decode(0, (table)))
#define OP_MULT   1000l
#define OP_ADD   1100l

Typedefs

typedef unsigned long tt

Functions

void srandom ()
long random ()
int unlink ()
static bdd decode (int var, tt table)
static double as_double (INT_PTR v1, INT_PTR v2)
static void as_INT_PTRs (double n, INT_PTR *r1, INT_PTR *r2)
static char * terminal_id_fn (cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, pointer junk)
static void print_bdd (bdd f)
static void error (va_alist)
static tt cofactor (tt table, int var, int value)
static void test_ite (bdd f1, tt table1, bdd f2, tt table2, bdd f3, tt table3)
static void test_and (bdd f1, tt table1, bdd f2, tt table2)
static void test_or (bdd f1, tt table1, bdd f2, tt table2)
static void test_xor (bdd f1, tt table1, bdd f2, tt table2)
static void test_id_not (bdd f, tt table)
static void test_compose (bdd f1, tt table1, bdd f2, tt table2)
static void test_qnt (bdd f, tt table)
static void test_rel_prod (bdd f1, tt table1, bdd f2, tt table2)
static void test_subst (bdd f1, tt table1, bdd f2, tt table2, bdd f3, tt table3)
static void test_inter_impl (bdd f1, tt table1, bdd f2, tt table2)
static void test_sat (bdd f, tt table)
static void test_gen_cof (bdd f1, tt table1, bdd f2, tt table2)
static void test_reduce (bdd f1, tt table1, bdd f2, tt table2)
static bdd apply_and (cmu_bdd_manager bddm, bdd *f, bdd *g, pointer env)
static void test_apply (bdd f1, tt table1, bdd f2, tt table2)
static void test_size (bdd f1, tt table1, bdd f2, tt table2)
static int canonical_fn (cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, pointer env)
static void transform_fn (cmu_bdd_manager bddm, INT_PTR v1, INT_PTR v2, INT_PTR *r1, INT_PTR *r2, pointer env)
static bdd terminal (double n)
static bdd walsh_matrix (int n)
static bdd mtbdd_mult_step (cmu_bdd_manager bddm, bdd f, bdd g)
static bdd mtbdd_mult (cmu_bdd_manager bddm, bdd f, bdd g)
static bdd mtbdd_add_step (cmu_bdd_manager bddm, bdd f, bdd g)
static bdd mtbdd_add (cmu_bdd_manager bddm, bdd f, bdd g)
static bdd transform (bdd f, bdd g, bdd *elim_vars)
static void test_mtbdd (bdd f1, tt table1)
static void test_swap (bdd f, tt table)
static void test_dump (bdd f, tt table)
static void check_leak ()
static void random_tests (int iterations)
int main ()

Variables

static cmu_bdd_manager bddm
static bdd vars [VARS]
static bdd aux_vars [VARS]
static tt cofactor_masks []
static union hack_u hack

Define Documentation

#define encoding_to_bdd ( table   )     (decode(0, (table)))

Definition at line 96 of file testbdd.c.

#define ITERATIONS   200

Definition at line 30 of file testbdd.c.

#define OP_ADD   1100l

Definition at line 938 of file testbdd.c.

#define OP_MULT   1000l

Definition at line 937 of file testbdd.c.

#define TT_BITS   32

Definition at line 24 of file testbdd.c.

#define TT_VARS   5

Definition at line 25 of file testbdd.c.

#define VARS   500

Definition at line 21 of file testbdd.c.

Typedef Documentation

typedef unsigned long tt

Definition at line 52 of file testbdd.c.

Function Documentation

static bdd apply_and ( cmu_bdd_manager  bddm,
bdd *  f,
bdd *  g,
pointer  env 
) [static]

Definition at line 750 of file testbdd.c.

00756 {
00757   bdd f1, g1;
00758 
00759   f1= *f;
00760   g1= *g;
00761   {
00762     if (f1 == BDD_ZERO(bddm))
00763       return (f1);
00764     if (g1 == BDD_ZERO(bddm))
00765       return (g1);
00766     if (f1 == BDD_ONE(bddm))
00767       return (g1);
00768     if (g1 == BDD_ONE(bddm))
00769       return (f1);
00770     if ((INT_PTR)f1 < (INT_PTR)g1)
00771       {
00772         *f=g1;
00773         *g=f1;
00774       }
00775     return ((bdd)0);
00776   }
00777 }

static double as_double ( INT_PTR  v1,
INT_PTR  v2 
) [static]

Definition at line 109 of file testbdd.c.

00113 {
00114   hack.as_double_space[0]=v1;
00115   hack.as_double_space[1]=v2;
00116   return (hack.double_value);
00117 }

static void as_INT_PTRs ( double  n,
INT_PTR *  r1,
INT_PTR *  r2 
) [static]

Definition at line 125 of file testbdd.c.

00130 {
00131   hack.double_value=n;
00132   *r1=hack.as_double_space[0];
00133   *r2=hack.as_double_space[1];
00134 }

static int canonical_fn ( cmu_bdd_manager  bddm,
INT_PTR  v1,
INT_PTR  v2,
pointer  env 
) [static]

Definition at line 866 of file testbdd.c.

00872 {
00873   return (as_double(v1, v2) > 0);
00874 }

static void check_leak (  )  [static]

Definition at line 1221 of file testbdd.c.

01223 {
01224   bdd assoc[1];
01225 
01226   assoc[0]=0;
01227   cmu_bdd_temp_assoc(bddm, assoc, 0);
01228   cmu_bdd_gc(bddm);
01229   if (cmu_bdd_total_size(bddm) != 2*TT_VARS+1l)
01230     fprintf(stderr, "Memory leak somewhere...\n");
01231 }

static tt cofactor ( tt  table,
int  var,
int  value 
) [static]

Definition at line 244 of file testbdd.c.

00249 {
00250   int shift;
00251 
00252   shift=1 << (TT_VARS-var-1);
00253   if (value)
00254     {
00255       table&=cofactor_masks[var];
00256       table|=table >> shift;
00257     }
00258   else
00259     {
00260       table&=~cofactor_masks[var];
00261       table|=table << shift;
00262     }
00263   return (table);
00264 }

static bdd decode ( int  var,
tt  table 
) [static]

Definition at line 77 of file testbdd.c.

00081 {
00082   bdd temp1, temp2;
00083   bdd result;
00084 
00085   if (var == TT_VARS)
00086     return ((table & 1) ? cmu_bdd_one(bddm) : cmu_bdd_zero(bddm));
00087   temp1=decode(var+1, table >> (1 << (TT_VARS-var-1)));
00088   temp2=decode(var+1, table);
00089   result=cmu_bdd_ite(bddm, vars[var], temp1, temp2);
00090   cmu_bdd_free(bddm, temp1);
00091   cmu_bdd_free(bddm, temp2);
00092   return (result);
00093 }

static void error ( va_alist   )  [static]

Definition at line 202 of file testbdd.c.

00204 {
00205   int i;
00206   va_list ap;
00207   char *op;
00208   bdd result;
00209   bdd expected;
00210   bdd f;
00211 
00212   va_start(ap);
00213   op=va_arg(ap, char *);
00214   result=va_arg(ap, bdd);
00215   expected=va_arg(ap, bdd);
00216   fprintf(stderr, "\nError: operation %s:\n", op);
00217   i=0;
00218   while (1)
00219     {
00220       f=va_arg(ap, bdd);
00221       if (f)
00222         {
00223           ++i;
00224           fprintf(stderr, "Argument %d:\n", i);
00225           print_bdd(f);
00226         }
00227       else
00228         break;
00229     }
00230   fprintf(stderr, "Result:\n");
00231   print_bdd(result);
00232   fprintf(stderr, "Expected result:\n");
00233   print_bdd(expected);
00234   va_end(ap);
00235 }

int main (  ) 

Definition at line 1313 of file testbdd.c.

01315 {
01316   (void) srandom((unsigned) 1);
01317   random_tests(ITERATIONS);
01318   exit(0);
01319 }

static bdd mtbdd_add ( cmu_bdd_manager  bddm,
bdd  f,
bdd  g 
) [static]

Definition at line 1052 of file testbdd.c.

01057 {
01058   if (bdd_check_arguments(2, f, g))
01059     {
01060       FIREWALL(bddm);
01061       RETURN_BDD(mtbdd_add_step(bddm, f, g));
01062     }
01063   return ((bdd)0);
01064 }

static bdd mtbdd_add_step ( cmu_bdd_manager  bddm,
bdd  f,
bdd  g 
) [static]

Definition at line 1009 of file testbdd.c.

01014 {
01015   bdd_indexindex_type top_indexindex;
01016   bdd f1, f2;
01017   bdd g1, g2;
01018   bdd temp1, temp2;
01019   bdd result;
01020   INT_PTR u1, u2;
01021   INT_PTR v1, v2;
01022   
01023   BDD_SETUP(f);
01024   BDD_SETUP(g);
01025   if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
01026     {
01027       cmu_mtbdd_terminal_value_aux(bddm, f, &u1, &u2);
01028       cmu_mtbdd_terminal_value_aux(bddm, g, &v1, &v2);
01029       as_INT_PTRs(as_double(u1, u2)+as_double(v1, v2), &u1, &u2);
01030       return (bdd_find_terminal(bddm, u1, u2));
01031     }
01032   if (BDD_OUT_OF_ORDER(f, g))
01033     BDD_SWAP(f, g);
01034   if (bdd_lookup_in_cache2(bddm, OP_ADD, f, g, &result))
01035     return (result);
01036   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
01037   BDD_COFACTOR(top_indexindex, f, f1, f2);
01038   BDD_COFACTOR(top_indexindex, g, g1, g2);
01039   temp1=mtbdd_add_step(bddm, f1, g1);
01040   temp2=mtbdd_add_step(bddm, f2, g2);
01041   result=bdd_find(bddm, top_indexindex, temp1, temp2);
01042   bdd_insert_in_cache2(bddm, OP_ADD, f, g, result);
01043   return (result);
01044 }

static bdd mtbdd_mult ( cmu_bdd_manager  bddm,
bdd  f,
bdd  g 
) [static]

Definition at line 989 of file testbdd.c.

00994 {
00995   if (bdd_check_arguments(2, f, g))
00996     {
00997       FIREWALL(bddm);
00998       RETURN_BDD(mtbdd_mult_step(bddm, f, g));
00999     }
01000   return ((bdd)0);
01001 }

static bdd mtbdd_mult_step ( cmu_bdd_manager  bddm,
bdd  f,
bdd  g 
) [static]

Definition at line 946 of file testbdd.c.

00951 {
00952   bdd_indexindex_type top_indexindex;
00953   bdd f1, f2;
00954   bdd g1, g2;
00955   bdd temp1, temp2;
00956   bdd result;
00957   INT_PTR u1, u2;
00958   INT_PTR v1, v2;
00959   
00960   BDD_SETUP(f);
00961   BDD_SETUP(g);
00962   if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
00963     {
00964       cmu_mtbdd_terminal_value_aux(bddm, f, &u1, &u2);
00965       cmu_mtbdd_terminal_value_aux(bddm, g, &v1, &v2);
00966       as_INT_PTRs(as_double(u1, u2)*as_double(v1, v2), &u1, &u2);
00967       return (bdd_find_terminal(bddm, u1, u2));
00968     }
00969   if (BDD_OUT_OF_ORDER(f, g))
00970     BDD_SWAP(f, g);
00971   if (bdd_lookup_in_cache2(bddm, OP_MULT, f, g, &result))
00972     return (result);
00973   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00974   BDD_COFACTOR(top_indexindex, f, f1, f2);
00975   BDD_COFACTOR(top_indexindex, g, g1, g2);
00976   temp1=mtbdd_mult_step(bddm, f1, g1);
00977   temp2=mtbdd_mult_step(bddm, f2, g2);
00978   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00979   bdd_insert_in_cache2(bddm, OP_MULT, f, g, result);
00980   return (result);
00981 }

static void print_bdd ( bdd  f  )  [static]

Definition at line 161 of file testbdd.c.

00164 {
00165   cmu_bdd_print_bdd(bddm, f, bdd_naming_fn_none, terminal_id_fn, (pointer)0, stderr);
00166 }

long random (  ) 
static void random_tests ( int  iterations  )  [static]

Definition at line 1239 of file testbdd.c.

01242 {
01243   int i;
01244   tt table1, table2, table3;
01245   bdd f1, f2, f3;
01246   INT_PTR v1, v2;
01247 
01248   printf("Random operation tests...\n");
01249   bddm=cmu_bdd_init();
01250   cmu_bdd_node_limit(bddm, 5000);
01251   mtbdd_transform_closure(bddm, canonical_fn, transform_fn, (pointer)0);
01252   as_INT_PTRs(-1.0, &v1, &v2);
01253   mtcmu_bdd_one_data(bddm, v1, v2);
01254   vars[1]=cmu_bdd_new_var_last(bddm);
01255   vars[0]=cmu_bdd_new_var_first(bddm);
01256   vars[4]=cmu_bdd_new_var_after(bddm, vars[1]);
01257   vars[3]=cmu_bdd_new_var_before(bddm, vars[4]);
01258   vars[2]=cmu_bdd_new_var_after(bddm, vars[1]);
01259   for (i=0; i < 5; ++i)
01260     aux_vars[i]=cmu_bdd_new_var_after(bddm, vars[i]);
01261   for (i=0; i < iterations; ++i)
01262     {
01263       if ((i & 0xf) == 0)
01264         {
01265           putchar('.');
01266           fflush(stdout);
01267         }
01268       if ((i & 0x3ff) == 0x3ff)
01269         {
01270           putchar('\n');
01271           fflush(stdout);
01272           check_leak();
01273         }
01274       table1=random();
01275       table2=random();
01276       table3=random();
01277       f1=encoding_to_bdd(table1);
01278       f2=encoding_to_bdd(table2);
01279       f3=encoding_to_bdd(table3);
01280       test_ite(f1, table1, f2, table2, f3, table3);
01281       test_and(f1, table1, f2, table2);
01282       test_or(f1, table1, f2, table2);
01283       test_xor(f1, table1, f2, table2);
01284       test_id_not(f1, table1);
01285       test_compose(f1, table1, f2, table2);
01286       test_qnt(f1, table1);
01287       test_rel_prod(f1, table1, f2, table2);
01288       test_subst(f1, table1, f2, table2, f3, table3);
01289       test_inter_impl(f1, table1, f2, table2);
01290       test_sat(f1, table1);
01291       test_gen_cof(f1, table1, f2, table2);
01292       test_reduce(f1, table1, f2, table2);
01293       test_apply(f1, table1, f2, table2);
01294       test_size(f1, table1, f2, table2);
01295       test_mtbdd(f1, table1);
01296       test_swap(f1, table1);
01297       if (i < 100)
01298         test_dump(f1, table1);
01299       cmu_bdd_free(bddm, f1);
01300       cmu_bdd_free(bddm, f2);
01301       cmu_bdd_free(bddm, f3);
01302     }
01303   putchar('\n');
01304   cmu_bdd_stats(bddm, stdout);
01305   cmu_bdd_quit(bddm);
01306 }

void srandom (  ) 
static bdd terminal ( double  n  )  [static]

Definition at line 900 of file testbdd.c.

00903 {
00904   INT_PTR v1, v2;
00905 
00906   as_INT_PTRs(n, &v1, &v2);
00907   return (cmu_mtbdd_get_terminal(bddm, v1, v2));
00908 }

static char* terminal_id_fn ( cmu_bdd_manager  bddm,
INT_PTR  v1,
INT_PTR  v2,
pointer  junk 
) [static]

Definition at line 142 of file testbdd.c.

00148 {
00149   static char result[100];
00150 
00151   sprintf(result, "%g", as_double(v1, v2));
00152   return (result);
00153 }

static void test_and ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 300 of file testbdd.c.

00306 {
00307   bdd result;
00308   tt resulttable;
00309   bdd expected;
00310 
00311   result=cmu_bdd_and(bddm, f1, f2);
00312   resulttable=table1 & table2;
00313   expected=encoding_to_bdd(resulttable);
00314   if (result != expected)
00315     error("and", result, expected, f1, f2, (bdd)0);
00316   cmu_bdd_free(bddm, result);
00317   cmu_bdd_free(bddm, expected);
00318 }

static void test_apply ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 785 of file testbdd.c.

00791 {
00792   bdd result;
00793   tt resulttable;
00794   bdd expected;
00795 
00796   result=bdd_apply2(bddm, apply_and, f1, f2, (pointer)0);
00797   resulttable=table1 & table2;
00798   expected=encoding_to_bdd(resulttable);
00799   if (result != expected)
00800     error("apply2", result, expected, f1, f2, (bdd)0);
00801   cmu_bdd_free(bddm, result);
00802   cmu_bdd_free(bddm, expected);
00803 }

static void test_compose ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 409 of file testbdd.c.

00415 {
00416   int var;
00417   bdd result;
00418   tt resulttable;
00419   bdd expected;
00420 
00421   var=((unsigned long)random())%TT_VARS;
00422   result=cmu_bdd_compose(bddm, f1, vars[var], cmu_bdd_one(bddm));
00423   resulttable=cofactor(table1, var, 1);
00424   expected=encoding_to_bdd(resulttable);
00425   if (result != expected)
00426     error("restrict1", result, expected, f1, vars[var], (bdd)0);
00427   cmu_bdd_free(bddm, result);
00428   cmu_bdd_free(bddm, expected);
00429   result=cmu_bdd_compose(bddm, f1, vars[var], cmu_bdd_zero(bddm));
00430   resulttable=cofactor(table1, var, 0);
00431   expected=encoding_to_bdd(resulttable);
00432   if (result != expected)
00433     error("restrict0", result, expected, f1, vars[var], (bdd)0);
00434   cmu_bdd_free(bddm, result);
00435   cmu_bdd_free(bddm, expected);
00436   result=cmu_bdd_compose(bddm, f1, vars[var], f2);
00437   resulttable=(table2 & cofactor(table1, var, 1)) | (~table2 & cofactor(table1, var, 0));
00438   expected=encoding_to_bdd(resulttable);
00439   if (result != expected)
00440     error("compose", result, expected, f1, vars[var], f2, (bdd)0);
00441   cmu_bdd_free(bddm, result);
00442   cmu_bdd_free(bddm, expected);
00443 }

static void test_dump ( bdd  f,
tt  table 
) [static]

Definition at line 1165 of file testbdd.c.

01169 {
01170   FILE *fp;
01171   int i, j;
01172   bdd dump_vars[TT_VARS+1];
01173   bdd temp;
01174   bdd result;
01175   int err;
01176 
01177   if (!(fp=tmpfile()))
01178     {
01179       fprintf(stderr, "could not open temporary file\n");
01180       exit(1);
01181     }
01182   for (i=0; i < TT_VARS; ++i)
01183     dump_vars[i]=vars[i];
01184   dump_vars[i]=0;
01185   for (i=0; i < TT_VARS-1; ++i)
01186     {
01187       j=i+((unsigned long)random())%(TT_VARS-i);
01188       temp=dump_vars[i];
01189       dump_vars[i]=dump_vars[j];
01190       dump_vars[j]=temp;
01191     }
01192   if (!cmu_bdd_dump_bdd(bddm, f, dump_vars, fp))
01193     {
01194       fprintf(stderr, "Error: dump failure:\n");
01195       fprintf(stderr, "Argument:\n");
01196       print_bdd(f);
01197       fclose(fp);
01198       return;
01199     }
01200   rewind(fp);
01201   if (!(result=cmu_bdd_undump_bdd(bddm, dump_vars, fp, &err)) || err)
01202     {
01203       fprintf(stderr, "Error: undump failure: code %d:\n", err);
01204       fprintf(stderr, "Argument:\n");
01205       print_bdd(f);
01206       fclose(fp);
01207       return;
01208     }
01209   fclose(fp);
01210   if (result != f)
01211     error("dump/undump", result, f, f, (bdd)0);
01212   cmu_bdd_free(bddm, result);
01213 }

static void test_gen_cof ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 676 of file testbdd.c.

00682 {
00683   int var1, var2;
00684   bdd result;
00685   bdd temp1, temp2, temp3;
00686   tt resulttable;
00687   bdd expected;
00688 
00689   result=cmu_bdd_cofactor(bddm, f1, f2);
00690   temp1=cmu_bdd_xnor(bddm, result, f1);
00691   temp2=cmu_bdd_not(bddm, f2);
00692   temp3=cmu_bdd_or(bddm, temp1, temp2);
00693   if (temp3 != cmu_bdd_one(bddm))
00694     error("d.c. comparison of generalized cofactor", temp3, cmu_bdd_one(bddm), f1, f2, (bdd)0);
00695   cmu_bdd_free(bddm, result);
00696   cmu_bdd_free(bddm, temp1);
00697   cmu_bdd_free(bddm, temp2);
00698   cmu_bdd_free(bddm, temp3);
00699   var1=((unsigned long)random())%TT_VARS;
00700   do
00701     var2=((unsigned long)random())%TT_VARS;
00702   while (var1 == var2);
00703   temp1=cmu_bdd_not(bddm, vars[var2]);
00704   temp2=cmu_bdd_and(bddm, vars[var1], temp1);
00705   cmu_bdd_free(bddm, temp1);
00706   result=cmu_bdd_cofactor(bddm, f1, temp2);
00707   resulttable=cofactor(cofactor(table1, var1, 1), var2, 0);
00708   expected=encoding_to_bdd(resulttable);
00709   if (result != expected)
00710     error("generalized cofactor", result, expected, f1, temp2, (bdd)0);
00711   cmu_bdd_free(bddm, result);
00712   cmu_bdd_free(bddm, expected);
00713   cmu_bdd_free(bddm, temp2);
00714 }

static void test_id_not ( bdd  f,
tt  table 
) [static]

Definition at line 378 of file testbdd.c.

00382 {
00383   bdd result;
00384   tt resulttable;
00385   bdd expected;
00386 
00387   result=cmu_bdd_not(bddm, f);
00388   resulttable= ~table;
00389   expected=encoding_to_bdd(resulttable);
00390   if (result != expected)
00391     error("not", result, expected, f, (bdd)0);
00392   cmu_bdd_free(bddm, result);
00393   cmu_bdd_free(bddm, expected);
00394   result=cmu_bdd_identity(bddm, f);
00395   resulttable=table;
00396   expected=encoding_to_bdd(resulttable);
00397   if (result != expected)
00398     error("identity", result, expected, f, (bdd)0);
00399   cmu_bdd_free(bddm, result);
00400   cmu_bdd_free(bddm, expected);
00401 }

static void test_inter_impl ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 587 of file testbdd.c.

00593 {
00594   bdd result;
00595   tt resulttable;
00596   bdd expected;
00597   bdd implies_result;
00598 
00599   result=cmu_bdd_intersects(bddm, f1, f2);
00600   resulttable=table1 & table2;
00601   expected=encoding_to_bdd(resulttable);
00602   implies_result=cmu_bdd_implies(bddm, result, expected);
00603   if (implies_result != cmu_bdd_zero(bddm))
00604     {
00605       error("intersection test", result, expected, f1, f2, (bdd)0);
00606       cmu_bdd_free(bddm, implies_result);
00607     }
00608   cmu_bdd_free(bddm, result);
00609   cmu_bdd_free(bddm, expected);
00610 }

static void test_ite ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2,
bdd  f3,
tt  table3 
) [static]

Definition at line 272 of file testbdd.c.

00280 {
00281   bdd result;
00282   tt resulttable;
00283   bdd expected;
00284 
00285   result=cmu_bdd_ite(bddm, f1, f2, f3);
00286   resulttable=(table1 & table2) | (~table1 & table3);
00287   expected=encoding_to_bdd(resulttable);
00288   if (result != expected)
00289     error("ITE", result, expected, f1, f2, f3, (bdd)0);
00290   cmu_bdd_free(bddm, result);
00291   cmu_bdd_free(bddm, expected);
00292 }

static void test_mtbdd ( bdd  f1,
tt  table1 
) [static]

Definition at line 1101 of file testbdd.c.

01105 {
01106   bdd wm;
01107   bdd temp1, temp2;
01108   bdd result;
01109 
01110   wm=walsh_matrix(0);
01111   temp1=transform(wm, f1, vars);
01112   temp2=temp1;
01113   temp1=transform(wm, temp2, aux_vars);
01114   cmu_bdd_free(bddm, wm);
01115   cmu_bdd_free(bddm, temp2);
01116   temp2=terminal(1.0/TT_BITS);
01117   result=mtbdd_mult(bddm, temp1, temp2);
01118   cmu_bdd_free(bddm, temp1);
01119   cmu_bdd_free(bddm, temp2);
01120   if (f1 != result)
01121     error("Walsh transformation and inverse", result, f1, (bdd)0);
01122   cmu_bdd_free(bddm, result);
01123 }

static void test_or ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 326 of file testbdd.c.

00332 {
00333   bdd result;
00334   tt resulttable;
00335   bdd expected;
00336 
00337   result=cmu_bdd_or(bddm, f1, f2);
00338   resulttable=table1 | table2;
00339   expected=encoding_to_bdd(resulttable);
00340   if (result != expected)
00341     error("or", result, expected, f1, f2, (bdd)0);
00342   cmu_bdd_free(bddm, result);
00343   cmu_bdd_free(bddm, expected);
00344 }

static void test_qnt ( bdd  f,
tt  table 
) [static]

Definition at line 451 of file testbdd.c.

00455 {
00456   int var1, var2;
00457   bdd assoc[3];
00458   bdd temp;
00459   bdd result;
00460   tt resulttable;
00461   bdd expected;
00462 
00463   var1=((unsigned long)random())%TT_VARS;
00464   do
00465     var2=((unsigned long)random())%TT_VARS;
00466   while (var1 == var2);
00467   assoc[0]=vars[var1];
00468   assoc[1]=vars[var2];
00469   assoc[2]=0;
00470   cmu_bdd_temp_assoc(bddm, assoc, 0);
00471   cmu_bdd_assoc(bddm, -1);
00472   if (random()%2)
00473     result=cmu_bdd_exists(bddm, f);
00474   else
00475     {
00476       temp=cmu_bdd_not(bddm, f);
00477       result=cmu_bdd_forall(bddm, temp);
00478       cmu_bdd_free(bddm, temp);
00479       temp=result;
00480       result=cmu_bdd_not(bddm, temp);
00481       cmu_bdd_free(bddm, temp);
00482     }
00483   resulttable=cofactor(table, var1, 1) | cofactor(table, var1, 0);
00484   resulttable=cofactor(resulttable, var2, 1) | cofactor(resulttable, var2, 0);
00485   expected=encoding_to_bdd(resulttable);
00486   if (result != expected)
00487     error("quantification", result, expected, f, vars[var1], vars[var2], (bdd)0);
00488   cmu_bdd_free(bddm, result);
00489   cmu_bdd_free(bddm, expected);
00490 }

static void test_reduce ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 722 of file testbdd.c.

00728 {
00729   bdd result;
00730   bdd temp1, temp2, temp3;
00731 
00732   result=cmu_bdd_reduce(bddm, f1, f2);
00733   temp1=cmu_bdd_xnor(bddm, result, f1);
00734   temp2=cmu_bdd_not(bddm, f2);
00735   temp3=cmu_bdd_or(bddm, temp1, temp2);
00736   if (temp3 != cmu_bdd_one(bddm))
00737     error("d.c. comparison of reduce", temp3, cmu_bdd_one(bddm), f1, f2, (bdd)0);
00738   cmu_bdd_free(bddm, result);
00739   cmu_bdd_free(bddm, temp1);
00740   cmu_bdd_free(bddm, temp2);
00741   cmu_bdd_free(bddm, temp3);
00742 }

static void test_rel_prod ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 498 of file testbdd.c.

00504 {
00505   int var1, var2;
00506   bdd assoc[3];
00507   bdd result;
00508   tt resulttable;
00509   bdd expected;
00510 
00511   var1=((unsigned long)random())%TT_VARS;
00512   do
00513     var2=((unsigned long)random())%TT_VARS;
00514   while (var1 == var2);
00515   assoc[0]=vars[var1];
00516   assoc[1]=vars[var2];
00517   assoc[2]=0;
00518   cmu_bdd_temp_assoc(bddm, assoc, 0);
00519   cmu_bdd_assoc(bddm, -1);
00520   result=cmu_bdd_rel_prod(bddm, f1, f2);
00521   table1&=table2;
00522   resulttable=cofactor(table1, var1, 1) | cofactor(table1, var1, 0);
00523   resulttable=cofactor(resulttable, var2, 1) | cofactor(resulttable, var2, 0);
00524   expected=encoding_to_bdd(resulttable);
00525   if (result != expected)
00526     error("relational product", result, expected, f1, f2, vars[var1], vars[var2], (bdd)0);
00527   cmu_bdd_free(bddm, result);
00528   cmu_bdd_free(bddm, expected);
00529 }

static void test_sat ( bdd  f,
tt  table 
) [static]

Definition at line 618 of file testbdd.c.

00622 {
00623   int var1, var2;
00624   bdd assoc[TT_VARS+1];
00625   bdd result;
00626   bdd temp1, temp2, temp3;
00627 
00628   if (f == cmu_bdd_zero(bddm))
00629     return;
00630   result=cmu_bdd_satisfy(bddm, f);
00631   temp1=cmu_bdd_not(bddm, f);
00632   temp2=cmu_bdd_intersects(bddm, temp1, result);
00633   if (temp2 != cmu_bdd_zero(bddm))
00634     error("intersection of satisfy result with negated argument", temp2, cmu_bdd_zero(bddm), f, (bdd)0);
00635   cmu_bdd_free(bddm, temp1);
00636   cmu_bdd_free(bddm, temp2);
00637   var1=((unsigned long)random())%TT_VARS;
00638   do
00639     var2=((unsigned long)random())%TT_VARS;
00640   while (var1 == var2);
00641   assoc[0]=vars[var1];
00642   assoc[1]=vars[var2];
00643   assoc[2]=0;
00644   cmu_bdd_temp_assoc(bddm, assoc, 0);
00645   cmu_bdd_assoc(bddm, -1);
00646   temp1=cmu_bdd_satisfy_support(bddm, result);
00647   temp2=cmu_bdd_not(bddm, result);
00648   temp3=cmu_bdd_intersects(bddm, temp2, temp1);
00649   if (temp3 != cmu_bdd_zero(bddm))
00650     error("intersection of satisfy support result with negated argument", temp3, cmu_bdd_zero(bddm), result, (bdd)0);
00651   cmu_bdd_free(bddm, result);
00652   cmu_bdd_free(bddm, temp1);
00653   cmu_bdd_free(bddm, temp2);
00654   cmu_bdd_free(bddm, temp3);
00655   temp1=cmu_bdd_compose(bddm, f, vars[var1], cmu_bdd_zero(bddm));
00656   temp2=cmu_bdd_compose(bddm, f, vars[var1], cmu_bdd_one(bddm));
00657   if (cmu_bdd_satisfying_fraction(bddm, temp1)+cmu_bdd_satisfying_fraction(bddm, temp2) !=
00658       2.0*cmu_bdd_satisfying_fraction(bddm, f))
00659     {
00660       fprintf(stderr, "\nError: operation satisfying fraction:\n");
00661       fprintf(stderr, "Argument:\n");
00662       print_bdd(f);
00663       fprintf(stderr, "Cofactor on:\n");
00664       print_bdd(vars[var1]);
00665     }
00666   cmu_bdd_free(bddm, temp1);
00667   cmu_bdd_free(bddm, temp2);
00668 }

static void test_size ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 811 of file testbdd.c.

00817 {
00818   int i;
00819   long size;
00820   long profile[2*TT_VARS+1];
00821   bdd fs[3];
00822 
00823   size=cmu_bdd_size(bddm, f1, 1);
00824   cmu_bdd_profile(bddm, f1, profile, 1);
00825   for (i=0; i < 2*TT_VARS+1; ++i)
00826     size-=profile[i];
00827   if (size)
00828     {
00829       fprintf(stderr, "\nError: size count vs. profile sum:\n");
00830       fprintf(stderr, "Argument:\n");
00831       print_bdd(f1);
00832     }
00833   size=cmu_bdd_size(bddm, f1, 0);
00834   cmu_bdd_profile(bddm, f1, profile, 0);
00835   for (i=0; i < 2*TT_VARS+1; ++i)
00836     size-=profile[i];
00837   if (size)
00838     {
00839       fprintf(stderr, "\nError: no negout size count vs. profile sum:\n");
00840       fprintf(stderr, "Argument:\n");
00841       print_bdd(f1);
00842     }
00843   fs[0]=f1;
00844   fs[1]=f2;
00845   fs[2]=0;
00846   size=cmu_bdd_size_multiple(bddm, fs, 1);
00847   cmu_bdd_profile_multiple(bddm, fs, profile, 1);
00848   for (i=0; i < 2*TT_VARS+1; ++i)
00849     size-=profile[i];
00850   if (size)
00851     {
00852       fprintf(stderr, "\nError: multiple size count vs. multiple profile sum:\n");
00853       fprintf(stderr, "Argument 1:\n");
00854       print_bdd(f1);
00855       fprintf(stderr, "Argument 2:\n");
00856       print_bdd(f2);
00857     }
00858 }

static void test_subst ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2,
bdd  f3,
tt  table3 
) [static]

Definition at line 537 of file testbdd.c.

00545 {
00546   int var1, var2;
00547   bdd assoc[6];
00548   bdd result;
00549   tt resulttable;
00550   tt temp1, temp2, temp3, temp4;
00551   bdd expected;
00552 
00553   var1=((unsigned long)random())%TT_VARS;
00554   do
00555     var2=((unsigned long)random())%TT_VARS;
00556   while (var1 == var2);
00557   assoc[0]=vars[var1];
00558   assoc[1]=f2;
00559   assoc[2]=vars[var2];
00560   assoc[3]=f3;
00561   assoc[4]=0;
00562   assoc[5]=0;
00563   cmu_bdd_temp_assoc(bddm, assoc, 1);
00564   cmu_bdd_assoc(bddm, -1);
00565   result=cmu_bdd_substitute(bddm, f1);
00566   temp1=cofactor(cofactor(table1, var1, 1), var2, 1);
00567   temp2=cofactor(cofactor(table1, var1, 1), var2, 0);
00568   temp3=cofactor(cofactor(table1, var1, 0), var2, 1);
00569   temp4=cofactor(cofactor(table1, var1, 0), var2, 0);
00570   resulttable=table2 & table3 & temp1;
00571   resulttable|=table2 & ~table3 & temp2;
00572   resulttable|=~table2 & table3 & temp3;
00573   resulttable|=~table2 & ~table3 & temp4;
00574   expected=encoding_to_bdd(resulttable);
00575   if (result != expected)
00576     error("substitute", result, expected, f1, vars[var1], f2, vars[var2], f3, (bdd)0);
00577   cmu_bdd_free(bddm, result);
00578   cmu_bdd_free(bddm, expected);
00579 }

static void test_swap ( bdd  f,
tt  table 
) [static]

Definition at line 1131 of file testbdd.c.

01135 {
01136   int var1, var2;
01137   bdd result;
01138   tt resulttable;
01139   tt temp1, temp2, temp3, temp4;
01140   bdd expected;
01141 
01142   var1=((unsigned long)random())%TT_VARS;
01143   var2=((unsigned long)random())%TT_VARS;
01144   result=cmu_bdd_swap_vars(bddm, f, vars[var1], vars[var2]);
01145   temp1=cofactor(cofactor(table, var1, 1), var2, 1);
01146   temp2=cofactor(cofactor(table, var1, 1), var2, 0);
01147   temp3=cofactor(cofactor(table, var1, 0), var2, 1);
01148   temp4=cofactor(cofactor(table, var1, 0), var2, 0);
01149   resulttable=cofactor_masks[var2] & cofactor_masks[var1] & temp1;
01150   resulttable|=cofactor_masks[var2] & ~cofactor_masks[var1] & temp2;
01151   resulttable|=~cofactor_masks[var2] & cofactor_masks[var1] & temp3;
01152   resulttable|=~cofactor_masks[var2] & ~cofactor_masks[var1] & temp4;
01153   expected=encoding_to_bdd(resulttable);
01154   if (result != expected)
01155     error("swap variables", result, expected, f, vars[var1], vars[var2], (bdd)0);
01156   cmu_bdd_free(bddm, result);
01157   cmu_bdd_free(bddm, expected);
01158 }

static void test_xor ( bdd  f1,
tt  table1,
bdd  f2,
tt  table2 
) [static]

Definition at line 352 of file testbdd.c.

00358 {
00359   bdd result;
00360   tt resulttable;
00361   bdd expected;
00362 
00363   result=cmu_bdd_xor(bddm, f1, f2);
00364   resulttable=table1 ^ table2;
00365   expected=encoding_to_bdd(resulttable);
00366   if (result != expected)
00367     error("xor", result, expected, f1, f2, (bdd)0);
00368   cmu_bdd_free(bddm, result);
00369   cmu_bdd_free(bddm, expected);
00370 }

static bdd transform ( bdd  f,
bdd  g,
bdd *  elim_vars 
) [static]

Definition at line 1072 of file testbdd.c.

01077 {
01078   int i;
01079   bdd temp1, temp2;
01080   bdd result;
01081 
01082   result=mtbdd_mult(bddm, f, g);
01083   for (i=0; i < TT_VARS; ++i)
01084     {
01085       temp1=cmu_bdd_compose(bddm, result, elim_vars[i], cmu_bdd_one(bddm));
01086       temp2=cmu_bdd_compose(bddm, result, elim_vars[i], cmu_bdd_zero(bddm));
01087       cmu_bdd_free(bddm, result);
01088       result=mtbdd_add(bddm, temp1, temp2);
01089       cmu_bdd_free(bddm, temp1);
01090       cmu_bdd_free(bddm, temp2);
01091     }
01092   return (result);
01093 }

static void transform_fn ( cmu_bdd_manager  bddm,
INT_PTR  v1,
INT_PTR  v2,
INT_PTR *  r1,
INT_PTR *  r2,
pointer  env 
) [static]

Definition at line 882 of file testbdd.c.

00890 {
00891   as_INT_PTRs(-as_double(v1, v2), r1, r2);
00892 }

int unlink (  ) 
static bdd walsh_matrix ( int  n  )  [static]

Definition at line 916 of file testbdd.c.

00919 {
00920   bdd temp1, temp2, temp3;
00921   bdd result;
00922 
00923   if (n == TT_VARS)
00924     return (terminal(1.0));
00925   temp1=walsh_matrix(n+1);
00926   temp2=mtbdd_transform(bddm, temp1);
00927   temp3=temp2;
00928   temp2=mtcmu_bdd_ite(bddm, aux_vars[n], temp3, temp1);
00929   cmu_bdd_free(bddm, temp3);
00930   result=mtcmu_bdd_ite(bddm, vars[n], temp2, temp1);
00931   cmu_bdd_free(bddm, temp1);
00932   cmu_bdd_free(bddm, temp2);
00933   return (result);
00934 }

Variable Documentation

bdd aux_vars[VARS] [static]

Definition at line 59 of file testbdd.c.

cmu_bdd_manager bddm [static]

Definition at line 55 of file testbdd.c.

tt cofactor_masks[] [static]
Initial value:
{
  0xffff0000,
  0xff00ff00,
  0xf0f0f0f0,
  0xcccccccc,
  0xaaaaaaaa,
}

Definition at line 62 of file testbdd.c.

union hack_u hack [static]
bdd vars[VARS] [static]

Definition at line 58 of file testbdd.c.

Generated on Tue Jan 12 13:57:16 2010 for glu-2.2 by  doxygen 1.6.1