source: vis_dev/glu-2.1/src/calBdd/calQuant.c @ 10

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

src glu
File size: 53.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calQuant.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for existential/universal quantification and
8  relational product.]
9
10  Description []
11
12  SeeAlso     [None]
13
14  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and
15               Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)]
16
17  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
18  All rights reserved.
19
20  Permission is hereby granted, without written agreement and without license
21  or royalty fees, to use, copy, modify, and distribute this software and its
22  documentation for any purpose, provided that the above copyright notice and
23  the following two paragraphs appear in all copies of this software.
24
25  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
26  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
27  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
28  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
29
30  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
31  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
32  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
33  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
34  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
35
36  Revision    [$Id: calQuant.c,v 1.1.1.4 1998/05/04 00:59:02 hsv Exp $]
37
38******************************************************************************/
39
40#include "calInt.h"
41
42/*---------------------------------------------------------------------------*/
43/* Constant declarations                                                     */
44/*---------------------------------------------------------------------------*/
45
46#define DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX 4
47#define DEFAULT_EXIST_HASH_TABLE_SIZE 16
48
49/*---------------------------------------------------------------------------*/
50/* Type declarations                                                         */
51/*---------------------------------------------------------------------------*/
52
53
54/*---------------------------------------------------------------------------*/
55/* Stucture declarations                                                     */
56/*---------------------------------------------------------------------------*/
57
58
59/*---------------------------------------------------------------------------*/
60/* Variable declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Macro declarations                                                        */
66/*---------------------------------------------------------------------------*/
67
68
69/**AutomaticStart*************************************************************/
70
71/*---------------------------------------------------------------------------*/
72/* Static function prototypes                                                */
73/*---------------------------------------------------------------------------*/
74
75static Cal_Bdd_t BddExistsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *association);
76static Cal_Bdd_t BddRelProdStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned short opCode, CalAssociation_t *assoc);
77static Cal_Bdd_t BddDFStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, CalOpProc_t calOpProc, unsigned short opCode);
78static void HashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t calOpProc, unsigned long opCode);
79static void HashTableReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t * uniqueTableForId);
80static void BddExistsApply(Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t *existHashTable, CalHashTable_t **existHashTableArray, CalOpProc1_t calOpProc, unsigned short opCode, CalAssociation_t *assoc);
81static void BddExistsBFAux(Cal_BddManager_t *bddManager, int minIndex, CalHashTable_t **existHashTableArray, CalHashTable_t **orHashTableArray, CalOpProc1_t calOpProc, unsigned short opCode, CalAssociation_t *assoc);
82static void BddExistsReduce(Cal_BddManager_t *bddManager, CalHashTable_t *existHashTable, CalHashTable_t **existHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *association);
83static Cal_Bdd_t BddExistsBFPlusDF(Cal_BddManager_t *bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *association);
84static void BddRelProdApply(Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t *relProdHashTable, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalOpProc_t calOpProc, unsigned short opCode, CalAssociation_t *assoc);
85static void BddRelProdReduce(Cal_BddManager_t *bddManager, CalHashTable_t *relProdHashTable, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *assoc);
86static void BddRelProdBFAux(Cal_BddManager_t *bddManager, int minIndex, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *assoc);
87static Cal_Bdd_t BddRelProdBFPlusDF(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned short opCode, CalAssociation_t *association);
88
89/**AutomaticEnd***************************************************************/
90
91
92/*---------------------------------------------------------------------------*/
93/* Definition of exported functions                                          */
94/*---------------------------------------------------------------------------*/
95/**Function********************************************************************
96
97  Synopsis    [Returns the result of existentially quantifying some
98  variables from the given BDD.]
99
100  Description [Returns the BDD for f with all the variables that are
101  paired with something in the current variable association
102  existentially quantified out.]
103
104  SideEffects [None.]
105
106  SeeAlso     [Cal_BddRelProd]
107
108******************************************************************************/
109Cal_Bdd
110Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
111{
112  Cal_Bdd_t result;
113  Cal_Bdd userResult;
114
115  if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
116    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
117    CalAssociation_t *assoc = bddManager->currentAssociation;
118    unsigned short opCode;
119   
120    if (assoc->id == -1){
121      opCode = bddManager->tempOpCode--;
122    }
123    else {
124      opCode = CAL_OP_QUANT + assoc->id;
125    }
126    if (bddManager->numNodes <= CAL_LARGE_BDD){
127      /* If number of nodes is small, call depth first routine. */
128      result = BddExistsStep(bddManager, f, opCode, assoc);
129    }
130    else {
131      result = BddExistsBFPlusDF(bddManager, f, opCode, assoc);
132    }
133    userResult =  CalBddGetExternalBdd(bddManager, result);
134    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
135      Cal_BddFree(bddManager, userResult);
136      Cal_BddManagerGC(bddManager);
137      return (Cal_Bdd) 0;
138    }
139    return userResult;
140  }
141  return (Cal_Bdd) 0;
142}
143
144
145/**Function********************************************************************
146
147  Synopsis    [Returns the result of taking the logical AND of the
148  argument BDDs and existentially quantifying some variables from the
149  product.]
150
151  Description [Returns the BDD for the logical AND of f and g with all
152  the variables that are paired with something in the current variable
153  association existentially quantified out.]
154
155  SideEffects [None.]
156
157******************************************************************************/
158Cal_Bdd
159Cal_BddRelProd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
160{
161  Cal_Bdd_t result;
162  Cal_Bdd userResult;
163 
164  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
165    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
166    Cal_Bdd_t g = CalBddGetInternalBdd(bddManager, gUserBdd);
167    CalAssociation_t *assoc = bddManager->currentAssociation;
168    unsigned short opCode;
169   
170    if (bddManager->currentAssociation->id == -1){
171      opCode = bddManager->tempOpCode--;
172      bddManager->tempOpCode--;
173    }
174    else {
175      opCode = CAL_OP_REL_PROD + assoc->id;
176    }
177    if (bddManager->numNodes <= CAL_LARGE_BDD){
178      /* If number of nodes is small, call depth first routine. */
179      result = BddRelProdStep(bddManager, f, g, opCode, assoc);
180    }
181    else {
182      result = BddRelProdBFPlusDF(bddManager, f, g, opCode, assoc);
183    }
184    userResult =  CalBddGetExternalBdd(bddManager, result);
185    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
186      Cal_BddFree(bddManager, userResult);
187      Cal_BddManagerGC(bddManager);
188      return (Cal_Bdd) 0;
189    }
190    return userResult;
191  }
192  return (Cal_Bdd) 0;
193}
194
195/**Function********************************************************************
196
197  Synopsis    [Returns the result of universally quantifying some
198  variables from the given BDD.]
199
200  Description [Returns the BDD for f with all the variables that are
201  paired with something in the current variable association
202  universally quantified out.]
203
204  SideEffects [None.]
205
206******************************************************************************/
207Cal_Bdd
208Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
209{
210  Cal_Bdd_t result;
211  Cal_Bdd userResult;
212
213  if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
214    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
215    CalAssociation_t *assoc = bddManager->currentAssociation;
216    unsigned short opCode;
217
218    CalBddNot(f, f);
219    if (assoc->id == -1){
220      opCode = bddManager->tempOpCode--;
221    }
222    else {
223      opCode = CAL_OP_QUANT + assoc->id;
224    }
225    if (bddManager->numNodes <= CAL_LARGE_BDD){
226      /* If number of nodes is small, call depth first routine. */
227      result = BddExistsStep(bddManager, f, opCode, assoc);
228    }
229    else {
230      result = BddExistsBFPlusDF(bddManager, f, opCode, assoc);
231    }
232    CalBddNot(result, result);
233    userResult =  CalBddGetExternalBdd(bddManager, result);
234    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
235      Cal_BddFree(bddManager, userResult);
236      Cal_BddManagerGC(bddManager);
237      return (Cal_Bdd) 0;
238    }
239    return userResult;
240  }
241  return (Cal_Bdd) 0;
242}
243
244/*---------------------------------------------------------------------------*/
245/* Definition of internal functions                                          */
246/*---------------------------------------------------------------------------*/
247 
248/**Function********************************************************************
249
250  Synopsis    [required]
251
252  Description [optional]
253
254  SideEffects [required]
255
256  SeeAlso     [optional]
257
258******************************************************************************/
259int
260CalOpExists(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t *
261            resultBddPtr) 
262{
263  if (((int)bddManager->idToIndex[CalBddGetBddId(f)]) >
264      bddManager->currentAssociation->lastBddIndex){ 
265    *resultBddPtr = f;
266    return 1;
267  }
268  return 0;
269}
270
271
272/**Function********************************************************************
273
274  Synopsis    [required]
275
276  Description [optional]
277
278  SideEffects [required]
279
280  SeeAlso     [optional]
281
282******************************************************************************/
283int
284CalOpRelProd(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t  g,
285             Cal_Bdd_t * resultBddPtr) 
286{
287  if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g) ||
288      CalBddIsComplementEqual(f, g)){
289    *resultBddPtr = bddManager->bddZero;
290    return 1;
291  }
292  else if (CalBddIsBddOne(bddManager, f) && CalBddIsBddOne(bddManager, g)){
293    *resultBddPtr = bddManager->bddOne;
294    return 1;
295  }
296  return 0;
297}
298/*---------------------------------------------------------------------------*/
299/* Definition of static functions                                            */
300/*---------------------------------------------------------------------------*/
301
302/**Function********************************************************************
303
304  Synopsis    [required]
305
306  Description [optional]
307
308  SideEffects [required]
309
310  SeeAlso     [optional]
311
312******************************************************************************/
313static Cal_Bdd_t
314BddExistsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, unsigned
315              short opCode, CalAssociation_t *association)
316{
317  Cal_Bdd_t temp1, temp2;
318  Cal_Bdd_t f1, f2;
319  Cal_Bdd_t result;
320  Cal_BddId_t topId;
321  int quantifying;
322 
323  if (((int)CalBddGetBddIndex(bddManager, f)) > association->lastBddIndex){
324    return f;
325  }
326  if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
327    return result;
328  }
329
330  topId = CalBddGetBddId(f);
331  quantifying = (CalBddIsBddNull(bddManager,
332                                 association->varAssociation[topId]) ? 0 : 1);
333  CalBddGetCofactors(f, topId, f1, f2);
334  temp1 = BddExistsStep(bddManager, f1, opCode, association);
335  if (quantifying && CalBddIsEqual(temp1, bddManager->bddOne)){
336    result=temp1;
337  }
338  else {
339    temp2 = BddExistsStep(bddManager, f2, opCode, association);
340    if (quantifying){
341      CalBddNot(temp1, temp1);
342      CalBddNot(temp2, temp2);
343          result = BddDFStep(bddManager, temp1, temp2, CalOpNand, CAL_OP_NAND);
344        }
345    else {
346      Cal_BddId_t id = CalBddGetBddId(f);
347      if (CalUniqueTableForIdFindOrAdd(bddManager, bddManager->uniqueTable[id],
348                                       temp1, temp2, &result) == 0){
349        CalBddIcrRefCount(temp1);
350        CalBddIcrRefCount(temp2);
351      }
352    }
353  } 
354  CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
355  return (result);
356}
357
358/**Function********************************************************************
359
360  Synopsis    [required]
361
362  Description [optional]
363
364  SideEffects [required]
365
366  SeeAlso     [optional]
367
368******************************************************************************/
369static Cal_Bdd_t
370BddRelProdStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t
371               g, unsigned short opCode, CalAssociation_t *assoc)
372{
373  Cal_BddId_t topId;
374  Cal_Bdd_t f1, f2, g1, g2;
375  Cal_Bdd_t temp1, temp2;
376  Cal_Bdd_t  result;
377  int quantifying;
378
379  if (CalBddIsBddConst(f) || CalBddIsBddConst(g)){
380    if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g)){
381      return bddManager->bddZero;
382    }
383    if (assoc->id != -1){
384      opCode = CAL_OP_QUANT+assoc->id;
385    }
386    else{
387      opCode--;
388    }
389    if (CalBddIsBddOne(bddManager, f)){
390      return (BddExistsStep(bddManager, g, opCode, assoc));
391    }
392    return (BddExistsStep(bddManager, f, opCode, assoc));
393  }
394  if ((((int)CalBddGetBddIndex(bddManager, f)) > assoc->lastBddIndex) &&
395      (((int)CalBddGetBddIndex(bddManager, g)) > assoc->lastBddIndex)){
396    result = BddDFStep(bddManager, f, g, CalOpNand, CAL_OP_NAND);
397    CalBddNot(result, result);
398    return result;
399  }
400  if(CalOpRelProd(bddManager, f, g, &result) == 1){
401    return result;
402  }
403  CalBddNormalize(f, g);
404  if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
405    return result;
406  }
407  CalBddGetMinId2(bddManager, f, g, topId);
408 
409  quantifying = (CalBddIsBddNull(bddManager, assoc->varAssociation[topId]) ? 0
410                 : 1);
411  CalBddGetCofactors(f, topId, f1, f2);
412  CalBddGetCofactors(g, topId, g1, g2);
413
414  temp1 = BddRelProdStep(bddManager, f1, g1, opCode, assoc);
415  if (quantifying && CalBddIsBddOne(bddManager, temp1)){
416    result=temp1;
417  }
418  else {
419    temp2 = BddRelProdStep(bddManager, f2, g2, opCode, assoc);
420    if (quantifying) {
421      CalBddNot(temp1, temp1);
422      CalBddNot(temp2, temp2);
423          result = BddDFStep(bddManager, temp1, temp2, CalOpNand, CAL_OP_NAND);
424          /*result = BddDFStep(bddManager, temp1, temp2, CalOpOr, CAL_OP_OR);*/
425        }
426    else {
427      if (CalUniqueTableForIdFindOrAdd(bddManager,
428                                       bddManager->uniqueTable[topId],
429                                       temp1, temp2, &result) == 0){
430        CalBddIcrRefCount(temp1);
431        CalBddIcrRefCount(temp2);
432      }
433    }
434  }
435  CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
436  return (result);
437}
438
439/**Function********************************************************************
440
441  Synopsis    [required]
442
443  Description [optional]
444
445  SideEffects [required]
446
447  SeeAlso     [optional]
448
449******************************************************************************/
450static Cal_Bdd_t
451BddDFStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t g,
452          CalOpProc_t calOpProc, unsigned short opCode)
453{
454  Cal_BddId_t topId;
455  Cal_Bdd_t temp1, temp2, fx, fxbar, gx, gxbar;
456  Cal_Bdd_t  result;
457
458  if((*calOpProc)(bddManager, f, g, &result) == 1){
459    return result;
460  }
461  CalBddNormalize(f, g);
462  if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
463    return result;
464  }
465  CalBddGetMinId2(bddManager, f, g, topId);
466  CalBddGetCofactors(f, topId, fx, fxbar);
467  CalBddGetCofactors(g, topId, gx, gxbar);
468  temp1 = BddDFStep(bddManager, fx, gx, calOpProc, opCode);
469  temp2 = BddDFStep(bddManager, fxbar, gxbar, calOpProc, opCode);
470
471  if (CalUniqueTableForIdFindOrAdd(bddManager,
472                                   bddManager->uniqueTable[topId],
473                                   temp1, temp2, &result) == 0){
474    CalBddIcrRefCount(temp1);
475    CalBddIcrRefCount(temp2);
476  }
477  CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
478  return (result);
479}
480/**Function********************************************************************
481
482  Synopsis    [required]
483
484  Description [optional]
485
486  SideEffects [required]
487
488  SeeAlso     [optional]
489
490******************************************************************************/
491static void
492HashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable,
493               CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t calOpProc,
494               unsigned long opCode) 
495{
496  int i, numBins = hashTable->numBins;
497  CalBddNode_t **bins = hashTable->bins;
498  CalRequestNode_t *requestNode;
499  Cal_Bdd_t fx, gx, fxbar, gxbar, result;
500  Cal_BddId_t bddId;
501 
502  for(i = 0; i < numBins; i++){
503    for(requestNode = bins[i];
504        requestNode != Cal_Nil(CalRequestNode_t);
505        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
506      CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
507      CalBddNormalize(fx, gx);
508      if((*calOpProc)(bddManager, fx, gx, &result) == 0){
509        if (CalCacheTableTwoLookup(bddManager, fx, gx, opCode, &result) == 0){
510          CalBddGetMinId2(bddManager, fx, gx, bddId);
511          CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fx, gx, &result);
512          CalCacheTableTwoInsert(bddManager, fx, gx, result, opCode, 1);
513        }
514        else {
515          CalRequestIsForwardedTo(result);
516        }
517      }
518      CalBddIcrRefCount(result);
519      CalRequestNodePutThenRequest(requestNode, result);
520      CalBddNormalize(fxbar, gxbar);
521      if((*calOpProc)(bddManager, fxbar, gxbar, &result) == 0){
522        if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode, &result)
523            == 0){ 
524          CalBddGetMinId2(bddManager, fxbar, gxbar, bddId);
525          CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fxbar, gxbar,
526                                &result); 
527          CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
528                                 opCode, 1);
529        }
530        else {
531          CalRequestIsForwardedTo(result);
532        }
533      }
534      CalBddIcrRefCount(result);
535      CalRequestNodePutElseRequest(requestNode, result);
536    }
537  }
538}
539
540/**Function********************************************************************
541
542  Synopsis    [required]
543
544  Description [optional]
545
546  SideEffects [required]
547
548  SeeAlso     [optional]
549
550******************************************************************************/
551static void
552HashTableReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable,
553                CalHashTable_t * uniqueTableForId)
554{
555  int i, numBins = hashTable->numBins;
556  CalBddNode_t **bins = hashTable->bins;
557  Cal_BddId_t currentBddId = uniqueTableForId->bddId;
558  CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
559  CalRequestNode_t *requestNode, *next;
560  CalBddNode_t *bddNode, *endNode;
561  Cal_Bdd_t thenBdd, elseBdd, result;
562  Cal_BddRefCount_t refCount;
563
564  /*requestNodeList = hashTable->requestNodeList;*/
565  endNode = hashTable->endNode;
566  hashTable->numEntries = 0;
567  for(i = 0; i < numBins; i++){
568    for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
569        requestNode != Cal_Nil(CalRequestNode_t);
570        requestNode = next){
571      next = CalRequestNodeGetNextRequestNode(requestNode);
572      /* Process the requestNode */
573      CalRequestNodeGetThenRequest(requestNode, thenBdd);
574      CalRequestNodeGetElseRequest(requestNode, elseBdd);
575      CalRequestIsForwardedTo(thenBdd);
576      CalRequestIsForwardedTo(elseBdd);
577      if(CalBddIsEqual(thenBdd, elseBdd)){
578        CalBddNodeGetRefCount(requestNode, refCount);
579        CalBddAddRefCount(thenBdd, refCount - 2);
580        CalRequestNodePutThenRequest(requestNode, thenBdd);
581        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
582        /*
583        ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
584        ** requestNodeList = requestNode;
585        */
586        /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
587        endNode->nextBddNode = requestNode;
588        endNode = requestNode;
589      }
590      else if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
591          thenBdd, elseBdd, &result) == 1){
592        CalBddDcrRefCount(thenBdd);
593        CalBddDcrRefCount(elseBdd);
594        CalBddNodeGetRefCount(requestNode, refCount);
595        CalBddAddRefCount(result, refCount);
596        CalRequestNodePutThenRequest(requestNode, result);
597        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
598        /*
599        ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
600        ** requestNodeList = requestNode;
601        */
602        /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
603        endNode->nextBddNode = requestNode;
604        endNode = requestNode;
605      }
606      else if(CalBddIsOutPos(thenBdd)){
607        CalRequestNodePutThenRequest(requestNode, thenBdd);
608        CalRequestNodePutElseRequest(requestNode, elseBdd);
609        CalHashTableAddDirect(uniqueTableForId, requestNode);
610        bddManager->numNodes++;
611        bddManager->gcCheck--;
612      }
613      else{
614        CalNodeManagerAllocNode(nodeManager, bddNode);
615        CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
616        CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
617        CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
618        CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
619        /*
620        CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd,
621                               Cal_Nil(CalBddNode_t), bddNode);
622                               */
623        CalBddNodeGetRefCount(requestNode, refCount);
624        CalBddNodePutRefCount(bddNode, refCount);
625        CalHashTableAddDirect(uniqueTableForId, bddNode);
626        bddManager->numNodes++;
627        bddManager->gcCheck--;
628        CalRequestNodePutThenRequestId(requestNode, currentBddId);
629        CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
630        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
631        /*
632        ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
633        ** requestNodeList = requestNode;
634        */
635        /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
636        endNode->nextBddNode = requestNode;
637        endNode = requestNode;
638      }
639    }
640  }
641  /* hashTable->requestNodeList = requestNodeList; */
642  hashTable->endNode = endNode;
643}
644
645/**Function********************************************************************
646
647  Synopsis    [required]
648
649  Description [optional]
650
651  SideEffects [required]
652
653  SeeAlso     [optional]
654
655******************************************************************************/
656static void
657BddExistsApply(Cal_BddManager_t *bddManager, int quantifying,
658               CalHashTable_t *existHashTable, CalHashTable_t
659               **existHashTableArray,  CalOpProc1_t calOpProc, 
660               unsigned short opCode, CalAssociation_t *assoc) 
661{
662  int i, numBins = existHashTable->numBins;
663  CalBddNode_t **bins = existHashTable->bins;
664  CalRequestNode_t *requestNode;
665  Cal_Bdd_t f, fx, fxbar, result, resultBar;
666  int lastBddIndex = assoc->lastBddIndex; 
667 
668  if (quantifying){
669    for(i = 0; i < numBins; i++){
670      for(requestNode = bins[i];
671          requestNode != Cal_Nil(CalRequestNode_t);
672          requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
673        CalRequestNodeGetF(requestNode, f);
674        CalBddGetThenBdd(f, fx);
675        CalBddGetElseBdd(f, fxbar);
676     
677        /*if(calOpProc(bddManager, fx, &result) == 0){*/
678        if (((int)bddManager->idToIndex[CalBddGetBddId(fx)]) <= lastBddIndex){
679          if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
680            CalRequestIsForwardedTo(result);
681          }
682          else {
683            CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fx)], fx,
684                                  bddManager->bddOne, &result);
685            CalCacheTableOneInsert(bddManager, fx, result,
686                                   opCode, 1);
687          }
688        }
689        else {
690          result = fx;
691        }
692        CalRequestNodePutThenRequest(requestNode, result);
693        CalRequestNodePutElseRequest(requestNode, fxbar);
694      }
695    }
696  }
697  else {
698    for(i = 0; i < numBins; i++){
699      for(requestNode = bins[i];
700          requestNode != Cal_Nil(CalRequestNode_t);
701          requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
702        CalRequestNodeGetF(requestNode, f);
703        CalBddGetThenBdd(f, fx);
704        CalBddGetElseBdd(f, fxbar);
705     
706        if (((int)bddManager->idToIndex[CalBddGetBddId(fx)]) <= lastBddIndex){
707          if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
708            CalRequestIsForwardedTo(result);
709          }
710          else {
711            CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fx)], fx,
712                                  bddManager->bddOne, &result);
713            CalCacheTableOneInsert(bddManager, fx, result,
714                                   opCode, 1);
715          }
716        }
717        else {
718          result = fx;
719        }
720        CalRequestNodePutThenRequest(requestNode, result);
721        CalBddIcrRefCount(result);
722        /*if(calOpProc(bddManager, fxbar, &resultBar) == 0){*/
723        if (((int)bddManager->idToIndex[CalBddGetBddId(fxbar)]) <= lastBddIndex){
724          if (CalCacheTableOneLookup(bddManager, fxbar, opCode,
725                                       &resultBar)){
726            CalRequestIsForwardedTo(resultBar);
727          }
728          else {
729            CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fxbar)], fxbar,
730                                  bddManager->bddOne, &resultBar);
731            CalCacheTableOneInsert(bddManager, fxbar, resultBar,
732                                   opCode, 1); 
733          }
734        }
735        else{
736          resultBar = fxbar;
737        }
738        CalBddIcrRefCount(resultBar);
739        CalRequestNodePutElseRequest(requestNode, resultBar);
740      }
741    }
742  }
743}
744
745/**Function********************************************************************
746
747  Synopsis    [required]
748
749  Description [optional]
750
751  SideEffects [required]
752
753  SeeAlso     [optional]
754
755******************************************************************************/
756static void 
757BddExistsBFAux(Cal_BddManager_t *bddManager, int minIndex,
758               CalHashTable_t **existHashTableArray, CalHashTable_t
759               **orHashTableArray,  CalOpProc1_t calOpProc, unsigned
760               short opCode, CalAssociation_t *assoc)   
761{
762  int index;
763  Cal_BddId_t bddId;
764  int quantifying;
765 
766  /* Apply phase */
767  for (index = minIndex; index < bddManager->numVars; index++){
768    bddId = bddManager->indexToId[index];
769    if (existHashTableArray[bddId]->numEntries){
770      quantifying = (CalBddIsBddNull(bddManager,
771                                     assoc->varAssociation[bddId]) ? 0 : 1); 
772      BddExistsApply(bddManager, quantifying,
773                     existHashTableArray[bddId], existHashTableArray,
774                     calOpProc, opCode, assoc);   
775    }
776  }
777 
778  /* Reduce phase */
779  for (index = bddManager->numVars-1; index >= minIndex; index--){
780    bddId = bddManager->indexToId[index];
781    if (existHashTableArray[bddId]->numEntries){
782      quantifying = (CalBddIsBddNull(bddManager,
783                                     assoc->varAssociation[bddId]) ? 0 : 1); 
784      if (quantifying){
785        BddExistsReduce(bddManager, existHashTableArray[bddId],
786                        existHashTableArray, orHashTableArray,
787                        opCode, assoc);
788      } 
789      else {
790        HashTableReduce(bddManager, existHashTableArray[bddId],
791                        bddManager->uniqueTable[bddId]);
792      }
793    }
794  }
795}
796
797/**Function********************************************************************
798
799  Synopsis    [required]
800
801  Description [optional]
802
803  SideEffects [required]
804
805  SeeAlso     [optional]
806
807******************************************************************************/
808static void
809BddExistsReduce(Cal_BddManager_t *bddManager, CalHashTable_t
810                *existHashTable, CalHashTable_t **existHashTableArray,
811                CalHashTable_t **orHashTableArray, unsigned short
812                opCode, CalAssociation_t *association) 
813{
814  int i, numBins = existHashTable->numBins;
815  CalBddNode_t **bins = existHashTable->bins;
816  CalRequestNode_t *requestNode, *next, *requestNodeListAux;
817  CalBddNode_t *endNode;
818 
819  int bddIndex;
820  /*Cal_BddIndex_t minIndex, elseIndex;*/
821  int minIndex, elseIndex;
822  Cal_BddId_t bddId, minId;
823  Cal_Bdd_t thenBdd, elseBdd, result, orResult;
824  Cal_BddRefCount_t refCount;
825  int lastBddIndex = association->lastBddIndex; 
826 
827
828  /* For those nodes which get processed in the first pass */
829  /* requestNodeList = existHashTable->requestNodeList; */
830  endNode = existHashTable->endNode;
831
832  /* For the other ones. This list is merged with the requestNodeList
833   * after processing is complete.
834   */
835  requestNodeListAux = Cal_Nil(CalRequestNode_t);
836  existHashTable->numEntries = 0;
837 
838  minIndex = bddManager->numVars;
839 
840  for(i = 0; i < numBins; i++){
841    for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
842        requestNode != Cal_Nil(CalRequestNode_t);
843        requestNode = next){
844      next = CalRequestNodeGetNextRequestNode(requestNode);
845      /* Process the requestNode */
846      CalRequestNodeGetThenRequest(requestNode, thenBdd);
847      CalRequestNodeGetElseRequest(requestNode, elseBdd);
848      CalRequestIsForwardedTo(thenBdd);
849      CalRequestNodePutThenRequest(requestNode, thenBdd);
850      if (CalBddIsBddOne(bddManager, thenBdd)){
851        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
852        /*
853        ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
854        ** requestNodeList = requestNode;
855        */
856        /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
857        endNode->nextBddNode = requestNode;
858        endNode = requestNode;
859        continue;
860      }
861     
862      CalRequestNodePutNextRequestNode(requestNode, requestNodeListAux);
863      requestNodeListAux = requestNode;
864
865      /*if(CalOpExists(bddManager, elseBdd, &result) == 0){*/
866      if (((int)bddManager->idToIndex[CalBddGetBddId(elseBdd)]) <= lastBddIndex){
867        if (CalCacheTableOneLookup(bddManager, elseBdd, opCode,
868                                   &result)){ 
869          CalRequestIsForwardedTo(result);
870        }
871        else{
872          CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(elseBdd)], elseBdd,
873                                bddManager->bddOne, &result);
874          CalCacheTableOneInsert(bddManager, elseBdd, result,
875                                 opCode, 1);
876          if (minIndex > (elseIndex = CalBddGetBddIndex(bddManager,
877                                                        elseBdd))){ 
878            minIndex = elseIndex;
879          }
880        }
881      }
882      else{
883        result = elseBdd;
884      }
885      CalRequestNodePutElseRequest(requestNode, result);
886    }
887  }
888 
889  if (!requestNodeListAux){
890    /* requestNodeList = requestNodeList; */
891    existHashTable->endNode = endNode;
892    return;
893  }
894 
895  BddExistsBFAux(bddManager, minIndex, existHashTableArray,
896                 orHashTableArray,  CalOpExists, opCode, association); 
897  minIndex = bddManager->numVars;
898  for (requestNode = requestNodeListAux; requestNode; requestNode = next){
899    Cal_Bdd_t thenResult, elseResult;
900    Cal_BddIndex_t orResultIndex;
901   
902    next = CalRequestNodeGetNextRequestNode(requestNode);
903    CalRequestNodeGetThenRequest(requestNode, thenResult);
904    CalRequestNodeGetElseRequest(requestNode, elseResult);
905    CalRequestIsForwardedTo(elseResult);
906    if (CalOpOr(bddManager, thenResult, elseResult, &orResult) == 0){
907      CalBddNormalize(thenResult, elseResult);
908      CalBddNot(thenResult, thenResult);
909      CalBddNot(elseResult, elseResult);
910      if (CalCacheTableTwoLookup(bddManager, thenResult,elseResult,
911                                 CAL_OP_NAND, &orResult)){
912        CalRequestIsForwardedTo(orResult);
913      }
914      else {
915        CalBddGetMinIdAndMinIndex(bddManager, thenResult, elseResult,
916                                  minId, orResultIndex);
917        CalHashTableFindOrAdd(orHashTableArray[minId], thenResult, elseResult,
918                              &orResult);
919        CalCacheTableTwoInsert(bddManager, thenResult, elseResult, orResult,
920                               CAL_OP_NAND, 1);
921        if (minIndex > orResultIndex) minIndex = orResultIndex;
922      }
923    }
924    CalRequestNodePutThenRequest(requestNode, orResult);
925  }
926 
927
928  /* Call "OR" apply and reduce */
929  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
930    bddId = bddManager->indexToId[bddIndex];
931    if(orHashTableArray[bddId]->numEntries){
932      HashTableApply(bddManager, orHashTableArray[bddId], orHashTableArray,
933                     CalOpNand, CAL_OP_NAND);
934    }
935  }
936 
937  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
938    CalHashTable_t *uniqueTableForId;
939    bddId = bddManager->indexToId[bddIndex];
940    uniqueTableForId = bddManager->uniqueTable[bddId];
941    if(orHashTableArray[bddId]->numEntries){
942      HashTableReduce(bddManager, orHashTableArray[bddId], uniqueTableForId);
943    }
944  }
945 
946  for (requestNode = requestNodeListAux; requestNode; requestNode = next){
947    next = CalRequestNodeGetNextRequestNode(requestNode);
948    CalRequestNodeGetThenRequest(requestNode, result);
949    CalRequestIsForwardedTo(result);
950    CalBddNodeGetRefCount(requestNode, refCount);
951    CalBddAddRefCount(result, refCount);
952    CalRequestNodePutThenRequest(requestNode, result);
953    CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
954    /*
955    ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
956    ** requestNodeList = requestNode;
957    */
958    /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
959    endNode->nextBddNode = requestNode;
960    endNode = requestNode;
961  }
962  /*existHashTable->requestNodeList = requestNodeList;*/
963  existHashTable->endNode = endNode;
964 
965}
966 
967/**Function********************************************************************
968
969  Synopsis    [required]
970
971  Description [optional]
972
973  SideEffects [required]
974
975  SeeAlso     [optional]
976
977******************************************************************************/
978static Cal_Bdd_t
979BddExistsBFPlusDF(Cal_BddManager_t *bddManager, Cal_Bdd_t f, unsigned
980                  short opCode, CalAssociation_t *association)
981{
982  Cal_BddId_t fId = CalBddGetBddId(f);
983  Cal_BddIndex_t bddIndex;
984  Cal_BddId_t bddId;
985 
986  Cal_BddIndex_t fIndex = bddManager->idToIndex[fId];
987  CalHashTable_t **orHashTableArray = bddManager->reqQue[4];
988  CalHashTable_t **existHashTableArray = bddManager->reqQue[5];
989  Cal_Bdd_t result;
990 
991  if (CalOpExists(bddManager, f, &result) == 1){
992    return result;
993  }
994
995  if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
996    return result;
997  }
998 
999  /*
1000   * Change the size of the exist hash table to min. size
1001   */
1002  for (bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
1003    bddId = bddManager->indexToId[bddIndex];
1004    existHashTableArray[bddId]->sizeIndex =
1005        DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX; 
1006    existHashTableArray[bddId]->numBins = DEFAULT_EXIST_HASH_TABLE_SIZE;
1007    Cal_MemFree(existHashTableArray[bddId]->bins);
1008    existHashTableArray[bddId]->bins = Cal_MemAlloc(CalBddNode_t*,
1009                                             DEFAULT_EXIST_HASH_TABLE_SIZE);
1010    memset((char *)existHashTableArray[bddId]->bins, 0,
1011           existHashTableArray[bddId]->numBins*sizeof(CalBddNode_t*));
1012  }
1013 
1014  CalHashTableFindOrAdd(existHashTableArray[fId], f, bddManager->bddOne,
1015                        &result); 
1016
1017
1018  BddExistsBFAux(bddManager, fIndex, existHashTableArray, orHashTableArray,
1019                 CalOpExists, opCode, association); 
1020
1021  CalRequestIsForwardedTo(result);
1022 
1023  CalCacheTableTwoFixResultPointers(bddManager);
1024  CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
1025  for (bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
1026    bddId = bddManager->indexToId[bddIndex];
1027    CalHashTableCleanUp(existHashTableArray[bddId]);
1028    CalHashTableCleanUp(orHashTableArray[bddId]);
1029  }
1030  return result;
1031}
1032
1033 
1034/**Function********************************************************************
1035
1036  Synopsis    [required]
1037
1038  Description [optional]
1039
1040  SideEffects [required]
1041
1042  SeeAlso     [optional]
1043
1044******************************************************************************/
1045static void
1046BddRelProdApply(Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t
1047                *relProdHashTable, CalHashTable_t **relProdHashTableArray,
1048                CalHashTable_t **andHashTableArray, CalOpProc_t
1049                calOpProc, unsigned short opCode, CalAssociation_t *assoc)
1050{
1051  int i, numBins = relProdHashTable->numBins;
1052  CalBddNode_t **bins = relProdHashTable->bins;
1053  Cal_BddId_t minId;
1054  CalRequestNode_t *requestNode;
1055  Cal_Bdd_t fx, fxbar, gx, gxbar, result, resultBar;
1056  /*Cal_BddIndex_t minIndex;*/
1057  int minIndex;
1058 
1059  for(i = 0; i < numBins; i++){
1060    for(requestNode = bins[i];
1061        requestNode != Cal_Nil(CalRequestNode_t);
1062        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
1063      CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
1064      CalBddNormalize(fx, gx);
1065      CalBddGetMinIdAndMinIndex(bddManager, fx, gx, minId, minIndex);
1066      if (minIndex > assoc->lastBddIndex){
1067        if (CalOpAnd(bddManager, fx, gx, &result) == 0){
1068          if (CalCacheTableTwoLookup(bddManager, fx, gx, CAL_OP_NAND,
1069                                     &result)){ 
1070            CalRequestIsForwardedTo(result);
1071          }
1072          else{
1073            CalHashTableFindOrAdd(andHashTableArray[minId], fx, gx, &result);
1074            CalCacheTableTwoInsert(bddManager, fx, gx, result,
1075                                   CAL_OP_NAND, 1);
1076          }
1077          CalBddNot(result, result);
1078        }
1079      }
1080      else {
1081        if(calOpProc(bddManager, fx, gx, &result) == 0){
1082          if (CalCacheTableTwoLookup(bddManager, fx, gx, opCode,
1083                                     &result)){     
1084            CalRequestIsForwardedTo(result);
1085          }
1086          else {
1087            CalHashTableFindOrAdd(relProdHashTableArray[minId], fx, gx,
1088                                  &result);   
1089            CalCacheTableTwoInsert(bddManager, fx, gx, result, opCode, 1); 
1090          }
1091        }
1092      }
1093      CalRequestNodePutThenRequest(requestNode, result);
1094      if (quantifying){
1095        Cal_Bdd_t elseRequest;
1096        Cal_BddId_t elseRequestId;
1097        CalBddNode_t *elseRequestNode;
1098       
1099        CalBddGetMinId2(bddManager, fxbar, gxbar, elseRequestId);
1100        CalNodeManagerInitBddNode(bddManager->nodeManagerArray[elseRequestId],
1101                                  fxbar, gxbar, Cal_Nil(CalBddNode_t),
1102                                  elseRequestNode);
1103        /*
1104          CalNodeManagerAllocNode(bddManager->nodeManagerArray[elseRequestId],
1105          elseRequestNode); 
1106          CalRequestNodePutF(elseRequestNode, fxbar);
1107          CalRequestNodePutG(elseRequestNode, gxbar);
1108        */
1109        CalRequestPutRequestId(elseRequest, elseRequestId);
1110        CalRequestPutRequestNode(elseRequest, elseRequestNode);
1111        CalRequestNodePutElseRequest(requestNode, elseRequest);
1112      }
1113      else {
1114        CalBddIcrRefCount(result);
1115        CalBddNormalize(fxbar, gxbar);
1116        CalBddGetMinIdAndMinIndex(bddManager, fxbar, gxbar, minId, minIndex);
1117        if (minIndex > assoc->lastBddIndex){
1118          if (CalOpAnd(bddManager, fxbar, gxbar, &resultBar) == 0){
1119            if( CalCacheTableTwoLookup(bddManager, fxbar, gxbar,
1120                                       CAL_OP_NAND, &resultBar)){ 
1121              CalRequestIsForwardedTo(resultBar);
1122            }
1123            else{
1124              CalHashTableFindOrAdd(andHashTableArray[minId], fxbar, gxbar,
1125                                    &resultBar); 
1126              CalCacheTableTwoInsert(bddManager, fxbar, gxbar, resultBar,
1127                                     CAL_OP_NAND, 1); 
1128            }
1129            CalBddNot(resultBar, resultBar);
1130          }
1131        }
1132        else {
1133          if(calOpProc(bddManager, fxbar, gxbar, &resultBar) == 0){
1134            if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode,
1135                                       &resultBar)){   
1136              CalRequestIsForwardedTo(resultBar);
1137            }
1138            else { 
1139              CalHashTableFindOrAdd(relProdHashTableArray[minId],
1140                                    fxbar, gxbar, &resultBar);
1141              CalCacheTableTwoInsert(bddManager, fxbar, gxbar,
1142                                     resultBar, opCode, 1); 
1143            }
1144          }
1145        }
1146        CalBddIcrRefCount(resultBar);
1147        CalRequestNodePutElseRequest(requestNode, resultBar);
1148      }
1149    }
1150  }
1151}
1152/**Function********************************************************************
1153
1154  Synopsis    [required]
1155
1156  Description [optional]
1157
1158  SideEffects [required]
1159
1160  SeeAlso     [optional]
1161
1162******************************************************************************/
1163static void
1164BddRelProdReduce(Cal_BddManager_t *bddManager, CalHashTable_t
1165                 *relProdHashTable, CalHashTable_t
1166                 **relProdHashTableArray, CalHashTable_t
1167                 **andHashTableArray, CalHashTable_t
1168                 **orHashTableArray, unsigned short opCode,
1169                 CalAssociation_t *assoc) 
1170{
1171  int i, numBins = relProdHashTable->numBins;
1172  CalBddNode_t **bins = relProdHashTable->bins;
1173  CalRequestNode_t *requestNode, *next, *requestNodeListAux;
1174  CalBddNode_t  *elseRequestNode;
1175  int bddIndex;
1176  /*Cal_BddIndex_t minIndex;*/
1177  int minIndex;
1178  Cal_BddId_t bddId, minId, elseRequestId;
1179  Cal_Bdd_t thenBdd, elseBdd, result, orResult;
1180  Cal_BddRefCount_t refCount;
1181  Cal_Bdd_t fxbar, gxbar;
1182  CalBddNode_t *endNode;
1183 
1184
1185  /* For those nodes which get processed in the first pass */
1186  /*requestNodeList = relProdHashTable->requestNodeList;*/
1187  endNode = relProdHashTable->endNode;
1188 
1189  /* For the other ones. This list is merged with the requestNodeList
1190   * after processing is complete.
1191   */
1192  requestNodeListAux = Cal_Nil(CalRequestNode_t);
1193 
1194  minIndex = bddManager->numVars;
1195 
1196  for(i = 0; i < numBins; i++){
1197    for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
1198        requestNode != Cal_Nil(CalRequestNode_t);
1199        requestNode = next){
1200      next = CalRequestNodeGetNextRequestNode(requestNode);
1201      /* Process the requestNode */
1202      CalRequestNodeGetThenRequest(requestNode, thenBdd);
1203      CalRequestIsForwardedTo(thenBdd);
1204      /*CalRequestNodePutThenRequest(requestNode, thenBdd);*/
1205      CalRequestNodeGetElseRequest(requestNode, elseBdd);
1206      CalRequestIsForwardedTo(elseBdd);
1207      CalRequestGetF(elseBdd, fxbar);
1208      CalRequestGetG(elseBdd, gxbar);
1209     
1210      /* Free the else request node because it is not needed */
1211      elseRequestNode = CalRequestNodeGetElseRequestNode(requestNode);
1212      elseRequestId = CalRequestNodeGetElseRequestId(requestNode);
1213      CalNodeManagerFreeNode(bddManager->nodeManagerArray[elseRequestId],
1214                             elseRequestNode);
1215      if (CalBddIsBddOne(bddManager, thenBdd)){
1216        CalRequestNodePutThenRequest(requestNode, bddManager->bddOne);
1217        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
1218        /*
1219        ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
1220        ** requestNodeList = requestNode;
1221        */
1222        /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
1223        endNode->nextBddNode = requestNode;
1224        endNode = requestNode;
1225        continue;
1226      }
1227     
1228      CalRequestNodePutNextRequestNode(requestNode, requestNodeListAux);
1229      requestNodeListAux = requestNode;
1230
1231      CalBddGetMinIdAndMinIndex(bddManager, fxbar, gxbar, bddId, bddIndex);
1232      CalBddNormalize(fxbar, gxbar);
1233      if (bddIndex > assoc->lastBddIndex){
1234        if (CalOpAnd(bddManager, fxbar, gxbar, &result) == 0){
1235          if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar,
1236                                     CAL_OP_NAND, &result)){
1237            CalRequestIsForwardedTo(result);
1238          }
1239          else {
1240            CalHashTableFindOrAdd(andHashTableArray[bddId], fxbar,
1241                                  gxbar, &result);
1242            CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
1243                                   CAL_OP_NAND, 1);
1244            if (minIndex > bddIndex) minIndex = bddIndex;
1245          }
1246          CalBddNot(result, result);
1247        }
1248      }
1249      else {
1250        if(CalOpRelProd(bddManager, fxbar, gxbar, &result) == 0){
1251          if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode,
1252                                     &result)){ 
1253            CalRequestIsForwardedTo(result);
1254          }
1255          else {
1256            CalHashTableFindOrAdd(relProdHashTableArray[bddId], fxbar, gxbar, 
1257                                  &result);
1258            CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
1259                                   opCode, 1); 
1260            if (minIndex > bddIndex) minIndex = bddIndex;
1261          }
1262        }
1263      }
1264      CalRequestNodePutElseRequest(requestNode, result);
1265    }
1266  }
1267
1268  if (!requestNodeListAux){
1269    /*relProdHashTable->requestNodeList = requestNodeList;*/
1270    relProdHashTable->endNode = endNode;
1271    return;
1272  }
1273 
1274  BddRelProdBFAux(bddManager, minIndex, relProdHashTableArray,
1275                  andHashTableArray, orHashTableArray, opCode, assoc);
1276 
1277  minIndex = bddManager->numVars;
1278  for (requestNode = requestNodeListAux; requestNode; requestNode = next){
1279    Cal_Bdd_t thenResult, elseResult;
1280    Cal_BddIndex_t orResultIndex;
1281   
1282    next = CalRequestNodeGetNextRequestNode(requestNode);
1283    CalRequestNodeGetThenRequest(requestNode, thenResult);
1284    CalRequestNodeGetElseRequest(requestNode, elseResult);
1285    CalRequestIsForwardedTo(elseResult);
1286    CalRequestIsForwardedTo(thenResult);
1287    CalBddNormalize(thenResult, elseResult);
1288    if (CalOpOr(bddManager, thenResult, elseResult, &orResult) == 0){
1289      CalBddNot(thenResult, thenResult);
1290      CalBddNot(elseResult, elseResult);
1291      if (CalCacheTableTwoLookup(bddManager, thenResult, elseResult,
1292                                 CAL_OP_NAND, &orResult)){ 
1293        CalRequestIsForwardedTo(orResult);
1294      }
1295      else {
1296        CalBddGetMinIdAndMinIndex(bddManager, thenResult, elseResult,
1297                                  minId, orResultIndex);
1298        CalHashTableFindOrAdd(orHashTableArray[minId], thenResult, elseResult,
1299                              &orResult);
1300        CalCacheTableTwoInsert(bddManager, thenResult, elseResult, orResult,
1301                                 CAL_OP_NAND, 1); 
1302        if (minIndex > orResultIndex) minIndex = orResultIndex;
1303      }
1304    }
1305    CalRequestNodePutThenRequest(requestNode, orResult);
1306  }
1307
1308  /* Call "OR" apply and reduce */
1309  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
1310    bddId = bddManager->indexToId[bddIndex];
1311    if(orHashTableArray[bddId]->numEntries){
1312        HashTableApply(bddManager, orHashTableArray[bddId], orHashTableArray,
1313                       CalOpNand, CAL_OP_NAND); 
1314    }
1315  }
1316 
1317  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
1318    CalHashTable_t *uniqueTableForId;
1319    bddId = bddManager->indexToId[bddIndex];
1320    uniqueTableForId = bddManager->uniqueTable[bddId];
1321    if(orHashTableArray[bddId]->numEntries){
1322      HashTableReduce(bddManager, orHashTableArray[bddId], uniqueTableForId);
1323    }
1324  }
1325  for (requestNode = requestNodeListAux; requestNode; requestNode = next){
1326    next = CalRequestNodeGetNextRequestNode(requestNode);
1327    CalRequestNodeGetThenRequest(requestNode, result);
1328    CalRequestIsForwardedTo(result);
1329    CalBddNodeGetRefCount(requestNode, refCount);
1330    CalBddAddRefCount(result, refCount);
1331    CalRequestNodePutThenRequest(requestNode, result);
1332    CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
1333    /*
1334    ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
1335    ** requestNodeList = requestNode;
1336    */
1337    /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
1338    endNode->nextBddNode = requestNode;
1339    endNode = requestNode;
1340  }
1341
1342  /*relProdHashTable->requestNodeList = requestNodeList;*/
1343  relProdHashTable->endNode = endNode;
1344}
1345
1346/**Function********************************************************************
1347
1348  Synopsis    [required]
1349
1350  Description [optional]
1351
1352  SideEffects [required]
1353
1354  SeeAlso     [optional]
1355
1356******************************************************************************/
1357static void
1358BddRelProdBFAux(Cal_BddManager_t *bddManager, int minIndex,
1359                CalHashTable_t **relProdHashTableArray, CalHashTable_t
1360                **andHashTableArray, CalHashTable_t
1361                **orHashTableArray, unsigned short opCode,
1362                CalAssociation_t *assoc)
1363{
1364  Cal_BddIndex_t bddIndex;
1365  int quantifying;
1366  int index;
1367  Cal_BddId_t bddId;
1368  CalHashTable_t *hashTable;
1369 
1370  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
1371    bddId = bddManager->indexToId[bddIndex];
1372    hashTable = andHashTableArray[bddId];
1373    if(hashTable->numEntries){
1374      HashTableApply(bddManager, hashTable, andHashTableArray, CalOpNand,
1375                     CAL_OP_NAND); 
1376    }
1377    hashTable = relProdHashTableArray[bddId];
1378    if(hashTable->numEntries){
1379      quantifying = (CalBddIsBddNull(bddManager,
1380                                     assoc->varAssociation[bddId]) ? 0 : 1); 
1381      BddRelProdApply(bddManager, quantifying, hashTable,
1382                      relProdHashTableArray, andHashTableArray,
1383                      CalOpRelProd, opCode, assoc); 
1384    }
1385  }
1386
1387  /* Reduce phase */
1388  for (index = bddManager->numVars-1; index >= minIndex; index--){
1389    CalHashTable_t *uniqueTableForId;
1390    bddId = bddManager->indexToId[index];
1391    uniqueTableForId = bddManager->uniqueTable[bddId];
1392    hashTable = andHashTableArray[bddId];
1393    if(hashTable->numEntries){
1394      HashTableReduce(bddManager, hashTable, uniqueTableForId);
1395    }
1396    if (relProdHashTableArray[bddId]->numEntries){
1397      quantifying = (CalBddIsBddNull(bddManager,
1398                                     assoc->varAssociation[bddId]) ? 0 : 1); 
1399      if (quantifying){
1400        BddRelProdReduce(bddManager, relProdHashTableArray[bddId],
1401                         relProdHashTableArray, andHashTableArray,
1402                         orHashTableArray, opCode, assoc); 
1403      }
1404      else {
1405        HashTableReduce(bddManager, relProdHashTableArray[bddId],
1406                        bddManager->uniqueTable[bddId]);
1407      }
1408    }
1409  }
1410}
1411
1412/**Function********************************************************************
1413
1414  Synopsis    [required]
1415
1416  Description [optional]
1417
1418  SideEffects [required]
1419
1420  SeeAlso     [optional]
1421
1422******************************************************************************/
1423static Cal_Bdd_t
1424BddRelProdBFPlusDF(Cal_BddManager_t * bddManager, Cal_Bdd_t  f,
1425                   Cal_Bdd_t  g, unsigned short opCode,
1426                   CalAssociation_t *association)
1427{
1428  Cal_Bdd_t result;
1429  /*Cal_BddIndex_t minIndex;*/
1430  int  minIndex;
1431  int bddIndex;
1432  CalHashTable_t **andHashTableArray = bddManager->reqQue[3];
1433  CalHashTable_t **relProdHashTableArray = bddManager->reqQue[4];
1434  CalHashTable_t **orHashTableArray = bddManager->reqQue[5];
1435  Cal_BddId_t bddId, minId;
1436
1437  if(CalOpRelProd(bddManager, f, g, &result) == 1){
1438    return result;
1439  }
1440  CalBddNormalize(f, g);
1441  if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
1442    return result;
1443  }
1444
1445  CalBddGetMinIdAndMinIndex(bddManager, f, g, minId, minIndex);
1446
1447  /*
1448   * Change the size of the exist hash table to min. size
1449   */
1450  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
1451    bddId = bddManager->indexToId[bddIndex];
1452    relProdHashTableArray[bddId]->sizeIndex =
1453        DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX; 
1454    relProdHashTableArray[bddId]->numBins = DEFAULT_EXIST_HASH_TABLE_SIZE;
1455    Cal_MemFree(relProdHashTableArray[bddId]->bins);
1456    relProdHashTableArray[bddId]->bins = Cal_MemAlloc(CalBddNode_t*,
1457                                             DEFAULT_EXIST_HASH_TABLE_SIZE);
1458    memset((char *)relProdHashTableArray[bddId]->bins, 0,
1459           relProdHashTableArray[bddId]->numBins*sizeof(CalBddNode_t*));
1460  }
1461
1462  if (minIndex > association->lastBddIndex) {
1463    if (CalOpAnd(bddManager, f, g, &result) == 0){
1464      if (CalCacheTableTwoLookup(bddManager, f, g, CAL_OP_NAND, &result)
1465          == 0){
1466        CalHashTableFindOrAdd(andHashTableArray[minId], f, g, &result);
1467      }
1468      else{
1469        CalCacheTableTwoInsert(bddManager, f, g, result, CAL_OP_NAND,
1470                               1);
1471      }
1472      CalBddNot(result, result);
1473    }
1474  }
1475  else {
1476    CalHashTableFindOrAdd(relProdHashTableArray[minId], f, g, &result); 
1477  }
1478
1479  BddRelProdBFAux(bddManager, minIndex, relProdHashTableArray,
1480                  andHashTableArray, orHashTableArray, opCode, association); 
1481  CalRequestIsForwardedTo(result);
1482  CalCacheTableTwoFixResultPointers(bddManager);
1483  CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
1484  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
1485    bddId = bddManager->indexToId[bddIndex];
1486    CalHashTableCleanUp(relProdHashTableArray[bddId]);
1487    CalHashTableCleanUp(andHashTableArray[bddId]);
1488    CalHashTableCleanUp(orHashTableArray[bddId]);
1489  }
1490  return result;
1491}
1492
Note: See TracBrowser for help on using the repository browser.