javabdd-checkins Mailing List for JavaBDD (Page 4)

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

Update of /cvsroot/javabdd/JavaBDD/net/sf/javabdd
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25939/net/sf/javabdd

Modified Files:
	JFactory.java 
Log Message:
Many fixes to dynamic variable reordering.

Index: JFactory.java
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/net/sf/javabdd/JFactory.java,v
retrieving revision 1.24
retrieving revision 1.25
diff -C2 -d -r1.24 -r1.25
*** JFactory.java	10 May 2005 02:54:35 -0000	1.24
--- JFactory.java	10 May 2005 21:16:00 -0000	1.25
***************
*** 3756,3761 ****
                  usednum_before = bddnodesize - bddfreenum;
          
!                 top.first = 0;
!                 top.last = bdd_varnum() - 1;
                  top.fixed = false;
                  top.interleaved = false;
--- 3756,3761 ----
                  usednum_before = bddnodesize - bddfreenum;
          
!                 top.firstVar = top.firstLevel = 0;
!                 top.lastVar = top.lastLevel = bdd_varnum() - 1;
                  top.fixed = false;
                  top.interleaved = false;
***************
*** 3779,3787 ****
          BddTree t = new BddTree();
  
!         t.first = t.last = -1;
          t.fixed = true;
!         t.interleaved = false;
!         t.next = t.prev = t.nextlevel = null;
!         t.seq = null;
          t.id = id;
          return t;
--- 3779,3787 ----
          BddTree t = new BddTree();
  
!         t.firstVar = t.lastVar = t.firstLevel = t.lastLevel = -1;
          t.fixed = true;
!         //t.interleaved = false;
!         //t.next = t.prev = t.nextlevel = null;
!         //t.seq = null;
          t.id = id;
          return t;
***************
*** 3825,3830 ****
  
          if (t.seq != null) {
!             //Arrays.sort(t.seq, 0, t.last-t.first + 1);
!             varseq_qsort(t.seq, 0, t.last-t.first + 1);
          }
  
--- 3825,3832 ----
  
          if (t.seq != null) {
!             //Arrays.sort(t.seq, 0, t.lastVar-t.firstVar + 1);
!             varseq_qsort(t.seq, 0, t.lastVar-t.firstVar + 1);
!             t.firstLevel = bddvar2level[t.seq[0]];
!             t.lastLevel = bddvar2level[t.seq[t.lastVar-t.firstVar]];
          }
  
***************
*** 4302,4307 ****
  
              /* Accumulate number of nodes for each block */
              p[n].val = 0;
!             for (v = dis.first; v <= dis.last; v++)
                  p[n].val -= levels[v].nodenum;
  
--- 4304,4310 ----
  
              /* Accumulate number of nodes for each block */
+             p[n] = new sizePair();
              p[n].val = 0;
!             for (v = dis.firstVar; v <= dis.lastVar; v++)
                  p[n].val -= levels[v].nodenum;
  
***************
*** 4364,4374 ****
      }
      
!     protected BddTree reverseDomain0(BDDDomain d) {
          int n = d.varNum();
          BddTree[] trees = new BddTree[n];
!         for (int i = 0; i < n; ++i) {
!             int v = d.ivar[i];
              addVarBlock(v, v, true);
              trees[i] = getBlock(vartree, v, v);
          }
          for (int i = 0; i < n; ++i) {
--- 4367,4385 ----
      }
      
!     protected void reverseDomain0(BDDDomain d) {
          int n = d.varNum();
          BddTree[] trees = new BddTree[n];
!         int v = d.ivar[0];
!         addVarBlock(v, v, true);
!         trees[0] = getBlock(vartree, v, v);
!         BddTree parent = getParent(trees[0]);
!         for (int i = 1; i < n; ++i) {
!             v = d.ivar[i];
              addVarBlock(v, v, true);
              trees[i] = getBlock(vartree, v, v);
+             BddTree parent2 = getParent(trees[i]);
+             if (parent != parent2) {
+                 throw new BDDException();
+             }
          }
          for (int i = 0; i < n; ++i) {
***************
*** 4377,4381 ****
              }
          }
!         return trees[n-1];
      }
      
--- 4388,4395 ----
              }
          }
!         BddTree newchild = trees[n-1];
!         while (newchild.prev != null) newchild = newchild.prev;
!         if (parent == null) vartree = newchild;
!         else parent.nextlevel = newchild;
      }
      
***************
*** 4438,4442 ****
       * @param domains  domain order
       */
!     public BddTree setVarOrder(List domains) {
          BddTree[] my_vartree = new BddTree[fdvarnum];
          boolean[] interleaved = new boolean[fdvarnum];
--- 4452,4456 ----
       * @param domains  domain order
       */
!     public void setVarOrder(List domains) {
          BddTree[] my_vartree = new BddTree[fdvarnum];
          boolean[] interleaved = new boolean[fdvarnum];
***************
*** 4451,4455 ****
                  int low = d.ivar[0];
                  int high = d.ivar[d.ivar.length-1];
!                 addVarBlock(low, high, false);
                  BddTree b = getBlock(vartree, low, high);
                  my_vartree[k] = b;
--- 4465,4469 ----
                  int low = d.ivar[0];
                  int high = d.ivar[d.ivar.length-1];
!                 bdd_intaddvarblock(low, high, false);
                  BddTree b = getBlock(vartree, low, high);
                  my_vartree[k] = b;
***************
*** 4458,4461 ****
--- 4472,4482 ----
              }
          }
+         if (k <= 1) return;
+         BddTree parent = getParent(my_vartree[0]);
+         for (int i = 0; i < k; ++i) {
+             if (parent != getParent(my_vartree[i])) {
+                 throw new BDDException("var block "+my_vartree[i].firstVar+".."+my_vartree[i].lastVar+" is in wrong place in tree");
+             }
+         }
          reorder_init();
          BddTree prev = null; boolean prev_interleaved = false;
***************
*** 4465,4483 ****
                  blockdown(t.prev);
              }
              if (prev_interleaved) {
                  blockinterleave(t.prev);
              }
!             prev = t;
!             prev_interleaved = interleaved[i];
          }
          reorder_done();
-         return my_vartree[0];
      }
      
!     BddTree getBlock(BddTree t, int low, int high) {
          if (t == null) return null;
          for (BddTree p = t; p != null; p = p.next) {
!             if (p.first == low && p.last == high) return p;
!             BddTree q = getBlock(t.nextlevel, low, high);
              if (q != null) return q;
          }
--- 4486,4531 ----
                  blockdown(t.prev);
              }
+             boolean inter = interleaved[i];
              if (prev_interleaved) {
                  blockinterleave(t.prev);
+                 //++i;
+                 prev = t.prev;
+             } else {
+                 prev = t;
              }
!             prev_interleaved = inter;
          }
+         BddTree newchild = my_vartree[0];
+         _assert(newchild.prev == null);
+         //while (newchild.prev != null) newchild = newchild.prev;
+         if (parent == null) vartree = newchild;
+         else parent.nextlevel = newchild;
          reorder_done();
      }
      
!     protected BddTree getParent(BddTree child) {
!         for (BddTree p = vartree; p != null; p = p.next) {
!             if (p == child) return null;
!             BddTree q = getParent(p, child);
!             if (q != null) return q;
!         }
!         throw new BDDException("Cannot find tree node "+child);
!     }
!     
!     protected BddTree getParent(BddTree parent, BddTree child) {
!         if (parent.nextlevel == null) return null;
!         for (BddTree p = parent.nextlevel; p != null; p = p.next) {
!             if (p == child) return parent;
!             BddTree q = getParent(p, child);
!             if (q != null) return q;
!         }
!         return null;
!     }
!     
!     protected BddTree getBlock(BddTree t, int low, int high) {
          if (t == null) return null;
          for (BddTree p = t; p != null; p = p.next) {
!             if (p.firstVar == low && p.lastVar == high) return p;
!             BddTree q = getBlock(p.nextlevel, low, high);
              if (q != null) return q;
          }
***************
*** 4489,4494 ****
          //System.out.println("Interleaving "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.last - left.first;
!         int rightsize = right.last - right.first;
          int[] lseq = left.seq;
          int[] rseq = right.seq;
--- 4537,4542 ----
          //System.out.println("Interleaving "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.lastVar - left.firstVar;
!         int rightsize = right.lastVar - right.firstVar;
          int[] lseq = left.seq;
          int[] rseq = right.seq;
***************
*** 4504,4508 ****
                  BddTree t = left.prev;
                  if (t == null || !t.interleaved) break outer;
!                 int tsize = t.last - t.first;
                  if (n <= tsize) {
                      int[] tseq = t.seq;
--- 4552,4556 ----
                  BddTree t = left.prev;
                  if (t == null || !t.interleaved) break outer;
!                 int tsize = t.lastVar - t.firstVar;
                  if (n <= tsize) {
                      int[] tseq = t.seq;
***************
*** 4514,4518 ****
              }
          }
!         left.interleaved = true;
      }
      
--- 4562,4571 ----
              }
          }
!         right.next.prev = left;
!         left.next = right.next;
!         left.firstVar = Math.min(left.firstVar, right.firstVar);
!         left.lastVar = Math.max(left.lastVar, right.lastVar);
!         left.seq = new int[left.lastVar - left.firstVar + 1];
!         update_seq(left);
      }
      
***************
*** 4521,4526 ****
          //System.out.println("Swapping "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.last - left.first;
!         int rightsize = right.last - right.first;
          int leftstart = bddvar2level[left.seq[0]];
          int[] lseq = left.seq;
--- 4574,4579 ----
          //System.out.println("Swapping "+left.first+".."+left.last+" and "+right.first+".."+right.last);
          int n;
!         int leftsize = left.lastVar - left.firstVar;
!         int rightsize = right.lastVar - right.firstVar;
          int leftstart = bddvar2level[left.seq[0]];
          int[] lseq = left.seq;
***************
*** 4571,4574 ****
--- 4624,4632 ----
          left.interleaved = false;
          right.interleaved = false;
+         
+         left.firstLevel = bddvar2level[lseq[0]];
+         left.lastLevel = bddvar2level[lseq[leftsize]];
+         right.firstLevel = bddvar2level[rseq[0]];
+         right.lastLevel = bddvar2level[rseq[rightsize]];
      }
  
***************
*** 5061,5065 ****
  
      static class BddTree {
!         int first, last; /* First and last variable in this block */
          int pos; /* Sifting position */
          int[] seq; /* Sequence of first...last in the current order */
--- 5119,5124 ----
  
      static class BddTree {
!         int firstVar, lastVar; /* First and last variable in this block */
!         int firstLevel, lastLevel; /* First and last level in this block */
          int pos; /* Sifting position */
          int[] seq; /* Sequence of first...last in the current order */
***************
*** 5361,5364 ****
--- 5420,5431 ----
                  int next = NEXT(r);
  
+ /***
+                 if (LOW(r) == -1) {
+                     System.out.println(r+": LOW="+LOW(r));
+                 }
+                 if (HIGH(r) == -1) {
+                     System.out.println(r+": HIGH="+HIGH(r));
+                 }
+ ***/
                  if (VARr(LOW(r)) != var1 && VARr(HIGH(r)) != var1) {
                      /* Node does not depend on next var, let it stay in the chain */
***************
*** 6332,6339 ****
          if (t == null) {
              t = bddtree_new(id);
!             t.first = first;
              t.fixed = fixed;
              t.seq = new int[last - first + 1];
!             t.last = last;
              update_seq(t);
              t.prev = prev;
--- 6399,6408 ----
          if (t == null) {
              t = bddtree_new(id);
!             t.firstVar = first;
!             t.firstLevel = bddvar2level[first];
              t.fixed = fixed;
              t.seq = new int[last - first + 1];
!             t.lastVar = last;
!             t.lastLevel = bddvar2level[last];
              update_seq(t);
              t.prev = prev;
***************
*** 6342,6350 ****
  
          /* Check for identity */
!         if (first == t.first && last == t.last)
              return t;
  
          /* Inside this section -> insert in next level */
!         if (first >= t.first && last <= t.last) {
              t.nextlevel =
                  bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id);
--- 6411,6422 ----
  
          /* Check for identity */
!         if (first == t.firstVar && last == t.lastVar)
              return t;
  
+         int firstLev = Math.min(bddvar2level[first], bddvar2level[last]);
+         int lastLev = Math.max(bddvar2level[first], bddvar2level[last]);
+         
          /* Inside this section -> insert in next level */
!         if (firstLev >= t.firstLevel && lastLev <= t.lastLevel) {
              t.nextlevel =
                  bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id);
***************
*** 6353,6360 ****
  
          /* Before this section -> insert */
!         if (last < t.first) {
              BddTree tnew = bddtree_new(id);
!             tnew.first = first;
!             tnew.last = last;
              tnew.fixed = fixed;
              tnew.seq = new int[last - first + 1];
--- 6425,6434 ----
  
          /* Before this section -> insert */
!         if (lastLev < t.firstLevel) {
              BddTree tnew = bddtree_new(id);
!             tnew.firstVar = first;
!             tnew.firstLevel = firstLev;
!             tnew.lastVar = last;
!             tnew.lastLevel = lastLev;
              tnew.fixed = fixed;
              tnew.seq = new int[last - first + 1];
***************
*** 6367,6371 ****
  
          /* After this this section -> go to next */
!         if (first > t.last) {
              t.next = bddtree_addrange_rec(t.next, t, first, last, fixed, id);
              return t;
--- 6441,6445 ----
  
          /* After this this section -> go to next */
!         if (firstLev > t.lastLevel) {
              t.next = bddtree_addrange_rec(t.next, t, first, last, fixed, id);
              return t;
***************
*** 6373,6377 ****
  
          /* Covering this section -> insert above this level */
!         if (first <= t.first) {
              BddTree tnew;
              BddTree dis = t;
--- 6447,6451 ----
  
          /* Covering this section -> insert above this level */
!         if (firstLev <= t.firstLevel) {
              BddTree tnew;
              BddTree dis = t;
***************
*** 6379,6389 ****
              while (true) {
                  /* Partial cover ->error */
!                 if (last >= dis.first && last < dis.last)
                      return null;
  
!                 if (dis.next == null || last < dis.next.first) {
                      tnew = bddtree_new(id);
!                     tnew.first = first;
!                     tnew.last = last;
                      tnew.fixed = fixed;
                      tnew.seq = new int[last - first + 1];
--- 6453,6465 ----
              while (true) {
                  /* Partial cover ->error */
!                 if (lastLev >= dis.firstLevel && lastLev < dis.lastLevel)
                      return null;
  
!                 if (dis.next == null || last < dis.next.firstLevel) {
                      tnew = bddtree_new(id);
!                     tnew.firstVar = first;
!                     tnew.firstLevel = firstLev;
!                     tnew.lastVar = last;
!                     tnew.lastLevel = lastLev;
                      tnew.fixed = fixed;
                      tnew.seq = new int[last - first + 1];
***************
*** 6409,6420 ****
      void update_seq(BddTree t) {
          int n;
!         int low = t.first;
  
!         for (n = t.first; n <= t.last; n++)
              if (bddvar2level[n] < bddvar2level[low])
                  low = n;
  
!         for (n = t.first; n <= t.last; n++)
              t.seq[bddvar2level[n] - bddvar2level[low]] = n;
      }
  
--- 6485,6503 ----
      void update_seq(BddTree t) {
          int n;
!         int low = t.firstVar;
!         int high = t.lastVar;
  
!         for (n = t.firstVar; n <= t.lastVar; n++) {
              if (bddvar2level[n] < bddvar2level[low])
                  low = n;
+             if (bddvar2level[n] > bddvar2level[high])
+                 high = n;
+         }
  
!         for (n = t.firstVar; n <= t.lastVar; n++)
              t.seq[bddvar2level[n] - bddvar2level[low]] = n;
+         
+         t.firstLevel = bddvar2level[low];
+         t.lastLevel = bddvar2level[high];
      }

2003	Jan	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov	Dec (4)
2004	Jan	Feb	Mar (6)	Apr (6)	May (4)	Jun (31)	Jul (64)	Aug (19)	Sep (28)	Oct (50)	Nov (25)	Dec
2005	Jan (44)	Feb (8)	Mar (2)	Apr (15)	May (48)	Jun (8)	Jul (7)	Aug	Sep (1)	Oct (3)	Nov	Dec
2006	Jan	Feb	Mar	Apr	May (1)	Jun (2)	Jul (14)	Aug	Sep	Oct	Nov (6)	Dec (4)
2007	Jan	Feb	Mar (2)	Apr	May	Jun (1)	Jul	Aug	Sep	Oct	Nov	Dec
2010	Jan	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct (1)	Nov (1)	Dec
2011	Jan	Feb (2)	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov (1)	Dec
2019	Jan	Feb	Mar	Apr (1)	May	Jun	Jul	Aug	Sep	Oct	Nov	Dec

javabdd-checkins Mailing List for JavaBDD (Page 4)

javabdd-checkins — CVS updates. High traffic.