Menu
▾
▴
[Javabdd-checkins] JavaBDD/org/sf/javabdd JFactory.java,1.10,1.11 CALFactory.java,1.6,1.7 BuDDyFactory.java,1.36,1.37 BDDFactory.java,1.29,1.30 BDD.java,1.37,1.38 TypedBDDFactory.java,1.20,1.21 TestBDDFactory.java,1.13,1.14 JDDFactory.java,1.7,1.8 CUDDFactory.java,1.18,1.19 BDDDomain.java,1.18,1.19
|
From: John W. <joe...@us...> - 2004-10-14 19:48:00
|
Update of /cvsroot/javabdd/JavaBDD/org/sf/javabdd In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20226/org/sf/javabdd Modified Files: JFactory.java CALFactory.java BuDDyFactory.java BDDFactory.java BDD.java TypedBDDFactory.java TestBDDFactory.java JDDFactory.java CUDDFactory.java BDDDomain.java Log Message: Updates to prepare for release. BDDDomains now use BigIntegers. Index: BDD.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDD.java,v retrieving revision 1.37 retrieving revision 1.38 diff -C2 -d -r1.37 -r1.38 *** BDD.java 12 Oct 2004 20:40:17 -0000 1.37 --- BDD.java 14 Oct 2004 19:47:36 -0000 1.38 *************** *** 1,2 **** --- 1,5 ---- + // BDD.java, created Jan 29, 2003 9:50:57 PM by jwhaley + // Copyright (C) 2003 John Whaley + // Licensed under the terms of the GNU LGPL; see COPYING for details. package org.sf.javabdd; *************** *** 352,360 **** * in var, and constant false if they are included in their negative form.</p> * * <p>Compare to bdd_restrict.</p> * * @param var BDD containing the variables to be restricted * @return the result of the restrict operation ! * @see org.sf.javabdd.BDDDomain#set() */ public abstract BDD restrict(BDD var); --- 355,366 ---- * in var, and constant false if they are included in their negative form.</p> * + * <p><i>Note that this is quite different than Coudert and Madre's restrict + * function.</i></p> + * * <p>Compare to bdd_restrict.</p> * * @param var BDD containing the variables to be restricted * @return the result of the restrict operation ! * @see org.sf.javabdd.BDD#simplify(BDD) */ public abstract BDD restrict(BDD var); *************** *** 366,369 **** --- 372,378 ---- * their negative form. The "that" BDD is consumed, and can no longer be used.</p> * + * <p><i>Note that this is quite different than Coudert and Madre's restrict + * function.</i></p> + * * <p>Compare to bdd_restrict and bdd_delref.</p> * *************** *** 397,401 **** /** ! * <p>Returns the result of applying the binary operator opr to the two BDDs.</p> * * <p>Compare to bdd_apply.</p> --- 406,411 ---- /** ! * <p>Returns the result of applying the binary operator <tt>opr</tt> to the ! * two BDDs.</p> * * <p>Compare to bdd_apply.</p> *************** *** 408,414 **** /** ! * <p>Makes this BDD be the result of the binary operator opr of two BDDs. The ! * "that" BDD is consumed, and can no longer be used. Attempting to use the ! * passed in BDD again will result in an exception being thrown.</p> * * <p>Compare to bdd_apply and bdd_delref.</p> --- 418,424 ---- /** ! * <p>Makes this BDD be the result of the binary operator <tt>opr</tt> of two ! * BDDs. The "that" BDD is consumed, and can no longer be used. Attempting ! * to use the passed in BDD again will result in an exception being thrown.</p> * * <p>Compare to bdd_apply and bdd_delref.</p> *************** *** 420,425 **** /** ! * <p>Applies the binary operator opr to two BDDs and then performs a universal ! * quantification of the variables from the variable set var.</p> * * <p>Compare to bdd_appall.</p> --- 430,436 ---- /** ! * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs a ! * universal quantification of the variables from the variable set ! * <tt>var</tt>.</p> * * <p>Compare to bdd_appall.</p> *************** *** 434,439 **** /** ! * <p>Applies the binary operator opr to two BDDs and then performs an ! * existential quantification of the variables from the variable set var.</p> * * <p>Compare to bdd_appex.</p> --- 445,451 ---- /** ! * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs ! * an existential quantification of the variables from the variable set ! * <tt>var</tt>.</p> * * <p>Compare to bdd_appex.</p> *************** *** 448,453 **** /** ! * <p>Applies the binary operator opr to two BDDs and then performs a unique ! * quantification of the variables from the variable set var.</p> * * <p>Compare to bdd_appuni.</p> --- 460,466 ---- /** ! * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs ! * a unique quantification of the variables from the variable set ! * <tt>var</tt>.</p> * * <p>Compare to bdd_appuni.</p> *************** *** 463,467 **** /** * <p>Finds one satisfying variable assignment. Finds a BDD with at most one ! * variable at each levels. The new BDD implies this BDD and is not false * unless this BDD is false.</p> * --- 476,480 ---- /** * <p>Finds one satisfying variable assignment. Finds a BDD with at most one ! * variable at each level. The new BDD implies this BDD and is not false * unless this BDD is false.</p> * *************** *** 485,493 **** /** * <p>Finds one satisfying variable assignment. Finds a minterm in this BDD. ! * The var argument is a set of variables that must be mentioned in the ! * result. The polarity of these variables in the result -- in case they ! * are undefined in this BDD, are defined by the pol parameter. If pol is ! * the false BDD then all variables will be in negative form, and otherwise ! * they will be in positive form.</p> * * <p>Compare to bdd_satoneset.</p> --- 498,506 ---- /** * <p>Finds one satisfying variable assignment. Finds a minterm in this BDD. ! * The <tt>var</tt> argument is a set of variables that must be mentioned in ! * the result. The polarity of these variables in the result - in case they ! * are undefined in this BDD - are defined by the <tt>pol</tt> parameter. ! * If <tt>pol</tt> is false, then all variables will be in negative form. ! * Otherwise they will be in positive form.</p> * * <p>Compare to bdd_satoneset.</p> *************** *** 496,501 **** * @param pol the polarity of the result * @return one satisfying variable assignment */ ! public abstract BDD satOne(BDD var, BDD pol); /** --- 509,515 ---- * @param pol the polarity of the result * @return one satisfying variable assignment + * @see org.sf.javabdd.BDDDomain#set() */ ! public abstract BDD satOne(BDD var, boolean pol); /** *************** *** 544,548 **** /** * <p>Scans this BDD and copies the stored variables into a integer array of ! * variable numbers. The numbers returned are guaranteed to be in * ascending order.</p> * --- 558,562 ---- /** * <p>Scans this BDD and copies the stored variables into a integer array of ! * BDDDomain variable numbers. The numbers returned are guaranteed to be in * ascending order.</p> * *************** *** 598,603 **** /** ! * <p>Finds one satisfying assignment of the domain d in this BDD and returns ! * that value.</p> * * <p>Compare to fdd_scanvar.</p> --- 612,617 ---- /** ! * <p>Finds one satisfying assignment of the domain <tt>d</tt> in this BDD ! * and returns that value.</p> * * <p>Compare to fdd_scanvar.</p> *************** *** 615,621 **** /** ! * <p>Finds one satisfying assignment in this BDD of all the defined FDD ! * variables. Each value is stored in an array which is returned. The size ! * of this array is exactly the number of FDD variables defined.</p> * * <p>Compare to fdd_scanallvar.</p> --- 629,635 ---- /** ! * <p>Finds one satisfying assignment in this BDD of all the defined ! * BDDDomain's. Each value is stored in an array which is returned. The size ! * of this array is exactly the number of BDDDomain's defined.</p> * * <p>Compare to fdd_scanallvar.</p> *************** *** 671,674 **** --- 685,694 ---- } + /** + * Utility function to convert from a BDD varset to an array of levels. + * + * @param r BDD varset + * @return array of levels + */ static int[] varset2levels(BDD r) { int size = 0; *************** *** 696,703 **** /** * <p>Returns an iteration of the satisfying assignments of this BDD. Returns ! * an iteration of minterms. The var argument is the set of variables that ! * will be mentioned in the result.</p> * * @return an iteration of minterms */ public BDDIterator iterator(final BDD var) { --- 716,725 ---- /** * <p>Returns an iteration of the satisfying assignments of this BDD. Returns ! * an iteration of minterms. The <tt>var</tt> argument is the set of variables ! * that will be mentioned in the result.</p> * + * @param var set of variables to mention in result * @return an iteration of minterms + * @see org.sf.javabdd.BDDDomain#set() */ public BDDIterator iterator(final BDD var) { *************** *** 705,715 **** } public static class BDDIterator implements Iterator { ! BDDFactory factory; ! int[] levels; ! boolean[] values; ! BDD[] nodes = null; ! boolean more = false; public BDDIterator(BDD dis, BDD var){ factory = dis.getFactory(); --- 727,751 ---- } + /** + * <p>BDDIterator is used to iterate through the satisfying assignments of a BDD. + * It includes the ability to check if bits are dont-cares and skip them.</p> + * + * @author jwhaley + * @version $Id$ + */ public static class BDDIterator implements Iterator { ! protected BDDFactory factory; ! protected int[] levels; ! protected boolean[] values; ! protected BDD[] nodes = null; ! protected boolean more = false; + /** + * <p>Construct a new BDDIterator on the given BDD. The <tt>var</tt> + * argument is the set of variables that will be mentioned in the result.</p> + * + * @param dis BDD to iterate over + * @param var variable set to mention in result + */ public BDDIterator(BDD dis, BDD var){ factory = dis.getFactory(); *************** *** 723,727 **** } ! void fillInSatisfyingAssignment(BDD node, int i) { while (!node.isOne() && !node.isZero()) { int v = node.level(); --- 759,763 ---- } ! protected void fillInSatisfyingAssignment(BDD node, int i) { while (!node.isOne() && !node.isZero()) { int v = node.level(); *************** *** 754,758 **** } ! boolean findNextSatisfyingAssignment() { int i = nodes.length - 1; for (;;) { --- 790,794 ---- } ! protected boolean findNextSatisfyingAssignment() { int i = nodes.length - 1; for (;;) { *************** *** 783,787 **** } ! void increment() { more = false; boolean carry = true; --- 819,823 ---- } ! protected void increment() { more = false; boolean carry = true; *************** *** 798,802 **** } ! BDD buildAndIncrement() { more = false; BDD b = factory.one(); --- 834,838 ---- } ! protected BDD buildAndIncrement() { more = false; BDD b = factory.one(); *************** *** 819,823 **** } ! void free() { for (int i = levels.length - 1; i >= 0; --i) { if (nodes[i] != null) { --- 855,859 ---- } ! protected void free() { for (int i = levels.length - 1; i >= 0; --i) { if (nodes[i] != null) { *************** *** 829,832 **** --- 865,871 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ public Object next() { BDD b; *************** *** 845,856 **** --- 884,909 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#hasNext() + */ public boolean hasNext() { return nodes != null; } + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ public void remove() { throw new UnsupportedOperationException(); } + /** + * <p>Returns true if the given BDD variable number is a dont-care. + * <tt>var</tt> must be a variable in the iteration set.</p> + * + * @param var variable number to check + * @return if the given variable is a dont-care + * @throws BDDException if var is not in the iteration set + */ public boolean isDontCare(int var) { if (nodes == null) return false; *************** *** 864,867 **** --- 917,928 ---- } + /** + * <p>Returns true if the BDD variables in the given BDD domain are + * all dont-care's.<p> + * + * @param d domain to check + * @return if the variables are all dont-cares + * @throws BDDException if d is not in the iteration set + */ public boolean isDontCare(BDDDomain d) { if (nodes == null) return false; *************** *** 873,877 **** } ! void fastForward0(int var) { if (levels == null) throw new BDDException(); --- 934,938 ---- } ! protected void fastForward0(int var) { if (levels == null) throw new BDDException(); *************** *** 885,888 **** --- 946,954 ---- } + /** + * Fast-forward the iteration such that the given variable number is true. + * + * @param var number of variable + */ public void fastForward(int var) { fastForward0(var); *************** *** 890,893 **** --- 956,965 ---- } + /** + * Assuming <tt>d</tt> is a dont-care, skip to the end of the iteration for + * <tt>d</tt> + * + * @param d BDD domain to fast-forward past + */ public void skipDontCare(BDDDomain d) { int[] vars = d.vars(); *************** *** 901,907 **** /** ! * <p>Returns an iteration of the satisfying assignments of this BDD. Returns ! * an iteration of minterms. The var argument is a set of variables that ! * must be mentioned in the result.</p> * * @return an iteration of minterms --- 973,978 ---- /** ! * <p>This is another version of iterator() that supports the remove() operation. ! * It is much slower than the other one.</p> * * @return an iteration of minterms *************** *** 911,915 **** BDD b = null; - BDD zero; BDD myVar; BDD last = null; --- 982,985 ---- *************** *** 917,925 **** if (!isZero()) { b = id(); - zero = getFactory().zero(); myVar = var.id(); } } public void remove() { if (last != null) { --- 987,997 ---- if (!isZero()) { b = id(); myVar = var.id(); } } + /* (non-Javadoc) + * @see java.util.Iterator#remove() + */ public void remove() { if (last != null) { *************** *** 931,947 **** } public boolean hasNext() { return b != null; } public Object next() { if (b == null) throw new NoSuchElementException(); ! BDD c = b.satOne(myVar, zero); b.applyWith(c.id(), BDDFactory.diff); if (b.isZero()) { myVar.free(); myVar = null; b.free(); b = null; - zero.free(); zero = null; } return last = c; --- 1003,1024 ---- } + /* (non-Javadoc) + * @see java.util.Iterator#hasNext() + */ public boolean hasNext() { return b != null; } + /* (non-Javadoc) + * @see java.util.Iterator#next() + */ public Object next() { if (b == null) throw new NoSuchElementException(); ! BDD c = b.satOne(myVar, false); b.applyWith(c.id(), BDDFactory.diff); if (b.isZero()) { myVar.free(); myVar = null; b.free(); b = null; } return last = c; *************** *** 1020,1024 **** } ! int printdot_rec(PrintStream out, int current, boolean[] visited, HashMap map) { Integer ri = ((Integer) map.get(this)); if (ri == null) { --- 1097,1101 ---- } ! protected int printdot_rec(PrintStream out, int current, boolean[] visited, HashMap map) { Integer ri = ((Integer) map.get(this)); if (ri == null) { *************** *** 1351,1362 **** if (val == 2) { pos |= 1L; - //System.out.print('1'); - } else if (val == 1) { - //System.out.print('0'); - } else { - //System.out.print('x'); } } - //System.out.println(); if (!hasDontCare) { sb.append(ts.elementName(n, pos)); --- 1428,1433 ---- *************** *** 1386,1405 **** } - static boolean[] fdddec2bin(BDDFactory bdd, int var, long val) { - boolean[] res; - int n = 0; - - res = new boolean[bdd.getDomain(var).varNum()]; - - while (val > 0) { - if ((val & 0x1) != 0) - res[n] = true; - val >>= 1; - n++; - } - - return res; - } - /** * <p>BDDToString is used to specify the printing behavior of BDDs with domains. --- 1457,1460 ---- Index: TestBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TestBDDFactory.java,v retrieving revision 1.13 retrieving revision 1.14 diff -C2 -d -r1.13 -r1.14 *** TestBDDFactory.java 12 Oct 2004 20:41:33 -0000 1.13 --- TestBDDFactory.java 14 Oct 2004 19:47:36 -0000 1.14 *************** *** 360,370 **** * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { BDD c1 = ((TestBDD)var).b1; BDD c2 = ((TestBDD)var).b2; ! BDD d1 = ((TestBDD)pol).b1; ! BDD d2 = ((TestBDD)pol).b2; ! BDD r1 = b1.satOne(c1, d1); ! BDD r2 = b2.satOne(c2, d2); return new TestBDD(r1, r2); } --- 360,368 ---- * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, boolean pol) { BDD c1 = ((TestBDD)var).b1; BDD c2 = ((TestBDD)var).b2; ! BDD r1 = b1.satOne(c1, pol); ! BDD r2 = b2.satOne(c2, pol); return new TestBDD(r1, r2); } Index: BDDDomain.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDDomain.java,v retrieving revision 1.18 retrieving revision 1.19 diff -C2 -d -r1.18 -r1.19 *** BDDDomain.java 9 Aug 2004 21:48:42 -0000 1.18 --- BDDDomain.java 14 Oct 2004 19:47:36 -0000 1.19 *************** *** 2,5 **** --- 2,6 ---- import java.util.Iterator; + import java.math.BigInteger; /** *************** *** 26,30 **** /* The specified domain (0...N-1) */ ! protected long realsize; /* Variable indices for the variable set */ protected int[] ivar; --- 27,31 ---- /* The specified domain (0...N-1) */ ! protected BigInteger realsize; /* Variable indices for the variable set */ protected int[] ivar; *************** *** 32,38 **** protected BDD var; protected BDDDomain(int index, long range) { ! long calcsize = 2L; ! if (range <= 0L || range > Long.MAX_VALUE/2) throw new BDDException(); this.name = Integer.toString(index); --- 33,47 ---- protected BDD var; + /** + * Default constructor. + * + * @param index index of this domain + * @param range size of this domain + */ protected BDDDomain(int index, long range) { ! } ! protected BDDDomain(int index, BigInteger range) { ! BigInteger calcsize = BigInteger.valueOf(2L); ! if (range.signum() <= 0) throw new BDDException(); this.name = Integer.toString(index); *************** *** 40,46 **** this.realsize = range; int binsize = 1; ! while (calcsize < range) { binsize++; ! calcsize <<= 1; } this.ivar = new int[binsize]; --- 49,55 ---- this.realsize = range; int binsize = 1; ! while (calcsize.compareTo(range) < 0) { binsize++; ! calcsize = calcsize.shiftLeft(1); } this.ivar = new int[binsize]; *************** *** 74,82 **** /** ! * Returns what corresponds to a disjunction of all possible values of this * domain. This is more efficient than doing ithVar(0) OR ithVar(1) ... ! * explicitly for all values in the domain. * ! * Compare to fdd_domain. */ public BDD domain() { --- 83,91 ---- /** ! * <p>Returns what corresponds to a disjunction of all possible values of this * domain. This is more efficient than doing ithVar(0) OR ithVar(1) ... ! * explicitly for all values in the domain.</p> * ! * <p>Compare to fdd_domain.</p> */ public BDD domain() { *************** *** 84,96 **** /* Encode V<=X-1. V is the variables in 'var' and X is the domain size */ ! long val = size() - 1L; BDD d = factory.one(); int[] ivar = vars(); for (int n = 0; n < this.varNum(); n++) { ! if ((val & 0x1L) != 0L) d.orWith(factory.nithVar(ivar[n])); else d.andWith(factory.nithVar(ivar[n])); ! val >>= 1; } return d; --- 93,105 ---- /* Encode V<=X-1. V is the variables in 'var' and X is the domain size */ ! BigInteger val = size().subtract(BigInteger.ONE); BDD d = factory.one(); int[] ivar = vars(); for (int n = 0; n < this.varNum(); n++) { ! if (val.testBit(0)) d.orWith(factory.nithVar(ivar[n])); else d.andWith(factory.nithVar(ivar[n])); ! val = val.shiftRight(1); } return d; *************** *** 102,106 **** * Compare to fdd_domainsize. */ ! public long size() { return this.realsize; } --- 111,115 ---- * Compare to fdd_domainsize. */ ! public BigInteger size() { return this.realsize; } *************** *** 209,216 **** */ public BDD ithVar(int val) { ! return ithVar((long) val); } public BDD ithVar(long val) { ! if (val < 0L || val >= this.size()) { throw new BDDException(val+" is out of range"); } --- 218,228 ---- */ public BDD ithVar(int val) { ! return ithVar(BigInteger.valueOf(val)); } public BDD ithVar(long val) { ! return ithVar(BigInteger.valueOf(val)); ! } ! public BDD ithVar(BigInteger val) { ! if (val.signum() < 0 || val.compareTo(size()) >= 0) { throw new BDDException(val+" is out of range"); } *************** *** 220,228 **** int[] ivar = this.vars(); for (int n = 0; n < ivar.length; n++) { ! if ((val & 0x1L) != 0L) v.andWith(factory.ithVar(ivar[n])); else v.andWith(factory.nithVar(ivar[n])); ! val >>= 1; } --- 232,240 ---- int[] ivar = this.vars(); for (int n = 0; n < ivar.length; n++) { ! if (val.testBit(0)) v.andWith(factory.ithVar(ivar[n])); else v.andWith(factory.nithVar(ivar[n])); ! val = val.shiftRight(1); } *************** *** 236,241 **** * @return BDD */ ! public BDD varRange(long lo, long hi) { ! if (lo < 0L || hi >= this.size() || lo > hi) { throw new BDDException("range <"+lo+", "+hi+"> is invalid"); } --- 248,253 ---- * @return BDD */ ! public BDD varRange(BigInteger lo, BigInteger hi) { ! if (lo.signum() < 0 || hi.compareTo(size()) >= 0 || lo.compareTo(hi) > 0) { throw new BDDException("range <"+lo+", "+hi+"> is invalid"); } *************** *** 244,263 **** BDD result = factory.zero(); int[] ivar = this.vars(); ! while (lo <= hi) { ! long bitmask = 1L << (ivar.length - 1); BDD v = factory.one(); for (int n = ivar.length - 1; ; n--) { ! long bit = lo & bitmask; ! if (bit != 0L) { v.andWith(factory.ithVar(ivar[n])); } else { v.andWith(factory.nithVar(ivar[n])); } ! long mask = bitmask - 1L; ! if ((lo & mask) == 0L && (lo | mask) <= hi) { ! lo = (lo | mask) + 1L; break; } - bitmask >>= 1; } result.orWith(v); --- 256,272 ---- BDD result = factory.zero(); int[] ivar = this.vars(); ! while (lo.compareTo(hi) <= 0) { BDD v = factory.one(); for (int n = ivar.length - 1; ; n--) { ! if (lo.testBit(n)) { v.andWith(factory.ithVar(ivar[n])); } else { v.andWith(factory.nithVar(ivar[n])); } ! BigInteger mask = BigInteger.ONE.shiftLeft(n).subtract(BigInteger.ONE); ! if (!lo.testBit(n) && lo.or(mask).compareTo(hi) <= 0) { ! lo = lo.or(mask).add(BigInteger.ONE); break; } } result.orWith(v); Index: JFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JFactory.java,v retrieving revision 1.10 retrieving revision 1.11 diff -C2 -d -r1.10 -r1.11 *** JFactory.java 12 Oct 2004 20:41:33 -0000 1.10 --- JFactory.java 14 Oct 2004 19:47:36 -0000 1.11 *************** *** 16,19 **** --- 16,20 ---- import java.io.IOException; import java.io.PrintStream; + import java.math.BigInteger; /** *************** *** 302,311 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { int x = _index; int y = ((bdd) var)._index; ! int z = ((bdd) pol)._index; return new bdd(bdd_satoneset(x, y, z)); } --- 303,312 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { int x = _index; int y = ((bdd) var)._index; ! int z = pol ? 1 : 0; return new bdd(bdd_satoneset(x, y, z)); } *************** *** 5935,5938 **** --- 5936,5942 ---- */ protected BDDDomain createDomain(int a, long b) { + return createDomain(a, BigInteger.valueOf(b)); + } + protected BDDDomain createDomain(int a, BigInteger b) { return new bddDomain(a, b); } *************** *** 5940,5944 **** class bddDomain extends BDDDomain { ! bddDomain(int a, long b) { super(a, b); } --- 5944,5948 ---- class bddDomain extends BDDDomain { ! bddDomain(int a, BigInteger b) { super(a, b); } Index: BDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BDDFactory.java,v retrieving revision 1.29 retrieving revision 1.30 diff -C2 -d -r1.29 -r1.30 *** BDDFactory.java 12 Oct 2004 20:37:19 -0000 1.29 --- BDDFactory.java 14 Oct 2004 19:47:36 -0000 1.30 *************** *** 903,907 **** d = domain[fdvarnum]; ! d.realsize = d1.realsize * d2.realsize; d.ivar = new int[d1.varNum() + d2.varNum()]; --- 903,907 ---- d = domain[fdvarnum]; ! d.realsize = d1.realsize.multiply(d2.realsize); d.ivar = new int[d1.varNum() + d2.varNum()]; Index: TypedBDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/TypedBDDFactory.java,v retrieving revision 1.20 retrieving revision 1.21 diff -C2 -d -r1.20 -r1.21 *** TypedBDDFactory.java 12 Oct 2004 20:41:33 -0000 1.20 --- TypedBDDFactory.java 14 Oct 2004 19:47:36 -0000 1.21 *************** *** 4,9 **** package org.sf.javabdd; - import java.io.IOException; - import java.io.PrintStream; import java.util.Collection; import java.util.Comparator; --- 4,7 ---- *************** *** 15,18 **** --- 13,19 ---- import java.util.TreeMap; import java.util.TreeSet; + import java.io.IOException; + import java.io.PrintStream; + import java.math.BigInteger; /** *************** *** 865,873 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { TypedBDD bdd1 = (TypedBDD) var; - TypedBDD bdd2 = (TypedBDD) pol; Set newDom = makeSet(); newDom.addAll(dom); --- 866,873 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { TypedBDD bdd1 = (TypedBDD) var; Set newDom = makeSet(); newDom.addAll(dom); *************** *** 878,882 **** } newDom.addAll(bdd1.dom); ! return new TypedBDD(bdd.satOne(bdd1.bdd, bdd2.bdd), newDom); } --- 878,882 ---- } newDom.addAll(bdd1.dom); ! return new TypedBDD(bdd.satOne(bdd1.bdd, pol), newDom); } *************** *** 1092,1096 **** * @see org.sf.javabdd.BDDDomain#varRange(long, long) */ ! public BDD varRange(long lo, long hi) { BDD v = domain.varRange(lo, hi); Set s = makeSet(); --- 1092,1096 ---- * @see org.sf.javabdd.BDDDomain#varRange(long, long) */ ! public BDD varRange(BigInteger lo, BigInteger hi) { BDD v = domain.varRange(lo, hi); Set s = makeSet(); Index: JDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/JDDFactory.java,v retrieving revision 1.7 retrieving revision 1.8 diff -C2 -d -r1.7 -r1.8 *** JDDFactory.java 12 Oct 2004 20:41:33 -0000 1.7 --- JDDFactory.java 14 Oct 2004 19:47:36 -0000 1.8 *************** *** 399,406 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { ! throw new BDDException(); } --- 399,407 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { ! // TODO Implement this. ! throw new UnsupportedOperationException(); } Index: BuDDyFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/BuDDyFactory.java,v retrieving revision 1.36 retrieving revision 1.37 diff -C2 -d -r1.36 -r1.37 *** BuDDyFactory.java 12 Oct 2004 20:41:33 -0000 1.36 --- BuDDyFactory.java 14 Oct 2004 19:47:36 -0000 1.37 *************** *** 764,773 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { BuDDyBDD c = (BuDDyBDD) var; ! BuDDyBDD d = (BuDDyBDD) pol; ! int b = satOne1(_id, c._id, d._id); return makeBDD(b); } --- 764,772 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { BuDDyBDD c = (BuDDyBDD) var; ! int b = satOne1(_id, c._id, pol?1:0); return makeBDD(b); } Index: CUDDFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/CUDDFactory.java,v retrieving revision 1.18 retrieving revision 1.19 diff -C2 -d -r1.18 -r1.19 *** CUDDFactory.java 12 Oct 2004 20:41:33 -0000 1.18 --- CUDDFactory.java 14 Oct 2004 19:47:36 -0000 1.19 *************** *** 658,664 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { // TODO Implement this. throw new UnsupportedOperationException(); --- 658,664 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); Index: CALFactory.java =================================================================== RCS file: /cvsroot/javabdd/JavaBDD/org/sf/javabdd/CALFactory.java,v retrieving revision 1.6 retrieving revision 1.7 diff -C2 -d -r1.6 -r1.7 *** CALFactory.java 12 Oct 2004 20:41:33 -0000 1.6 --- CALFactory.java 14 Oct 2004 19:47:36 -0000 1.7 *************** *** 654,660 **** /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, org.sf.javabdd.BDD) */ ! public BDD satOne(BDD var, BDD pol) { // TODO Implement this. throw new UnsupportedOperationException(); --- 654,660 ---- /* (non-Javadoc) ! * @see org.sf.javabdd.BDD#satOne(org.sf.javabdd.BDD, boolean) */ ! public BDD satOne(BDD var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); |
