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

00001 #include "bddint.h"
00002 /*
00003  * Recursively determine if f is a cube. f is a cube if there is a single
00004  * path to the constant one.
00005  */
00006 int
00007 cmu_bdd_is_cube(struct bdd_manager_ *manager, struct bdd_ *f)
00008 {
00009   struct bdd_ *f0, *f1;
00010 
00011   BDD_SETUP(f);
00012   if (BDD_IS_CONST(f)){
00013     if (f == BDD_ZERO(manager)){
00014       cmu_bdd_fatal("cmu_bdd_is_cube called with 0");
00015     }
00016     else return 1;
00017   }
00018   BDD_COFACTOR(BDD_INDEXINDEX(f), f, f1, f0);
00019   
00020   /*
00021    * Exactly one branch of f must point to ZERO to be a cube.
00022    */
00023   if (f1 == BDD_ZERO(manager)) {
00024         return (cmu_bdd_is_cube(manager, f0));
00025   } else if (f0 == BDD_ZERO(manager)) {
00026         return (cmu_bdd_is_cube(manager, f1));
00027   } else { /* not a cube, because neither branch is zero */
00028         return 0;
00029   }
00030 }
00031