[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [calBddSupport.c] |
---|
| 4 | |
---|
| 5 | PackageName [cal] |
---|
| 6 | |
---|
| 7 | Synopsis [Routines related to the support of a BDD.] |
---|
| 8 | |
---|
| 9 | |
---|
| 10 | Description [ ] |
---|
| 11 | |
---|
| 12 | SeeAlso [optional] |
---|
| 13 | |
---|
| 14 | Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 15 | Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 16 | Originally written by David Long. |
---|
| 17 | ] |
---|
| 18 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
| 19 | All rights reserved. |
---|
| 20 | |
---|
| 21 | Permission is hereby granted, without written agreement and without license |
---|
| 22 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
| 23 | documentation for any purpose, provided that the above copyright notice and |
---|
| 24 | the following two paragraphs appear in all copies of this software. |
---|
| 25 | |
---|
| 26 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
| 27 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
| 28 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
| 29 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
| 30 | |
---|
| 31 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
| 32 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
| 33 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
| 34 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
| 35 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
| 36 | |
---|
| 37 | Revision [$Id: calBddSupport.c,v 1.1.1.3 1998/05/04 00:58:54 hsv Exp $] |
---|
| 38 | |
---|
| 39 | ******************************************************************************/ |
---|
| 40 | #include "calInt.h" |
---|
| 41 | |
---|
| 42 | /*---------------------------------------------------------------------------*/ |
---|
| 43 | /* Constant declarations */ |
---|
| 44 | /*---------------------------------------------------------------------------*/ |
---|
| 45 | |
---|
| 46 | /*---------------------------------------------------------------------------*/ |
---|
| 47 | /* Type declarations */ |
---|
| 48 | /*---------------------------------------------------------------------------*/ |
---|
| 49 | |
---|
| 50 | /*---------------------------------------------------------------------------*/ |
---|
| 51 | /* Stucture declarations */ |
---|
| 52 | /*---------------------------------------------------------------------------*/ |
---|
| 53 | |
---|
| 54 | /*---------------------------------------------------------------------------*/ |
---|
| 55 | /* Variable declarations */ |
---|
| 56 | /*---------------------------------------------------------------------------*/ |
---|
| 57 | |
---|
| 58 | /*---------------------------------------------------------------------------*/ |
---|
| 59 | /* Macro declarations */ |
---|
| 60 | /*---------------------------------------------------------------------------*/ |
---|
| 61 | |
---|
| 62 | /**AutomaticStart*************************************************************/ |
---|
| 63 | |
---|
| 64 | /*---------------------------------------------------------------------------*/ |
---|
| 65 | /* Static function prototypes */ |
---|
| 66 | /*---------------------------------------------------------------------------*/ |
---|
| 67 | |
---|
| 68 | static Cal_Bdd_t * CalBddSupportStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * support); |
---|
| 69 | static void CalBddUnmarkNodes(Cal_BddManager_t * bddManager, Cal_Bdd_t f); |
---|
| 70 | static int CalBddDependsOnStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_BddIndex_t varIndex, int mark); |
---|
| 71 | |
---|
| 72 | /**AutomaticEnd***************************************************************/ |
---|
| 73 | |
---|
| 74 | /*---------------------------------------------------------------------------*/ |
---|
| 75 | /* Definition of exported functions */ |
---|
| 76 | /*---------------------------------------------------------------------------*/ |
---|
| 77 | |
---|
| 78 | /**Function******************************************************************** |
---|
| 79 | |
---|
| 80 | Name [Cal_BddSupport] |
---|
| 81 | |
---|
| 82 | Synopsis [returns the support of f as a null-terminated array of variables] |
---|
| 83 | |
---|
| 84 | Description [optional] |
---|
| 85 | |
---|
| 86 | SideEffects [None] |
---|
| 87 | |
---|
| 88 | SeeAlso [optional] |
---|
| 89 | |
---|
| 90 | ******************************************************************************/ |
---|
| 91 | void |
---|
| 92 | Cal_BddSupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd, |
---|
| 93 | Cal_Bdd *support) |
---|
| 94 | { |
---|
| 95 | if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ |
---|
| 96 | Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); |
---|
| 97 | Cal_Bdd_t *internalSupport = Cal_MemAlloc(Cal_Bdd_t, bddManager->numVars+1); |
---|
| 98 | Cal_Bdd_t *end; |
---|
| 99 | int i = 0; |
---|
| 100 | end = CalBddSupportStep(bddManager, f, internalSupport); |
---|
| 101 | *end = CalBddNull(bddManager); |
---|
| 102 | CalBddUnmarkNodes(bddManager, f); |
---|
| 103 | while (CalBddIsBddNull(bddManager, internalSupport[i]) == 0){ |
---|
| 104 | *support = CalBddGetExternalBdd(bddManager, internalSupport[i]); |
---|
| 105 | support++; |
---|
| 106 | i++; |
---|
| 107 | } |
---|
| 108 | Cal_MemFree(internalSupport); |
---|
| 109 | } |
---|
| 110 | *support = (Cal_Bdd) 0; |
---|
| 111 | } |
---|
| 112 | |
---|
| 113 | /**Function******************************************************************** |
---|
| 114 | |
---|
| 115 | Name [Cal_BddDependsOn] |
---|
| 116 | |
---|
| 117 | Synopsis [Returns 1 if f depends on var and returns 0 otherwise.] |
---|
| 118 | |
---|
| 119 | Description [Returns 1 if f depends on var and returns 0 otherwise.] |
---|
| 120 | |
---|
| 121 | SideEffects [None] |
---|
| 122 | |
---|
| 123 | ******************************************************************************/ |
---|
| 124 | int |
---|
| 125 | Cal_BddDependsOn(Cal_BddManager bddManager, Cal_Bdd fUserBdd, |
---|
| 126 | Cal_Bdd varUserBdd) |
---|
| 127 | { |
---|
| 128 | Cal_BddIndex_t bddIndex; |
---|
| 129 | Cal_Bdd_t f, var; |
---|
| 130 | |
---|
| 131 | if(CalBddPreProcessing(bddManager, 2, fUserBdd, varUserBdd)){ |
---|
| 132 | f = CalBddGetInternalBdd(bddManager, fUserBdd); |
---|
| 133 | var = CalBddGetInternalBdd(bddManager, varUserBdd); |
---|
| 134 | if(CalBddIsBddConst(var)){ |
---|
| 135 | return 1; |
---|
| 136 | } |
---|
| 137 | bddIndex = CalBddGetBddIndex(bddManager, var); |
---|
| 138 | CalBddDependsOnStep(bddManager, f, bddIndex, 1); |
---|
| 139 | return CalBddDependsOnStep(bddManager, f, bddIndex, 0); |
---|
| 140 | } |
---|
| 141 | return (0); |
---|
| 142 | } |
---|
| 143 | |
---|
| 144 | |
---|
| 145 | /*---------------------------------------------------------------------------*/ |
---|
| 146 | /* Definition of internal functions */ |
---|
| 147 | /*---------------------------------------------------------------------------*/ |
---|
| 148 | |
---|
| 149 | /*---------------------------------------------------------------------------*/ |
---|
| 150 | /* Definition of static functions */ |
---|
| 151 | /*---------------------------------------------------------------------------*/ |
---|
| 152 | |
---|
| 153 | /**Function******************************************************************** |
---|
| 154 | |
---|
| 155 | Name [CalBddSupportStep] |
---|
| 156 | |
---|
| 157 | Synopsis [returns the support of f as a null-terminated array of variables] |
---|
| 158 | |
---|
| 159 | Description [optional] |
---|
| 160 | |
---|
| 161 | SideEffects [required] |
---|
| 162 | |
---|
| 163 | SeeAlso [optional] |
---|
| 164 | |
---|
| 165 | ******************************************************************************/ |
---|
| 166 | static Cal_Bdd_t * |
---|
| 167 | CalBddSupportStep( |
---|
| 168 | Cal_BddManager_t * bddManager, |
---|
| 169 | Cal_Bdd_t f, |
---|
| 170 | Cal_Bdd_t * support) |
---|
| 171 | { |
---|
| 172 | Cal_Bdd_t tempBdd; |
---|
| 173 | |
---|
| 174 | if(CalBddIsMarked(f) || CalBddIsBddConst(f)){ |
---|
| 175 | return support; |
---|
| 176 | } |
---|
| 177 | tempBdd = bddManager->varBdds[CalBddGetBddId(f)]; |
---|
| 178 | if(!CalBddIsMarked(tempBdd)){ |
---|
| 179 | CalBddMark(tempBdd); |
---|
| 180 | *support = tempBdd; |
---|
| 181 | ++support; |
---|
| 182 | } |
---|
| 183 | CalBddMark(f); |
---|
| 184 | CalBddGetThenBdd(f, tempBdd); |
---|
| 185 | support = CalBddSupportStep(bddManager, tempBdd, support); |
---|
| 186 | CalBddGetElseBdd(f, tempBdd); |
---|
| 187 | return CalBddSupportStep(bddManager, tempBdd, support); |
---|
| 188 | } |
---|
| 189 | |
---|
| 190 | |
---|
| 191 | /**Function******************************************************************** |
---|
| 192 | |
---|
| 193 | Name [CalBddUnmarkNodes] |
---|
| 194 | |
---|
| 195 | Synopsis [recursively unmarks the nodes] |
---|
| 196 | |
---|
| 197 | Description [optional] |
---|
| 198 | |
---|
| 199 | SideEffects [required] |
---|
| 200 | |
---|
| 201 | SeeAlso [optional] |
---|
| 202 | |
---|
| 203 | ******************************************************************************/ |
---|
| 204 | static void |
---|
| 205 | CalBddUnmarkNodes( |
---|
| 206 | Cal_BddManager_t * bddManager, |
---|
| 207 | Cal_Bdd_t f) |
---|
| 208 | { |
---|
| 209 | Cal_Bdd_t tempBdd; |
---|
| 210 | |
---|
| 211 | if(!CalBddIsMarked(f) || CalBddIsBddConst(f)){ |
---|
| 212 | return; |
---|
| 213 | } |
---|
| 214 | CalBddUnmark(f); |
---|
| 215 | tempBdd = bddManager->varBdds[CalBddGetBddId(f)]; |
---|
| 216 | CalBddUnmark(tempBdd); |
---|
| 217 | CalBddGetThenBdd(f, tempBdd); |
---|
| 218 | CalBddUnmarkNodes(bddManager, tempBdd); |
---|
| 219 | CalBddGetElseBdd(f, tempBdd); |
---|
| 220 | CalBddUnmarkNodes(bddManager, tempBdd); |
---|
| 221 | } |
---|
| 222 | |
---|
| 223 | |
---|
| 224 | /**Function******************************************************************** |
---|
| 225 | |
---|
| 226 | |
---|
| 227 | Synopsis [required] |
---|
| 228 | |
---|
| 229 | Description [optional] |
---|
| 230 | |
---|
| 231 | SideEffects [required] |
---|
| 232 | |
---|
| 233 | SeeAlso [optional] |
---|
| 234 | |
---|
| 235 | ******************************************************************************/ |
---|
| 236 | static int |
---|
| 237 | CalBddDependsOnStep( |
---|
| 238 | Cal_BddManager_t * bddManager, |
---|
| 239 | Cal_Bdd_t f, |
---|
| 240 | Cal_BddIndex_t varIndex, |
---|
| 241 | int mark) |
---|
| 242 | { |
---|
| 243 | Cal_BddIndex_t fIndex; |
---|
| 244 | Cal_Bdd_t tempBdd; |
---|
| 245 | |
---|
| 246 | fIndex=CalBddGetBddIndex(bddManager, f); |
---|
| 247 | if(fIndex > varIndex){ |
---|
| 248 | return 0; |
---|
| 249 | } |
---|
| 250 | if(fIndex == varIndex){ |
---|
| 251 | return 1; |
---|
| 252 | } |
---|
| 253 | if((mark && CalBddIsMarked(f)) || (!mark && !CalBddIsMarked(f))){ |
---|
| 254 | return (0); |
---|
| 255 | } |
---|
| 256 | if(mark){ |
---|
| 257 | CalBddMark(f); |
---|
| 258 | } |
---|
| 259 | else{ |
---|
| 260 | CalBddUnmark(f); |
---|
| 261 | } |
---|
| 262 | CalBddGetThenBdd(f, tempBdd); |
---|
| 263 | if(CalBddDependsOnStep(bddManager, tempBdd, varIndex, mark)){ |
---|
| 264 | return 1; |
---|
| 265 | } |
---|
| 266 | CalBddGetElseBdd(f, tempBdd); |
---|
| 267 | return CalBddDependsOnStep(bddManager, tempBdd, varIndex, mark); |
---|
| 268 | } |
---|
| 269 | |
---|
| 270 | |
---|
| 271 | |
---|
| 272 | |
---|
| 273 | |
---|
| 274 | |
---|
| 275 | |
---|
| 276 | |
---|
| 277 | |
---|
| 278 | |
---|
| 279 | |
---|