src/calBdd/calTerminal.c File Reference

#include "calInt.h"
Include dependency graph for calTerminal.c:

Go to the source code of this file.

Functions

int CalOpAnd (Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t *resultBddPtr)
int CalOpNand (Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t *resultBddPtr)
int CalOpOr (Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t *resultBddPtr)
int CalOpXor (Cal_BddManager_t *bddManager, Cal_Bdd_t F, Cal_Bdd_t G, Cal_Bdd_t *resultBddPtr)
Cal_Bdd_t CalOpITE (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t h, CalHashTable_t **reqQueForITE)

Function Documentation

int CalOpAnd ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  F,
Cal_Bdd_t  G,
Cal_Bdd_t *  resultBddPtr 
)

CFile***********************************************************************

FileName [calTerminal.c]

PackageName [cal]

Synopsis [Contains the terminal function for various BDD operations.]

Description []

SeeAlso []

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
calTerminal.c,v 1.1.1.2 1997/02/12 21:11:30 hsv Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 95 of file calTerminal.c.

00099 {
00100   if(CalBddIsBddConst(F)){
00101     if(CalBddIsBddOne(bddManager, F)){
00102       *resultBddPtr = G;
00103     }
00104     else{
00105       *resultBddPtr = F;
00106     }
00107     return 1;
00108   }
00109   else if(CalBddIsBddConst(G)){
00110     if(CalBddIsBddOne(bddManager, G)){
00111       *resultBddPtr = F;
00112     }
00113     else{
00114       *resultBddPtr = G;
00115     }
00116     return 1;
00117   }
00118   else{
00119     CalBddNode_t *bddNodeF, *bddNodeG;
00120     bddNodeF = CalBddGetBddNode(F);
00121     bddNodeG = CalBddGetBddNode(G);
00122     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00123       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00124         *resultBddPtr = CalBddZero(bddManager);
00125       }
00126       else{
00127         *resultBddPtr = F;
00128       }
00129       return 1;
00130     }
00131     else{
00132       return 0;
00133     }
00134   }
00135 }

Cal_Bdd_t CalOpITE ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  g,
Cal_Bdd_t  h,
CalHashTable_t **  reqQueForITE 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 313 of file calTerminal.c.

00319 {
00320   CalBddNode_t *bddNode1, *bddNode2;
00321   int complementFlag = 0;
00322 
00323   /*
00324    * First phase: Make substitutions 
00325    * ITE(F,F,H) = ITE(F,1,H)
00326    * ITE(F,F',H) = ITE(F,0,H)
00327    * ITE(F,G,F) = ITE(F,G,0)
00328    * ITE(F,G,F') = ITE(F,G,1)
00329    */
00330   bddNode1 = CalBddGetBddNode(f);
00331   bddNode2 = CalBddGetBddNode(g);
00332   if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
00333     if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
00334       g = CalBddZero(bddManager);
00335     }
00336     else{
00337       g = CalBddOne(bddManager);
00338     }
00339   }
00340   bddNode2 = CalBddGetBddNode(h);
00341   if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
00342     if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
00343       h = CalBddOne(bddManager);
00344     }
00345     else{
00346       h = CalBddZero(bddManager);
00347     }
00348   }
00349 
00350   /*
00351    * Second phase: Fix the complement pointers.
00352    * There are 3 possible cases:
00353    * F +ve G -ve: ITE(F ,G',H ) = ITE(F ,G ,H')'
00354    * F -ve H +ve: ITE(F',G ,H ) = ITE(F ,H ,G)
00355    * F -ve H -ve: ITE(F',G ,H') = ITE(F ,H ,G')'
00356    */
00357   if(CalBddIsOutPos(f)){
00358     if(!CalBddIsOutPos(g)){
00359       CalBddNot(g, g);
00360       CalBddNot(h, h);
00361       complementFlag = 1;
00362     }
00363   }
00364   else{
00365     Cal_Bdd_t tmpBdd;
00366     CalBddNot(f, f);
00367     if(CalBddIsOutPos(h)){
00368       tmpBdd = g;
00369       g = h;
00370       h = tmpBdd;
00371     }
00372     else{
00373       tmpBdd = g;
00374       CalBddNot(h, g);
00375       CalBddNot(tmpBdd, h);
00376       complementFlag = 1;
00377     }
00378   }
00379 
00380   /*
00381    * Third phase: Check for the terminal cases; create new request if needed
00382    * ite(1,G,H) = G
00383    * ite(0,G,H) = H (impossible by construction in second phase)
00384    * ite(F,G,G) = G
00385    * ite(F,1,0) = F
00386    * ite(F,0,1) = F'(impossible by construction in second phase)
00387    */
00388   if(CalBddIsBddConst(f) || CalBddIsEqual(g, h)){
00389     CalBddUpdatePhase(g, complementFlag);
00390     return g;
00391   }
00392   else if(CalBddIsBddConst(g) && CalBddIsBddConst(h)){
00393     CalBddUpdatePhase(f, complementFlag);
00394     return f;
00395   }
00396   else{
00397     Cal_BddId_t bddId;
00398     Cal_Bdd_t result;
00399     CalBddGetMinId3(bddManager, f, g, h, bddId);
00400     CalHashTableThreeFindOrAdd(reqQueForITE[bddId], f, g, h, &result);
00401     CalBddUpdatePhase(result, complementFlag);
00402     return result;
00403   }
00404 }

int CalOpNand ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  F,
Cal_Bdd_t  G,
Cal_Bdd_t *  resultBddPtr 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 149 of file calTerminal.c.

00153 {
00154   if(CalBddIsBddConst(F)){
00155     if(CalBddIsBddOne(bddManager, F)){
00156       CalBddNot(G, *resultBddPtr);
00157     }
00158     else{
00159       CalBddNot(F, *resultBddPtr);
00160     }
00161     return 1;
00162   }
00163   else if(CalBddIsBddConst(G)){
00164     if(CalBddIsBddOne(bddManager, G)){
00165       CalBddNot(F, *resultBddPtr);
00166     }
00167     else{
00168       CalBddNot(G, *resultBddPtr);
00169     }
00170     return 1;
00171   }
00172   else{
00173     CalBddNode_t *bddNodeF, *bddNodeG;
00174     bddNodeF = CalBddGetBddNode(F);
00175     bddNodeG = CalBddGetBddNode(G);
00176     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00177       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00178         *resultBddPtr = CalBddOne(bddManager);
00179       }
00180       else{
00181         CalBddNot(F, *resultBddPtr);
00182       }
00183       return 1;
00184     }
00185     else{
00186       return 0;
00187     }
00188   }
00189 }

int CalOpOr ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  F,
Cal_Bdd_t  G,
Cal_Bdd_t *  resultBddPtr 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 203 of file calTerminal.c.

00208 {
00209   if(CalBddIsBddConst(F)){
00210     if(CalBddIsBddOne(bddManager, F)){
00211       *resultBddPtr = F;
00212     }
00213     else{
00214       *resultBddPtr = G;
00215     }
00216     return 1;
00217   }
00218   else if(CalBddIsBddConst(G)){
00219     if(CalBddIsBddOne(bddManager, G)){
00220       *resultBddPtr = G;
00221     }
00222     else{
00223       *resultBddPtr = F;
00224     }
00225     return 1;
00226   }
00227   else{
00228     CalBddNode_t *bddNodeF, *bddNodeG;
00229     bddNodeF = CalBddGetBddNode(F);
00230     bddNodeG = CalBddGetBddNode(G);
00231     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00232       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00233         *resultBddPtr = CalBddOne(bddManager);
00234       }
00235       else{
00236         *resultBddPtr = F;
00237       }
00238       return 1;
00239     }
00240     else{
00241       return 0;
00242     }
00243   }
00244 }

int CalOpXor ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  F,
Cal_Bdd_t  G,
Cal_Bdd_t *  resultBddPtr 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 258 of file calTerminal.c.

00263 {
00264   if(CalBddIsBddConst(F)){
00265     if(CalBddIsBddOne(bddManager, F)){
00266       CalBddNot(G, *resultBddPtr);
00267     }
00268     else{
00269       *resultBddPtr = G;
00270     }
00271     return 1;
00272   }
00273   else if(CalBddIsBddConst(G)){
00274     if(CalBddIsBddOne(bddManager, G)){
00275       CalBddNot(F, *resultBddPtr);
00276     }
00277     else{
00278       *resultBddPtr = F;
00279     }
00280     return 1;
00281   }
00282   else{
00283     CalBddNode_t *bddNodeF, *bddNodeG;
00284     bddNodeF = CalBddGetBddNode(F);
00285     bddNodeG = CalBddGetBddNode(G);
00286     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00287       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00288         *resultBddPtr = CalBddOne(bddManager);
00289       }
00290       else{
00291         *resultBddPtr = CalBddZero(bddManager);
00292       }
00293       return 1;
00294     }
00295     else{
00296       return 0;
00297     }
00298   }
00299 }

Generated on Tue Jan 12 13:57:13 2010 for glu-2.2 by  doxygen 1.6.1