src/cmuBdd/bdd_is_cube.c File Reference

#include "bddint.h"

Include dependency graph for bdd_is_cube.c:

Go to the source code of this file.

Functions
int	cmu_bdd_is_cube (struct bdd_manager_ *manager, struct bdd_ *f)

---

Function Documentation

int cmu_bdd_is_cube	(	struct bdd_manager_ *	manager,
		struct bdd_ *	f
	)

Definition at line 7 of file bdd_is_cube.c.

{
  struct bdd_ *f0, *f1;

  BDD_SETUP(f);
  if (BDD_IS_CONST(f)){
    if (f == BDD_ZERO(manager)){
      cmu_bdd_fatal("cmu_bdd_is_cube called with 0");
    }
    else return 1;
  }
  BDD_COFACTOR(BDD_INDEXINDEX(f), f, f1, f0);
  
  /*
   * Exactly one branch of f must point to ZERO to be a cube.
   */
  if (f1 == BDD_ZERO(manager)) {
        return (cmu_bdd_is_cube(manager, f0));
  } else if (f0 == BDD_ZERO(manager)) {
        return (cmu_bdd_is_cube(manager, f1));
  } else { /* not a cube, because neither branch is zero */
        return 0;
  }
}