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