ROBDD Make and Build.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## ROBDD(Reduced Ordered Binary Decision Diagram)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Creating a ROBDD using Make and Build"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Make Function\n",
    "-  This is neccesary to reduce the tree while it is made.\n",
    "-  It takes input node in the form of the (i,l,h) tuple and returns exisiting node or else creates a new one.\n",
    "\n",
    "`node(u)<-make(self,i,l,h)`\n",
    "\n",
    "#### Build Function\n",
    "-  Recursive function which traverses through through your expression to create the Table for ROBDD\n",
    "-  Uses make to create or check for exisiting nodes\n",
    "-  Initialises with i=0 for the first node.\n",
    "\n",
    "`build(self,i=0)`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from ROBDD import ROBDD\n",
    "import time"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "# Quick and Easy print Table Function for ROBDDs\n",
    "def printROBDD(ROBDD):    \n",
    "    print('============================')\n",
    "    print('|  u  |  i  |   l  |   h  |')\n",
    "    print('============================')    \n",
    "    n = ROBDD.nNodes\n",
    "    for idx in range(0,n):\n",
    "        node = ROBDD.T[idx]       \n",
    "        print('   '+str(idx)+'     '+str(node[0])+'     '+str(node[1])+'     '+str(node[2])+'  ')\n",
    "        print('---------------------------')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Test Case 1 - Simple Test Case\n",
    "\n",
    "Create a ROBDD with 3 variables and the following equation:-\n",
    "\n",
    "`or(equiv(x0,x1),x2)`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Time Spent\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "0.00038153053690020896"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "start = time.clock()\n",
    "ROBDD1 = ROBDD(nVars = 3,switch = 0)\n",
    "print('Time Spent')\n",
    "time.clock() - start"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "============================\n",
      "|  u  |  i  |   l  |   h  |\n",
      "============================\n",
      "   0     4     -1     -1  \n",
      "---------------------------\n",
      "   1     4     -2     -2  \n",
      "---------------------------\n",
      "   2     2     0     1  \n",
      "---------------------------\n",
      "   3     1     1     2  \n",
      "---------------------------\n",
      "   4     1     2     1  \n",
      "---------------------------\n",
      "   5     0     3     4  \n",
      "---------------------------\n"
     ]
    }
   ],
   "source": [
    "# Display the table created by the ROBDD\n",
    "printROBDD(ROBDD1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Test Case 2 - Testing all the functions (and,or,implies,equiv and not)\n",
    "\n",
    "Create a ROBDD with 3 variables and the following equation:-\n",
    "\n",
    "`and(implies(not(x0),equiv(1,x1)),not(x2))`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Time Spent\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "0.00038646716122239105"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "start = time.clock()\n",
    "ROBDD2 = ROBDD(3,switch=2)\n",
    "print('Time Spent')\n",
    "time.clock() - start"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "============================\n",
      "|  u  |  i  |   l  |   h  |\n",
      "============================\n",
      "   0     4     -1     -1  \n",
      "---------------------------\n",
      "   1     4     -2     -2  \n",
      "---------------------------\n",
      "   2     2     1     0  \n",
      "---------------------------\n",
      "   3     1     0     2  \n",
      "---------------------------\n",
      "   4     0     3     2  \n",
      "---------------------------\n"
     ]
    }
   ],
   "source": [
    "printROBDD(ROBDD2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Test Case 3 - Increasing the Number of Variables\n",
    "Create a ROBDD with 8 variables and the following equation:-\n",
    "\n",
    "`and(and(and(x0,x1),and(x2,x3)),and(and(x4,x5),and(x6,x7)))`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Time Spent\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "0.0009256170604094727"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "start = time.clock()\n",
    "ROBDD3 = ROBDD(8,switch=3)\n",
    "print('Time Spent')\n",
    "time.clock() - start"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "============================\n",
      "|  u  |  i  |   l  |   h  |\n",
      "============================\n",
      "   0     9     -1     -1  \n",
      "---------------------------\n",
      "   1     9     -2     -2  \n",
      "---------------------------\n",
      "   2     7     0     1  \n",
      "---------------------------\n",
      "   3     6     0     2  \n",
      "---------------------------\n",
      "   4     5     0     3  \n",
      "---------------------------\n",
      "   5     4     0     4  \n",
      "---------------------------\n",
      "   6     3     0     5  \n",
      "---------------------------\n",
      "   7     2     0     6  \n",
      "---------------------------\n",
      "   8     1     0     7  \n",
      "---------------------------\n",
      "   9     0     0     8  \n",
      "---------------------------\n"
     ]
    }
   ],
   "source": [
    "printROBDD(ROBDD3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}