[Javabdd-checkins] JavaBDD/buddy/src kernel.c,1.5,1.6

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Update of /cvsroot/javabdd/JavaBDD/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22921/buddy/src

Modified Files:
	kernel.c 
Log Message:
Updates to buddy to support small (4 word) BDD nodes.

Index: kernel.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/kernel.c,v
retrieving revision 1.5
retrieving revision 1.6
diff -C2 -d -r1.5 -r1.6
*** kernel.c	17 Nov 2004 23:05:14 -0000	1.5
--- kernel.c	31 Jan 2005 10:03:20 -0000	1.6
***************
*** 213,227 ****
       
       for (n=0 ; n<bddnodesize ; n++) {
!        CLRLEVELREF(n);
!        LOW(n) = -1;
!        bddnodes[n].hash = 0;
!        bddnodes[n].next = n+1;
       }
!      bddnodes[bddnodesize-1].next = 0;
       
!      SETREF(0, MAXREF);
!      SETREF(1, MAXREF);
!      LOW(0) = HIGH(0) = 0;
!      LOW(1) = HIGH(1) = 1;
       
       if ((err=bdd_operator_init(cs)) < 0) {
--- 213,224 ----
       
       for (n=0 ; n<bddnodesize ; n++) {
!        INIT_NODE(n);
       }
!      SETNEXT(bddnodesize-1, 0);
       
!      SETMAXREF(0);
!      SETMAXREF(1);
!      SETLOW(0,0); SETHIGH(0,0);
!      SETLOW(1,1); SETHIGH(1,1);
       
       if ((err=bdd_operator_init(cs)) < 0) {
***************
*** 394,399 ****
        }
        
!       SETREF(bddvarset[bddvarnum*2], MAXREF);
!       SETREF(bddvarset[bddvarnum*2+1], MAXREF);
        bddlevel2var[bddvarnum] = bddvarnum;
        bddvar2level[bddvarnum] = bddvarnum;
--- 391,396 ----
        }
        
!       SETMAXREF(bddvarset[bddvarnum*2]);
!       SETMAXREF(bddvarset[bddvarnum*2+1]);
        bddlevel2var[bddvarnum] = bddvarnum;
        bddvar2level[bddvarnum] = bddvarnum;
***************
*** 731,735 ****
  char *bdd_versionstr(void)
  {
!    static char str[] = "BuDDy -  release " PACKAGE_VERSION;
     BUDDY_PROLOGUE;
     RETURN(str);
--- 728,732 ----
  char *bdd_versionstr(void)
  {
!    static char str[] = "BuDDy - release " PACKAGE_VERSION;
     BUDDY_PROLOGUE;
     RETURN(str);
***************
*** 944,947 ****
--- 941,945 ----
  BDD bdd_ithvar(int var)
  {
+    int res;
     BUDDY_PROLOGUE;
     ADD_ARG1(T_INT,var);
***************
*** 952,956 ****
     }
  
!    RETURN_BDD(bddvarset[var*2]);
  }
  
--- 950,955 ----
     }
  
!    res = bddvarset[var*2];
!    RETURN_BDD(res);
  }
  
***************
*** 972,975 ****
--- 971,975 ----
  BDD bdd_nithvar(int var)
  {
+    int res;
     BUDDY_PROLOGUE;
     ADD_ARG1(T_INT,var);
***************
*** 980,984 ****
     }
     
!    RETURN_BDD(bddvarset[var*2+1]);
  }
  
--- 980,985 ----
     }
     
!    res = bddvarset[var*2+1];
!    RETURN_BDD(res);
  }
  
***************
*** 1095,1109 ****
        register BddNode *node = &bddnodes[n];
  
!       if (LOWp(node) != -1)
        {
  	 register unsigned int hash;
  
  	 hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
! 	 node->next = bddnodes[hash].hash;
! 	 bddnodes[hash].hash = n;
        }
        else
        {
! 	 node->next = bddfreepos;
  	 bddfreepos = n;
  	 bddfreenum++;
--- 1096,1110 ----
        register BddNode *node = &bddnodes[n];
  
!       if (LOWp(node) != INVALID_BDD)
        {
  	 register unsigned int hash;
  
  	 hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
! 	 SETNEXTp(node, HASH(hash));
! 	 SETHASH(hash, n);
        }
        else
        {
! 	 SETNEXTpz(node, bddfreepos);
  	 bddfreepos = n;
  	 bddfreenum++;
***************
*** 1135,1141 ****
     for (n=0 ; n<bddnodesize ; n++)
     {
!       if (REF(n) > 0)
! 	 bdd_mark(n);
!       bddnodes[n].hash = 0;
     }
     
--- 1136,1141 ----
     for (n=0 ; n<bddnodesize ; n++)
     {
!       if (HASREF(n)) bdd_mark(n);
!       SETHASH(n, 0);
     }
     
***************
*** 1147,1151 ****
        register BddNode *node = &bddnodes[n];
  
!       if (MARKEDp(node)  &&  LOWp(node) != -1)
        {
  	 register unsigned int hash;
--- 1147,1151 ----
        register BddNode *node = &bddnodes[n];
  
!       if (MARKEDp(node)  &&  LOWp(node) != INVALID_BDD)
        {
  	 register unsigned int hash;
***************
*** 1153,1163 ****
           UNMARKp(node);
  	 hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
! 	 node->next = bddnodes[hash].hash;
! 	 bddnodes[hash].hash = n;
        }
        else
        {
! 	 LOWp(node) = -1;
! 	 node->next = bddfreepos;
  	 bddfreepos = n;
  	 bddfreenum++;
--- 1153,1163 ----
           UNMARKp(node);
  	 hash = NODEHASH(LEVELp(node), LOWp(node), HIGHp(node));
! 	 SETNEXTp(node, HASH(hash));
! 	 SETHASH(hash, n);
        }
        else
        {
! 	 SETLOWpz(node, INVALID_BDD); // obliterates refcount
! 	 SETNEXTpz(node, bddfreepos); // obliterates lev, mark
  	 bddfreepos = n;
  	 bddfreenum++;
***************
*** 1205,1209 ****
     if (root >= bddnodesize)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
!    if (LOW(root) == -1)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
  
--- 1205,1209 ----
     if (root >= bddnodesize)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
!    if (LOW(root) == INVALID_BDD)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
  
***************
*** 1233,1237 ****
     if (root >= bddnodesize)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
!    if (LOW(root) == -1)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
  
--- 1233,1237 ----
     if (root >= bddnodesize)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
!    if (LOW(root) == INVALID_BDD)
        RETURN_BDD(bdd_error(BDD_ILLBDD));
  
***************
*** 1257,1261 ****
  
     node = &bddnodes[i];
!    if (MARKEDp(node)  ||  LOWp(node) == -1)
        return;
     
--- 1257,1261 ----
  
     node = &bddnodes[i];
!    if (MARKEDp(node)  ||  LOWp(node) == INVALID_BDD)
        return;
     
***************
*** 1274,1278 ****
        return;
     
!    if (MARKEDp(node)  ||  LOWp(node) == -1)
        return;
     
--- 1274,1278 ----
        return;
     
!    if (MARKEDp(node)  ||  LOWp(node) == INVALID_BDD)
        return;
     
***************
*** 1295,1299 ****
  
     node = &bddnodes[i];
!    if (MARKEDp(node)  ||  LOWp(node) == -1)
        return;
     
--- 1295,1299 ----
  
     node = &bddnodes[i];
!    if (MARKEDp(node)  ||  LOWp(node) == INVALID_BDD)
        return;
     
***************
*** 1315,1319 ****
     node = &bddnodes[i];
  
!    if (!MARKEDp(node)  ||  LOWp(node) == -1)
        return;
     UNMARKp(node);
--- 1315,1319 ----
     node = &bddnodes[i];
  
!    if (!MARKEDp(node)  ||  LOWp(node) == INVALID_BDD)
        return;
     UNMARKp(node);
***************
*** 1364,1368 ****
        /* Try to find an existing node of this kind */
     hash = NODEHASH(level, low, high);
!    res = bddnodes[hash].hash;
  
     while(res != 0)
--- 1364,1368 ----
        /* Try to find an existing node of this kind */
     hash = NODEHASH(level, low, high);
!    res = HASH(hash);
  
     while(res != 0)
***************
*** 1376,1380 ****
        }
  
!       res = bddnodes[res].next;
  #ifdef CACHESTATS
        bddcachestats.uniqueChain++;
--- 1376,1380 ----
        }
  
!       res = NEXT(res);
  #ifdef CACHESTATS
        bddcachestats.uniqueChain++;
***************
*** 1419,1434 ****
        /* Build new node */
     res = bddfreepos;
!    bddfreepos = bddnodes[bddfreepos].next;
     bddfreenum--;
     bddproduced++;
     
!    node = &bddnodes[res];
!    SETLEVELp(node, level);
!    LOWp(node) = low;
!    HIGHp(node) = high;
!    
!       /* Insert node */
!    node->next = bddnodes[hash].hash;
!    bddnodes[hash].hash = res;
  
     return res;
--- 1419,1432 ----
        /* Build new node */
     res = bddfreepos;
!    bddfreepos = NEXT(bddfreepos);
     bddfreenum--;
     bddproduced++;
     
!    {
!        int next = HASH(hash);
!        CREATE_NODE(res, level, low, high, next);
!        /* Insert node */
!        SETHASH(hash, res);
!    }
  
     return res;
***************
*** 1461,1474 ****
     if (doRehash)
        for (n=0 ; n<oldsize ; n++)
! 	 bddnodes[n].hash = 0;
     
     for (n=oldsize ; n<bddnodesize ; n++)
     {
!       CLRLEVELREF(n);
!       bddnodes[n].hash = 0;
!       LOW(n) = -1;
!       bddnodes[n].next = n+1;
     }
!    bddnodes[bddnodesize-1].next = bddfreepos;
     bddfreepos = oldsize;
     bddfreenum += bddnodesize - oldsize;
--- 1459,1469 ----
     if (doRehash)
        for (n=0 ; n<oldsize ; n++)
! 	 SETHASH(n, 0);
     
     for (n=oldsize ; n<bddnodesize ; n++)
     {
!       INIT_NODE(n);
     }
!    SETNEXT(bddnodesize-1, bddfreepos);
     bddfreepos = oldsize;
     bddfreenum += bddnodesize - oldsize;