Menu
▾
▴
[Javabdd-checkins] JavaBDD/net/sf/javabdd JFactory.java,1.13,1.14
|
From: John W. <joe...@us...> - 2005-01-31 10:09:11
|
Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24209/net/sf/javabdd Modified Files: JFactory.java Log Message: Small cleanups here and there. Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v retrieving revision 1.13 retrieving revision 1.14 diff -C2 -d -r1.13 -r1.14 *** JFactory.java 31 Jan 2005 00:05:17 -0000 1.13 --- JFactory.java 31 Jan 2005 10:08:59 -0000 1.14 *************** *** 72,77 **** int _index; - static final int INVALID_BDD = -1; - bdd(int index) { this._index = index; --- 72,75 ---- *************** *** 442,445 **** --- 440,445 ---- static final int MARK_MASK = 0x00200000; static final int LEV_MASK = 0x001FFFFF; + static final int MAXVAR = LEV_MASK; + static final int INVALID_BDD = -1; static final int REF_INC = 0x00400000; *************** *** 703,707 **** "Division by zero" }; - static final int MAXVAR = 0x1FFFFF; static final int DEFAULTMAXNODEINC = 50000; --- 703,706 ---- *************** *** 779,783 **** else if (r < 0 || r >= bddnodesize) bdd_error(BDD_ILLBDD); ! else if (r >= 2 && LOW(r) == -1) bdd_error(BDD_ILLBDD); } --- 778,782 ---- else if (r < 0 || r >= bddnodesize) bdd_error(BDD_ILLBDD); ! else if (r >= 2 && LOW(r) == INVALID_BDD) bdd_error(BDD_ILLBDD); } *************** *** 2377,2381 **** return; ! if (MARKED(r) || LOW(r) == -1) return; --- 2376,2380 ---- return; ! if (MARKED(r) || LOW(r) == INVALID_BDD) return; *************** *** 2645,2649 **** for (n = bddnodesize - 1; n >= 2; n--) { ! if (LOW(n) != -1) { int hash2; --- 2644,2648 ---- for (n = bddnodesize - 1; n >= 2; n--) { ! if (LOW(n) != INVALID_BDD) { int hash2; *************** *** 2897,2901 **** for (n = bddnodesize - 1; n >= 2; n--) { ! if (MARKED(n) && LOW(n) != -1) { int hash2; --- 2896,2900 ---- for (n = bddnodesize - 1; n >= 2; n--) { ! if (MARKED(n) && LOW(n) != INVALID_BDD) { int hash2; *************** *** 2905,2909 **** SETHASH(hash2, n); } else { ! SETLOW(n, -1); SETNEXT(n, bddfreepos); bddfreepos = n; --- 2904,2908 ---- SETHASH(hash2, n); } else { ! SETLOW(n, INVALID_BDD); SETNEXT(n, bddfreepos); bddfreepos = n; *************** *** 2936,2940 **** int bdd_addref(int root) { ! if (root == -1) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) --- 2935,2939 ---- int bdd_addref(int root) { ! if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) *************** *** 2942,2946 **** if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == -1) return bdd_error(BDD_ILLBDD); --- 2941,2945 ---- if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == INVALID_BDD) return bdd_error(BDD_ILLBDD); *************** *** 2951,2955 **** int bdd_delref(int root) { ! if (root == -1) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) --- 2950,2954 ---- int bdd_delref(int root) { ! if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) *************** *** 2957,2961 **** if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == -1) return bdd_error(BDD_ILLBDD); --- 2956,2960 ---- if (root >= bddnodesize) return bdd_error(BDD_ILLBDD); ! if (LOW(root) == INVALID_BDD) return bdd_error(BDD_ILLBDD); *************** *** 2974,2978 **** return; ! if (MARKED(i) || LOW(i) == -1) return; --- 2973,2977 ---- return; ! if (MARKED(i) || LOW(i) == INVALID_BDD) return; *************** *** 2983,3003 **** } - void bdd_mark_upto(int i, int level) { - - if (i < 2) - return; - - if (MARKED(i) || LOW(i) == -1) - return; - - if (LEVEL(i) > level) - return; - - SETMARK(i); - - bdd_mark_upto(LOW(i), level); - bdd_mark_upto(LOW(i), level); - } - void bdd_markcount(int i, int[] cou) { --- 2982,2985 ---- *************** *** 3005,3009 **** return; ! if (MARKED(i) || LOW(i) == -1) return; --- 2987,2991 ---- return; ! if (MARKED(i) || LOW(i) == INVALID_BDD) return; *************** *** 3020,3024 **** return; ! if (!MARKED(i) || LOW(i) == -1) return; UNMARK(i); --- 3002,3006 ---- return; ! if (!MARKED(i) || LOW(i) == INVALID_BDD) return; UNMARK(i); *************** *** 3028,3048 **** } - void bdd_unmark_upto(int i, int level2) { - - if (i < 2) - return; - - if (!MARKED(i)) - return; - - UNMARK(i); - - if (LEVEL(i) > level2) - return; - - bdd_unmark_upto(LOW(i), level2); - bdd_unmark_upto(HIGH(i), level2); - } - public static final boolean CACHESTATS = false; --- 3010,3013 ---- *************** *** 3181,3185 **** for (n = oldsize; n < bddnodesize; n++) { ! SETLOW(n, -1); //SETREFCOU(n, 0); //SETHASH(n, 0); --- 3146,3150 ---- for (n = oldsize; n < bddnodesize; n++) { ! SETLOW(n, INVALID_BDD); //SETREFCOU(n, 0); //SETHASH(n, 0); *************** *** 3215,3219 **** for (n = 0; n < bddnodesize; n++) { ! SETLOW(n, -1); //SETREFCOU(n, 0); //SETHASH(n, 0); --- 3180,3184 ---- for (n = 0; n < bddnodesize; n++) { ! SETLOW(n, INVALID_BDD); //SETREFCOU(n, 0); //SETHASH(n, 0); *************** *** 3510,3514 **** for (n = 0; n < cache.tablesize; n++) { int a = cache.table[n].a; ! if (a >= 0 && LOW(a) == -1) { cache.table[n].a = -1; } --- 3475,3479 ---- for (n = 0; n < cache.tablesize; n++) { int a = cache.table[n].a; ! if (a >= 0 && LOW(a) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 3522,3527 **** int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == -1 || ! LOW(((BddCacheDataI)cache.table[n]).res) == -1) { cache.table[n].a = -1; } --- 3487,3492 ---- int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == INVALID_BDD || ! LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 3535,3541 **** int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == -1 || ! (cache.table[n].b != 0 && LOW(cache.table[n].b) == -1) || ! LOW(((BddCacheDataI)cache.table[n]).res) == -1) { cache.table[n].a = -1; } --- 3500,3506 ---- int a = cache.table[n].a; if (a < 0) continue; ! if (LOW(a) == INVALID_BDD || ! (cache.table[n].b != 0 && LOW(cache.table[n].b) == INVALID_BDD) || ! LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 3550,3556 **** if (a < 0) continue; if (LOW(a) == -1 || ! LOW(cache.table[n].b) == -1 || ! LOW(cache.table[n].c) == -1 || ! LOW(((BddCacheDataI)cache.table[n]).res) == -1) { cache.table[n].a = -1; } --- 3515,3521 ---- if (a < 0) continue; if (LOW(a) == -1 || ! LOW(cache.table[n].b) == INVALID_BDD || ! LOW(cache.table[n].c) == INVALID_BDD || ! LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) { cache.table[n].a = -1; } *************** *** 5093,5097 **** DECREF(HIGH(r)); ! SETLOW(r, -1); SETNEXT(r, bddfreepos); bddfreepos = r; --- 5058,5062 ---- DECREF(HIGH(r)); ! SETLOW(r, INVALID_BDD); SETNEXT(r, bddfreepos); bddfreepos = r; *************** *** 5220,5224 **** DECREF(HIGH(r)); ! SETLOW(r, -1); SETNEXT(r, bddfreepos); bddfreepos = r; --- 5185,5189 ---- DECREF(HIGH(r)); ! SETLOW(r, INVALID_BDD); SETNEXT(r, bddfreepos); bddfreepos = r; *************** *** 5547,5551 **** } else { ! SETLOW(n, -1); SETNEXT(n, bddfreepos); bddfreepos = n; --- 5512,5516 ---- } else { ! SETLOW(n, INVALID_BDD); SETNEXT(n, bddfreepos); bddfreepos = n; *************** *** 5750,5754 **** for (n = 0; n < bddnodesize; n++) { ! if (LOW(n) != -1) { out.print( "[" --- 5715,5719 ---- for (n = 0; n < bddnodesize; n++) { ! if (LOW(n) != INVALID_BDD) { out.print( "[" |
