src/cmuBdd/bddsat.c File Reference

#include "bddint.h"
Include dependency graph for bddsat.c:

Go to the source code of this file.

Functions

void qsort (pointer, unsigned long, unsigned long, int(*)(const void *, const void *))
static bdd cmu_bdd_satisfy_step (cmu_bdd_manager bddm, bdd f)
bdd cmu_bdd_satisfy (cmu_bdd_manager bddm, bdd f)
static bdd cmu_bdd_satisfy_support_step (cmu_bdd_manager bddm, bdd f, bdd_indexindex_type *support)
static int index_cmp (pointer p1, pointer p2)
bdd cmu_bdd_satisfy_support (cmu_bdd_manager bddm, bdd f)
double cmu_bdd_satisfying_fraction_step (cmu_bdd_manager bddm, bdd f)
double cmu_bdd_satisfying_fraction (cmu_bdd_manager bddm, bdd f)

Function Documentation

bdd cmu_bdd_satisfy ( cmu_bdd_manager  bddm,
bdd  f 
)

Definition at line 41 of file bddsat.c.

00042 {
00043   if (bdd_check_arguments(1, f))
00044     {
00045       if (f == BDD_ZERO(bddm))
00046         {
00047           cmu_bdd_warning("cmu_bdd_satisfy: argument is false");
00048           return (f);
00049         }
00050       FIREWALL(bddm);
00051       RETURN_BDD(cmu_bdd_satisfy_step(bddm, f));
00052     }
00053   return ((bdd)0);
00054 }

static bdd cmu_bdd_satisfy_step ( cmu_bdd_manager  bddm,
bdd  f 
) [static]

Definition at line 14 of file bddsat.c.

00015 {
00016   bdd temp;
00017   bdd result;
00018 
00019   BDD_SETUP(f);
00020   if (BDD_IS_CONST(f))
00021     return (f);
00022   if (BDD_THEN(f) == BDD_ZERO(bddm))
00023     {
00024       temp=cmu_bdd_satisfy_step(bddm, BDD_ELSE(f));
00025       result=bdd_find(bddm, BDD_INDEXINDEX(f), BDD_ZERO(bddm), temp);
00026     }
00027   else
00028     {
00029       temp=cmu_bdd_satisfy_step(bddm, BDD_THEN(f));
00030       result=bdd_find(bddm, BDD_INDEXINDEX(f), temp, BDD_ZERO(bddm));
00031     }
00032   return (result);
00033 }

bdd cmu_bdd_satisfy_support ( cmu_bdd_manager  bddm,
bdd  f 
)

Definition at line 114 of file bddsat.c.

00115 {
00116   bdd_indexindex_type *support, *p;
00117   long i;
00118   bdd result;
00119 
00120   if (bdd_check_arguments(1, f))
00121     {
00122       if (f == BDD_ZERO(bddm))
00123         {
00124           cmu_bdd_warning("cmu_bdd_satisfy_support: argument is false");
00125           return (f);
00126         }
00127       support=(bdd_indexindex_type *)mem_get_block((bddm->vars+1)*sizeof(bdd));
00128       FIREWALL1(bddm,
00129                 if (retcode == BDD_ABORTED || retcode == BDD_OVERFLOWED)
00130                   {
00131                     mem_free_block((pointer)support);
00132                     return ((bdd)0);
00133                   }
00134                 );
00135       for (i=0, p=support; i < bddm->vars; ++i)
00136         if (bddm->curr_assoc->assoc[i+1])
00137           {
00138             *p=bddm->indexes[i+1];
00139             ++p;
00140           }
00141       *p=0;
00142       qsort((pointer)support, (unsigned)(p-support),
00143             sizeof(bdd_indexindex_type),
00144             (int (*)(const void *, const void *))index_cmp);
00145       while (p != support)
00146         {
00147           --p;
00148           *p=bddm->indexindexes[*p];
00149         }
00150       result=cmu_bdd_satisfy_support_step(bddm, f, support);
00151       mem_free_block((pointer)support);
00152       RETURN_BDD(result);
00153     }
00154   return ((bdd)0);
00155 }

static bdd cmu_bdd_satisfy_support_step ( cmu_bdd_manager  bddm,
bdd  f,
bdd_indexindex_type *  support 
) [static]

Definition at line 59 of file bddsat.c.

00060 {
00061   bdd temp;
00062   bdd result;
00063 
00064   BDD_SETUP(f);
00065   if (!*support)
00066     return (cmu_bdd_satisfy_step(bddm, f));
00067   if (BDD_INDEX(bddm, f) <= bddm->indexes[*support])
00068     {
00069       if (BDD_INDEXINDEX(f) == *support)
00070         ++support;
00071       if (BDD_THEN(f) == BDD_ZERO(bddm))
00072         {
00073           temp=cmu_bdd_satisfy_support_step(bddm, BDD_ELSE(f), support);
00074           result=bdd_find(bddm, BDD_INDEXINDEX(f), BDD_ZERO(bddm), temp);
00075         }
00076       else
00077         {
00078           temp=cmu_bdd_satisfy_support_step(bddm, BDD_THEN(f), support);
00079           result=bdd_find(bddm, BDD_INDEXINDEX(f), temp, BDD_ZERO(bddm));
00080         }
00081     }
00082   else
00083     {
00084       temp=cmu_bdd_satisfy_support_step(bddm, f, support+1);
00085       result=bdd_find(bddm, *support, BDD_ZERO(bddm), temp);
00086     }
00087   return (result);
00088 }

double cmu_bdd_satisfying_fraction ( cmu_bdd_manager  bddm,
bdd  f 
)

Definition at line 191 of file bddsat.c.

00192 {
00193   if (bdd_check_arguments(1, f))
00194     return (cmu_bdd_satisfying_fraction_step(bddm, f));
00195   return (0.0);
00196 }

double cmu_bdd_satisfying_fraction_step ( cmu_bdd_manager  bddm,
bdd  f 
)

Definition at line 159 of file bddsat.c.

00160 {
00161   union {
00162     long cache_result[2];
00163     double result;
00164   } u;
00165 
00166   BDD_SETUP(f);
00167   if (BDD_IS_CONST(f))
00168     {
00169       if (f == BDD_ZERO(bddm))
00170         return (0.0);
00171       return (1.0);
00172     }
00173   if (bdd_lookup_in_cache1d(bddm, OP_SATFRAC, f,
00174                             &(u.cache_result[0]), &(u.cache_result[1])))
00175     {
00176       return (u.result);
00177     }
00178   u.result=0.5*cmu_bdd_satisfying_fraction_step(bddm, BDD_THEN(f))+
00179     0.5*cmu_bdd_satisfying_fraction_step(bddm, BDD_ELSE(f));
00180   bdd_insert_in_cache1d(bddm, OP_SATFRAC, f, u.cache_result[0],
00181                         u.cache_result[1]);
00182   return (u.result);
00183 }

static int index_cmp ( pointer  p1,
pointer  p2 
) [static]

Definition at line 93 of file bddsat.c.

00094 {
00095   bdd_index_type i1, i2;
00096 
00097   i1= *(bdd_indexindex_type *)p1;
00098   i2= *(bdd_indexindex_type *)p2;
00099   if (i1 < i2)
00100     return (-1);
00101   if (i1 > i2)
00102     return (1);
00103   return (0);
00104 }

void qsort ( pointer  ,
unsigned  long,
unsigned  long,
int(*)(const void *, const void *)   
)
Generated on Tue Jan 12 13:57:15 2010 for glu-2.2 by  doxygen 1.6.1