BDD Ite(const BDD& g, const BDD& h, unsigned int limit = 0) const;

The variable order is the order in which variables are created. The first created variable is the least variable that sits highest in the BDD. The most recent created variable is the greatest variable that sits just above the terminals. Using such an order will match the ordering in CUDD, and it will match the expected (assumed) ordering for the bddToDot function.

The source is in a GIT repository which need to clone. The repository is located on the CS Open Lab under the egm account: ~egm/public-git/cs686/bdd-package. You must use GIT to clone the repository as well as to get updates and revisions throughout the semester. The GIT clone can be done as:

$ git clone ssh://_YOURID_@schizo.cs.byu.edu/~egm/public-git/cs686/bdd-package
   Cloning into 'bdd-package'...
   remote: Counting objects: 9, done.
   remote: Compressing objects: 100% (8/8), done.
   remote: Total 9 (delta 0), reused 0 (delta 0)
   Receiving objects: 100% (9/9), 8.15 KiB, done.

Please note that <user> should be your user name for the CS system. Also, some versions of GIT do not like the ~-expansion so you might need to include the full path to my home directory (/users/faculty/egm/public-git/cs431/lectures).

This source distribution will not compile and link out of the box as it is configured to use CUDD. You need to edit the Makefile to set any machine specific items that you may have including install location for CUDD. If you do not wish to use CUDD, then simply do not define USE_CUDD as explained in Makefile. You should now be able to issue make to build the bdd-test exectuble. Type the command:

   > make; bdd-test

1) Download and build the CUDD libraries (make clean; make; make testobj) (ftp://vlsi.colorado.edu/pub/cudd-2.5.0.tar.gz direct link).

2) Create a lib directory in the CUDD source directory.

3) Create symbolic links in the lib directory for the following libraries:

    > ln -s ../obj/libobj.a
    > ln -s ../cudd/libcudd.a
    > ln -s ../mtr/libmtr.a
    > ln -s ../util/libutil.a
    > ln -s ../st/libst.a
    > ln -s ../epd/libepd.a

4) Set the USE_CUDD variable to 1 in the Makefile 5) Set the CUDD variable to the source tree for your installation for CUDD 6) For OSX Mavericks with the latest version of Xcode, you will need to add -stdlib=libstdc++ to the CLFAGS when you try to link against the libraries using g++.

Using bddToDot is not mandatory for completing the homework. It is very possible to test your results by traversing your unique table and comparing to expected answers. If you would like to use it however, then please read on. When I made the choice to use C++ and CUDD rather than Java JBDD, I lost the simple functions f.getHigh() and f.getLow(); these are internal to CUDD and not available for public consumption. CUDD also does not have the “basic” cofactor that we discussed in class:

BDD basicCofactor(BDD f, int v, int pos) {
   if (v > f.getVariable()) {
      assert(0);
   }
   if (v == f.getVariable() && pos == 1) {
      return f.getHigh()
   }
   if (v == f.getVariable() && pos == 0) {
      return f.getLow()
   }
   return f;
}

CUDD does provide several versions of the more powerful cofactor that operates not on just a variable but any arbitrary function. One of these more powerful cofactor methods is restrict. The function f.Restrict(g) returns a new function that is f only variables in f are restricted to specific values which are those that make g true. If you call restrict as

BDD x = bddMgr.getVar(2);
f.Restrict(x);

The you get the function f with x set to true, which is a positive cofactor. f.Restrict(~x) is the negative cofactor. The Restrict method devolves into our basic cofactor if you only call it as suggested above (i.e., the answer is always either this.getLow(), this.getHigh(), or this). If you want to use bddToDot, then you need to add back into the interface the restrict function: BDD BDD::Restrict(BDD g) And implement that function in a manner similar to basic cofactor as below:

BDD Restrict(BDD g) {
   if (isOne() || isZero()) return *this; 
   int varIng = g.getVariable();
   int varInf = this.getVariable();
   BDD high = g.getHigh();
   BDD low = g.getLow();
   // Make sure g is a variable or a negated variable
   assert (high == bddMgr.getOne() || high == bddMgr.getZero());
   assert (low == bddMgr.getOne() || low == bddMgr.getZero());
   if (varIng > varInf) {
      assert(0);
   }
   if (varIng == varInf) {
      if (high == bddMgr.getOne())
         return this.getHigh();
      else 
         return this.getLow();
   }
   return *this;
}

The above code is only a template, and you will need to satisfy yourself that it is correct (or otherwise).

• 20 points: Ite Implementation
• 5 points: Using Ite to implement all Boolean connectives where apprioriate
• 15 points: Tests and documentation (implementation details and how to test your code). Your documentation can be a separate file or the body of your commit comment (see me for help with Git).

Please submit a patch to the original repository via the Homework 5 link in Learning Suite.