src/calBdd/calBddSatisfy.c File Reference

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

Go to the source code of this file.

Functions

static Cal_Bdd_t BddSatisfyStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f)
static Cal_Bdd_t BddSatisfySupportStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_BddId_t *support)
static int IndexCmp (const void *p1, const void *p2)
static double BddSatisfyingFractionStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalHashTable_t *hashTable)
Cal_Bdd Cal_BddSatisfy (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Cal_Bdd Cal_BddSatisfySupport (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
double Cal_BddSatisfyingFraction (Cal_BddManager bddManager, Cal_Bdd fUserBdd)

Function Documentation

static double BddSatisfyingFractionStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
CalHashTable_t *  hashTable 
) [static]

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

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 348 of file calBddSatisfy.c.

00352 {
00353   double *resultPtr, result;
00354   Cal_Bdd_t thenBdd, elseBdd;
00355 
00356   if(CalBddIsBddConst(f)){
00357     if(CalBddIsBddZero(bddManager, f)){
00358       return 0.0;
00359     }
00360     return 1.0;
00361   }
00362   if(CalHashTableOneLookup(hashTable, f, (char **)&resultPtr)){
00363     return (*resultPtr);
00364   }
00365   CalBddGetThenBdd(f, thenBdd);
00366   CalBddGetElseBdd(f, elseBdd);
00367   result = 
00368       0.5 * BddSatisfyingFractionStep(bddManager, thenBdd, hashTable) +
00369       0.5 * BddSatisfyingFractionStep(bddManager, elseBdd, hashTable);
00370   CalHashTableOneInsert(hashTable, f, (char *)&result);
00371   return (result);
00372 }

static Cal_Bdd_t BddSatisfyStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f 
) [static]

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

FileName [calBddSatisfy.c]

PackageName [cal]

Synopsis [Routines for BDD satisfying valuation.]

Description [ ]

SeeAlso [optional]

Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@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
calBddSatisfy.c,v 1.1.1.3 1998/05/04 00:58:53 hsv Exp

]AutomaticStart

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

Name [BddSatisfyStep]

Synopsis [Returns a BDD which implies f, is true for some valuation on which f is true, and which has at most one node at each level]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 217 of file calBddSatisfy.c.

00220 {
00221   Cal_Bdd_t tempBdd;
00222   Cal_Bdd_t result;
00223 
00224   if(CalBddIsBddConst(f)){
00225     return (f);
00226   }
00227   CalBddGetThenBdd(f, tempBdd);
00228   if(CalBddIsBddZero(bddManager, tempBdd)){
00229     CalBddGetElseBdd(f, tempBdd);
00230     tempBdd = BddSatisfyStep(bddManager, tempBdd);
00231     if(!CalUniqueTableForIdFindOrAdd(bddManager,
00232         bddManager->uniqueTable[CalBddGetBddId(f)],
00233         CalBddZero(bddManager), tempBdd, &result)){
00234       CalBddIcrRefCount(tempBdd);
00235     }
00236   }
00237   else{
00238     tempBdd = BddSatisfyStep(bddManager, tempBdd);
00239     if(!CalUniqueTableForIdFindOrAdd(bddManager,
00240         bddManager->uniqueTable[CalBddGetBddId(f)],
00241         tempBdd, CalBddZero(bddManager), &result)){
00242       CalBddIcrRefCount(tempBdd);
00243     }
00244   }
00245   return (result);
00246 }

static Cal_Bdd_t BddSatisfySupportStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_BddId_t *  support 
) [static]

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

Name [BddSatisfySupportStep]

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 263 of file calBddSatisfy.c.

00267 {
00268   Cal_Bdd_t tempBdd;
00269   Cal_Bdd_t result;
00270 
00271   if(!*support){
00272     return BddSatisfyStep(bddManager, f);
00273   }
00274   if(CalBddGetBddIndex(bddManager, f) <= bddManager->idToIndex[*support]){
00275     if(CalBddGetBddId(f) == *support){
00276         ++support;
00277     }
00278     CalBddGetThenBdd(f, tempBdd);
00279     if(CalBddIsBddZero(bddManager, tempBdd)){
00280       CalBddGetElseBdd(f, tempBdd);
00281       tempBdd = BddSatisfySupportStep(bddManager, tempBdd, support);
00282       if(!CalUniqueTableForIdFindOrAdd(bddManager,
00283           bddManager->uniqueTable[CalBddGetBddId(f)],
00284           CalBddZero(bddManager), tempBdd, &result)){
00285         CalBddIcrRefCount(tempBdd);
00286       }
00287     }
00288     else{
00289       tempBdd = BddSatisfySupportStep(bddManager, tempBdd, support);
00290       if(!CalUniqueTableForIdFindOrAdd(bddManager,
00291           bddManager->uniqueTable[CalBddGetBddId(f)],
00292           tempBdd, CalBddZero(bddManager), &result)){
00293         CalBddIcrRefCount(tempBdd);
00294       }
00295     }
00296   }
00297   else{
00298     tempBdd = BddSatisfySupportStep(bddManager, f, support+1);
00299     if(!CalUniqueTableForIdFindOrAdd(bddManager,
00300         bddManager->uniqueTable[*support],
00301         CalBddZero(bddManager), tempBdd, &result)){
00302       CalBddIcrRefCount(tempBdd);
00303     }
00304   }
00305   return (result);
00306 }

Cal_Bdd Cal_BddSatisfy ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

AutomaticEnd Function********************************************************************

Name [Cal_BddSatisfy]

Synopsis [Returns a BDD which implies f, true for some valuation on which f is true, and which has at most one node at each level]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 97 of file calBddSatisfy.c.

00098 {
00099   Cal_Bdd_t f;
00100   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00101     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00102     if(CalBddIsBddZero(bddManager, f)){
00103       CalBddWarningMessage("Cal_BddSatisfy: argument is false");
00104       return (fUserBdd);
00105     }
00106     f = BddSatisfyStep(bddManager, f);
00107     return CalBddGetExternalBdd(bddManager, f);
00108   }
00109   return (Cal_Bdd) 0;
00110 }

double Cal_BddSatisfyingFraction ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

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

Synopsis [Returns the fraction of valuations which make f true. (Note that this fraction is independent of whatever set of variables f is supposed to be a function of)]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 179 of file calBddSatisfy.c.

00180 {
00181   double fraction;
00182   CalHashTable_t *hashTable;
00183   Cal_Bdd_t f;
00184   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00185     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00186     hashTable = CalHashTableOneInit(bddManager, sizeof(double));
00187     fraction = BddSatisfyingFractionStep(bddManager, f, hashTable);
00188     CalHashTableOneQuit(hashTable);
00189     return fraction;
00190   }
00191   return 0.0;
00192 }

Cal_Bdd Cal_BddSatisfySupport ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

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

Name [Cal_BddSatisfySupport]

Synopsis [Returns a special cube contained in f.]

Description [The returned BDD which implies f, is true for some valuation on which f is true, which has at most one node at each level, and which has exactly one node corresponding to each variable which is associated with something in the current variable association.]

SideEffects [required]

SeeAlso [optional]

Definition at line 131 of file calBddSatisfy.c.

00132 {
00133   Cal_BddId_t *support, *p;
00134   long i;
00135   Cal_Bdd_t result;
00136   Cal_Bdd_t f;
00137   
00138   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00139     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00140     if(CalBddIsBddZero(bddManager, f)){
00141       CalBddWarningMessage("Cal_BddSatisfySupport: argument is false");
00142       return (fUserBdd);
00143     }
00144     support = Cal_MemAlloc(Cal_BddId_t, bddManager->numVars+1);
00145     for(i = 1, p = support; i <= bddManager->numVars; i++){
00146       if(!CalBddIsBddNull(bddManager,
00147           bddManager->currentAssociation->varAssociation[i])){
00148         *p = bddManager->idToIndex[i];
00149         ++p;
00150       }
00151     }
00152     *p = 0;
00153     qsort(support, (unsigned)(p - support), sizeof(Cal_BddId_t), IndexCmp);
00154     while(p != support){
00155       --p;
00156       *p = bddManager->indexToId[*p];
00157     }
00158     result = BddSatisfySupportStep(bddManager, f, support);
00159     Cal_MemFree(support);
00160     return CalBddGetExternalBdd(bddManager, result);
00161   }
00162   return (Cal_Bdd) 0;
00163 }

static int IndexCmp ( const void *  p1,
const void *  p2 
) [static]

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

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 321 of file calBddSatisfy.c.

00322 {
00323   Cal_BddIndex_t i1, i2;
00324 
00325   i1 = *(Cal_BddId_t *)p1;
00326   i2 = *(Cal_BddId_t *)p2;
00327   if(i1 < i2){
00328     return (-1);
00329   }
00330   if(i1 > i2){
00331     return (1);
00332   }
00333   return (0);
00334 }

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