source: vis_dev/glu-2.3/src/calBdd/calBddSatisfy.c @ 36

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

library glu 2.3
File size: 11.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddSatisfy.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for BDD satisfying valuation.]
8             
9
10  Description [ ]
11
12  SeeAlso     [optional]
13
14  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
15               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
16              ]
17
18  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
19  All rights reserved.
20
21  Permission is hereby granted, without written agreement and without license
22  or royalty fees, to use, copy, modify, and distribute this software and its
23  documentation for any purpose, provided that the above copyright notice and
24  the following two paragraphs appear in all copies of this software.
25
26  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
27  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
28  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
29  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30
31  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
32  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
33  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
34  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
35  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
36
37  Revision    [$Id: calBddSatisfy.c,v 1.1.1.3 1998/05/04 00:58:53 hsv Exp $]
38
39******************************************************************************/
40
41#include "calInt.h"
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47/*---------------------------------------------------------------------------*/
48/* Type declarations                                                         */
49/*---------------------------------------------------------------------------*/
50
51/*---------------------------------------------------------------------------*/
52/* Stucture declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Variable declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Macro declarations                                                        */
61/*---------------------------------------------------------------------------*/
62
63
64/**AutomaticStart*************************************************************/
65
66/*---------------------------------------------------------------------------*/
67/* Static function prototypes                                                */
68/*---------------------------------------------------------------------------*/
69
70static Cal_Bdd_t BddSatisfyStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f);
71static Cal_Bdd_t BddSatisfySupportStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_BddId_t * support);
72static int IndexCmp(const void * p1, const void * p2);
73static double BddSatisfyingFractionStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, CalHashTable_t * hashTable);
74
75/**AutomaticEnd***************************************************************/
76
77/*---------------------------------------------------------------------------*/
78/* Definition of exported functions                                          */
79/*---------------------------------------------------------------------------*/
80
81/**Function********************************************************************
82
83  Name        [Cal_BddSatisfy]
84
85  Synopsis    [Returns a BDD which implies f, true for
86               some valuation on which f is true, and which has at most
87               one node at each level]
88
89  Description [optional]
90
91  SideEffects [required]
92
93  SeeAlso     [optional]
94
95******************************************************************************/
96Cal_Bdd
97Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd  fUserBdd)
98{
99  Cal_Bdd_t f;
100  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
101    f = CalBddGetInternalBdd(bddManager, fUserBdd);
102    if(CalBddIsBddZero(bddManager, f)){
103      CalBddWarningMessage("Cal_BddSatisfy: argument is false");
104      return (fUserBdd);
105    }
106    f = BddSatisfyStep(bddManager, f);
107    return CalBddGetExternalBdd(bddManager, f);
108  }
109  return (Cal_Bdd) 0;
110}
111
112
113/**Function********************************************************************
114
115  Name        [Cal_BddSatisfySupport]
116
117  Synopsis    [Returns a special cube contained in f.]
118
119  Description [The returned BDD which implies f, is true for some valuation on
120               which f is true, which has at most one node at each level,
121               and which has exactly one node corresponding to each variable
122               which is associated with something in the current variable
123               association.]
124
125  SideEffects [required]
126
127  SeeAlso     [optional]
128
129******************************************************************************/
130Cal_Bdd
131Cal_BddSatisfySupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
132{
133  Cal_BddId_t *support, *p;
134  long i;
135  Cal_Bdd_t result;
136  Cal_Bdd_t f;
137 
138  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
139    f = CalBddGetInternalBdd(bddManager, fUserBdd);
140    if(CalBddIsBddZero(bddManager, f)){
141      CalBddWarningMessage("Cal_BddSatisfySupport: argument is false");
142      return (fUserBdd);
143    }
144    support = Cal_MemAlloc(Cal_BddId_t, bddManager->numVars+1);
145    for(i = 1, p = support; i <= bddManager->numVars; i++){
146      if(!CalBddIsBddNull(bddManager,
147          bddManager->currentAssociation->varAssociation[i])){
148        *p = bddManager->idToIndex[i];
149        ++p;
150      }
151    }
152    *p = 0;
153    qsort(support, (unsigned)(p - support), sizeof(Cal_BddId_t), IndexCmp);
154    while(p != support){
155      --p;
156      *p = bddManager->indexToId[*p];
157    }
158    result = BddSatisfySupportStep(bddManager, f, support);
159    Cal_MemFree(support);
160    return CalBddGetExternalBdd(bddManager, result);
161  }
162  return (Cal_Bdd) 0;
163}
164
165/**Function********************************************************************
166
167  Synopsis    [Returns the fraction of valuations which make f true. (Note that
168  this fraction is independent of whatever set of variables f is supposed to be
169  a function of)]
170
171  Description [optional]
172
173  SideEffects [required]
174
175  SeeAlso     [optional]
176
177******************************************************************************/
178double
179Cal_BddSatisfyingFraction(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
180{
181  double fraction;
182  CalHashTable_t *hashTable;
183  Cal_Bdd_t f;
184  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
185    f = CalBddGetInternalBdd(bddManager, fUserBdd);
186    hashTable = CalHashTableOneInit(bddManager, sizeof(double));
187    fraction = BddSatisfyingFractionStep(bddManager, f, hashTable);
188    CalHashTableOneQuit(hashTable);
189    return fraction;
190  }
191  return 0.0;
192}
193
194/*---------------------------------------------------------------------------*/
195/* Definition of internal functions                                          */
196/*---------------------------------------------------------------------------*/
197
198/*---------------------------------------------------------------------------*/
199/* Definition of static functions                                            */
200/*---------------------------------------------------------------------------*/
201
202/**Function********************************************************************
203
204  Name        [BddSatisfyStep]
205
206  Synopsis    [Returns a BDD which implies f, is true for some valuation
207  on which f is true, and which has at most one node at each level]
208
209  Description [optional]
210
211  SideEffects [required]
212
213  SeeAlso     [optional]
214
215******************************************************************************/
216static Cal_Bdd_t
217BddSatisfyStep(
218  Cal_BddManager_t * bddManager,
219  Cal_Bdd_t  f)
220{
221  Cal_Bdd_t tempBdd;
222  Cal_Bdd_t result;
223
224  if(CalBddIsBddConst(f)){
225    return (f);
226  }
227  CalBddGetThenBdd(f, tempBdd);
228  if(CalBddIsBddZero(bddManager, tempBdd)){
229    CalBddGetElseBdd(f, tempBdd);
230    tempBdd = BddSatisfyStep(bddManager, tempBdd);
231    if(!CalUniqueTableForIdFindOrAdd(bddManager,
232        bddManager->uniqueTable[CalBddGetBddId(f)],
233        CalBddZero(bddManager), tempBdd, &result)){
234      CalBddIcrRefCount(tempBdd);
235    }
236  }
237  else{
238    tempBdd = BddSatisfyStep(bddManager, tempBdd);
239    if(!CalUniqueTableForIdFindOrAdd(bddManager,
240        bddManager->uniqueTable[CalBddGetBddId(f)],
241        tempBdd, CalBddZero(bddManager), &result)){
242      CalBddIcrRefCount(tempBdd);
243    }
244  }
245  return (result);
246}
247
248
249/**Function********************************************************************
250
251  Name        [BddSatisfySupportStep]
252
253  Synopsis    []
254
255  Description [optional]
256
257  SideEffects [required]
258
259  SeeAlso     [optional]
260
261******************************************************************************/
262static Cal_Bdd_t
263BddSatisfySupportStep(
264  Cal_BddManager_t * bddManager,
265  Cal_Bdd_t  f,
266  Cal_BddId_t * support)
267{
268  Cal_Bdd_t tempBdd;
269  Cal_Bdd_t result;
270
271  if(!*support){
272    return BddSatisfyStep(bddManager, f);
273  }
274  if(CalBddGetBddIndex(bddManager, f) <= bddManager->idToIndex[*support]){
275    if(CalBddGetBddId(f) == *support){
276        ++support;
277    }
278    CalBddGetThenBdd(f, tempBdd);
279    if(CalBddIsBddZero(bddManager, tempBdd)){
280      CalBddGetElseBdd(f, tempBdd);
281      tempBdd = BddSatisfySupportStep(bddManager, tempBdd, support);
282      if(!CalUniqueTableForIdFindOrAdd(bddManager,
283          bddManager->uniqueTable[CalBddGetBddId(f)],
284          CalBddZero(bddManager), tempBdd, &result)){
285        CalBddIcrRefCount(tempBdd);
286      }
287    }
288    else{
289      tempBdd = BddSatisfySupportStep(bddManager, tempBdd, support);
290      if(!CalUniqueTableForIdFindOrAdd(bddManager,
291          bddManager->uniqueTable[CalBddGetBddId(f)],
292          tempBdd, CalBddZero(bddManager), &result)){
293        CalBddIcrRefCount(tempBdd);
294      }
295    }
296  }
297  else{
298    tempBdd = BddSatisfySupportStep(bddManager, f, support+1);
299    if(!CalUniqueTableForIdFindOrAdd(bddManager,
300        bddManager->uniqueTable[*support],
301        CalBddZero(bddManager), tempBdd, &result)){
302      CalBddIcrRefCount(tempBdd);
303    }
304  }
305  return (result);
306}
307
308
309/**Function********************************************************************
310
311  Synopsis    []
312
313  Description [optional]
314
315  SideEffects [required]
316
317  SeeAlso     [optional]
318
319******************************************************************************/
320static int
321IndexCmp(const void * p1, const void * p2)
322{
323  Cal_BddIndex_t i1, i2;
324
325  i1 = *(Cal_BddId_t *)p1;
326  i2 = *(Cal_BddId_t *)p2;
327  if(i1 < i2){
328    return (-1);
329  }
330  if(i1 > i2){
331    return (1);
332  }
333  return (0);
334}
335
336/**Function********************************************************************
337
338  Synopsis    []
339
340  Description [optional]
341
342  SideEffects [required]
343
344  SeeAlso     [optional]
345
346******************************************************************************/
347static double
348BddSatisfyingFractionStep(
349  Cal_BddManager_t * bddManager,
350  Cal_Bdd_t  f,
351  CalHashTable_t * hashTable)
352{
353  double *resultPtr, result;
354  Cal_Bdd_t thenBdd, elseBdd;
355
356  if(CalBddIsBddConst(f)){
357    if(CalBddIsBddZero(bddManager, f)){
358      return 0.0;
359    }
360    return 1.0;
361  }
362  if(CalHashTableOneLookup(hashTable, f, (char **)&resultPtr)){
363    return (*resultPtr);
364  }
365  CalBddGetThenBdd(f, thenBdd);
366  CalBddGetElseBdd(f, elseBdd);
367  result = 
368      0.5 * BddSatisfyingFractionStep(bddManager, thenBdd, hashTable) +
369      0.5 * BddSatisfyingFractionStep(bddManager, elseBdd, hashTable);
370  CalHashTableOneInsert(hashTable, f, (char *)&result);
371  return (result);
372}
373
Note: See TracBrowser for help on using the repository browser.