00001 #include "mdd.h"
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018 mdd_t *
00019 mdd_func2c(
00020 mdd_manager *mgr,
00021 int mvar1,
00022 int mvar2,
00023 int constant,
00024 boolean (*func3)(int, int, int))
00025 {
00026 mvar_type x, y;
00027 array_t *child_list_x, *child_list_y;
00028 int i, j;
00029 mdd_t *tx, *ty;
00030 array_t *mvar_list = mdd_ret_mvar_list(mgr);
00031 mdd_t *one, *zero;
00032
00033 x = array_fetch(mvar_type, mvar_list, mvar1);
00034 y = array_fetch(mvar_type, mvar_list, mvar2);
00035
00036 if (x.status == MDD_BUNDLED) {
00037 (void) fprintf(stderr,
00038 "\nWarning: mdd_func2c, bundled variable %s is used\n", x.name);
00039 fail("");
00040 }
00041
00042 if (y.status == MDD_BUNDLED) {
00043 (void) fprintf(stderr,
00044 "\nWarning: mdd_func2c, bundled variable %s is used\n", y.name);
00045 fail("");
00046 }
00047
00048
00049 one = mdd_one(mgr);
00050 zero = mdd_zero(mgr);
00051
00052 child_list_x = array_alloc(mdd_t *, 0);
00053 for (i=0; i<x.values; i++) {
00054 child_list_y = array_alloc(mdd_t *, 0);
00055 for (j=0; j<y.values; j++) {
00056 if (func3(i,j,constant))
00057 array_insert_last(mdd_t *, child_list_y, one);
00058 else
00059 array_insert_last(mdd_t *, child_list_y, zero);
00060 }
00061 ty = mdd_case(mgr, mvar2, child_list_y);
00062 array_insert_last(mdd_t *, child_list_x, ty);
00063 array_free(child_list_y);
00064 }
00065 tx = mdd_case(mgr, mvar1, child_list_x);
00066 array_free(child_list_x);
00067
00068 mdd_free(zero);
00069 mdd_free(one);
00070
00071 return tx;
00072 }
00073
00074
00075
00076
00077
00078