source: vis_dev/glu-2.3/src/calBdd/calTerminal.c @ 23

Last change on this file since 23 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 10.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calTerminal.c]
4
5  PackageName [cal]
6
7  Synopsis    [Contains the terminal function for various BDD operations.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and
14               Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: calTerminal.c,v 1.1.1.2 1997/02/12 21:11:30 hsv Exp $]
36
37******************************************************************************/
38
39#include "calInt.h"
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45
46/*---------------------------------------------------------------------------*/
47/* Type declarations                                                         */
48/*---------------------------------------------------------------------------*/
49
50
51/*---------------------------------------------------------------------------*/
52/* Stucture declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55
56/*---------------------------------------------------------------------------*/
57/* Variable declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60
61/*---------------------------------------------------------------------------*/
62/* Macro declarations                                                        */
63/*---------------------------------------------------------------------------*/
64
65
66/**AutomaticStart*************************************************************/
67
68/*---------------------------------------------------------------------------*/
69/* Static function prototypes                                                */
70/*---------------------------------------------------------------------------*/
71
72
73/**AutomaticEnd***************************************************************/
74
75
76/*---------------------------------------------------------------------------*/
77/* Definition of exported functions                                          */
78/*---------------------------------------------------------------------------*/
79
80/*---------------------------------------------------------------------------*/
81/* Definition of internal functions                                          */
82/*---------------------------------------------------------------------------*/
83/**Function********************************************************************
84
85  Synopsis    [required]
86
87  Description [optional]
88
89  SideEffects [required]
90
91  SeeAlso     [optional]
92
93******************************************************************************/
94int
95CalOpAnd(Cal_BddManager_t * bddManager,
96         Cal_Bdd_t  F,
97         Cal_Bdd_t  G,
98         Cal_Bdd_t * resultBddPtr)
99{
100  if(CalBddIsBddConst(F)){
101    if(CalBddIsBddOne(bddManager, F)){
102      *resultBddPtr = G;
103    }
104    else{
105      *resultBddPtr = F;
106    }
107    return 1;
108  }
109  else if(CalBddIsBddConst(G)){
110    if(CalBddIsBddOne(bddManager, G)){
111      *resultBddPtr = F;
112    }
113    else{
114      *resultBddPtr = G;
115    }
116    return 1;
117  }
118  else{
119    CalBddNode_t *bddNodeF, *bddNodeG;
120    bddNodeF = CalBddGetBddNode(F);
121    bddNodeG = CalBddGetBddNode(G);
122    if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
123      if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
124        *resultBddPtr = CalBddZero(bddManager);
125      }
126      else{
127        *resultBddPtr = F;
128      }
129      return 1;
130    }
131    else{
132      return 0;
133    }
134  }
135}
136
137/**Function********************************************************************
138
139  Synopsis    [required]
140
141  Description [optional]
142
143  SideEffects [required]
144
145  SeeAlso     [optional]
146
147******************************************************************************/
148int
149CalOpNand(Cal_BddManager_t * bddManager,
150          Cal_Bdd_t  F,
151          Cal_Bdd_t  G,
152          Cal_Bdd_t * resultBddPtr)
153{
154  if(CalBddIsBddConst(F)){
155    if(CalBddIsBddOne(bddManager, F)){
156      CalBddNot(G, *resultBddPtr);
157    }
158    else{
159      CalBddNot(F, *resultBddPtr);
160    }
161    return 1;
162  }
163  else if(CalBddIsBddConst(G)){
164    if(CalBddIsBddOne(bddManager, G)){
165      CalBddNot(F, *resultBddPtr);
166    }
167    else{
168      CalBddNot(G, *resultBddPtr);
169    }
170    return 1;
171  }
172  else{
173    CalBddNode_t *bddNodeF, *bddNodeG;
174    bddNodeF = CalBddGetBddNode(F);
175    bddNodeG = CalBddGetBddNode(G);
176    if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
177      if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
178        *resultBddPtr = CalBddOne(bddManager);
179      }
180      else{
181        CalBddNot(F, *resultBddPtr);
182      }
183      return 1;
184    }
185    else{
186      return 0;
187    }
188  }
189}
190
191/**Function********************************************************************
192
193  Synopsis    [required]
194
195  Description [optional]
196
197  SideEffects [required]
198
199  SeeAlso     [optional]
200
201******************************************************************************/
202int
203CalOpOr(
204  Cal_BddManager_t * bddManager,
205  Cal_Bdd_t  F,
206  Cal_Bdd_t  G,
207  Cal_Bdd_t * resultBddPtr)
208{
209  if(CalBddIsBddConst(F)){
210    if(CalBddIsBddOne(bddManager, F)){
211      *resultBddPtr = F;
212    }
213    else{
214      *resultBddPtr = G;
215    }
216    return 1;
217  }
218  else if(CalBddIsBddConst(G)){
219    if(CalBddIsBddOne(bddManager, G)){
220      *resultBddPtr = G;
221    }
222    else{
223      *resultBddPtr = F;
224    }
225    return 1;
226  }
227  else{
228    CalBddNode_t *bddNodeF, *bddNodeG;
229    bddNodeF = CalBddGetBddNode(F);
230    bddNodeG = CalBddGetBddNode(G);
231    if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
232      if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
233        *resultBddPtr = CalBddOne(bddManager);
234      }
235      else{
236        *resultBddPtr = F;
237      }
238      return 1;
239    }
240    else{
241      return 0;
242    }
243  }
244}
245
246/**Function********************************************************************
247
248  Synopsis    [required]
249
250  Description [optional]
251
252  SideEffects [required]
253
254  SeeAlso     [optional]
255
256******************************************************************************/
257int
258CalOpXor(
259  Cal_BddManager_t * bddManager,
260  Cal_Bdd_t  F,
261  Cal_Bdd_t  G,
262  Cal_Bdd_t * resultBddPtr)
263{
264  if(CalBddIsBddConst(F)){
265    if(CalBddIsBddOne(bddManager, F)){
266      CalBddNot(G, *resultBddPtr);
267    }
268    else{
269      *resultBddPtr = G;
270    }
271    return 1;
272  }
273  else if(CalBddIsBddConst(G)){
274    if(CalBddIsBddOne(bddManager, G)){
275      CalBddNot(F, *resultBddPtr);
276    }
277    else{
278      *resultBddPtr = F;
279    }
280    return 1;
281  }
282  else{
283    CalBddNode_t *bddNodeF, *bddNodeG;
284    bddNodeF = CalBddGetBddNode(F);
285    bddNodeG = CalBddGetBddNode(G);
286    if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
287      if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
288        *resultBddPtr = CalBddOne(bddManager);
289      }
290      else{
291        *resultBddPtr = CalBddZero(bddManager);
292      }
293      return 1;
294    }
295    else{
296      return 0;
297    }
298  }
299}
300
301/**Function********************************************************************
302
303  Synopsis    [required]
304
305  Description [optional]
306
307  SideEffects [required]
308
309  SeeAlso     [optional]
310
311******************************************************************************/
312Cal_Bdd_t
313CalOpITE(
314  Cal_BddManager_t *bddManager,
315  Cal_Bdd_t f,
316  Cal_Bdd_t g,
317  Cal_Bdd_t h,
318  CalHashTable_t **reqQueForITE)
319{
320  CalBddNode_t *bddNode1, *bddNode2;
321  int complementFlag = 0;
322
323  /*
324   * First phase: Make substitutions
325   * ITE(F,F,H) = ITE(F,1,H)
326   * ITE(F,F',H) = ITE(F,0,H)
327   * ITE(F,G,F) = ITE(F,G,0)
328   * ITE(F,G,F') = ITE(F,G,1)
329   */
330  bddNode1 = CalBddGetBddNode(f);
331  bddNode2 = CalBddGetBddNode(g);
332  if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
333    if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
334      g = CalBddZero(bddManager);
335    }
336    else{
337      g = CalBddOne(bddManager);
338    }
339  }
340  bddNode2 = CalBddGetBddNode(h);
341  if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
342    if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
343      h = CalBddOne(bddManager);
344    }
345    else{
346      h = CalBddZero(bddManager);
347    }
348  }
349
350  /*
351   * Second phase: Fix the complement pointers.
352   * There are 3 possible cases:
353   * F +ve G -ve: ITE(F ,G',H ) = ITE(F ,G ,H')'
354   * F -ve H +ve: ITE(F',G ,H ) = ITE(F ,H ,G)
355   * F -ve H -ve: ITE(F',G ,H') = ITE(F ,H ,G')'
356   */
357  if(CalBddIsOutPos(f)){
358    if(!CalBddIsOutPos(g)){
359      CalBddNot(g, g);
360      CalBddNot(h, h);
361      complementFlag = 1;
362    }
363  }
364  else{
365    Cal_Bdd_t tmpBdd;
366    CalBddNot(f, f);
367    if(CalBddIsOutPos(h)){
368      tmpBdd = g;
369      g = h;
370      h = tmpBdd;
371    }
372    else{
373      tmpBdd = g;
374      CalBddNot(h, g);
375      CalBddNot(tmpBdd, h);
376      complementFlag = 1;
377    }
378  }
379
380  /*
381   * Third phase: Check for the terminal cases; create new request if needed
382   * ite(1,G,H) = G
383   * ite(0,G,H) = H (impossible by construction in second phase)
384   * ite(F,G,G) = G
385   * ite(F,1,0) = F
386   * ite(F,0,1) = F'(impossible by construction in second phase)
387   */
388  if(CalBddIsBddConst(f) || CalBddIsEqual(g, h)){
389    CalBddUpdatePhase(g, complementFlag);
390    return g;
391  }
392  else if(CalBddIsBddConst(g) && CalBddIsBddConst(h)){
393    CalBddUpdatePhase(f, complementFlag);
394    return f;
395  }
396  else{
397    Cal_BddId_t bddId;
398    Cal_Bdd_t result;
399    CalBddGetMinId3(bddManager, f, g, h, bddId);
400    CalHashTableThreeFindOrAdd(reqQueForITE[bddId], f, g, h, &result);
401    CalBddUpdatePhase(result, complementFlag);
402    return result;
403  }
404}
405
406/*---------------------------------------------------------------------------*/
407/* Definition of static functions                                            */
408/*---------------------------------------------------------------------------*/
409
410
411
412
413
414
415
416
417
418
419
420
421
Note: See TracBrowser for help on using the repository browser.