1/*======================================================================== 2 Copyright (C) 1996-2001 by Jorn Lind-Nielsen 3 All rights reserved 4 5 Permission is hereby granted, without written agreement and without 6 license or royalty fees, to use, reproduce, prepare derivative 7 works, distribute, and display this software and its documentation 8 for any purpose, provided that (1) the above copyright notice and 9 the following two paragraphs appear in all copies of the source code 10 and (2) redistributions, including without limitation binaries, 11 reproduce these notices in the supporting documentation. Substantial 12 modifications to this software may be copyrighted by their authors 13 and need not follow the licensing terms described here, provided 14 that the new terms are clearly indicated in all files where they apply. 15 16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 21 22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 27 MODIFICATIONS. 28========================================================================*/ 29 30/************************************************************************* 31 $Header$ 32 FILE: pairs.c 33 DESCR: Pair management for BDD package. 34 AUTH: Jorn Lind 35 DATE: february 1997 36*************************************************************************/ 37#include <stdlib.h> 38#include <limits.h> 39#include "kernel.h" 40 41/*======================================================================*/ 42 43static int pairsid; /* Pair identifier */ 44static bddPair* pairs; /* List of all replacement pairs in use */ 45 46 47/************************************************************************* 48*************************************************************************/ 49 50void bdd_pairs_init(void) 51{ 52 pairsid = 0; 53 pairs = NULL; 54} 55 56 57void bdd_pairs_done(void) 58{ 59 bddPair *p = pairs; 60 int n; 61 62 while (p != NULL) 63 { 64 bddPair *next = p->next; 65 for (n=0 ; n<bddvarnum ; n++) 66 bdd_delref( p->result[n] ); 67 free(p->result); 68 free(p); 69 p = next; 70 } 71} 72 73 74static int update_pairsid(void) 75{ 76 pairsid++; 77 78 if (pairsid == (INT_MAX >> 2)) 79 { 80 bddPair *p; 81 pairsid = 0; 82 for (p=pairs ; p!=NULL ; p=p->next) 83 p->id = pairsid++; 84 bdd_operator_reset(); 85 } 86 87 return pairsid; 88} 89 90 91void bdd_register_pair(bddPair *p) 92{ 93 p->next = pairs; 94 pairs = p; 95} 96 97 98void bdd_pairs_vardown(int level) 99{ 100 bddPair *p; 101 102 for (p=pairs ; p!=NULL ; p=p->next) 103 { 104 int tmp; 105 106 tmp = p->result[level]; 107 p->result[level] = p->result[level+1]; 108 p->result[level+1] = tmp; 109 110 if (p->last == level) 111 p->last++; 112 } 113} 114 115 116int bdd_pairs_resize(int oldsize, int newsize) 117{ 118 bddPair *p; 119 int n; 120 121 for (p=pairs ; p!=NULL ; p=p->next) 122 { 123 if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == NULL) 124 return bdd_error(BDD_MEMORY); 125 126 for (n=oldsize ; n<newsize ; n++) 127 p->result[n] = bdd_ithvar(bddlevel2var[n]); 128 } 129 130 return 0; 131} 132 133 134/* 135NAME {* bdd\_newpair *} 136SECTION {* kernel *} 137SHORT {* creates an empty variable pair table *} 138PROTO {* bddPair *bdd_newpair(void) *} 139DESCR {* Variable pairs of the type {\tt bddPair} are used in 140 {\tt bdd\_replace} to define which variables to replace with 141 other variables. This function allocates such an empty table. The 142 table can be freed by a call to {\em bdd\_freepair}. *} 143RETURN {* Returns a new table of pairs. *} 144ALSO {* bdd\_freepair, bdd\_replace, bdd\_setpair, bdd\_setpairs *} 145*/ 146bddPair *bdd_newpair(void) 147{ 148 int n; 149 bddPair *p; 150 151 if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL) 152 { 153 bdd_error(BDD_MEMORY); 154 return NULL; 155 } 156 157 if ((p->result=(BDD*)malloc(sizeof(BDD)*bddvarnum)) == NULL) 158 { 159 free(p); 160 bdd_error(BDD_MEMORY); 161 return NULL; 162 } 163 164 for (n=0 ; n<bddvarnum ; n++) 165 p->result[n] = bdd_ithvar(bddlevel2var[n]); 166 p->id = update_pairsid(); 167 p->last = -1; 168 169 bdd_register_pair(p); 170 return p; 171} 172 173 174/* 175NAME {* bdd\_setpair *} 176EXTRA {* bdd\_setbddpair *} 177SECTION {* kernel *} 178SHORT {* set one variable pair *} 179PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar) 180int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *} 181DESCR {* Adds the pair {\tt (oldvar,newvar)} to the table of pairs 182 {\tt pair}. This results in {\tt oldvar} being substituted 183 with {\tt newvar} in a call to {\tt bdd\_replace}. In the first 184 version {\tt newvar} is an integer representing the variable 185 to be replaced with the old variable. 186 In the second version {\tt oldvar} is a BDD. 187 In this case the variable {\tt oldvar} is substituted with the 188 BDD {\tt newvar}. 189 The possibility to substitute with any BDD as {\tt newvar} is 190 utilized in bdd\_compose, whereas only the topmost variable 191 in the BDD is used in bdd\_replace. *} 192RETURN {* Zero on success, otherwise a negative error code. *} 193ALSO {* bdd\_newpair, bdd\_setpairs, bdd\_resetpair, bdd\_replace, bdd\_compose *} 194*/ 195int bdd_setpair(bddPair *pair, int oldvar, int newvar) 196{ 197 if (pair == NULL) 198 return 0; 199 200 if (oldvar < 0 || oldvar > bddvarnum-1) 201 return bdd_error(BDD_VAR); 202 if (newvar < 0 || newvar > bddvarnum-1) 203 return bdd_error(BDD_VAR); 204 205 bdd_delref( pair->result[bddvar2level[oldvar]] ); 206 pair->result[bddvar2level[oldvar]] = bdd_ithvar(newvar); 207 pair->id = update_pairsid(); 208 209 if (bddvar2level[oldvar] > pair->last) 210 pair->last = bddvar2level[oldvar]; 211 212 return 0; 213} 214 215 216int bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar) 217{ 218 int oldlevel; 219 220 if (pair == NULL) 221 return 0; 222 223 CHECK(newvar); 224 if (oldvar < 0 || oldvar >= bddvarnum) 225 return bdd_error(BDD_VAR); 226 oldlevel = bddvar2level[oldvar]; 227 228 bdd_delref( pair->result[oldlevel] ); 229 pair->result[oldlevel] = bdd_addref(newvar); 230 pair->id = update_pairsid(); 231 232 if (oldlevel > pair->last) 233 pair->last = oldlevel; 234 235 return 0; 236} 237 238 239/* 240NAME {* bdd\_setpairs *} 241EXTRA {* bdd\_setbddpairs *} 242SECTION {* kernel *} 243SHORT {* defines a whole set of pairs *} 244PROTO {* int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size) 245int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size) *} 246DESCR {* As for {\tt bdd\_setpair} but with {\tt oldvar} and {\tt newvar} 247 being arrays of variables (BDDs) of size {\tt size}. *} 248RETURN {* Zero on success, otherwise a negative error code. *} 249ALSO {* bdd\_newpair, bdd\_setpair, bdd\_replace, bdd\_compose *} 250*/ 251int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size) 252{ 253 int n,e; 254 if (pair == NULL) 255 return 0; 256 257 for (n=0 ; n<size ; n++) 258 if ((e=bdd_setpair(pair, oldvar[n], newvar[n])) < 0) 259 return e; 260 261 return 0; 262} 263 264 265int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size) 266{ 267 int n,e; 268 if (pair == NULL) 269 return 0; 270 271 for (n=0 ; n<size ; n++) 272 if ((e=bdd_setbddpair(pair, oldvar[n], newvar[n])) < 0) 273 return e; 274 275 return 0; 276} 277 278 279/* 280NAME {* bdd\_freepair *} 281SECTION {* kernel *} 282SHORT {* frees a table of pairs *} 283PROTO {* void bdd_freepair(bddPair *pair) *} 284DESCR {* Frees the table of pairs {\tt pair} that has been allocated 285 by a call to {\tt bdd\_newpair}. *} 286ALSO {* bdd\_replace, bdd\_newpair, bdd\_setpair, bdd\_resetpair *} 287*/ 288void bdd_freepair(bddPair *p) 289{ 290 int n; 291 292 if (p == NULL) 293 return; 294 295 if (pairs != p) 296 { 297 bddPair *bp = pairs; 298 while (bp != NULL && bp->next != p) 299 bp = bp->next; 300 301 if (bp != NULL) 302 bp->next = p->next; 303 } 304 else 305 pairs = p->next; 306 307 for (n=0 ; n<bddvarnum ; n++) 308 bdd_delref( p->result[n] ); 309 free(p->result); 310 free(p); 311} 312 313 314/* 315NAME {* bdd\_resetpair *} 316SECTION {* kernel *} 317SHORT {* clear all variable pairs *} 318PROTO {* void bdd_resetpair(bddPair *pair) *} 319DESCR {* Resets the table of pairs {\tt pair} by setting all substitutions 320 to their default values (that is no change). *} 321ALSO {* bdd\_newpair, bdd\_setpair, bdd\_freepair *} 322*/ 323void bdd_resetpair(bddPair *p) 324{ 325 int n; 326 327 for (n=0 ; n<bddvarnum ; n++) 328 p->result[n] = bdd_ithvar(n); 329 p->last = 0; 330} 331 332 333/* EOF */ 334 335