glu-2.2: src/cmuBdd/bddsupport.c Source File

00001 /* BDD support routines */
00002 
00003 
00004 #include "bddint.h"
00005 
00006 
00007 static
00008 int
00009 cmu_bdd_depends_on_step(cmu_bdd_manager bddm, bdd f, bdd_index_type var_index, int mark)
00010 {
00011   bdd_index_type f_index;
00012 
00013   BDD_SETUP(f);
00014   f_index=BDD_INDEX(bddm, f);
00015   if (f_index > var_index)
00016     return (0);
00017   if (f_index == var_index)
00018     return (1);
00019   if (BDD_MARK(f) == mark)
00020     return (0);
00021   BDD_MARK(f)=mark;
00022   if (cmu_bdd_depends_on_step(bddm, BDD_THEN(f), var_index, mark))
00023     return (1);
00024   return (cmu_bdd_depends_on_step(bddm, BDD_ELSE(f), var_index, mark));
00025 }
00026 
00027 
00028 /* cmu_bdd_depends_on(bddm, f, var) returns 1 if f depends on var and */
00029 /* returns 0 otherwise. */
00030 
00031 int
00032 cmu_bdd_depends_on(cmu_bdd_manager bddm, bdd f, bdd var)
00033 {
00034   if (bdd_check_arguments(2, f, var))
00035     {
00036       BDD_SETUP(var);
00037       if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
00038         {
00039           cmu_bdd_warning("cmu_bdd_depends_on: second argument is not a positive variable");
00040           if (BDD_IS_CONST(var))
00041             return (1);
00042         }
00043       (void)cmu_bdd_depends_on_step(bddm, f, BDD_INDEX(bddm, var), 1);
00044       return (cmu_bdd_depends_on_step(bddm, f, BDD_INDEX(bddm, var), 0));
00045     }
00046   return (0);
00047 }
00048 
00049 
00050 static
00051 void
00052 bdd_unmark_nodes(cmu_bdd_manager bddm, bdd f)
00053 {
00054   bdd temp;
00055 
00056   BDD_SETUP(f);
00057   if (!BDD_MARK(f) || BDD_IS_CONST(f))
00058     return;
00059   BDD_MARK(f)=0;
00060   temp=BDD_IF(bddm, f);
00061   {
00062     BDD_SETUP(temp);
00063     BDD_MARK(temp)=0;
00064   }
00065   bdd_unmark_nodes(bddm, BDD_THEN(f));
00066   bdd_unmark_nodes(bddm, BDD_ELSE(f));
00067 }
00068 
00069 
00070 static
00071 bdd *
00072 cmu_bdd_support_step(cmu_bdd_manager bddm, bdd f, bdd *support)
00073 {
00074   bdd temp;
00075 
00076   BDD_SETUP(f);
00077   if (BDD_MARK(f) || BDD_IS_CONST(f))
00078     return (support);
00079   temp=BDD_IF(bddm, f);
00080   {
00081     BDD_SETUP(temp);
00082     if (!BDD_MARK(temp))
00083       {
00084         BDD_MARK(temp)=1;
00085         *support=temp;
00086         ++support;
00087       }
00088   }
00089   BDD_MARK(f)=1;
00090   support=cmu_bdd_support_step(bddm, BDD_THEN(f), support);
00091   return (cmu_bdd_support_step(bddm, BDD_ELSE(f), support));
00092 }
00093 
00094 
00095 /* cmu_bdd_support(bddm, f, support) returns the support of f as a */
00096 /* null-terminated array of variables. */
00097 
00098 void
00099 cmu_bdd_support(cmu_bdd_manager bddm, bdd f, bdd *support)
00100 {
00101   bdd *end;
00102 
00103   if (bdd_check_arguments(1, f))
00104     {
00105       end=cmu_bdd_support_step(bddm, f, support);
00106       *end=0;
00107       bdd_unmark_nodes(bddm, f);
00108     }
00109   else
00110     *support=0;
00111 }