| 1 | #include "mdd.h" | 
|---|
| 2 |  | 
|---|
| 3 | /* | 
|---|
| 4 |  * MDD Package | 
|---|
| 5 |  * | 
|---|
| 6 |  * $Id: mdd_andsmoot.c,v 1.13 2009/01/07 17:14:47 fabio Exp $ | 
|---|
| 7 |  *  | 
|---|
| 8 |  * Author: Timothy Kam | 
|---|
| 9 |  * | 
|---|
| 10 |  * Copyright 1992 by the Regents of the University of California. | 
|---|
| 11 |  * | 
|---|
| 12 |  * All rights reserved.  Permission to use, copy, modify and distribute | 
|---|
| 13 |  * this software is hereby granted, provided that the above copyright | 
|---|
| 14 |  * notice and this permission notice appear in all copies.  This software | 
|---|
| 15 |  * is made available as is, with no warranties. | 
|---|
| 16 |  */ | 
|---|
| 17 |  | 
|---|
| 18 | mdd_t * | 
|---|
| 19 | mdd_and_smooth( | 
|---|
| 20 |   mdd_manager *mgr, | 
|---|
| 21 |   mdd_t *f, | 
|---|
| 22 |   mdd_t *g, | 
|---|
| 23 |   array_t *mvars) | 
|---|
| 24 | { | 
|---|
| 25 |     int i, j, mv_no; | 
|---|
| 26 |     mvar_type mv; | 
|---|
| 27 |     mdd_t *top; | 
|---|
| 28 |     bdd_t *temp; | 
|---|
| 29 |  | 
|---|
| 30 |     array_t *bdd_vars = array_alloc(bdd_t *, 0); | 
|---|
| 31 |     array_t *mvar_list = mdd_ret_mvar_list(mgr); | 
|---|
| 32 |  | 
|---|
| 33 |  | 
|---|
| 34 |     if ( mvars == NIL( array_t ) || array_n(mvars) == 0) { | 
|---|
| 35 |         printf("\nWARNING: Empty Array of Smoothing Variables\n"); | 
|---|
| 36 |         array_free(bdd_vars); | 
|---|
| 37 |         return ( bdd_and(f, g, 1, 1) ) ; | 
|---|
| 38 |     } | 
|---|
| 39 |  | 
|---|
| 40 |     for (i=0; i<array_n(mvars); i++) { | 
|---|
| 41 |         mv_no = array_fetch(int, mvars, i); | 
|---|
| 42 |         mv = array_fetch(mvar_type, mvar_list, mv_no); | 
|---|
| 43 |         if (mv.status == MDD_BUNDLED) { | 
|---|
| 44 |             (void) fprintf(stderr,  | 
|---|
| 45 |                 "\nmdd_andsmooth: bundled variable %s used\n",mv.name); | 
|---|
| 46 |             fail(""); | 
|---|
| 47 |         } | 
|---|
| 48 |  | 
|---|
| 49 |         for (j = 0; j < mv.encode_length; j++) { | 
|---|
| 50 |             temp = bdd_get_variable(mgr, mdd_ret_bvar_id(&mv,j) ); | 
|---|
| 51 |             array_insert_last(bdd_t *, bdd_vars, temp); | 
|---|
| 52 |         } | 
|---|
| 53 |     } | 
|---|
| 54 |  | 
|---|
| 55 |     assert( array_n(bdd_vars) != 0 ); | 
|---|
| 56 |     top = bdd_and_smooth(f, g, bdd_vars); | 
|---|
| 57 |  | 
|---|
| 58 |     for (i = 0; i < array_n(bdd_vars); i++) { | 
|---|
| 59 |         temp = array_fetch(bdd_t *, bdd_vars, i); | 
|---|
| 60 |         bdd_free(temp); | 
|---|
| 61 |     } | 
|---|
| 62 |     array_free(bdd_vars); | 
|---|
| 63 |  | 
|---|
| 64 |     return top; | 
|---|
| 65 | } | 
|---|
| 66 |  | 
|---|
| 67 |  | 
|---|
| 68 | mdd_t * | 
|---|
| 69 | mdd_and_smooth_with_limit( | 
|---|
| 70 |   mdd_manager *mgr, | 
|---|
| 71 |   mdd_t *f, | 
|---|
| 72 |   mdd_t *g, | 
|---|
| 73 |   array_t *mvars, | 
|---|
| 74 |   unsigned int limit) | 
|---|
| 75 | { | 
|---|
| 76 |     int i, j, mv_no; | 
|---|
| 77 |     mvar_type mv; | 
|---|
| 78 |     mdd_t *top; | 
|---|
| 79 |     bdd_t *temp; | 
|---|
| 80 |  | 
|---|
| 81 |     array_t *bdd_vars = array_alloc(bdd_t *, 0); | 
|---|
| 82 |     array_t *mvar_list = mdd_ret_mvar_list(mgr); | 
|---|
| 83 |  | 
|---|
| 84 |  | 
|---|
| 85 |     if ( mvars == NIL( array_t ) ) { | 
|---|
| 86 |         printf("\nWARNING: Empty Array of Smoothing Variables\n"); | 
|---|
| 87 |         array_free(bdd_vars); | 
|---|
| 88 |         return ( bdd_and_with_limit(f, g, 1, 1, limit) ) ; | 
|---|
| 89 |     } | 
|---|
| 90 |     else if ( array_n(mvars) == 0)  { | 
|---|
| 91 |         printf("\nWARNING: Empty Array of Smoothing Variables\n"); | 
|---|
| 92 |         array_free(bdd_vars); | 
|---|
| 93 |         return ( bdd_and_with_limit(f, g, 1, 1, limit) ) ; | 
|---|
| 94 |     } | 
|---|
| 95 |  | 
|---|
| 96 |     for (i=0; i<array_n(mvars); i++) { | 
|---|
| 97 |         mv_no = array_fetch(int, mvars, i); | 
|---|
| 98 |         mv = array_fetch(mvar_type, mvar_list, mv_no); | 
|---|
| 99 |         if (mv.status == MDD_BUNDLED) { | 
|---|
| 100 |             (void) fprintf(stderr,  | 
|---|
| 101 |                 "\nmdd_andsmooth: bundled variable %s used\n",mv.name); | 
|---|
| 102 |             fail(""); | 
|---|
| 103 |         } | 
|---|
| 104 |  | 
|---|
| 105 |         for (j = 0; j < mv.encode_length; j++) { | 
|---|
| 106 |             temp = bdd_get_variable(mgr, mdd_ret_bvar_id(&mv,j) ); | 
|---|
| 107 |             array_insert_last(bdd_t *, bdd_vars, temp); | 
|---|
| 108 |         } | 
|---|
| 109 |     } | 
|---|
| 110 |  | 
|---|
| 111 |     assert( array_n(bdd_vars) != 0 ); | 
|---|
| 112 |     top = bdd_and_smooth_with_limit(f, g, bdd_vars, limit); | 
|---|
| 113 |  | 
|---|
| 114 |     for (i = 0; i < array_n(bdd_vars); i++) { | 
|---|
| 115 |         temp = array_fetch(bdd_t *, bdd_vars, i); | 
|---|
| 116 |         bdd_free(temp); | 
|---|
| 117 |     } | 
|---|
| 118 |     array_free(bdd_vars); | 
|---|
| 119 |  | 
|---|
| 120 |     return top; | 
|---|
| 121 | } | 
|---|
| 122 |  | 
|---|
| 123 | /*---------------------------------------------------------------------------*/ | 
|---|
| 124 | /* Static function prototypes                                                */ | 
|---|
| 125 | /*---------------------------------------------------------------------------*/ | 
|---|
| 126 |  | 
|---|
| 127 |  | 
|---|