Thread: [Javabdd-checkins] SF.net SVN: javabdd: [452] trunk/JavaBDD/net/sf/javabdd
Brought to you by:
joewhaley
Menu
▾
▴
javabdd-checkins
|
From: <joe...@us...> - 2006-07-16 21:50:09
|
Revision: 452 Author: joewhaley Date: 2006-07-16 14:50:02 -0700 (Sun, 16 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=452&view=rev Log Message: ----------- Update to add a new type, BDDVarSet. This replaces the use of raw BDDs for variable sets. Library users will have to update their code (sorry!) Also added preliminary (untested) code for ZDD support. Modified Paths: -------------- trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDDomain.java trunk/JavaBDD/net/sf/javabdd/BDDFactory.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/CALFactory.java trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java trunk/JavaBDD/net/sf/javabdd/TryVarOrder.java trunk/JavaBDD/net/sf/javabdd/TypedBDDFactory.java Added Paths: ----------- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-16 21:50:02 UTC (rev 452) @@ -18,15 +18,6 @@ * * <p>Use an implementation of BDDFactory to create BDD objects.</p> * - * <p>Some methods, namely <tt>exist()</tt>, <tt>forall()</tt>, <tt>unique()</tt>, - * <tt>relprod()</tt>, <tt>applyAll()</tt>, <tt>applyEx()</tt>, <tt>applyUni()</tt>, - * and <tt>satCount()</tt> take a 'set of variables' argument that is also of type BDD. - * Those BDDs must be a boolean function that represents the all-true minterm - * of the BDD variables of interest. They only serve to identify the set of - * variables of interest, however. For example, for a given BDDDomain, a BDD var set - * representing all BDD variables of that domain can be obtained - * by calling <tt>BDDDomain.set()</tt>.</p> - * * @see net.sf.javabdd.BDDFactory * @see net.sf.javabdd.BDDDomain#set() * @@ -57,6 +48,18 @@ public abstract boolean isOne(); /** + * <p>Converts this BDD to a new BDDVarSet.</p> + * + * <p>This BDD must be a boolean function that represents the all-true minterm + * of the BDD variables of interest.</p> + * + * @return the contents of this BDD as a new BDDVarSet + */ + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(id()); + } + + /** * <p>Gets the variable labeling the BDD.</p> * * <p>Compare to bdd_var.</p> @@ -265,11 +268,11 @@ * <p>Compare to bdd_relprod.</p> * * @param that the BDD to 'and' with - * @param var the BDD to existentially quantify with + * @param var the BDDVarSet to existentially quantify with * @return the result of the relational product * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD relprod(BDD that, BDD var); + public abstract BDD relprod(BDD that, BDDVarSet var); /** * <p>Functional composition. Substitutes the variable var with the BDD that @@ -317,11 +320,11 @@ * * <p>Compare to bdd_exist.</p> * - * @param var BDD containing the variables to be existentially quantified + * @param var BDDVarSet containing the variables to be existentially quantified * @return the result of the existential quantification * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD exist(BDD var); + public abstract BDD exist(BDDVarSet var); /** * <p>Universal quantification of variables. Removes all occurrences of this @@ -329,11 +332,11 @@ * * <p>Compare to bdd_forall.</p> * - * @param var BDD containing the variables to be universally quantified + * @param var BDDVarSet containing the variables to be universally quantified * @return the result of the universal quantification * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD forAll(BDD var); + public abstract BDD forAll(BDDVarSet var); /** * <p>Unique quantification of variables. This type of quantification uses a @@ -342,11 +345,11 @@ * * <p>Compare to bdd_unique.</p> * - * @param var BDD containing the variables to be uniquely quantified + * @param var BDDVarSet containing the variables to be uniquely quantified * @return the result of the unique quantification * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD unique(BDD var); + public abstract BDD unique(BDDVarSet var); /** * <p>Restrict a set of variables to constant values. Restricts the variables @@ -388,10 +391,10 @@ * * <p>Compare to bdd_simplify.</p> * - * @param d BDD containing the variables in the domain + * @param d BDDVarSet containing the variables in the domain * @return the result of the simplify operation */ - public abstract BDD simplify(BDD d); + public abstract BDD simplify(BDDVarSet d); /** * <p>Returns the variable support of this BDD. The support is all the @@ -436,11 +439,11 @@ * * @param that the BDD to apply the operator on * @param opr the operator to apply - * @param var BDD containing the variables to quantify + * @param var BDDVarSet containing the variables to quantify * @return the result * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDD var); + public abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var); /** * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs @@ -451,11 +454,11 @@ * * @param that the BDD to apply the operator on * @param opr the operator to apply - * @param var BDD containing the variables to quantify + * @param var BDDVarSet containing the variables to quantify * @return the result * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDD var); + public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var); /** * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs @@ -466,11 +469,11 @@ * * @param that the BDD to apply the operator on * @param opr the operator to apply - * @param var BDD containing the variables to quantify + * @param var BDDVarSet containing the variables to quantify * @return the result * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDD var); + public abstract BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var); /** * <p>Finds one satisfying variable assignment. Finds a BDD with at most one @@ -504,12 +507,12 @@ * * <p>Compare to bdd_satoneset.</p> * - * @param var BDD containing the set of variables that must be mentioned in the result + * @param var BDDVarSet containing the set of variables that must be mentioned in the result * @param pol the polarity of the result * @return one satisfying variable assignment * @see net.sf.javabdd.BDDDomain#set() */ - public abstract BDD satOne(BDD var, boolean pol); + public abstract BDD satOne(BDDVarSet var, boolean pol); /** * <p>Finds all satisfying variable assignments.</p> @@ -557,7 +560,8 @@ useLevel = lev; if (r.isZero()) return; allsatProfile = new byte[f.varNum()]; - Arrays.fill(allsatProfile, (byte) -1); + if (!f.isZDD()) + Arrays.fill(allsatProfile, (byte) -1); loStack = new LinkedList(); hiStack = new LinkedList(); if (!r.isOne()) { @@ -808,7 +812,8 @@ * @param r BDD varset * @return array of levels */ - private static int[] varset2levels(BDD r) { + /* + private static int[] varset2levels(BDDVarSet r) { int size = 0; BDD p = r.id(); while (!p.isOne() && !p.isZero()) { @@ -830,6 +835,7 @@ p.free(); return result; } + */ /** * <p>Returns an iteration of the satisfying assignments of this BDD. Returns @@ -840,7 +846,7 @@ * @return an iteration of minterms * @see net.sf.javabdd.BDDDomain#set() */ - public BDDIterator iterator(final BDD var) { + public BDDIterator iterator(final BDDVarSet var) { return new BDDIterator(this, var); } @@ -872,32 +878,14 @@ * @param bdd BDD to iterate over * @param var variable set to mention in result */ - public BDDIterator(BDD bdd, BDD var) { + public BDDIterator(BDD bdd, BDDVarSet var) { initialBDD = bdd; f = bdd.getFactory(); i = new AllSatIterator(bdd, true); // init v[] - int n = 0; - BDD p = var.id(); - while (!p.isOne()) { - ++n; - BDD q = p.high(); - p.free(); - p = q; - } - p.free(); - v = new int[n]; - n = 0; - p = var.id(); - while (!p.isOne()) { - v[n++] = p.level(); - BDD q = p.high(); - p.free(); - p = q; - } - p.free(); + v = var.toLevelArray(); // init b[] - b = new boolean[n]; + b = new boolean[v.length]; gotoNext(); } @@ -1291,21 +1279,14 @@ * * @return the number of satisfying variable assignments */ - public double satCount(BDD varset) { + public double satCount(BDDVarSet varset) { BDDFactory factory = getFactory(); - double unused = factory.varNum(); - if (varset.isZero() || varset.isOne() || isZero()) /* empty set */ + if (varset.isEmpty() || isZero()) /* empty set */ return 0.; - BDD n = varset.id(); - do { - BDD n2 = n.high(); - n.free(); n = n2; - unused--; - } while (!n.isOne() && !n.isZero()); - n.free(); - + double unused = factory.varNum(); + unused -= varset.size(); unused = satCount() / Math.pow(2.0, unused); return unused >= 1.0 ? unused : 1.0; @@ -1330,7 +1311,7 @@ * * @return the logarithm of the number of satisfying variable assignments */ - public double logSatCount(BDD varset) { + public double logSatCount(BDDVarSet varset) { return Math.log(satCount(varset)); } Modified: trunk/JavaBDD/net/sf/javabdd/BDDDomain.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BDDDomain.java 2006-07-16 21:50:02 UTC (rev 452) @@ -33,7 +33,7 @@ /* Variable indices for the variable set */ protected int[] ivar; /* The BDD variable set. Actually constructed in extDomain(), etc. */ - protected BDD var; + protected BDDVarSet var; /** * Default constructor. @@ -203,9 +203,9 @@ * * Compare to fdd_ithset. * - * @return BDD + * @return BDDVarSet */ - public BDD set() { + public BDDVarSet set() { return var.id(); } @@ -331,9 +331,9 @@ this.ivar = new_ivar; //System.out.println("Domain "+this+" old var = "+var); this.var.free(); - BDD nvar = factory.one(); + BDDVarSet nvar = factory.emptySet(); for (int i = 0; i < ivar.length; ++i) { - nvar.andWith(factory.ithVar(ivar[i])); + nvar.unionWith(ivar[i]); } this.var = nvar; //System.out.println("Domain "+this+" new var = "+var); @@ -375,7 +375,7 @@ * @see #ithVar(long) */ public BigInteger[] getVarIndices(BDD bdd, int max) { - BDD myvarset = set(); // can't use var here, must respect subclass a factory may provide + BDDVarSet myvarset = set(); // can't use var here, must respect subclass a factory may provide int n = (int) bdd.satCount(myvarset); if (max != -1 && n > max) n = max; Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -177,6 +177,11 @@ } /** + * <p>Returns true if this is a ZDD factory, false otherwise.</p> + */ + public boolean isZDD() { return false; } + + /** * <p>Get the constant false BDD.</p> * * <p>Compare to bdd_false.</p> @@ -191,6 +196,15 @@ public abstract BDD one(); /** + * <p>Get an empty BDDVarSet.</p> + * + * <p>Compare to bdd_true.</p> + */ + public BDDVarSet emptySet() { + return new BDDVarSet.DefaultImpl(one()); + } + + /** * <p>Build a cube from an array of variables.</p> * * <p>Compare to bdd_buildcube.</p> @@ -238,11 +252,11 @@ * * <p>Compare to bdd_makeset.</p> */ - public BDD makeSet(int[] varset) { - BDD res = one(); + public BDDVarSet makeSet(int[] varset) { + BDDVarSet res = emptySet(); int varnum = varset.length; - for (int v = varnum-1 ; v>=0 ; v--) { - res.andWith(ithVar(varset[v])); + for (int v = varnum-1; v >= 0; --v) { + res.unionWith(varset[v]); } return res; } @@ -711,17 +725,12 @@ root.free(); return 1; } - //Integer i = (Integer) visited.get(root); int i = root.hashCode(); - //if (i != null) { if (visited.get(i)) { root.free(); - //return i.intValue(); return i; } - //int v = visited.size() + 2; int v = i; - //visited.put(root, new Integer(v)); visited.set(i); BDD h = root.high(); @@ -735,7 +744,6 @@ int hi = save_rec(out, visited, h); - //out.write(v + " "); out.write(i + " "); out.write(rootvar + " "); out.write(lo + " "); @@ -1449,12 +1457,12 @@ * * <p>Compare to fdd_makeset.</p> */ - public BDD makeSet(BDDDomain[] v) { - BDD res = one(); + public BDDVarSet makeSet(BDDDomain[] v) { + BDDVarSet res = emptySet(); int n; for (n = 0; n < v.length; n++) { - res.andWith(v[n].set()); + res.unionWith(v[n].set()); } return res; Added: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java (rev 0) +++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-07-16 21:50:02 UTC (rev 452) @@ -0,0 +1,302 @@ +// BDDVarSet.java, created Jul 13, 2006 8:53:13 PM by jwhaley +// Copyright (C) 2004 John Whaley <jw...@al...> +// Licensed under the terms of the GNU LGPL; see COPYING for details. +package net.sf.javabdd; + +/** + * <p>Some BDD methods, namely <tt>exist()</tt>, <tt>forall()</tt>, <tt>unique()</tt>, + * <tt>relprod()</tt>, <tt>applyAll()</tt>, <tt>applyEx()</tt>, <tt>applyUni()</tt>, + * and <tt>satCount()</tt> take a BDDVarSet argument.</p> + * + * @author jwhaley + * @version $Id$ + */ +public abstract class BDDVarSet { + + /** + * <p>Returns the factory that created this BDDVarSet.</p> + * + * @return factory that created this BDDVarSet + */ + public abstract BDDFactory getFactory(); + + public abstract BDD toBDD(); + + public abstract BDDVarSet id(); + public abstract void free(); + + public abstract int size(); + public abstract boolean isEmpty(); + + public abstract int[] toArray(); + public abstract int[] toLevelArray(); + + /** + * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet + * and the given BDDVarSet. This constructs a new set; neither the current + * nor the given BDDVarSet is modified.</p> + * + * @param b BDDVarSet to union with + * @return a new BDDVarSet that is the union of the two sets + */ + public abstract BDDVarSet union(BDDVarSet b); + + /** + * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet + * and the given variable. This constructs a new set; the current BDDVarSet + * is not modified.</p> + * + * @param b variable to add to set + * @return a new BDDVarSet that includes the given variable + */ + public abstract BDDVarSet union(int var); + + /** + * <p>Modifies this BDDVarSet to include all of the vars in the given set. + * This modifies the current set in place and consumes the given set.</p> + * + * @param b BDDVarSet to union in + * @return this + */ + public abstract BDDVarSet unionWith(BDDVarSet b); + + /** + * <p>Modifies this BDDVarSet to include the given variable. This modifies + * the current set in place.</p> + * + * @param b variable to add to set + * @return this + */ + public abstract BDDVarSet unionWith(int var); + + /** + * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet + * and the given BDDVarSet. This constructs a new set; neither the current + * nor the given BDDVarSet is modified.</p> + * + * @param b BDDVarSet to union with + * @return a new BDDVarSet that is the union of the two sets + */ + public abstract BDDVarSet intersect(BDDVarSet b); + + /** + * <p>Modifies this BDDVarSet to include all of the vars in the given set. + * This modifies the current set in place and consumes the given set.</p> + * + * @param b BDDVarSet to union in + * @return this + */ + public abstract BDDVarSet intersectWith(BDDVarSet b); + + /* (non-Javadoc) + * @see java.lang.Object#hashCode() + */ + public abstract int hashCode(); + + /** + * Returns true if the sets are equal. + * + * @param that other set + * @return true if the sets are equal + */ + public abstract boolean equals(BDDVarSet that); + + /* (non-Javadoc) + * @see java.lang.Object#equals(java.lang.Object) + */ + public final boolean equals(Object o) { + if (o instanceof BDDVarSet) + return equals((BDDVarSet) o); + return false; + } + + /** + * Default implementation of BDDVarSet based on BDDs. + * + * @author jwhaley + * @version $Id$ + */ + public static class DefaultImpl extends BDDVarSet { + + /** + * BDD representation of the set of variables. + * Treated like a linked list of variables. + */ + protected BDD b; + + /** + * Construct a BDDVarSet backed by the given BDD. + * Ownership of the given BDD is transferred to this BDDVarSet, + * so you should not touch it after construction! + * + * @param b BDD to use in constructing BDDVarSet + */ + public DefaultImpl(BDD b) { + this.b = b; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#free() + */ + public void free() { + if (b != null) { + b.free(); + b = null; + } + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#getFactory() + */ + public BDDFactory getFactory() { + return b.getFactory(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#id() + */ + public BDDVarSet id() { + return new DefaultImpl(b.id()); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#intersect(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet intersect(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + return new DefaultImpl(b.or(i.b)); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#intersectWith(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet intersectWith(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + b.orWith(i.b); i.b = null; + return this; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#isEmpty() + */ + public boolean isEmpty() { + return b.isOne(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#size() + */ + public int size() { + int result = 0; + BDD r = b.id(); + while (!r.isOne()) { + if (r.isZero()) throw new BDDException("varset contains zero"); + ++result; + BDD q = r.high(); + r.free(); + r = q; + } + r.free(); + return result; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#toArray() + */ + public int[] toArray() { + int[] result = new int[size()]; + int i = -1; + BDD r = b.id(); + while (!r.isOne()) { + if (r.isZero()) throw new BDDException("varset contains zero"); + result[++i] = r.var(); + BDD q = r.high(); + r.free(); + r = q; + } + r.free(); + return result; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#toBDD() + */ + public BDD toBDD() { + return b.id(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#toLevelArray() + */ + public int[] toLevelArray() { + int[] result = new int[size()]; + int i = -1; + BDD r = b.id(); + while (!r.isOne()) { + if (r.isZero()) throw new BDDException("varset contains zero"); + result[++i] = r.level(); + BDD q = r.high(); + r.free(); + r = q; + } + r.free(); + return result; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#union(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet union(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + return new DefaultImpl(b.and(i.b)); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#union(int) + */ + public BDDVarSet union(int var) { + BDD ith = b.getFactory().ithVar(var); + DefaultImpl j = new DefaultImpl(b.and(ith)); + ith.free(); + return j; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#unionWith(net.sf.javabdd.BDDVarSet) + */ + public BDDVarSet unionWith(BDDVarSet s) { + DefaultImpl i = (DefaultImpl) s; + b.andWith(i.b); i.b = null; + return this; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#unionWith(int) + */ + public BDDVarSet unionWith(int var) { + b.andWith(b.getFactory().ithVar(var)); + return this; + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#hashCode() + */ + public int hashCode() { + return b.hashCode(); + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDVarSet#equals(net.sf.javabdd.BDDVarSet) + */ + public boolean equals(BDDVarSet s) { + if (s instanceof DefaultImpl) + return equals((DefaultImpl) s); + return false; + } + + public boolean equals(DefaultImpl s) { + return b.equals(s.b); + } + } + +} Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -127,6 +127,10 @@ return b; } + private static BDDVarSet.DefaultImpl makeBDDVarSet(int id) { + return new BDDVarSet.DefaultImpl(makeBDD(id)); + } + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#zero() */ @@ -176,9 +180,9 @@ /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#makeSet(int[]) */ - public BDD makeSet(int[] v) { + public BDDVarSet makeSet(int[] v) { int id = makeSet0(v); - return makeBDD(id); + return makeBDDVarSet(id); } private static native int makeSet0(int[] var); @@ -690,11 +694,11 @@ private static native int ite0(int b, int c, int d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = relprod0(_id, c._id, d._id); return makeBDD(b); } @@ -721,30 +725,30 @@ private static native int constrain0(int b, int c); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD exist(BDDVarSet var) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = exist0(_id, c._id); return makeBDD(b); } private static native int exist0(int b, int var); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD forAll(BDDVarSet var) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = forAll0(_id, c._id); return makeBDD(b); } private static native int forAll0(int b, int var); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD unique(BDDVarSet var) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = unique0(_id, c._id); return makeBDD(b); } @@ -777,10 +781,10 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { - BuDDyBDD c = (BuDDyBDD) d; + public BDD simplify(BDDVarSet d) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) d).b; int b = simplify0(_id, c._id); return makeBDD(b); } @@ -822,33 +826,33 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDD var) { + public BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = applyAll0(_id, c._id, opr.id, d._id); return makeBDD(b); } private static native int applyAll0(int b, int c, int opr, int d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDD var) { + public BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = applyEx0(_id, c._id, opr.id, d._id); return makeBDD(b); } private static native int applyEx0(int b, int c, int opr, int d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDD var) { + public BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) { BuDDyBDD c = (BuDDyBDD) that; - BuDDyBDD d = (BuDDyBDD) var; + BuDDyBDD d = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = applyUni0(_id, c._id, opr.id, d._id); return makeBDD(b); } @@ -873,10 +877,10 @@ private static native int fullSatOne0(int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { - BuDDyBDD c = (BuDDyBDD) var; + public BDD satOne(BDDVarSet var, boolean pol) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) var).b; int b = satOne1(_id, c._id, pol?1:0); return makeBDD(b); } @@ -923,10 +927,10 @@ private static native double satCount0(int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#satCount(net.sf.javabdd.BDDVarSet) */ - public double satCount(BDD varset) { - BuDDyBDD c = (BuDDyBDD) varset; + public double satCount(BDDVarSet varset) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) varset).b; return satCount1(_id, c._id); } private static native double satCount1(int b, int c); @@ -940,10 +944,10 @@ private static native double logSatCount0(int b); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#logSatCount(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#logSatCount(net.sf.javabdd.BDDVarSet) */ - public double logSatCount(BDD varset) { - BuDDyBDD c = (BuDDyBDD) varset; + public double logSatCount(BDDVarSet varset) { + BuDDyBDD c = (BuDDyBDD) ((BDDVarSet.DefaultImpl) varset).b; return logSatCount1(_id, c._id); } private static native double logSatCount1(int b, int c); @@ -1016,6 +1020,13 @@ return this._id; } + /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return makeBDDVarSet(this._id); + } + } private static class BuDDyBDDWithFinalizer extends BuDDyBDD { Modified: trunk/JavaBDD/net/sf/javabdd/CALFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CALFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/CALFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -505,11 +505,11 @@ private static native long ite0(long b, long c, long d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { CALBDD c = (CALBDD) that; - CALBDD d = (CALBDD) var; + CALBDD d = (CALBDD) ((BDDVarSet.DefaultImpl) var).b; long b = relprod0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr); return new CALBDD(b); } @@ -534,25 +534,25 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { + public BDD exist(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { + public BDD forAll(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -584,9 +584,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -627,25 +627,25 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyAll(BDD that, BDDOp opr, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyEx(BDD that, BDDOp opr, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyUni(BDD that, BDDOp opr, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -668,9 +668,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -787,6 +787,10 @@ return (int) this._ddnode_ptr; } + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(new CALBDD(this._ddnode_ptr)); + } + } /* (non-Javadoc) Modified: trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/CUDDFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -534,11 +534,11 @@ private static native long ite0(long b, long c, long d); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { CUDDBDD c = (CUDDBDD) that; - CUDDBDD d = (CUDDBDD) var; + CUDDBDD d = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b; long b = relprod0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr); return new CUDDBDD(b); } @@ -563,29 +563,29 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { - CUDDBDD c = (CUDDBDD) var; + public BDD exist(BDDVarSet var) { + CUDDBDD c = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b; long b = exist0(_ddnode_ptr, c._ddnode_ptr); return new CUDDBDD(b); } private static native long exist0(long b, long c); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { - CUDDBDD c = (CUDDBDD) var; + public BDD forAll(BDDVarSet var) { + CUDDBDD c = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b; long b = forAll0(_ddnode_ptr, c._ddnode_ptr); return new CUDDBDD(b); } private static native long forAll0(long b, long c); /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -617,9 +617,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -660,25 +660,25 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyAll(BDD that, BDDOp opr, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyEx(BDD that, BDDOp opr, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyUni(BDD that, BDDOp opr, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -701,9 +701,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -819,6 +819,13 @@ return (int) this._ddnode_ptr; } + /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(new CUDDBDD(this._ddnode_ptr)); + } + } /* (non-Javadoc) Modified: trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/FindBestOrder.java 2006-07-16 21:50:02 UTC (rev 452) @@ -24,7 +24,7 @@ boolean newbdd = true; BDD b1 = null; BDD b2 = null; - BDD b3 = null; + BDDVarSet b3 = null; String filename0 = "fbo.bi"; String filename1 = "fbo.1"; @@ -59,7 +59,7 @@ this.DELAY_TIME = delayTime; } - public void init(BDD b1, BDD b2, BDD dom, BDDFactory.BDDOp op) throws IOException { + public void init(BDD b1, BDD b2, BDDVarSet dom, BDDFactory.BDDOp op) throws IOException { this.op = op; f0 = File.createTempFile("fbo", "a"); filename0 = f0.getAbsolutePath(); @@ -77,7 +77,7 @@ writeBDDConfig(b1.getFactory(), filename0); b1.getFactory().save(filename1, b1); b2.getFactory().save(filename2, b2); - dom.getFactory().save(filename3, dom); + dom.getFactory().save(filename3, dom.toBDD()); //System.out.println("done."); } @@ -167,7 +167,7 @@ if (newbdd) { b1 = bdd.load(filename1); b2 = bdd.load(filename2); - b3 = bdd.load(filename3); + b3 = bdd.load(filename3).toVarSet(); newbdd = false; } long t = System.currentTimeMillis(); Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -6,6 +6,7 @@ import java.util.Collection; import java.math.BigInteger; + /** * JDDFactory * @@ -119,12 +120,12 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; - int z = ((bdd) var)._index; + int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return new bdd(bdd.relProd(x, y, z)); } @@ -155,29 +156,29 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { + public BDD exist(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return new bdd(bdd.exists(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { + public BDD forAll(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return new bdd(bdd.forall(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return null; // todo. } @@ -207,11 +208,11 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { int x = _index; - int y = ((bdd) d)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; return new bdd(bdd.simplify(x, y)); } @@ -267,13 +268,13 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyAll(BDD that, BDDOp opr, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; // todo: combine. int r = apply0(x, y, z); bdd.ref(r); @@ -283,13 +284,13 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyEx(BDD that, BDDOp opr, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; // todo: combine. int r = apply0(x, y, z); bdd.ref(r); @@ -299,13 +300,13 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyUni(BDD that, BDDOp opr, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; throw new BDDException(); // todo. } @@ -399,9 +400,9 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { // TODO Implement this. throw new UnsupportedOperationException(); } @@ -419,6 +420,13 @@ public int[] varProfile() { throw new BDDException(); } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return new BDDVarSet.DefaultImpl(new bdd(_index)); + } } Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-06-06 23:38:30 UTC (rev 451) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-16 21:50:02 UTC (rev 452) @@ -68,6 +68,14 @@ } /** + * Private helper function to create BDD objects. + */ + private BDDVarSet makeBDDVarSet(int id) { + BDDVarSet b = new BDDVarSet.DefaultImpl(makeBDD(id)); + return b; + } + + /** * Wrapper for the BDD index number used internally in the representation. */ private class bdd extends BDD { @@ -86,6 +94,13 @@ } /* (non-Javadoc) + * @see net.sf.javabdd.BDD#toVarSet() + */ + public BDDVarSet toVarSet() { + return makeBDDVarSet(_index); + } + + /* (non-Javadoc) * @see net.sf.javabdd.BDD#isZero() */ public boolean isZero() { @@ -145,12 +160,12 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) */ - public BDD relprod(BDD that, BDD var) { + public BDD relprod(BDD that, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; - int z = ((bdd) var)._index; + int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_relprod(x, y, z)); } @@ -181,29 +196,29 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) */ - public BDD exist(BDD var) { + public BDD exist(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_exist(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) */ - public BDD forAll(BDD var) { + public BDD forAll(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_forall(x, y)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) */ - public BDD unique(BDD var) { + public BDD unique(BDDVarSet var) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_unique(x, y)); } @@ -232,11 +247,11 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) */ - public BDD simplify(BDD d) { + public BDD simplify(BDDVarSet d) { int x = _index; - int y = ((bdd) d)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; return makeBDD(bdd_simplify(x, y)); } @@ -275,35 +290,35 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyAll(BDD that, BDDOp opr, BDD var) { + public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_appall(x, y, z, a)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyEx(BDD that, BDDOp opr, BDD var) { + public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_appex(x, y, z, a)); } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDD) + * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) */ - public BDD applyUni(BDD that, BDDOp opr, BDD var) { + public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { int x = _index; int y = ((bdd) that)._index; int z = opr.id; - int a = ((bdd) var)._index; + int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; return makeBDD(bdd_appuni(x, y, z, a)); } @@ -324,11 +339,11 @@ } /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDD, boolean) + * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) */ - public BDD satOne(BDD var, boolean pol) { + public BDD satOne(BDDVarSet var, boolean pol) { int x = _index; - int y = ((bdd) var)._index; + int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; int z = pol ? 1 : 0; return makeBDD(bdd_satoneset(x, y, z)); } @@ -649,37 +664,27 @@ static final int BDD_MEMORY = (-1); /* Out of memory */ static final int BDD_VAR = (-2); /* Unknown variable */ - static final int BDD_RANGE = (-3); - /* Variable value out of range (not in domain) */ - static final int BDD_DEREF = (-4); - /* Removing external reference to unknown node */ - static final int BDD_RUNNING = (-5); - /* Called bdd_init() twice whithout bdd_done() */ + static final int BDD_RANGE = (-3); /* Variable value out of range (not in domain) */ + static final int BDD_DEREF = (-4); /* Removing external reference to unknown node */ + static final int BDD_RUNNING = (-5); /* Called bdd_init() twice without bdd_done() */ static final int BDD_FILE = (-6); /* Some file operation failed */ static final int BDD_FORMAT = (-7); /* Incorrect file format */ - static final int BDD_ORDER = (-8); - /* Vars. not in order for vector based functions */ + static final int BDD_ORDER = (-8); /* Vars. not in order for vector based functions */ static final int BDD_BREAK = (-9); /* User called break */ - static final int BDD_VARNUM = (-10); - /* Different number of vars. for vector pair */ - static final int BDD_NODES = (-11); - /* Tried to set max. number of nodes to be fewer */ - /* than there already has been allocated */ + static final int BDD_VARNUM = (-10); /* Different number of vars. for vector pair */ + static final int BDD_NODES = (-11); /* Tried to set max. number of nodes to be fewer */ + /* than there already has been allocated */ static final int BDD_OP = (-12); /* Unknown operator */ static final int BDD_VARSET = (-13); /* Illegal variable set */ static final int BDD_VARBLK = (-14); /* Bad variable block operation */ - static final int BDD_DECVNUM = (-15); - /* Trying to decrease the number of variables */ - static final int BDD_REPLACE = (-16); - /* Replacing to already existing variables */ - static final int BDD_NODENUM = (-17); - /* Number of nodes reached user defined maximum */ + static final int BDD_DECVNUM = (-15); /* Trying to decrease the number of variables */ + static final int BDD_REPLACE = (-16); /* Replacing to already existing variables */ + static final int BDD_NODENUM = (-17); /* Number of nodes reached user defined maximum */ static final int BDD_ILLBDD = (-18); /* Illegal bdd argument */ static final int BDD_SIZE = (-19); /* Illegal size argument */ static final int BVEC_SIZE = (-20); /* Mismatch in bitvector size */ - static final int BVEC_SHIFT = (-21); - /* Illegal shift-left/right parameter */ + static final int BVEC_SHIFT = (-21); /* Illegal shift-left/right parameter */ static final int BVEC_DIVZERO = (-22); /* Division by zero */ static final int BDD_ERRNUM = 24; @@ -729,6 +734,11 @@ } /* (non-Javadoc) + * @see net.sf.javabdd.BDDFactory#isZDD() + */ + public boolean isZDD() { return ZDD; } + + /* (non-Javadoc) * @see net.sf.javabdd.BDDFactory#zero() */ public BDD zero() { @@ -742,6 +752,10 @@ return makeBDD(bddtrue); } + public BDDVarSet emptySet() { + return makeBDDVarSet(bddtrue); + } + int bdd_ithvar(int var) { if (var < 0 || var >= bddvarnum) { bdd_error(BDD_VAR); @@ -900,7 +914,7 @@ if (firstReorder == 0) bdd_disable_reorder(); - res = not_rec(r); + res = ZDD ? znot_rec(r) : not_rec(r); if (firstReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { @@ -948,6 +962,36 @@ return res; } + int znot_rec(int r) { + BddCacheDataI entry; + int res; + + if (ISZERO(r)) + return bddtrue; + if (ISONE(r)) + return bddfalse; + + entry = BddCache_lookupI(applycache, NOTHASH(r)); + + if (entry.a == r && entry.c == bddop_not) { + if (CACHESTATS) + cachestats.opHit++; + return entry.res; + } + if (CACHESTATS) + cachestats.opMiss++; + + PUSHREF(znot_rec(LOW(r))); + res = bdd_makenode(LEVEL(r), READREF(1), HIGH(r)); + POPREF(1); + + entry.a = r; + entry.c = bddop_not; + entry.res = res; + + return res; + } + int bdd_ite(int f, int g, int h) { int res; firstReorder = 1; @@ -965,7 +1009,7 @@ if (firstReorder == 0) ... [truncated message content] |
|
From: <joe...@us...> - 2006-07-21 14:32:09
|
Revision: 461 Author: joewhaley Date: 2006-07-21 07:32:02 -0700 (Fri, 21 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=461&view=rev Log Message: ----------- Changed MicroFactory, JDDFactory to use new BDDFactoryIntImpl shared superclass. More bug fixes in the test cases. Now the test cases won't fail if a BDD library doesn't support a (nonessential) operation and throws UnsupportedOperationException. Modified Paths: -------------- trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-21 14:32:02 UTC (rev 461) @@ -588,7 +588,8 @@ allsatProfile[useLevel?LEVEL_r:f.level2Var(LEVEL_r)] = lo_empty ? (byte)1 : (byte)0; BDD rn = lo_empty ? r.high() : r.low(); - for (int v = rn.level() - 1; v > LEVEL_r; --v) { + int v = rn.isOne()||rn.isZero() ? f.varNum() - 1 : rn.level() - 1; + for ( ; v > LEVEL_r; --v) { allsatProfile[useLevel?v:f.level2Var(v)] = -1; } if (!lo_empty) { Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-21 14:32:02 UTC (rev 461) @@ -16,49 +16,49 @@ static final boolean USE_FINALIZER = false; - protected abstract void addref_impl(int v); - protected abstract void delref_impl(int v); - protected abstract int zero_impl(); - protected abstract int one_impl(); - protected abstract int invalid_bdd_impl(); - protected abstract int var_impl(int v); - protected abstract int level_impl(int v); - protected abstract int low_impl(int v); - protected abstract int high_impl(int v); - protected abstract int ithVar_impl(int var); - protected abstract int nithVar_impl(int var); + protected abstract void addref_impl(/*bdd*/int v); + protected abstract void delref_impl(/*bdd*/int v); + protected abstract /*bdd*/int zero_impl(); + protected abstract /*bdd*/int one_impl(); + protected abstract /*bdd*/int invalid_bdd_impl(); + protected abstract int var_impl(/*bdd*/int v); + protected abstract int level_impl(/*bdd*/int v); + protected abstract /*bdd*/int low_impl(/*bdd*/int v); + protected abstract /*bdd*/int high_impl(/*bdd*/int v); + protected abstract /*bdd*/int ithVar_impl(int var); + protected abstract /*bdd*/int nithVar_impl(int var); - protected abstract int ite_impl(int v1, int v2, int v3); - protected abstract int apply_impl(int v1, int v2, BDDOp opr); - protected abstract int not_impl(int v1); - protected abstract int applyAll_impl(int v1, int v2, BDDOp opr, int v3); - protected abstract int applyEx_impl(int v1, int v2, BDDOp opr, int v3); - protected abstract int applyUni_impl(int v1, int v2, BDDOp opr, int v3); - protected abstract int compose_impl(int v1, int v2, int var); - protected abstract int constrain_impl(int v1, int v2); - protected abstract int restrict_impl(int v1, int v2); - protected abstract int simplify_impl(int v1, int v2); - protected abstract int support_impl(int v); - protected abstract int exist_impl(int v1, int v2); - protected abstract int forAll_impl(int v1, int v2); - protected abstract int unique_impl(int v1, int v2); - protected abstract int fullSatOne_impl(int v); + protected abstract /*bdd*/int ite_impl(/*bdd*/int v1, /*bdd*/int v2, /*bdd*/int v3); + protected abstract /*bdd*/int apply_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr); + protected abstract /*bdd*/int not_impl(/*bdd*/int v1); + protected abstract /*bdd*/int applyAll_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3); + protected abstract /*bdd*/int applyEx_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3); + protected abstract /*bdd*/int applyUni_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3); + protected abstract /*bdd*/int compose_impl(/*bdd*/int v1, /*bdd*/int v2, int var); + protected abstract /*bdd*/int constrain_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int restrict_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int simplify_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int support_impl(/*bdd*/int v); + protected abstract /*bdd*/int exist_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int forAll_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int unique_impl(/*bdd*/int v1, /*bdd*/int v2); + protected abstract /*bdd*/int fullSatOne_impl(/*bdd*/int v); - protected abstract int replace_impl(int v, BDDPairing p); - protected abstract int veccompose_impl(int v, BDDPairing p); + protected abstract /*bdd*/int replace_impl(/*bdd*/int v, BDDPairing p); + protected abstract /*bdd*/int veccompose_impl(/*bdd*/int v, BDDPairing p); - protected abstract int nodeCount_impl(int v); - protected abstract double pathCount_impl(int v); - protected abstract double satCount_impl(int v); - protected abstract int satOne_impl(int v); - protected abstract int satOne_impl2(int v1, int v2, boolean pol); - protected abstract int nodeCount_impl2(int[] v); - protected abstract int[] varProfile_impl(int v); - protected abstract void printTable_impl(int v); + protected abstract int nodeCount_impl(/*bdd*/int v); + protected abstract double pathCount_impl(/*bdd*/int v); + protected abstract double satCount_impl(/*bdd*/int v); + protected abstract /*bdd*/int satOne_impl(/*bdd*/int v); + protected abstract /*bdd*/int satOne_impl2(/*bdd*/int v1, /*bdd*/int v2, boolean pol); + protected abstract int nodeCount_impl2(/*bdd*/int[] v); + protected abstract int[] varProfile_impl(/*bdd*/int v); + protected abstract void printTable_impl(/*bdd*/int v); public class IntBDD extends BDD { - protected int v; - protected IntBDD(int v) { + protected /*bdd*/int v; + protected IntBDD(/*bdd*/int v) { this.v = v; addref_impl(v); } @@ -75,8 +75,8 @@ return makeBDD(applyUni_impl(v, unwrap(that), opr, unwrap(var))); } public BDD applyWith(BDD that, BDDOp opr) { - int v2 = unwrap(that); - int v3 = apply_impl(v, v2, opr); + /*bdd*/int v2 = unwrap(that); + /*bdd*/int v3 = apply_impl(v, v2, opr); addref_impl(v3); delref_impl(v); if (this != that) @@ -146,7 +146,7 @@ return makeBDD(replace_impl(v, pair)); } public BDD replaceWith(BDDPairing pair) { - int v3 = replace_impl(v, pair); + /*bdd*/int v3 = replace_impl(v, pair); addref_impl(v3); delref_impl(v); v = v3; @@ -156,8 +156,8 @@ return makeBDD(restrict_impl(v, unwrap(var))); } public BDD restrictWith(BDD that) { - int v2 = unwrap(that); - int v3 = restrict_impl(v, v2); + /*bdd*/int v2 = unwrap(that); + /*bdd*/int v3 = restrict_impl(v, v2); addref_impl(v3); delref_impl(v); if (this != that) @@ -198,7 +198,7 @@ } public class IntBDDWithFinalizer extends IntBDD { - protected IntBDDWithFinalizer(int v) { + protected IntBDDWithFinalizer(/*bdd*/int v) { super(v); } @@ -214,19 +214,19 @@ } - protected IntBDD makeBDD(int v) { + protected IntBDD makeBDD(/*bdd*/int v) { if (USE_FINALIZER) return new IntBDDWithFinalizer(v); else return new IntBDD(v); } - protected static final int unwrap(BDD b) { + protected static final /*bdd*/int unwrap(BDD b) { return ((IntBDD) b).v; } - protected static final int[] unwrap(Collection/*<BDD>*/ c) { - int[] result = new int[c.size()]; + protected static final /*bdd*/int[] unwrap(Collection/*<BDD>*/ c) { + /*bdd*/int[] result = new /*bdd*/int[c.size()]; int k = -1; for (Iterator i = c.iterator(); i.hasNext(); ) { result[++k] = ((IntBDD) i.next()).v; @@ -235,8 +235,8 @@ } public class IntBDDVarSet extends BDDVarSet { - int v; - private IntBDDVarSet(int v) { + /*bdd*/int v; + private IntBDDVarSet(/*bdd*/int v) { this.v = v; addref_impl(v); } @@ -260,8 +260,8 @@ return makeBDDVarSet(apply_impl(v, unwrap(b), or)); } public BDDVarSet intersectWith(BDDVarSet b) { - int v2 = unwrap(b); - int v3 = apply_impl(v, v2, or); + /*bdd*/int v2 = unwrap(b); + /*bdd*/int v3 = apply_impl(v, v2, or); addref_impl(v3); delref_impl(v); if (this != b) @@ -274,7 +274,7 @@ } public int size() { int result = 0; - for (int p = v; p != one_impl(); p = high_impl(p)) { + for (/*bdd*/int p = v; p != one_impl(); p = high_impl(p)) { if (p == zero_impl()) throw new BDDException("varset contains zero"); ++result; @@ -284,7 +284,7 @@ public int[] toArray() { int[] result = new int[size()]; int k = -1; - for (int p = v; p != one_impl(); p = high_impl(p)) { + for (/*bdd*/int p = v; p != one_impl(); p = high_impl(p)) { result[++k] = var_impl(p); } return result; @@ -304,14 +304,14 @@ return makeBDDVarSet(apply_impl(v, unwrap(b), and)); } public BDDVarSet union(int var) { - int v2 = ithVar_impl(var); - int v3 = apply_impl(v, v2, and); + /*bdd*/int v2 = ithVar_impl(var); + /*bdd*/int v3 = apply_impl(v, v2, and); delref_impl(v2); return makeBDDVarSet(v3); } public BDDVarSet unionWith(BDDVarSet b) { - int v2 = unwrap(b); - int v3 = apply_impl(v, v2, and); + /*bdd*/int v2 = unwrap(b); + /*bdd*/int v3 = apply_impl(v, v2, and); addref_impl(v3); delref_impl(v); if (this != b) @@ -320,8 +320,8 @@ return this; } public BDDVarSet unionWith(int var) { - int v2 = ithVar_impl(var); - int v3 = apply_impl(v, v2, and); + /*bdd*/int v2 = ithVar_impl(var); + /*bdd*/int v3 = apply_impl(v, v2, and); addref_impl(v3); delref_impl(v); delref_impl(v2); @@ -348,14 +348,14 @@ } - protected IntBDDVarSet makeBDDVarSet(int v) { + protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) { if (USE_FINALIZER) return new IntBDDVarSetWithFinalizer(v); else return new IntBDDVarSet(v); } - protected static final int unwrap(BDDVarSet b) { + protected static final /*bdd*/int unwrap(BDDVarSet b) { return ((IntBDDVarSet) b).v; } @@ -371,11 +371,11 @@ } - public BDD ithVar(int var) { + public BDD ithVar(/*bdd*/int var) { return makeBDD(ithVar_impl(var)); } - public BDD nithVar(int var) { + public BDD nithVar(/*bdd*/int var) { return makeBDD(nithVar_impl(var)); } @@ -399,12 +399,12 @@ return makeBDD(zero_impl()); } - protected int[] to_free = new int[8]; - protected int to_free_length = 0; + protected /*bdd*/int[] to_free = new /*bdd*/int[8]; + protected /*bdd*/int to_free_length = 0; public void deferredFree(int v) { synchronized(to_free) { if (to_free_length == to_free.length) { - int[] t = new int[to_free.length * 2]; + /*bdd*/int[] t = new /*bdd*/int[to_free.length * 2]; System.arraycopy(to_free, 0, t, 0, to_free.length); to_free = t; } Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-21 14:32:02 UTC (rev 461) @@ -3,632 +3,257 @@ // Licensed under the terms of the GNU LGPL; see COPYING for details. package net.sf.javabdd; -import java.util.Collection; -import java.math.BigInteger; +import java.lang.reflect.Method; - /** * JDDFactory * * @author John Whaley * @version $Id$ */ -public class JDDFactory extends BDDFactory { +public class JDDFactory extends BDDFactoryIntImpl { - private final jdd.bdd.BDD bdd; - private int[] vars; // indexed by EXTERNAL - private int[] level2var; // internal -> external - private int[] var2level; // external -> internal + public static final String REVISION = "$Revision$"; - private JDDFactory(int nodenum, int cachesize) { - bdd = new jdd.bdd.BDD(nodenum, cachesize); - vars = new int[256]; - jdd.util.Options.verbose = true; + public String getVersion() { + return "JDDFactory "+REVISION.substring(11, REVISION.length()-2); } - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#init(int, int) - */ - public static BDDFactory init(int nodenum, int cachesize) { - BDDFactory f = new JDDFactory(nodenum, cachesize); - return f; + static final int INVALID_BDD = -1; + + // Redirection functions. + + protected void addref_impl(int v) { bdd.ref(v); } + protected void delref_impl(int v) { bdd.deref(v); } + protected int zero_impl() { return bdd.getZero(); } + protected int one_impl() { return bdd.getOne(); } + protected int invalid_bdd_impl() { return INVALID_BDD; } + protected int var_impl(int index) { + int v = level_impl(index); + return level2var != null ? level2var[v] : v; } - - /** - * Wrapper for the BDD index number used internally in the representation. - */ - private class bdd extends BDD { - int _index; - - static final int INVALID_BDD = -1; - - bdd(int index) { - this._index = index; - bdd.ref(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#getFactory() - */ - public BDDFactory getFactory() { - return JDDFactory.this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isZero() - */ - public boolean isZero() { - return _index == bdd.getZero(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#isOne() - */ - public boolean isOne() { - return _index == bdd.getOne(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#var() - */ - public int var() { - int v = bdd.getVar(_index); - return level2var != null ? level2var[v] : v; - } - - public int level() { - int v = bdd.getVar(_index); - return v; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#high() - */ - public BDD high() { - return new bdd(bdd.getHigh(_index)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#low() - */ - public BDD low() { - return new bdd(bdd.getLow(_index)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#id() - */ - public BDD id() { - return new bdd(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#not() - */ - public BDD not() { - return new bdd(bdd.not(_index)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD) - */ - public BDD ite(BDD thenBDD, BDD elseBDD) { - int x = _index; - int y = ((bdd) thenBDD)._index; - int z = ((bdd) elseBDD)._index; - return new bdd(bdd.ite(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet) - */ - public BDD relprod(BDD that, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return new bdd(bdd.relProd(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int) - */ - public BDD compose(BDD g, int var) { - int x = _index; - int y = ((bdd) g)._index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing) - */ - public BDD veccompose(BDDPairing pair) { - int x = _index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD) - */ - public BDD constrain(BDD that) { - int x = _index; - int y = ((bdd) that)._index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet) - */ - public BDD exist(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return new bdd(bdd.exists(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet) - */ - public BDD forAll(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return new bdd(bdd.forall(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet) - */ - public BDD unique(BDDVarSet var) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - return null; // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD) - */ - public BDD restrict(BDD var) { - int x = _index; - int y = ((bdd) var)._index; - return new bdd(bdd.restrict(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD) - */ - public BDD restrictWith(BDD that) { - int x = _index; - int y = ((bdd) that)._index; - int a = bdd.restrict(x, y); - //System.out.println("restrictWith("+System.identityHashCode(this)+") "+x+" -> "+a); - bdd.deref(x); - if (this != that) - that.free(); - bdd.deref(a); - this._index = a; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet) - */ - public BDD simplify(BDDVarSet d) { - int x = _index; - int y = ((bdd) ((BDDVarSet.DefaultImpl) d).b)._index; - return new bdd(bdd.simplify(x, y)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#support() - */ - public BDDVarSet support() { - int x = _index; - return new BDDVarSet.DefaultImpl(new bdd(bdd.support(x))); - } - - private int apply0(int x, int y, int z) { - int r; - switch (z) { - case 0: r = bdd.and(x, y); break; - case 1: r = bdd.xor(x, y); break; - case 2: r = bdd.or(x, y); break; - case 3: r = bdd.nand(x, y); break; - case 4: r = bdd.nor(x, y); break; - case 5: r = bdd.imp(x, y); break; - case 6: r = bdd.biimp(x, y); break; - case 7: r = bdd.and(x, bdd.not(y)); break; // diff - default: - throw new BDDException(); // TODO. - } - return r; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD apply(BDD that, BDDOp opr) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - return new bdd(apply0(x, y, z)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp) - */ - public BDD applyWith(BDD that, BDDOp opr) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = apply0(x, y, z); - bdd.deref(x); - if (this != that) - that.free(); - bdd.ref(a); - this._index = a; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) - */ - public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - // todo: combine. - int r = apply0(x, y, z); - bdd.ref(r); - int r2 = bdd.forall(r, a); - bdd.deref(r); - return new bdd(r2); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) - */ - public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - // todo: combine. - int r = apply0(x, y, z); - bdd.ref(r); - int r2 = bdd.exists(r, a); - bdd.deref(r); - return new bdd(r2); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet) - */ - public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) { - int x = _index; - int y = ((bdd) that)._index; - int z = opr.id; - int a = ((bdd) ((BDDVarSet.DefaultImpl) var).b)._index; - throw new BDDException(); // todo. - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne() - */ - public BDD satOne() { - int x = _index; - return new bdd(bdd.oneSat(x)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing) - */ - public BDD replace(BDDPairing pair) { - int x = _index; - return new bdd(bdd.replace(x, ((bddPairing) pair).pairing)); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing) - */ - public BDD replaceWith(BDDPairing pair) { - int x = _index; - int y = bdd.replace(x, ((bddPairing) pair).pairing); - //System.out.println("replaceWith("+System.identityHashCode(this)+") "+x+" -> "+y); - bdd.deref(x); - bdd.ref(y); - _index = y; - return this; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#nodeCount() - */ - public int nodeCount() { - return bdd.nodeCount(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satCount() - */ - public double satCount() { - return bdd.satCount(_index); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD) - */ - public boolean equals(BDD that) { - return this._index == ((bdd) that)._index; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#hashCode() - */ - public int hashCode() { - return _index; - } - - static final boolean USE_FINALIZER = false; - - /** - * @see java.lang.Object#finalize() - */ - /* - protected void finalize() throws Throwable { - super.finalize(); - if (USE_FINALIZER) { - if (false && _index >= 0) { - System.out.println("BDD not freed! "+System.identityHashCode(this)); - } - this.free(); - } - } - */ - - /** - * @see net.sf.javabdd.BDD#free() - */ - public void free() { - bdd.deref(_index); - _index = INVALID_BDD; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#fullSatOne() - */ - public BDD fullSatOne() { + protected int level_impl(int index) { + // NOTE: jdd seems to returns the total number of variables when + // calling getVar() on a terminal. + int v = bdd.getVar(index); + if (index == bdd.getOne() || index == bdd.getZero()) throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean) - */ - public BDD satOne(BDDVarSet var, boolean pol) { - // TODO Implement this. - throw new UnsupportedOperationException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#pathCount() - */ - public double pathCount() { + if (v == -1) throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#varProfile() - */ - public int[] varProfile() { + return v; + } + protected int low_impl(int v) { + if (v == bdd.getOne() || v == bdd.getZero()) throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDD#toVarSet() - */ - public BDDVarSet toVarSet() { - return new BDDVarSet.DefaultImpl(new bdd(_index)); - } - + return bdd.getLow(v); } - - private class bddPairing extends BDDPairing { - - private int[] from; - private int[] to; - private jdd.bdd.Permutation pairing; - - private bddPairing() { - reset(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDPairing#set(int, int) - */ - public void set(int oldvar, int newvar) { - for (int i = 0; i < from.length; ++i) { - if (from[i] == vars[oldvar]) { - to[i] = vars[newvar]; - pairing = bdd.createPermutation(from, to); - return; - } - } - int[] oldfrom = from; - from = new int[from.length + 1]; - System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); - from[oldfrom.length] = vars[oldvar]; - int[] oldto = to; - to = new int[to.length + 1]; - System.arraycopy(oldto, 0, to, 0, oldto.length); - to[oldto.length] = vars[newvar]; - pairing = bdd.createPermutation(from, to); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD) - */ - public void set(int oldvar, BDD newvar) { + protected int high_impl(int v) { + if (v == bdd.getOne() || v == bdd.getZero()) throw new BDDException(); + return bdd.getHigh(v); + } + protected int ithVar_impl(int var) { + if (var >= bdd.numberOfVariables()) + throw new BDDException(); + return vars[var]; + } + protected int nithVar_impl(int var) { + if (var >= bdd.numberOfVariables()) + throw new BDDException(); + return bdd.not(vars[var]); + } + protected int ite_impl(int v1, int v2, int v3) { return bdd.ite(v1, v2, v3); } + protected int apply_impl(int x, int y, BDDOp opr) { + int r; + switch (opr.id) { + case 0: r = bdd.and(x, y); break; + case 1: r = bdd.xor(x, y); break; + case 2: r = bdd.or(x, y); break; + case 3: r = bdd.nand(x, y); break; + case 4: r = bdd.nor(x, y); break; + case 5: r = bdd.imp(x, y); break; + case 6: r = bdd.biimp(x, y); break; + case 7: r = bdd.and(x, bdd.not(y)); break; // diff + default: + throw new UnsupportedOperationException(); // TODO. } - - public void set(int[] oldvar, int[] newvar) { - int[] oldfrom = from; - from = new int[from.length + oldvar.length]; - System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); - for (int i = 0; i < oldvar.length; ++i) { - from[i + oldfrom.length] = vars[oldvar[i]]; - } - int[] oldto = to; - to = new int[to.length + newvar.length]; - System.arraycopy(oldto, 0, to, 0, oldto.length); - for (int i = 0; i < newvar.length; ++i) { - to[i + oldto.length] = vars[newvar[i]]; - } - //debug(); - pairing = bdd.createPermutation(from, to); + return r; + } + protected int not_impl(int v1) { return bdd.not(v1); } + protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { + // todo: combine. + int r = apply_impl(v1, v2, opr); + bdd.ref(r); + int r2 = bdd.forall(r, v3); + bdd.deref(r); + return r2; + } + protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { + if (opr == and) + return bdd.relProd(v1, v2, v3); + // todo: combine. + int r = apply_impl(v1, v2, opr); + bdd.ref(r); + int r2 = bdd.exists(r, v3); + bdd.deref(r); + return r2; + } + protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { + throw new UnsupportedOperationException(); // todo. + } + protected int compose_impl(int v1, int v2, int var) { + throw new UnsupportedOperationException(); // todo. + } + protected int constrain_impl(int v1, int v2) { + throw new UnsupportedOperationException(); // todo. + } + protected int restrict_impl(int v1, int v2) { return bdd.restrict(v1, v2); } + protected int simplify_impl(int v1, int v2) { return bdd.simplify(v1, v2); } + protected int support_impl(int v) { return bdd.support(v); } + protected int exist_impl(int v1, int v2) { return bdd.exists(v1, v2); } + protected int forAll_impl(int v1, int v2) { return bdd.forall(v1, v2); } + protected int unique_impl(int v1, int v2) { + throw new UnsupportedOperationException(); // todo. + } + protected int fullSatOne_impl(int v) { + if (v == bdd.getZero()) + return v; + int[] res = bdd.oneSat(v, null); + int result = bdd.getOne(); + for (int i = res.length - 1; i >= 0; --i) { + int u; + if (res[i] == 1) + u = bdd.mk(i, 0, result); + else + u = bdd.mk(i, result, 0); + bdd.ref(u); bdd.deref(result); + result = u; } - - void debug() { - for (int i = 0; i < from.length; ++i) { - System.out.println(bdd.getVar(from[i])+" -> "+bdd.getVar(to[i])); + bdd.deref(result); + return result; + } + + protected int replace_impl(int v, BDDPairing p) { return bdd.replace(v, ((bddPairing) p).pairing); } + protected int veccompose_impl(int v, BDDPairing p) { + throw new UnsupportedOperationException(); // todo. + } + + protected int nodeCount_impl(int v) { return bdd.nodeCount(v); } + protected double pathCount_impl(int v) { + throw new UnsupportedOperationException(); // todo. + } + protected double satCount_impl(int v) { return bdd.satCount(v); } + protected int satOne_impl(int v) { return bdd.oneSat(v); } + protected int satOne_impl2(int v1, int v2, boolean pol) { + if (v1 == bdd.getZero()) + return v1; + int[] res = bdd.oneSat(v1, null); + int result = bdd.getOne(); + for (int i = res.length - 1; i >= 0; --i) { + while (bdd.getVar(v2) < i) + v2 = bdd.getHigh(v2); + boolean p; + if (res[i] == 1) p = true; + else if (res[i] == 0) p = false; + else { + if (bdd.getVar(v2) != i) + continue; + p = pol; } + int u = bdd.mk(i, p?0:result, p?result:0); + bdd.ref(u); bdd.deref(result); + result = u; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDPairing#reset() - */ - public void reset() { - from = to = new int[] { }; - pairing = null; - } - + bdd.deref(result); + return result; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#zero() - */ - public BDD zero() { - return new bdd(bdd.getZero()); + protected int nodeCount_impl2(int[] v) { + throw new UnsupportedOperationException(); // todo. } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#one() - */ - public BDD one() { - return new bdd(bdd.getOne()); + protected int[] varProfile_impl(int v) { + throw new UnsupportedOperationException(); // todo. } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#initialize(int, int) - */ - protected void initialize(int nodenum, int cachesize) { - throw new BDDException(); + protected void printTable_impl(int v) { + throw new UnsupportedOperationException(); // todo. } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#isInitialized() - */ - public boolean isInitialized() { - // TODO Auto-generated method stub - return true; + + // More redirection functions. + + protected void initialize(int initnodesize, int cs) { + bdd = new jdd.bdd.BDD(initnodesize, cs); + vars = new int[256]; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#done() - */ - public void done() { - bdd.cleanup(); + public void addVarBlock(int first, int last, boolean fixed) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setError(int) - */ + public void varBlockAll() { + throw new UnsupportedOperationException(); + } + public void clearVarBlocks() { + throw new UnsupportedOperationException(); + } + public void printOrder() { + throw new UnsupportedOperationException(); + } + public int getNodeTableSize() { + // todo. + return bdd.countRootNodes(); + } + public int setNodeTableSize(int x) { + // TODO. + return getNodeTableSize(); + } + public int setCacheSize(int x) { + // TODO. + return 0; + } + public boolean isInitialized() { return true; } + public void done() { bdd.cleanup(); bdd = null; } public void setError(int code) { - // TODO Implement this. + // todo: implement this } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#clearError() - */ public void clearError() { - // TODO Implement this. + // todo: implement this } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setMaxNodeNum(int) - */ public int setMaxNodeNum(int size) { - // TODO Auto-generated method stub - //throw new BDDException(); + // todo: implement this return 0; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setMinFreeNodes(double) - */ public double setMinFreeNodes(double x) { int old = jdd.util.Configuration.minFreeNodesProcent; jdd.util.Configuration.minFreeNodesProcent = (int)(x * 100); return (double) old / 100.; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double) - */ - public double setIncreaseFactor(double x) { - // TODO. - return 0.; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setMaxIncrease(int) - */ public int setMaxIncrease(int x) { int old = jdd.util.Configuration.maxNodeIncrease; jdd.util.Configuration.maxNodeIncrease = x; return old; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setNodeTableSize(int) - */ - public int setNodeTableSize(int x) { - // TODO. - return getNodeTableSize(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setCacheSize(int) - */ - public int setCacheSize(int x) { - // TODO. + public double setIncreaseFactor(double x) { + // todo: implement this return 0; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getCacheSize() - */ + public int getNodeNum() { + // todo. + return bdd.countRootNodes(); + } public int getCacheSize() { // TODO Implement this. + return 0; + } + public int reorderGain() { throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setCacheRatio(int) - */ + public void printStat() { + bdd.showStats(); + } public double setCacheRatio(double x) { - // TODO Auto-generated method stub + // TODO Implement this. return 0; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#varNum() - */ public int varNum() { return bdd.numberOfVariables(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setVarNum(int) - */ public int setVarNum(int num) { if (num > Integer.MAX_VALUE / 2) throw new BDDException(); @@ -664,128 +289,13 @@ } return old; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#duplicateVar(int) - */ - public int duplicateVar(int var) { - // TODO Implement this. + public void printAll() { throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#ithVar(int) - */ - public BDD ithVar(int var) { - if (var >= bdd.numberOfVariables()) - throw new BDDException(); - //int v = var2level != null ? var2level[var] : var; - int v = var; - return new bdd(vars[v]); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#nithVar(int) - */ - public BDD nithVar(int var) { - if (var >= bdd.numberOfVariables()) - throw new BDDException(); - //int v = var2level != null ? var2level[var] : var; - int v = var; - return new bdd(bdd.not(vars[v])); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printAll() - */ - public void printAll() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD) - */ - public void printTable(BDD b) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#level2Var(int) - */ - public int level2Var(int level) { - return level2var != null ? level2var[level] : level; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#var2Level(int) - */ - public int var2Level(int var) { - return var2level != null ? var2level[var] : var; - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod) - */ - public void reorder(ReorderMethod m) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod) - */ - public void autoReorder(ReorderMethod method) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int) - */ - public void autoReorder(ReorderMethod method, int max) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getReorderMethod() - */ - public ReorderMethod getReorderMethod() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getReorderTimes() - */ - public int getReorderTimes() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#disableReorder() - */ - public void disableReorder() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#enableReorder() - */ - public void enableReorder() { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorderVerbose(int) - */ - public int reorderVerbose(int v) { - throw new BDDException(); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#setVarOrder(int[]) - */ public void setVarOrder(int[] neworder) { - // todo: setting var order corrupts all existing BDD's! + // todo: setting var order corrupts all existing BDDs! if (var2level != null) - throw new BDDException(); + throw new UnsupportedOperationException(); if (bdd.numberOfVariables() != neworder.length) throw new BDDException(); @@ -809,139 +319,149 @@ //System.out.println("Set for domain "+d+": "+d.var.toStringWithDomains()); } } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean) - */ - public void addVarBlock(BDD var, boolean fixed) { - throw new BDDException(); + public int level2Var(int level) { return level2var != null ? level2var[level] : level; } + public int var2Level(int var) { return var2level != null ? var2level[var] : var; } + public ReorderMethod getReorderMethod() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean) - */ - public void addVarBlock(int first, int last, boolean fixed) { - throw new BDDException(); + public int getReorderTimes() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#varBlockAll() - */ - public void varBlockAll() { - throw new BDDException(); + public void disableReorder() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#clearVarBlocks() - */ - public void clearVarBlocks() { - throw new BDDException(); + public void enableReorder() { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printOrder() - */ - public void printOrder() { - throw new BDDException(); + public int reorderVerbose(int v) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection) - */ - public int nodeCount(Collection r) { - throw new BDDException(); + public void reorder(ReorderMethod m) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getNodeTableSize() - */ - public int getNodeTableSize() { - // todo. - return bdd.countRootNodes(); + public void autoReorder(ReorderMethod method) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getNodeNum() - */ - public int getNodeNum() { - // todo. - return bdd.countRootNodes(); + public void autoReorder(ReorderMethod method, int max) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#reorderGain() - */ - public int reorderGain() { - throw new BDDException(); + public void swapVar(int v1, int v2) { + throw new UnsupportedOperationException(); } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#printStat() - */ - public void printStat() { - bdd.showStats(); + + private jdd.bdd.BDD bdd; + private int[] vars; // indexed by EXTERNAL + private int[] level2var; // internal -> external + private int[] var2level; // external -> internal + + static { + jdd.util.Options.verbose = true; } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#makePair() - */ - public BDDPairing makePair() { - return new bddPairing(); + + private JDDFactory(int nodenum, int cachesize) { + initialize(nodenum, cachesize); } - + /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#swapVar(int, int) + * @see net.sf.javabdd.BDDFactory#init(int, int) */ - public void swapVar(int v1, int v2) { - throw new BDDException(); + public static BDDFactory init(int nodenum, int cachesize) { + BDDFactory f = new JDDFactory(nodenum, cachesize); + return f; } - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger) - */ - protected BDDDomain createDomain(int a, BigInteger b) { - return new bddDomain(a, b); - } - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#createBitVector(int) - */ - protected BDDBitVector createBitVector(int a) { - return new bddBitVector(a); - } - - private class bddDomain extends BDDDomain { - - private bddDomain(int a, BigInteger b) { - super(a, b); + private class bddPairing extends BDDPairing { + + private int[] from; + private int[] to; + private jdd.bdd.Permutation pairing; + + private bddPairing() { + reset(); } - + /* (non-Javadoc) - * @see net.sf.javabdd.BDDBitVector#getFactory() + * @see net.sf.javabdd.BDDPairing#set(int, int) */ - public BDDFactory getFactory() { return JDDFactory.this; } - - } - - private class bddBitVector extends BDDBitVector { - - private bddBitVector(int a) { - super(a); + public void set(int oldvar, int newvar) { + for (int i = 0; i < from.length; ++i) { + if (from[i] == vars[oldvar]) { + to[i] = vars[newvar]; + pairing = bdd.createPermutation(from, to); + return; + } + } + int[] oldfrom = from; + from = new int[from.length + 1]; + System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); + from[oldfrom.length] = vars[oldvar]; + int[] oldto = to; + to = new int[to.length + 1]; + System.arraycopy(oldto, 0, to, 0, oldto.length); + to[oldto.length] = vars[newvar]; + pairing = bdd.createPermutation(from, to); } - + /* (non-Javadoc) - * @see net.sf.javabdd.BDDBitVector#getFactory() + * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD) */ - public BDDFactory getFactory() { return JDDFactory.this; } - + public void set(int oldvar, BDD newvar) { + throw new UnsupportedOperationException(); + } + + public void set(int[] oldvar, int[] newvar) { + int[] oldfrom = from; + from = new int[from.length + oldvar.length]; + System.arraycopy(oldfrom, 0, from, 0, oldfrom.length); + for (int i = 0; i < oldvar.length; ++i) { + from[i + oldfrom.length] = vars[oldvar[i]]; + } + int[] oldto = to; + to = new int[to.length + newvar.length]; + System.arraycopy(oldto, 0, to, 0, oldto.length); + for (int i = 0; i < newvar.length; ++i) { + to[i + oldto.length] = vars[newvar[i]]; + } + //debug(); + pairing = bdd.createPermutation(from, to); + } + + void debug() { + for (int i = 0; i < from.length; ++i) { + System.out.println(bdd.getVar(from[i])+" -> "+bdd.getVar(to[i])); + } + } + + /* (non-Javadoc) + * @see net.sf.javabdd.BDDPairing#reset() + */ + public void reset() { + from = to = new int[] { }; + pairing = null; + } + } - public static final String REVISION = "$Revision$"; - - /* (non-Javadoc) - * @see net.sf.javabdd.BDDFactory#getVersion() - */ - public String getVersion() { - return "JDD "+REVISION.substring(11, REVISION.length()-2); + public BDDPairing makePair() { + return new bddPairing(); } + + public void registerGCCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void unregisterGCCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void registerReorderCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void unregisterReorderCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void registerResizeCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } + public void unregisterResizeCallback(Object o, Method m) { + throw new UnsupportedOperationException(); + } } Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-17 16:03:04 UTC (rev 460) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-21 14:32:02 UTC (rev 461) @@ -28,8 +28,16 @@ */ public class JFactory extends BDDFactoryIntImpl { - static final boolean VERIFY_ASSERTIONS = false; + /**** Options ****/ + + /** + * Flush the operation cache on every garbage collection. If this is false, + * we only clean the collected entries on every GC, rather than emptying the + * whole cache. For most problems, you should keep this set to true. + */ public static boolean FLUSH_CACHE_ON_GC = true; + + static final boolean VERIFY_ASSERTIONS = false; static final boolean CACHESTATS = false; static final boolean SWAPCOUNT = false; @@ -47,11 +55,20 @@ public static BDDFactory init(int nodenum, int cachesize) { BDDFactory f = new JFactory(); f.initialize(nodenum, cachesize); + if (CACHESTATS) addShutdownHook(f); return f; } - public boolean ZDD = false; + static void addShutdownHook(final BDDFactory f) { + Runtime.getRuntime().addShutdownHook(new Thread() { + public void run() { + System.out.println(f.getCacheStats().toString()); + } + }); + } + boolean ZDD = false; + /** * Implementation of BDDPairing used by JFactory. */ @@ -122,7 +139,7 @@ protected void addref_impl(int v) { bdd_addref(v); } protected void delref_impl(int v) { bdd_delref(v); } protected int zero_impl() { return BDDZERO; } - protected int one_impl() {return BDDONE; } + protected int one_impl() { return BDDONE; } protected int invalid_bdd_impl() { return INVALID_BDD; } protected int var_impl(int v) { return bdd_var(v); } protected int level_impl(int v) { return LEVEL(v); } @@ -917,25 +934,20 @@ int bdd_not(int r) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(r, bddfalse); if (applycache == null) applycache = BddCacheI_init(cachesize); again : for (;;) { try { INITREF(); - - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); res = ZDD ? znot_rec(r) : not_rec(r); - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - if (firstReorder-- == 1) - continue again; - res = bddfalse; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -948,10 +960,8 @@ BddCacheDataI entry; int res; - if (ISZERO(r)) - return bddtrue; - if (ISONE(r)) - return bddfalse; + if (ISCONST(r)) + return 1 - r; entry = BddCache_lookupI(applycache, NOTHASH(r)); @@ -1007,7 +1017,7 @@ int bdd_ite(int f, int g, int h) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(f, bddfalse); CHECKa(g, bddfalse); @@ -1020,18 +1030,13 @@ try { INITREF(); - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); res = ZDD ? zite_rec(f, g, h) : ite_rec(f, g, h); - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -1201,7 +1206,7 @@ int bdd_replace(int r, bddPair pair) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(r, bddfalse); @@ -1214,18 +1219,13 @@ replacelast = pair.last; replaceid = (pair.id << 2) | CACHEID_REPLACE; - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); res = replace_rec(r); - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -1298,7 +1298,7 @@ int bdd_apply(int l, int r, int op) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(l, bddfalse); CHECKa(r, bddfalse); @@ -1315,29 +1315,22 @@ INITREF(); applyop = op; - if (firstReorder == 0) - bdd_disable_reorder(); + if (numReorder == 0) bdd_disable_reorder(); switch (op) { case bddop_and: res = ZDD ? zand_rec(l, r) : and_rec(l, r); break; case bddop_or: res = ZDD ? zor_rec(l, r) : or_rec(l, r); break; case bddop_diff: res = ZDD ? zdiff_rec(l, r) : apply_rec(l, r); break; default: res = apply_rec(l, r); break; } - if (firstReorder == 0) - bdd_enable_reorder(); + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } - //validate(res); - checkresize(); return res; } @@ -1705,7 +1698,7 @@ int bdd_appex(int l, int r, int opr, int var) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(l, bddfalse); CHECKa(r, bddfalse); @@ -1734,18 +1727,16 @@ appexid = (var << 5) | (appexop << 1); /* FIXME: range! */ quantid = (appexid << 3) | CACHEID_APPEX; - if (firstReorder == 0) + if (numReorder == 0) bdd_disable_reorder(); res = opr == bddop_and ? relprod_rec(l, r) : appquant_rec(l, r); - if (firstReorder == 0) + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -2073,7 +2064,7 @@ int bdd_constrain(int f, int c) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(f, bddfalse); CHECKa(c, bddfalse); @@ -2085,18 +2076,16 @@ INITREF(); miscid = CACHEID_CONSTRAIN; - if (firstReorder == 0) + if (numReorder == 0) bdd_disable_reorder(); res = constrain_rec(f, c); - if (firstReorder == 0) + if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); - if (firstReorder-- == 1) - continue again; - res = BDDZERO; - /* avoid warning about res being uninitialized */ + numReorder--; + continue again; } break; } @@ -2166,7 +2155,7 @@ int bdd_compose(int f, int g, int var) { int res; - firstReorder = 1; + int numReorder = 1; CHECKa(f, bddfalse); CHECKa(g, bddfalse); @@ -2184,18 +2173,16 @@ composelevel = bddvar2level[var]; replaceid = (composelevel << 2) | CACHEID_COMPOSE; - if (firstReorder == 0) + if (numReorder == 0) bdd_disable_reorder(); res = compose_rec(f, g); - if (fir... [truncated message content] |
|
From: <joe...@us...> - 2006-07-26 17:46:44
|
Revision: 465 Author: joewhaley Date: 2006-07-26 09:42:44 -0700 (Wed, 26 Jul 2006) ViewCVS: http://svn.sourceforge.net/javabdd/?rev=465&view=rev Log Message: ----------- Improved ZDD support. Modified Paths: -------------- trunk/JavaBDD/net/sf/javabdd/BDD.java trunk/JavaBDD/net/sf/javabdd/BDDFactory.java trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java trunk/JavaBDD/net/sf/javabdd/JDDFactory.java trunk/JavaBDD/net/sf/javabdd/JFactory.java trunk/JavaBDD/net/sf/javabdd/MicroFactory.java Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-07-26 16:42:44 UTC (rev 465) @@ -48,6 +48,14 @@ public abstract boolean isOne(); /** + * <p>Returns true if this BDD is the universe BDD. + * The universal BDD differs from the one BDD in ZDD mode.</p> + * + * @return true if this BDD is the universe BDD + */ + public boolean isUniverse() { return isOne(); } + + /** * <p>Converts this BDD to a new BDDVarSet.</p> * * <p>This BDD must be a boolean function that represents the all-true minterm Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -196,6 +196,14 @@ public abstract BDD one(); /** + * <p>Get the constant universe BDD. + * (The universe BDD differs from the one BDD in ZDD mode.)</p> + * + * <p>Compare to bdd_true.</p> + */ + public BDD universe() { return one(); } + + /** * <p>Get an empty BDDVarSet.</p> * * <p>Compare to bdd_true.</p> Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-07-26 16:42:44 UTC (rev 465) @@ -20,6 +20,7 @@ protected abstract void delref_impl(/*bdd*/int v); protected abstract /*bdd*/int zero_impl(); protected abstract /*bdd*/int one_impl(); + protected /*bdd*/int universe_impl() { return one_impl(); } protected abstract /*bdd*/int invalid_bdd_impl(); protected abstract int var_impl(/*bdd*/int v); protected abstract int level_impl(/*bdd*/int v); @@ -28,6 +29,7 @@ protected abstract /*bdd*/int ithVar_impl(int var); protected abstract /*bdd*/int nithVar_impl(int var); + protected abstract /*bdd*/int makenode_impl(int lev, /*bdd*/int lo, /*bdd*/int hi); protected abstract /*bdd*/int ite_impl(/*bdd*/int v1, /*bdd*/int v2, /*bdd*/int v3); protected abstract /*bdd*/int apply_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr); protected abstract /*bdd*/int not_impl(/*bdd*/int v1); @@ -121,6 +123,9 @@ public boolean isOne() { return v == one_impl(); } + public boolean isUniverse() { + return v == universe_impl(); + } public boolean isZero() { return v == zero_impl(); } @@ -236,7 +241,7 @@ public class IntBDDVarSet extends BDDVarSet { /*bdd*/int v; - private IntBDDVarSet(/*bdd*/int v) { + protected IntBDDVarSet(/*bdd*/int v) { this.v = v; addref_impl(v); } @@ -256,12 +261,15 @@ public BDDVarSet id() { return makeBDDVarSet(v); } + protected int do_intersect(int v1, int v2) { + return apply_impl(v1, v2, or); + } public BDDVarSet intersect(BDDVarSet b) { - return makeBDDVarSet(apply_impl(v, unwrap(b), or)); + return makeBDDVarSet(do_intersect(v, unwrap(b))); } public BDDVarSet intersectWith(BDDVarSet b) { /*bdd*/int v2 = unwrap(b); - /*bdd*/int v3 = apply_impl(v, v2, or); + /*bdd*/int v3 = do_intersect(v, v2); addref_impl(v3); delref_impl(v); if (this != b) @@ -300,18 +308,21 @@ } return result; } + protected int do_unionvar(int v, int var) { + return apply_impl(v, ithVar_impl(var), and); + } + protected int do_union(int v1, int v2) { + return apply_impl(v1, v2, and); + } public BDDVarSet union(BDDVarSet b) { - return makeBDDVarSet(apply_impl(v, unwrap(b), and)); + return makeBDDVarSet(do_union(v, unwrap(b))); } public BDDVarSet union(int var) { - /*bdd*/int v2 = ithVar_impl(var); - /*bdd*/int v3 = apply_impl(v, v2, and); - delref_impl(v2); - return makeBDDVarSet(v3); + return makeBDDVarSet(do_unionvar(v, var)); } public BDDVarSet unionWith(BDDVarSet b) { /*bdd*/int v2 = unwrap(b); - /*bdd*/int v3 = apply_impl(v, v2, and); + /*bdd*/int v3 = do_union(v, v2); addref_impl(v3); delref_impl(v); if (this != b) @@ -320,11 +331,9 @@ return this; } public BDDVarSet unionWith(int var) { - /*bdd*/int v2 = ithVar_impl(var); - /*bdd*/int v3 = apply_impl(v, v2, and); + /*bdd*/int v3 = do_unionvar(v, var); addref_impl(v3); delref_impl(v); - delref_impl(v2); v = v3; return this; } @@ -348,11 +357,106 @@ } + public class IntZDDVarSet extends IntBDDVarSet { + protected IntZDDVarSet(/*bdd*/int v) { + super(v); + } + protected int do_intersect(int v1, int v2) { + if (v1 == one_impl()) return v2; + if (v2 == one_impl()) return v1; + int l1, l2; + l1 = level_impl(v1); + l2 = level_impl(v2); + for (;;) { + if (v1 == v2) + return v1; + if (l1 < l2) { + v1 = high_impl(v1); + if (v1 == one_impl()) return v2; + l1 = level_impl(v1); + } else if (l1 > l2) { + v2 = high_impl(v2); + if (v2 == one_impl()) return v1; + l2 = level_impl(v2); + } else { + int k = do_intersect(high_impl(v1), high_impl(v2)); + addref_impl(k); + int result = makenode_impl(l1, zero_impl(), k); + delref_impl(k); + return result; + } + } + } + protected int do_union(int v1, int v2) { + if (v1 == v2) return v1; + if (v1 == one_impl()) return v2; + if (v2 == one_impl()) return v1; + int l1, l2; + l1 = level_impl(v1); + l2 = level_impl(v2); + int vv1 = v1, vv2 = v2, lev = l1; + if (l1 <= l2) + vv1 = high_impl(v1); + if (l1 >= l2) { + vv2 = high_impl(v2); + lev = l2; + } + int k = do_union(vv1, vv2); + addref_impl(k); + int result = makenode_impl(lev, zero_impl(), k); + delref_impl(k); + return result; + } + protected int do_unionvar(int v, int var) { + return do_unionlevel(v, var2Level(var)); + } + private int do_unionlevel(int v, int lev) { + if (v == one_impl()) + return makenode_impl(lev, zero_impl(), one_impl()); + int l = level_impl(v); + if (l == lev) { + return v; + } else if (l > lev) { + return makenode_impl(lev, zero_impl(), v); + } else { + int k = do_unionlevel(high_impl(v), lev); + addref_impl(k); + int result = makenode_impl(lev, zero_impl(), k); + return result; + } + } + } + + public class IntZDDVarSetWithFinalizer extends IntZDDVarSet { + + protected IntZDDVarSetWithFinalizer(int v) { + super(v); + } + + protected void finalize() throws Throwable { + super.finalize(); + if (USE_FINALIZER) { + if (false && v != invalid_bdd_impl()) { + System.out.println("BDD not freed! "+System.identityHashCode(this)); + } + deferredFree(v); + } + } + + } + protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) { - if (USE_FINALIZER) - return new IntBDDVarSetWithFinalizer(v); - else - return new IntBDDVarSet(v); + if (true || isZDD()) { + if (USE_FINALIZER) + return new IntZDDVarSetWithFinalizer(v); + else + return new IntZDDVarSet(v); + } else { + if (USE_FINALIZER) + return new IntBDDVarSetWithFinalizer(v); + else + return new IntBDDVarSet(v); + } } protected static final /*bdd*/int unwrap(BDDVarSet b) { @@ -387,6 +491,10 @@ return makeBDD(one_impl()); } + public BDD universe() { + return makeBDD(universe_impl()); + } + public BDDVarSet emptySet() { return makeBDDVarSet(one_impl()); } Modified: trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/BuDDyFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -115,6 +115,7 @@ protected int nithVar_impl(int var) { return nithVar0(var); } private static native int nithVar0(int var); + protected int makenode_impl(int lev, int lo, int hi) { return ite0(ithVar_impl(level2Var0(lev)), hi, lo); } protected int ite_impl(int v1, int v2, int v3) { return ite0(v1, v2, v3); } private static native int ite0(int b, int c, int d); protected int apply_impl(int v1, int v2, BDDOp opr) { return apply0(v1, v2, opr.id); } Modified: trunk/JavaBDD/net/sf/javabdd/JDDFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/JDDFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -62,6 +62,7 @@ throw new BDDException(); return bdd.not(vars[var]); } + protected int makenode_impl(int lev, int lo, int hi) { return bdd.mk(lev, lo, hi); } protected int ite_impl(int v1, int v2, int v3) { return bdd.ite(v1, v2, v3); } protected int apply_impl(int x, int y, BDDOp opr) { int r; Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -37,7 +37,7 @@ */ public static boolean FLUSH_CACHE_ON_GC = true; - static final boolean VERIFY_ASSERTIONS = false; + static final boolean VERIFY_ASSERTIONS = true; static final boolean CACHESTATS = false; static final boolean SWAPCOUNT = false; @@ -67,7 +67,7 @@ }); } - boolean ZDD = false; + boolean ZDD = true; /** * Implementation of BDDPairing used by JFactory. @@ -102,6 +102,7 @@ sb.append('{'); boolean any = false; for (int i = 0; i < result.length; ++i) { + // TODO: revisit for zdd if (result[i] != bdd_ithvar(bddlevel2var[i])) { if (any) sb.append(", "); any = true; @@ -124,6 +125,7 @@ bddPair p = new bddPair(); p.result = new int[bddvarnum]; int n; + // TODO: revisit for zdd for (n = 0; n < bddvarnum; n++) p.result[n] = bdd_ithvar(bddlevel2var[n]); @@ -140,6 +142,7 @@ protected void delref_impl(int v) { bdd_delref(v); } protected int zero_impl() { return BDDZERO; } protected int one_impl() { return BDDONE; } + protected int universe_impl() { return univ; } protected int invalid_bdd_impl() { return INVALID_BDD; } protected int var_impl(int v) { return bdd_var(v); } protected int level_impl(int v) { return LEVEL(v); } @@ -148,6 +151,12 @@ protected int ithVar_impl(int var) { return bdd_ithvar(var); } protected int nithVar_impl(int var) { return bdd_nithvar(var); } + protected int makenode_impl(int lev, int lo, int hi) { + if (ZDD) + return zdd_makenode(lev, lo, hi); + else + return bdd_makenode(lev, lo, hi); + } protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); } protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); } protected int not_impl(int v1) { return bdd_not(v1); } @@ -456,7 +465,7 @@ prev_interleaved = inter; } BddTree newchild = my_vartree[0]; - _assert(newchild.prev == null); + if (VERIFY_ASSERTIONS) _assert(newchild.prev == null); //while (newchild.prev != null) newchild = newchild.prev; if (parent == null) vartree = newchild; else parent.nextlevel = newchild; @@ -492,8 +501,6 @@ return null; } - - /***** IMPLEMENTATION BELOW *****/ static final int REF_MASK = 0xFFC00000; @@ -710,6 +717,7 @@ /*=== PRIVATE KERNEL VARIABLES =========================================*/ int[] bddvarset; /* Set of defined BDD variables */ + int univ = 1; /* Universal set (used for ZDD) */ int gbcollectnum; /* Number of garbage collections */ int cachesize; /* Size of the operator caches */ long gbcclock; /* Clock ticks used in GBC */ @@ -941,8 +949,10 @@ again : for (;;) { try { INITREF(); + if (numReorder == 0) bdd_disable_reorder(); - res = ZDD ? znot_rec(r) : not_rec(r); + if (ZDD) res = zdiff_rec(univ, r); + else res = not_rec(r); if (numReorder == 0) bdd_enable_reorder(); } catch (ReorderException x) { bdd_checkreorder(); @@ -985,36 +995,6 @@ return res; } - int znot_rec(int r) { - BddCacheDataI entry; - int res; - - if (ISZERO(r)) - return bddtrue; - if (ISONE(r)) - return bddfalse; - - entry = BddCache_lookupI(applycache, NOTHASH(r)); - - if (entry.a == r && entry.c == bddop_not) { - if (CACHESTATS) - cachestats.opHit++; - return entry.res; - } - if (CACHESTATS) - cachestats.opMiss++; - - PUSHREF(znot_rec(LOW(r))); - res = bdd_makenode(LEVEL(r), READREF(1), HIGH(r)); - POPREF(1); - - entry.a = r; - entry.c = bddop_not; - entry.res = res; - - return res; - } - int bdd_ite(int f, int g, int h) { int res; int numReorder = 1; @@ -1136,7 +1116,7 @@ if (ISONE(g) && ISZERO(h)) return f; if (ISZERO(g) && ISONE(h)) - return znot_rec(f); + return zdiff_rec(univ, f); int v = Math.min(LEVEL(g), LEVEL(h)); if (LEVEL(f) < v) @@ -1155,43 +1135,43 @@ if (LEVEL(f) == LEVEL(h)) { PUSHREF(zite_rec(LOW(f), LOW(g), LOW(h))); PUSHREF(zite_rec(HIGH(f), HIGH(g), HIGH(h))); - res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(f), READREF(2), READREF(1)); POPREF(2); } else if (LEVEL(f) < LEVEL(h)) { PUSHREF(zite_rec(LOW(f), LOW(g), h)); PUSHREF(zite_rec(HIGH(f), HIGH(g), 0)); - res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(f), READREF(2), READREF(1)); POPREF(2); } else /* f > h */ { PUSHREF(zite_rec(f, g, LOW(h))); - res = bdd_makenode(LEVEL(h), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1)); POPREF(1); } } else if (LEVEL(f) < LEVEL(g)) { if (LEVEL(f) == LEVEL(h)) { PUSHREF(zite_rec(LOW(f), g, LOW(h))); PUSHREF(zite_rec(HIGH(f), 0, HIGH(h))); - res = bdd_makenode(LEVEL(f), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(f), READREF(2), READREF(1)); POPREF(2); } else if (LEVEL(f) < LEVEL(h)) { res = zite_rec(LOW(f), g, h); } else /* f > h */ { PUSHREF(zite_rec(f, g, LOW(h))); - res = bdd_makenode(LEVEL(h), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1)); POPREF(1); } } else /* f > g */ { if (LEVEL(g) == LEVEL(h)) { PUSHREF(zite_rec(f, LOW(g), LOW(h))); - res = bdd_makenode(LEVEL(g), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(g), HIGH(h), READREF(1)); POPREF(1); } else if (LEVEL(g) < LEVEL(h)) { PUSHREF(zite_rec(f, LOW(g), h)); - res = bdd_makenode(LEVEL(g), 0, READREF(1)); + res = zdd_makenode(LEVEL(g), 0, READREF(1)); POPREF(1); } else /* g > h */ { PUSHREF(zite_rec(f, g, LOW(h))); - res = bdd_makenode(LEVEL(h), HIGH(h), READREF(1)); + res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1)); POPREF(1); } } @@ -1253,11 +1233,18 @@ PUSHREF(replace_rec(LOW(r))); PUSHREF(replace_rec(HIGH(r))); - res = - bdd_correctify( - LEVEL(replacepair[LEVEL(r)]), - READREF(2), - READREF(1)); + if (ZDD) + res = + zdd_correctify( + LEVEL(replacepair[LEVEL(r)]), + READREF(2), + READREF(1)); + else + res = + bdd_correctify( + LEVEL(replacepair[LEVEL(r)]), + READREF(2), + READREF(1)); POPREF(2); entry.a = r; @@ -1296,6 +1283,36 @@ return res; /* FIXME: cache ? */ } + int zdd_correctify(int level, int l, int r) { + // TODO: This function is wrong. Need to figure out how to do replace in ZDD. + int res; + + if (level < LEVEL(l) && level < LEVEL(r)) + return zdd_makenode(level, l, r); + + if (level == LEVEL(l) || level == LEVEL(r)) { + bdd_error(BDD_REPLACE); + return 0; + } + + if (LEVEL(l) == LEVEL(r)) { + PUSHREF(zdd_correctify(level, LOW(l), LOW(r))); + PUSHREF(zdd_correctify(level, HIGH(l), HIGH(r))); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else if (LEVEL(l) < LEVEL(r)) { + PUSHREF(zdd_correctify(level, LOW(l), r)); + PUSHREF(zdd_correctify(level, HIGH(l), r)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); + } else { + PUSHREF(zdd_correctify(level, l, LOW(r))); + PUSHREF(zdd_correctify(level, l, HIGH(r))); + res = zdd_makenode(LEVEL(r), READREF(2), READREF(1)); + } + POPREF(2); + + return res; /* FIXME: cache ? */ + } + int bdd_apply(int l, int r, int op) { int res; int numReorder = 1; @@ -1483,7 +1500,7 @@ PUSHREF(zand_rec(LOW(l), LOW(r))); PUSHREF(zand_rec(HIGH(l), HIGH(r))); - res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); POPREF(2); @@ -1547,8 +1564,8 @@ if (l == r) return l; - if (ISONE(l) || ISONE(r)) - return 1; + //if (ISONE(l) || ISONE(r)) + // return 1; if (ISZERO(l)) return r; if (ISZERO(r)) @@ -1566,15 +1583,15 @@ if (LEVEL(l) == LEVEL(r)) { PUSHREF(zor_rec(LOW(l), LOW(r))); PUSHREF(zor_rec(HIGH(l), HIGH(r))); - res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); POPREF(2); } else { if (LEVEL(l) < LEVEL(r)) { PUSHREF(zor_rec(LOW(l), r)); - res = bdd_makenode(LEVEL(l), READREF(1), HIGH(l)); + res = zdd_makenode(LEVEL(l), READREF(1), HIGH(l)); } else { PUSHREF(zor_rec(l, LOW(r))); - res = bdd_makenode(LEVEL(r), READREF(1), HIGH(r)); + res = zdd_makenode(LEVEL(r), READREF(1), HIGH(r)); } POPREF(1); } @@ -1591,16 +1608,16 @@ BddCacheDataI entry; int res; - if (ISZERO(l) || ISONE(r) || l == r) + if (ISZERO(l) /*|| ISONE(r)*/ || l == r) return 0; if (ISZERO(r)) return l; if (LEVEL(l) > LEVEL(r)) return zdiff_rec(l, LOW(r)); - entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and)); + entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_diff)); - if (entry.a == l && entry.b == r && entry.c == bddop_and) { + if (entry.a == l && entry.b == r && entry.c == bddop_diff) { if (CACHESTATS) cachestats.opHit++; return entry.res; @@ -1611,11 +1628,11 @@ if (LEVEL(l) == LEVEL(r)) { PUSHREF(zdiff_rec(LOW(l), LOW(r))); PUSHREF(zdiff_rec(HIGH(l), HIGH(r))); - res = bdd_makenode(LEVEL(l), READREF(2), READREF(1)); + res = zdd_makenode(LEVEL(l), READREF(2), READREF(1)); POPREF(2); } else { PUSHREF(zdiff_rec(LOW(l), r)); - res = bdd_makenode(LEVEL(l), READREF(1), HIGH(l)); + res = zdd_makenode(LEVEL(l), READREF(1), HIGH(l)); POPREF(1); } @@ -2050,7 +2067,9 @@ default: res = apply_rec(r2, r1); break; } } else { - res = bdd_makenode(LEVEL(r), READREF(2), READREF(1)); + res = ZDD + ? zdd_makenode(LEVEL(r), READREF(2), READREF(1)) + : bdd_makenode(LEVEL(r), READREF(2), READREF(1)); } POPREF(2); @@ -3207,22 +3226,36 @@ } int bdd_makenode(int level, int low, int high) { - int hash2; - int res; + if (VERIFY_ASSERTIONS) _assert(!ZDD); + + if (CACHESTATS) + cachestats.uniqueAccess++; + // check whether children are equal + if (low == high) + return low; + + return makenode(level, low, high); + } + + int zdd_makenode(int level, int low, int high) { + if (VERIFY_ASSERTIONS) _assert(ZDD); + if (CACHESTATS) cachestats.uniqueAccess++; + + // check whether high child is zero + if (high == 0) + return low; + + return makenode(level, low, high); + } + + // Don't call directly - call bdd_makenode or zdd_makenode instead. + private int makenode(int level, int low, int high) { + int hash2; + int res; - if (ZDD) { - /* check whether high child is zero */ - if (high == 0) - return low; - } else { - /* check whether childs are equal */ - if (low == high) - return low; - } - /* Try to find an existing node of this kind */ hash2 = NODEHASH(level, low, high); res = HASH(hash2); @@ -3715,6 +3748,7 @@ bdd_error(BDD_VAR); bdd_delref(pair.result[bddvar2level[oldvar]]); + // TODO: revisit for zdd pair.result[bddvar2level[oldvar]] = bdd_ithvar(newvar); pair.id = update_pairsid(); @@ -3748,6 +3782,7 @@ void bdd_resetpair(bddPair p) { int n; + // TODO: revisit for zdd for (n = 0; n < bddvarnum; n++) p.result[n] = bdd_ithvar(bddlevel2var[n]); p.last = 0; @@ -3826,6 +3861,7 @@ System.arraycopy(p.result, 0, new_result, 0, oldsize); p.result = new_result; + // TODO: revisit for zdd for (n = oldsize; n < newsize; n++) p.result[n] = bdd_ithvar(bddlevel2var[n]); } @@ -4757,16 +4793,36 @@ bddrefstack = new int[num * 2 + 1]; bddrefstacktop = 0; + if (ZDD) + bddvarnum = 0; // need to recreate all of them for ZDD + + univ = 1; for (bdv = bddvarnum; bddvarnum < num; bddvarnum++) { - bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1)); - bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0); - POPREF(1); + if (ZDD) { + int res = 1, res_not = 1; + for (int k = num-1; k >= 0; --k) { + PUSHREF(res); + PUSHREF(res_not); + PUSHREF(univ); + res = zdd_makenode(k, (k == bddvarnum)?0:res, res); + res_not = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not); + if (bdv == bddvarnum) univ = zdd_makenode(k, univ, univ); + POPREF(3); + } + bddvarset[bddvarnum * 2] = res; + bddvarset[bddvarnum * 2 + 1] = res_not; + SETMAXREF(univ); + } else { + bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1)); + bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0); + POPREF(1); + } if (bdderrorcond != 0) { bddvarnum = bdv; return -bdderrorcond; } - + SETMAXREF(bddvarset[bddvarnum * 2]); SETMAXREF(bddvarset[bddvarnum * 2 + 1]); bddlevel2var[bddvarnum] = bddvarnum; @@ -5717,6 +5773,7 @@ int next; } + // TODO: revisit for zdd int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException { int key, var, low, high, root = 0, n; Modified: trunk/JavaBDD/net/sf/javabdd/MicroFactory.java =================================================================== --- trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-26 16:42:39 UTC (rev 464) +++ trunk/JavaBDD/net/sf/javabdd/MicroFactory.java 2006-07-26 16:42:44 UTC (rev 465) @@ -149,6 +149,7 @@ protected int ithVar_impl(int var) { return bdd_ithvar(var); } protected int nithVar_impl(int var) { return bdd_nithvar(var); } + protected int makenode_impl(int lev, int lo, int hi) { return bdd_makenode(lev, lo, hi); } protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); } protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); } protected int not_impl(int v1) { return bdd_not(v1); } This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
|
From: <joe...@us...> - 2006-11-30 09:22:44
|
Revision: 470
http://svn.sourceforge.net/javabdd/?rev=470&view=rev
Author: joewhaley
Date: 2006-11-30 01:22:42 -0800 (Thu, 30 Nov 2006)
Log Message:
-----------
Implement ZDD iterators.
Modified Paths:
--------------
trunk/JavaBDD/net/sf/javabdd/BDD.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-11-29 08:07:31 UTC (rev 469)
+++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-11-30 09:22:42 UTC (rev 470)
@@ -598,10 +598,25 @@
BDD rn = lo_empty ? r.high() : r.low();
int v = rn.isOne()||rn.isZero() ? f.varNum() - 1 : rn.level() - 1;
for ( ; v > LEVEL_r; --v) {
- allsatProfile[useLevel?v:f.level2Var(v)] = -1;
+ allsatProfile[useLevel?v:f.level2Var(v)] = f.isZDD()?(byte)0:(byte)-1;
}
if (!lo_empty) {
- hiStack.addLast(r);
+ if (f.isZDD()) {
+ // Check for dont-care bits in ZDD.
+ BDD rh = r.high();
+ boolean isDontCare = rn.equals(rh);
+ rh.free();
+ if (isDontCare) {
+ // low child == high child, this is a dont-care bit.
+ allsatProfile[useLevel?v:f.level2Var(v)] = -1;
+ r.free();
+ } else {
+ hiStack.addLast(r);
+ }
+ } else {
+ // BDD.
+ hiStack.addLast(r);
+ }
} else {
r.free();
}
@@ -965,7 +980,7 @@
throw new NoSuchElementException();
}
//if (lastReturned != null) lastReturned.free();
- lastReturned = f.one();
+ lastReturned = f.universe();
//for (int i = 0; i < v.length; ++i) {
for (int i = v.length-1; i >= 0; --i) {
int li = v[i];
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-29 08:07:31 UTC (rev 469)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-30 09:22:42 UTC (rev 470)
@@ -2978,37 +2978,42 @@
return r;
if (LEVEL(r) < LEVEL(var)) {
+ // r is not in the set
if (ISZERO(LOW(r))) {
int res = satoneset_rec(HIGH(r), var);
- int m = bdd_makenode(LEVEL(r), BDDZERO, res);
+ int m = makenode_impl(LEVEL(r), BDDZERO, res);
PUSHREF(m);
return m;
} else {
int res = satoneset_rec(LOW(r), var);
- int m = bdd_makenode(LEVEL(r), res, BDDZERO);
+ int m = makenode_impl(LEVEL(r), res, (ZDD && LOW(r) == HIGH(r))?res:BDDZERO);
PUSHREF(m);
return m;
}
} else if (LEVEL(var) < LEVEL(r)) {
int res = satoneset_rec(r, HIGH(var));
- if (satPolarity) {
- int m = bdd_makenode(LEVEL(var), BDDZERO, res);
+ if (!ZDD && satPolarity) {
+ int m = makenode_impl(LEVEL(var), BDDZERO, res);
PUSHREF(m);
return m;
} else {
- int m = bdd_makenode(LEVEL(var), res, BDDZERO);
+ int m = makenode_impl(LEVEL(var), res, BDDZERO);
PUSHREF(m);
return m;
}
} else /* LEVEL(r) == LEVEL(var) */ {
if (ISZERO(LOW(r))) {
int res = satoneset_rec(HIGH(r), HIGH(var));
- int m = bdd_makenode(LEVEL(r), BDDZERO, res);
+ int m = makenode_impl(LEVEL(r), BDDZERO, res);
PUSHREF(m);
return m;
} else {
int res = satoneset_rec(LOW(r), HIGH(var));
- int m = bdd_makenode(LEVEL(r), res, BDDZERO);
+ int m;
+ if (ZDD && satPolarity && LOW(r) == HIGH(r))
+ m = zdd_makenode(LEVEL(r), BDDZERO, res);
+ else
+ m = makenode_impl(LEVEL(r), res, BDDZERO);
PUSHREF(m);
return m;
}
@@ -3030,7 +3035,7 @@
res = fullsatone_rec(r);
for (v = LEVEL(r) - 1; v >= 0; v--) {
- res = PUSHREF(ZDD?zdd_makenode(v, res, 0):bdd_makenode(v, res, 0));
+ res = PUSHREF(makenode_impl(v, res, 0));
}
bdd_enable_reorder();
@@ -3048,19 +3053,19 @@
int v;
for (v = LEVEL(LOW(r)) - 1; v > LEVEL(r); v--) {
- res = PUSHREF(ZDD?zdd_makenode(v, res, 0):bdd_makenode(v, res, 0));
+ res = PUSHREF(makenode_impl(v, res, 0));
}
- return PUSHREF(ZDD?zdd_makenode(LEVEL(r), res, 0):bdd_makenode(LEVEL(r), res, 0));
+ return PUSHREF(makenode_impl(LEVEL(r), res, 0));
} else {
int res = fullsatone_rec(HIGH(r));
int v;
for (v = LEVEL(HIGH(r)) - 1; v > LEVEL(r); v--) {
- res = PUSHREF(ZDD?zdd_makenode(v, res, 0):bdd_makenode(v, res, 0));
+ res = PUSHREF(makenode_impl(v, res, 0));
}
- return PUSHREF(ZDD?zdd_makenode(LEVEL(r), 0, res):bdd_makenode(LEVEL(r), 0, res));
+ return PUSHREF(makenode_impl(LEVEL(r), 0, res));
}
}
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <joe...@us...> - 2006-12-03 10:32:29
|
Revision: 472
http://svn.sourceforge.net/javabdd/?rev=472&view=rev
Author: joewhaley
Date: 2006-12-03 02:32:26 -0800 (Sun, 03 Dec 2006)
Log Message:
-----------
For ZDD: Fixed toString() and an embarrassing bug in ithVar/setvarnum.
Updated TestBDDFactory to work with ZDDs and newer APIs.
Modified Paths:
--------------
trunk/JavaBDD/net/sf/javabdd/BDD.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java
Modified: trunk/JavaBDD/net/sf/javabdd/BDD.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-11-30 09:23:43 UTC (rev 471)
+++ trunk/JavaBDD/net/sf/javabdd/BDD.java 2006-12-03 10:32:26 UTC (rev 472)
@@ -546,6 +546,11 @@
protected byte[] allsatProfile;
protected final boolean useLevel;
+ protected AllSatIterator(BDDFactory factory, boolean level) {
+ f = factory;
+ useLevel = level;
+ }
+
/**
* Constructs a satisfying-assignment iterator on the given BDD.
* next() returns a byte array indexed by BDD variable number.
@@ -1289,6 +1294,8 @@
public String toString() {
BDDFactory f = this.getFactory();
int[] set = new int[f.varNum()];
+ if (f.isZDD())
+ Arrays.fill(set, 1);
StringBuffer sb = new StringBuffer();
bdd_printset_rec(f, sb, this, set);
return sb.toString();
@@ -1316,17 +1323,34 @@
}
sb.append('>');
} else {
- set[f.var2Level(r.var())] = 1;
- BDD rl = r.low();
- bdd_printset_rec(f, sb, rl, set);
- rl.free();
-
- set[f.var2Level(r.var())] = 2;
- BDD rh = r.high();
- bdd_printset_rec(f, sb, rh, set);
- rh.free();
-
- set[f.var2Level(r.var())] = 0;
+ if (f.isZDD()) {
+ if (r.low().equals(r.high())) {
+ set[f.var2Level(r.var())] = 0;
+ } else {
+ BDD rl = r.low();
+ bdd_printset_rec(f, sb, rl, set);
+ rl.free();
+
+ set[f.var2Level(r.var())] = 2;
+ }
+ BDD rl = r.high();
+ bdd_printset_rec(f, sb, rl, set);
+ rl.free();
+
+ set[f.var2Level(r.var())] = 1;
+ } else {
+ set[f.var2Level(r.var())] = 1;
+ BDD rl = r.low();
+ bdd_printset_rec(f, sb, rl, set);
+ rl.free();
+
+ set[f.var2Level(r.var())] = 2;
+ BDD rh = r.high();
+ bdd_printset_rec(f, sb, rh, set);
+ rh.free();
+
+ set[f.var2Level(r.var())] = 0;
+ }
}
}
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-11-30 09:23:43 UTC (rev 471)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-12-03 10:32:26 UTC (rev 472)
@@ -2943,12 +2943,12 @@
if (ISZERO(LOW(r))) {
int res = satone_rec(HIGH(r));
- int m = bdd_makenode(LEVEL(r), BDDZERO, res);
+ int m = makenode_impl(LEVEL(r), BDDZERO, res);
PUSHREF(m);
return m;
} else {
int res = satone_rec(LOW(r));
- int m = bdd_makenode(LEVEL(r), res, BDDZERO);
+ int m = makenode_impl(LEVEL(r), res, (ZDD && LOW(r)==HIGH(r))?res:BDDZERO);
PUSHREF(m);
return m;
}
@@ -5003,13 +5003,22 @@
if (ZDD) {
int res = 1, res_not = 1;
for (int k = num-1; k >= 0; --k) {
- PUSHREF(res);
- PUSHREF(res_not);
- PUSHREF(univ);
- res = zdd_makenode(k, (k == bddvarnum)?0:res, res);
- res_not = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not);
- if (bdv == bddvarnum) univ = zdd_makenode(k, univ, univ);
- POPREF(3);
+ int res2 = zdd_makenode(k, (k == bddvarnum)?0:res, res);
+ INCREF(res2);
+ DECREF(res);
+ res = res2;
+
+ int res_not2 = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not);
+ INCREF(res_not2);
+ DECREF(res_not);
+ res_not = res_not2;
+
+ if (bdv == bddvarnum) {
+ int univ2 = zdd_makenode(k, univ, univ);
+ INCREF(univ2);
+ DECREF(univ);
+ univ = univ2;
+ }
}
bddvarset[bddvarnum * 2] = res;
bddvarset[bddvarnum * 2 + 1] = res_not;
@@ -5040,7 +5049,7 @@
bdd_operator_varresize();
if (ZDD) {
- System.out.println("Changed number of ZDD variables, all existing ZDDs are now invalid.");
+ System.out.println("Changed number of ZDD variables to "+num+", all existing ZDDs are now invalid.");
// Need to rebuild varsets for existing domains.
for (int n = 0; n < fdvarnum; n++) {
domain[n].var.free();
Modified: trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java 2006-11-30 09:23:43 UTC (rev 471)
+++ trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java 2006-12-03 10:32:26 UTC (rev 472)
@@ -11,9 +11,11 @@
import java.math.BigInteger;
/**
- * <p>This BDD factory is used to test other BDD factories. It is a wrapper around
- * two BDD factories, and all operations are performed on both factories. It
- * throws an exception if the results from the two implementations do not match.</p>
+ * <p>
+ * This BDD factory is used to test other BDD factories. It is a wrapper around
+ * two BDD factories, and all operations are performed on both factories. It
+ * throws an exception if the results from the two implementations do not match.
+ * </p>
*
* @see net.sf.javabdd.BDDFactory
*
@@ -21,11 +23,11 @@
* @version $Id$
*/
public class TestBDDFactory extends BDDFactory {
-
BDDFactory f1, f2;
public TestBDDFactory(BDDFactory a, BDDFactory b) {
- f1 = a; f2 = b;
+ f1 = a;
+ f2 = b;
}
public static BDDFactory init(int nodenum, int cachesize) {
@@ -41,36 +43,34 @@
throw new InternalError(s);
}
}
-
+
public static final void assertSame(BDD b1, BDD b2, String s) {
if (!b1.toString().equals(b2.toString())) {
//if (b1.nodeCount() != b2.nodeCount()) {
- System.out.println("b1 = "+b1.nodeCount());
- System.out.println("b2 = "+b2.nodeCount());
- System.out.println("b1 = "+b1.toString());
- System.out.println("b2 = "+b2.toString());
+ System.out.println("b1 = " + b1.nodeCount());
+ System.out.println("b2 = " + b2.nodeCount());
+ System.out.println("b1 = " + b1.toString());
+ System.out.println("b2 = " + b2.toString());
throw new InternalError(s);
}
}
public static final void assertSame(boolean b, BDD b1, BDD b2, String s) {
if (!b) {
- System.err.println("b1 = "+b1);
- System.err.println("b2 = "+b2);
+ System.err.println("b1 = " + b1);
+ System.err.println("b2 = " + b2);
throw new InternalError(s);
}
}
-
+
public static final void assertSame(BDDVarSet b1, BDDVarSet b2, String s) {
assertSame(b1.toBDD(), b2.toBDD(), s);
}
-
+
public static final void assertSame(boolean b, BDDVarSet b1, BDDVarSet b2, String s) {
assertSame(b, b1.toBDD(), b2.toBDD(), s);
}
-
private class TestBDD extends BDD {
-
BDD b1, b2;
TestBDD(BDD a, BDD b) {
@@ -79,21 +79,27 @@
assertSame(a, b, "constructor");
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#getFactory()
*/
public BDDFactory getFactory() {
return TestBDDFactory.this;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#toVarSet()
*/
public BDDVarSet toVarSet() {
return new TestBDDVarSet(b1.toVarSet(), b2.toVarSet());
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#isZero()
*/
public boolean isZero() {
@@ -103,7 +109,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#isOne()
*/
public boolean isOne() {
@@ -113,7 +121,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#var()
*/
public int var() {
@@ -123,7 +133,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#high()
*/
public BDD high() {
@@ -132,7 +144,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#low()
*/
public BDD low() {
@@ -141,7 +155,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#id()
*/
public BDD id() {
@@ -150,7 +166,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#not()
*/
public BDD not() {
@@ -159,133 +177,158 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD)
*/
public BDD ite(BDD thenBDD, BDD elseBDD) {
- BDD c1 = ((TestBDD)thenBDD).b1;
- BDD c2 = ((TestBDD)thenBDD).b2;
- BDD d1 = ((TestBDD)elseBDD).b1;
- BDD d2 = ((TestBDD)elseBDD).b2;
+ BDD c1 = ((TestBDD) thenBDD).b1;
+ BDD c2 = ((TestBDD) thenBDD).b2;
+ BDD d1 = ((TestBDD) elseBDD).b1;
+ BDD d2 = ((TestBDD) elseBDD).b2;
BDD r1 = b1.ite(c1, d1);
BDD r2 = b2.ite(c2, d2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDVarSet)
*/
public BDD relprod(BDD that, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet d1 = ((TestBDDVarSet)var).b1;
- BDDVarSet d2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet d1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet d2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.relprod(c1, d1);
BDD r2 = b2.relprod(c2, d2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int)
*/
public BDD compose(BDD g, int var) {
- BDD c1 = ((TestBDD)g).b1;
- BDD c2 = ((TestBDD)g).b2;
+ BDD c1 = ((TestBDD) g).b1;
+ BDD c2 = ((TestBDD) g).b2;
BDD r1 = b1.compose(c1, var);
BDD r2 = b2.compose(c2, var);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing)
*/
public BDD veccompose(BDDPairing pair) {
- BDDPairing c1 = ((TestBDDPairing)pair).b1;
- BDDPairing c2 = ((TestBDDPairing)pair).b2;
+ BDDPairing c1 = ((TestBDDPairing) pair).b1;
+ BDDPairing c2 = ((TestBDDPairing) pair).b2;
BDD r1 = b1.veccompose(c1);
BDD r2 = b2.veccompose(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD)
*/
public BDD constrain(BDD that) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
BDD r1 = b1.constrain(c1);
BDD r2 = b2.constrain(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet)
*/
public BDD exist(BDDVarSet var) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.exist(c1);
BDD r2 = b2.exist(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD)
*/
public BDD forAll(BDDVarSet var) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.forAll(c1);
BDD r2 = b2.forAll(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD)
*/
public BDD unique(BDDVarSet var) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.unique(c1);
BDD r2 = b2.unique(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD)
*/
public BDD restrict(BDD var) {
- BDD c1 = ((TestBDD)var).b1;
- BDD c2 = ((TestBDD)var).b2;
+ BDD c1 = ((TestBDD) var).b1;
+ BDD c2 = ((TestBDD) var).b2;
BDD r1 = b1.restrict(c1);
BDD r2 = b2.restrict(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD)
*/
public BDD restrictWith(BDD var) {
- BDD c1 = ((TestBDD)var).b1;
- BDD c2 = ((TestBDD)var).b2;
+ BDD c1 = ((TestBDD) var).b1;
+ BDD c2 = ((TestBDD) var).b2;
b1.restrictWith(c1);
b2.restrictWith(c2);
assertSame(b1, b2, "restrict");
return this;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet)
*/
public BDD simplify(BDDVarSet d) {
- BDDVarSet c1 = ((TestBDDVarSet)d).b1;
- BDDVarSet c2 = ((TestBDDVarSet)d).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) d).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) d).b2;
BDD r1 = b1.simplify(c1);
BDD r2 = b2.simplify(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#support()
*/
public BDDVarSet support() {
@@ -294,69 +337,86 @@
return new TestBDDVarSet(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp)
*/
public BDD apply(BDD that, BDDOp opr) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
BDD r1 = b1.apply(c1, opr);
BDD r2 = b2.apply(c2, opr);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp)
*/
public BDD applyWith(BDD that, BDDOp opr) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
b1.applyWith(c1, opr);
b2.applyWith(c2, opr);
- assertSame(b1, b2, "applyWith "+opr);
+ assertSame(b1, b2, "applyWith " + opr);
return this;
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
*/
public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet e1 = ((TestBDDVarSet)var).b1;
- BDDVarSet e2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet e1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet e2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.applyAll(c1, opr, e1);
BDD r2 = b2.applyAll(c2, opr, e2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
*/
public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet e1 = ((TestBDDVarSet)var).b1;
- BDDVarSet e2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet e1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet e2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.applyEx(c1, opr, e1);
BDD r2 = b2.applyEx(c2, opr, e2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD,
+ * net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
*/
public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
- BDDVarSet e1 = ((TestBDDVarSet)var).b1;
- BDDVarSet e2 = ((TestBDDVarSet)var).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
+ BDDVarSet e1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet e2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.applyUni(c1, opr, e1);
BDD r2 = b2.applyUni(c2, opr, e2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#satOne()
*/
public BDD satOne() {
@@ -365,7 +425,9 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#fullSatOne()
*/
public BDD fullSatOne() {
@@ -374,41 +436,49 @@
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean)
*/
public BDD satOne(BDDVarSet var, boolean pol) {
- BDDVarSet c1 = ((TestBDDVarSet)var).b1;
- BDDVarSet c2 = ((TestBDDVarSet)var).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) var).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) var).b2;
BDD r1 = b1.satOne(c1, pol);
BDD r2 = b2.satOne(c2, pol);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing)
*/
public BDD replace(BDDPairing pair) {
- BDDPairing c1 = ((TestBDDPairing)pair).b1;
- BDDPairing c2 = ((TestBDDPairing)pair).b2;
+ BDDPairing c1 = ((TestBDDPairing) pair).b1;
+ BDDPairing c2 = ((TestBDDPairing) pair).b2;
BDD r1 = b1.replace(c1);
BDD r2 = b2.replace(c2);
return new TestBDD(r1, r2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing)
*/
public BDD replaceWith(BDDPairing pair) {
- BDDPairing c1 = ((TestBDDPairing)pair).b1;
- BDDPairing c2 = ((TestBDDPairing)pair).b2;
+ BDDPairing c1 = ((TestBDDPairing) pair).b1;
+ BDDPairing c2 = ((TestBDDPairing) pair).b2;
b1.replaceWith(c1);
b2.replaceWith(c2);
assertSame(b1, b2, "replaceWith");
return this;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#printDot()
*/
public void printDot() {
@@ -416,17 +486,81 @@
b1.printDot();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#toString()
+ */
+ public String toString() {
+ // String already checked.
+ return b1.toString();
+ }
+
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#toStringWithDomains(net.sf.javabdd.BDD.BDDToString)
+ */
+ public String toStringWithDomains(BDDToString ts) {
+ String s1 = b1.toStringWithDomains(ts);
+ String s2 = b2.toStringWithDomains(ts);
+ assertSame(s1.equals(s2), "toStringWithDomains");
+ return s1;
+ }
+
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#allsat()
+ */
+ public AllSatIterator allsat() {
+ return new AllSatIterator(TestBDDFactory.this, false) {
+ AllSatIterator i1 = b1.allsat();
+ AllSatIterator i2 = b2.allsat();
+
+ public boolean hasNext() {
+ boolean r1 = i1.hasNext();
+ boolean r2 = i2.hasNext();
+ assertSame(r1 == r2, b1, b2, "allsat.hasNext");
+ return r1;
+ }
+
+ public byte[] nextSat() {
+ byte[] r1 = i1.nextSat();
+ byte[] r2 = i2.nextSat();
+ assertSame(Arrays.equals(r1, r2), b1, b2, "allsat.nextSat");
+ return r1;
+ }
+ };
+ }
+
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDD#scanAllVar()
+ */
+ public BigInteger[] scanAllVar() {
+ BigInteger[] r1 = b1.scanAllVar();
+ BigInteger[] r2 = b2.scanAllVar();
+ assertSame(Arrays.equals(r1, r2), b1, b2, "scanAllVar");
+ return r1;
+ }
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#nodeCount()
*/
public int nodeCount() {
int r1 = b1.nodeCount();
int r2 = b2.nodeCount();
- assertSame(r1 == r2, b1, b2, "nodeCount");
+ if (false) assertSame(r1 == r2, b1, b2, "nodeCount");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#pathCount()
*/
public double pathCount() {
@@ -436,7 +570,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#satCount()
*/
public double satCount() {
@@ -446,32 +582,35 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#varProfile()
*/
public int[] varProfile() {
int[] r1 = b1.varProfile();
int[] r2 = b2.varProfile();
- assertSame(r1.length == r2.length, "varProfile");
- for (int i=0; i<r1.length; ++i) {
- assertSame(r1[i] == r2[i], "varProfile");
- }
+ assertSame(Arrays.equals(r1, r2), "varProfile");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD)
*/
public boolean equals(BDD that) {
- BDD c1 = ((TestBDD)that).b1;
- BDD c2 = ((TestBDD)that).b2;
+ BDD c1 = ((TestBDD) that).b1;
+ BDD c2 = ((TestBDD) that).b2;
boolean r1 = b1.equals(c1);
boolean r2 = b2.equals(c2);
assertSame(r1 == r2, b1, b2, "equals");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#hashCode()
*/
public int hashCode() {
@@ -480,7 +619,9 @@
return b2.hashCode();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDD#free()
*/
public void free() {
@@ -488,9 +629,7 @@
b2.free();
}
}
-
private class TestBDDVarSet extends BDDVarSet {
-
BDDVarSet b1, b2;
TestBDDVarSet(BDDVarSet a, BDDVarSet b) {
@@ -513,7 +652,7 @@
BDD r2 = b2.toBDD();
return new TestBDD(r1, r2);
}
-
+
public BDDVarSet id() {
BDDVarSet r1 = b1.id();
BDDVarSet r2 = b2.id();
@@ -521,16 +660,16 @@
}
public BDDVarSet intersect(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
BDDVarSet r1 = b1.intersect(c1);
BDDVarSet r2 = b2.intersect(c2);
return new TestBDDVarSet(r1, r2);
}
public BDDVarSet intersectWith(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
b1.intersectWith(c1);
b2.intersectWith(c2);
assertSame(b1, b2, "intersectWith");
@@ -566,8 +705,8 @@
}
public BDDVarSet union(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
BDDVarSet r1 = b1.union(c1);
BDDVarSet r2 = b2.union(c2);
return new TestBDDVarSet(r1, r2);
@@ -580,8 +719,8 @@
}
public BDDVarSet unionWith(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
b1.unionWith(c1);
b2.unionWith(c2);
assertSame(b1, b2, "unionWith");
@@ -594,45 +733,62 @@
assertSame(b1, b2, "unionWith");
return this;
}
-
+
public int hashCode() {
// TODO Compare!
b1.hashCode();
return b2.hashCode();
}
-
+
public boolean equals(BDDVarSet that) {
- BDDVarSet c1 = ((TestBDDVarSet)that).b1;
- BDDVarSet c2 = ((TestBDDVarSet)that).b2;
+ BDDVarSet c1 = ((TestBDDVarSet) that).b1;
+ BDDVarSet c2 = ((TestBDDVarSet) that).b2;
boolean r1 = b1.equals(c1);
boolean r2 = b2.equals(c2);
assertSame(r1 == r2, b1, b2, "equals");
return r1;
}
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#zero()
*/
public BDD zero() {
return new TestBDD(f1.zero(), f2.zero());
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#one()
*/
public BDD one() {
return new TestBDD(f1.one(), f2.one());
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDDFactory#universe()
+ */
+ public BDD universe() {
+ return new TestBDD(f1.universe(), f2.universe());
+ }
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#emptySet()
*/
public BDDVarSet emptySet() {
return new TestBDDVarSet(f1.emptySet(), f2.emptySet());
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#initialize(int, int)
*/
protected void initialize(int nodenum, int cachesize) {
@@ -640,7 +796,9 @@
f2.initialize(nodenum, cachesize);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#isInitialized()
*/
public boolean isInitialized() {
@@ -650,7 +808,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#done()
*/
public void done() {
@@ -658,23 +818,29 @@
f2.done();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setError(int)
*/
public void setError(int code) {
f1.setError(code);
f2.setError(code);
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#clearError()
*/
public void clearError() {
f1.clearError();
f2.clearError();
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setMaxNodeNum(int)
*/
public int setMaxNodeNum(int size) {
@@ -684,7 +850,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setMinFreeNodes(double)
*/
public double setMinFreeNodes(double x) {
@@ -694,17 +862,21 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double)
*/
public double setIncreaseFactor(double x) {
double r1 = f1.setIncreaseFactor(x);
double r2 = f2.setIncreaseFactor(x);
- assertSame(r1 == r2, "setIncreaseFactor");
+ if (false) assertSame(r1 == r2, "setIncreaseFactor");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setMaxIncrease(int)
*/
public int setMaxIncrease(int x) {
@@ -714,7 +886,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setCacheRatio(double)
*/
public double setCacheRatio(double x) {
@@ -724,17 +898,21 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setNodeTableSize(int)
*/
public int setNodeTableSize(int size) {
int r1 = f1.setNodeTableSize(size);
int r2 = f2.setNodeTableSize(size);
- assertSame(r1 == r2, "setNodeTableSize");
+ if (false) assertSame(r1 == r2, "setNodeTableSize");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setCacheSize(int)
*/
public int setCacheSize(int size) {
@@ -743,8 +921,10 @@
assertSame(r1 == r2, "setCacheSize");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#varNum()
*/
public int varNum() {
@@ -754,31 +934,39 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setVarNum(int)
*/
public int setVarNum(int num) {
int r1 = f1.setVarNum(num);
int r2 = f2.setVarNum(num);
- //assertSame(r1 == r2, "setVarNum");
+ // assertSame(r1 == r2, "setVarNum");
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#ithVar(int)
*/
public BDD ithVar(int var) {
return new TestBDD(f1.ithVar(var), f2.ithVar(var));
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#nithVar(int)
*/
public BDD nithVar(int var) {
return new TestBDD(f1.nithVar(var), f2.nithVar(var));
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printAll()
*/
public void printAll() {
@@ -786,32 +974,40 @@
f1.printAll();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD)
*/
public void printTable(BDD b) {
// TODO Compare!
- BDD b1 = ((TestBDD)b).b1;
+ BDD b1 = ((TestBDD) b).b1;
f1.printTable(b1);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#load(java.lang.String)
*/
public BDD load(String filename) throws IOException {
return new TestBDD(f1.load(filename), f2.load(filename));
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#save(java.lang.String, net.sf.javabdd.BDD)
*/
public void save(String filename, BDD var) throws IOException {
// TODO Compare!
- BDD b1 = ((TestBDD)var).b1;
+ BDD b1 = ((TestBDD) var).b1;
f1.save(filename, b1);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#level2Var(int)
*/
public int level2Var(int level) {
@@ -821,7 +1017,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#var2Level(int)
*/
public int var2Level(int var) {
@@ -831,7 +1029,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod)
*/
public void reorder(ReorderMethod m) {
@@ -839,7 +1039,9 @@
f2.reorder(m);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod)
*/
public void autoReorder(ReorderMethod method) {
@@ -847,15 +1049,20 @@
f2.autoReorder(method);
}
- /* (non-Javadoc)
- * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int)
+ /*
+ * (non-Javadoc)
+ *
+ * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod,
+ * int)
*/
public void autoReorder(ReorderMethod method, int max) {
f1.autoReorder(method, max);
f2.autoReorder(method, max);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getReorderMethod()
*/
public ReorderMethod getReorderMethod() {
@@ -865,7 +1072,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getReorderTimes()
*/
public int getReorderTimes() {
@@ -875,7 +1084,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#disableReorder()
*/
public void disableReorder() {
@@ -883,7 +1094,9 @@
f2.disableReorder();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#enableReorder()
*/
public void enableReorder() {
@@ -891,7 +1104,9 @@
f2.enableReorder();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#reorderVerbose(int)
*/
public int reorderVerbose(int v) {
@@ -901,7 +1116,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#setVarOrder(int[])
*/
public void setVarOrder(int[] neworder) {
@@ -909,7 +1126,9 @@
f2.setVarOrder(neworder);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean)
*/
public void addVarBlock(int first, int last, boolean fixed) {
@@ -917,7 +1136,9 @@
f2.addVarBlock(first, last, fixed);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#varBlockAll()
*/
public void varBlockAll() {
@@ -925,7 +1146,9 @@
f2.varBlockAll();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#clearVarBlocks()
*/
public void clearVarBlocks() {
@@ -933,7 +1156,9 @@
f2.clearVarBlocks();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printOrder()
*/
public void printOrder() {
@@ -941,14 +1166,16 @@
f1.printOrder();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection)
*/
public int nodeCount(Collection r) {
LinkedList a1 = new LinkedList();
LinkedList a2 = new LinkedList();
- for (Iterator i=r.iterator(); i.hasNext();) {
- TestBDD b = (TestBDD)i.next();
+ for (Iterator i = r.iterator(); i.hasNext();) {
+ TestBDD b = (TestBDD) i.next();
a1.add(b.b1);
a2.add(b.b2);
}
@@ -958,7 +1185,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getNodeTableSize()
*/
public int getNodeTableSize() {
@@ -968,7 +1197,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getNodeNum()
*/
public int getNodeNum() {
@@ -978,7 +1209,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getCacheSize()
*/
public int getCacheSize() {
@@ -987,8 +1220,10 @@
assertSame(r1 == r2, "getCacheSize");
return r1;
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#reorderGain()
*/
public int reorderGain() {
@@ -998,7 +1233,9 @@
return r1;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#printStat()
*/
public void printStat() {
@@ -1006,7 +1243,9 @@
f1.printStat();
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#makePair()
*/
public BDDPairing makePair() {
@@ -1015,7 +1254,9 @@
return new TestBDDPairing(p1, p2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#swapVar(int, int)
*/
public void swapVar(int v1, int v2) {
@@ -1023,30 +1264,34 @@
f2.swapVar(v1, v2);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger)
*/
protected BDDDomain createDomain(int a, BigInteger b) {
return new TestBDDDomain(a, b);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#createBitVector(int)
*/
protected BDDBitVector createBitVector(int a) {
return new TestBDDBitVector(a);
}
-
private static class TestBDDPairing extends BDDPairing {
-
BDDPairing b1, b2;
-
+
TestBDDPairing(BDDPairing p1, BDDPairing p2) {
this.b1 = p1;
this.b2 = p2;
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDPairing#set(int, int)
*/
public void set(int oldvar, int newvar) {
@@ -1054,7 +1299,9 @@
b2.set(oldvar, newvar);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
*/
public void set(int oldvar, BDD newvar) {
@@ -1062,53 +1309,53 @@
b2.set(oldvar, newvar);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDPairing#reset()
*/
public void reset() {
b1.reset();
b2.reset();
}
-
}
-
private class TestBDDDomain extends BDDDomain {
-
private TestBDDDomain(int a, BigInteger b) {
super(a, b);
}
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDDomain#getFactory()
*/
public BDDFactory getFactory() {
return TestBDDFactory.this;
}
-
}
-
private class TestBDDBitVector extends BDDBitVector {
-
TestBDDBitVector(int a) {
super(a);
}
-
- /* (non-Javadoc)
+
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDBitVector#getFactory()
*/
public BDDFactory getFactory() {
return TestBDDFactory.this;
}
-
}
-
public static final String REVISION = "$Revision$";
- /* (non-Javadoc)
+ /*
+ * (non-Javadoc)
+ *
* @see net.sf.javabdd.BDDFactory#getVersion()
*/
public String getVersion() {
- return "TestBDD "+REVISION.substring(11, REVISION.length()-2)+
- " of ("+f1.getVersion()+","+f2.getVersion()+")";
+ return "TestBDD " + REVISION.substring(11, REVISION.length() - 2)
+ + " of (" + f1.getVersion() + "," + f2.getVersion() + ")";
}
}
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <joe...@us...> - 2006-12-05 10:58:18
|
Revision: 474
http://svn.sourceforge.net/javabdd/?rev=474&view=rev
Author: joewhaley
Date: 2006-12-05 02:58:16 -0800 (Tue, 05 Dec 2006)
Log Message:
-----------
Working ZDD exists() and relprod().
Modified Paths:
--------------
trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java
trunk/JavaBDD/net/sf/javabdd/JFactory.java
trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java
Modified: trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-12-03 10:34:02 UTC (rev 473)
+++ trunk/JavaBDD/net/sf/javabdd/BDDFactoryIntImpl.java 2006-12-05 10:58:16 UTC (rev 474)
@@ -421,7 +421,8 @@
} else {
int k = do_unionlevel(high_impl(v), lev);
addref_impl(k);
- int result = makenode_impl(lev, zero_impl(), k);
+ int result = makenode_impl(l, zero_impl(), k);
+ delref_impl(k);
return result;
}
}
Modified: trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-12-03 10:34:02 UTC (rev 473)
+++ trunk/JavaBDD/net/sf/javabdd/BDDVarSet.java 2006-12-05 10:58:16 UTC (rev 474)
@@ -3,6 +3,8 @@
// Licensed under the terms of the GNU LGPL; see COPYING for details.
package net.sf.javabdd;
+import java.util.Arrays;
+
/**
* <p>Some BDD methods, namely <tt>exist()</tt>, <tt>forall()</tt>, <tt>unique()</tt>,
* <tt>relprod()</tt>, <tt>applyAll()</tt>, <tt>applyEx()</tt>, <tt>applyUni()</tt>,
@@ -31,6 +33,10 @@
public abstract int[] toArray();
public abstract int[] toLevelArray();
+ public String toString() {
+ return Arrays.toString(toArray());
+ }
+
/**
* <p>Scans this BDD and copies the stored variables into an array of BDDDomains.
* The domains returned are guaranteed to be in ascending order.</p>
Modified: trunk/JavaBDD/net/sf/javabdd/JFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-12-03 10:34:02 UTC (rev 473)
+++ trunk/JavaBDD/net/sf/javabdd/JFactory.java 2006-12-05 10:58:16 UTC (rev 474)
@@ -37,7 +37,7 @@
*/
public static boolean FLUSH_CACHE_ON_GC = true;
- static final boolean VERIFY_ASSERTIONS = true;
+ static final boolean VERIFY_ASSERTIONS = false;
static final boolean CACHESTATS = false;
static final boolean SWAPCOUNT = false;
@@ -1431,6 +1431,7 @@
}
checkresize();
+ if (true) bdd_validate(res);
return res;
}
@@ -1565,7 +1566,7 @@
return zand_rec(LOW(l), r);
else if (LEVEL(l) > LEVEL(r))
return zand_rec(l, LOW(r));
- _assert(!ISCONST(l) && !ISCONST(r));
+ if (VERIFY_ASSERTIONS) _assert(!ISCONST(l) && !ISCONST(r));
entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
@@ -1591,6 +1592,82 @@
return res;
}
+ int zrelprod_rec(int l, int r, int lev) {
+ BddCacheDataI entry;
+ int res;
+
+ if (l == r)
+ return zquant_rec(l, lev);
+ if (ISZERO(l) || ISZERO(r))
+ return 0;
+
+ int LEVEL_l = LEVEL(l);
+ int LEVEL_r = LEVEL(r);
+
+ for (;;) {
+ if (lev > quantlast) {
+ applyop = bddop_and;
+ res = zand_rec(l, r);
+ applyop = bddop_or;
+ return res;
+ }
+ if (lev >= LEVEL_l || lev >= LEVEL_r)
+ break;
+ if (INVARSET(lev)) {
+ res = zrelprod_rec(l, r, lev+1);
+ PUSHREF(res);
+ res = zdd_makenode(lev, res, res);
+ POPREF(1);
+ return res;
+ }
+ ++lev;
+ }
+
+ entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and));
+ if (entry.a == l && entry.b == r && entry.c == appexid) {
+ if (CACHESTATS)
+ cachestats.opHit++;
+ return entry.res;
+ }
+ if (CACHESTATS)
+ cachestats.opMiss++;
+
+ if (LEVEL_l == LEVEL_r) {
+ if (VERIFY_ASSERTIONS) _assert(LEVEL_l == lev);
+ PUSHREF(zrelprod_rec(LOW(l), LOW(r), lev+1));
+ PUSHREF(zrelprod_rec(HIGH(l), HIGH(r), lev+1));
+ if (INVARSET(lev)) {
+ res = zor_rec(READREF(2), READREF(1));
+ POPREF(2);
+ PUSHREF(res);
+ res = zdd_makenode(lev, res, res);
+ POPREF(1);
+ } else {
+ res = zdd_makenode(lev, READREF(2), READREF(1));
+ POPREF(2);
+ }
+ } else {
+ if (LEVEL_l < LEVEL_r) {
+ if (VERIFY_ASSERTIONS) _assert(LEVEL_l == lev);
+ res = zrelprod_rec(LOW(l), r, lev+1);
+ } else {
+ if (VERIFY_ASSERTIONS) _assert(LEVEL_r == lev);
+ res = zrelprod_rec(l, LOW(r), lev+1);
+ }
+ if (INVARSET(lev)) {
+ PUSHREF(res);
+ res = zdd_makenode(lev, res, res);
+ POPREF(1);
+ }
+ }
+ entry.a = l;
+ entry.b = r;
+ entry.c = appexid;
+ entry.res = res;
+
+ return res;
+ }
+
int or_rec(int l, int r) {
BddCacheDataI entry;
int res;
@@ -1808,14 +1885,6 @@
if (var < 2) /* Empty set */
return bdd_apply(l, r, opr);
- if (ZDD) {
- // TODO: A real ZDD implementation.
- int x = bdd_addref(bdd_apply(l, r, opr));
- int y = bdd_exist(x, var);
- bdd_delref(x);
- return y;
- }
-
if (applycache == null) applycache = BddCacheI_init(cachesize);
if (appexcache == null) appexcache = BddCacheI_init(cachesize);
if (quantcache == null) quantcache = BddCacheI_init(cachesize);
@@ -1833,7 +1902,11 @@
if (numReorder == 0)
bdd_disable_reorder();
- res = opr == bddop_and ? relprod_rec(l, r) : appquant_rec(l, r);
+ if (opr == bddop_and)
+ res = ZDD ? zrelprod_rec(l, r, 0) : relprod_rec(l, r);
+ else
+ res = appquant_rec(l, r);
+
if (numReorder == 0)
bdd_enable_reorder();
} catch (ReorderException x) {
@@ -2166,13 +2239,32 @@
return res;
}
- int zquant_rec(int r) {
+ int zquant_rec(int r, int lev) {
BddCacheDataI entry;
int res;
- if (r < 2 || LEVEL(r) > quantlast)
+ for (;;) {
+ if (lev > quantlast)
+ return r;
+ if (lev == LEVEL(r))
+ break;
+ if (INVARSET(lev)) {
+ switch (applyop) {
+ case bddop_and: return 0;
+ case bddop_or:
+ PUSHREF(zquant_rec(r, lev+1));
+ res = zdd_makenode(lev, READREF(1), READREF(1));
+ POPREF(1);
+ return res;
+ default: throw new BDDException();
+ }
+ }
+ lev++;
+ }
+
+ if (r < 2)
return r;
-
+
entry = BddCache_lookupI(quantcache, QUANTHASH(r));
if (entry.a == r && entry.c == quantid) {
if (CACHESTATS)
@@ -2182,8 +2274,9 @@
if (CACHESTATS)
cachestats.opMiss++;
- PUSHREF(zquant_rec(LOW(r)));
- PUSHREF(zquant_rec(HIGH(r)));
+ int nlev = LEVEL(r) + 1;
+ PUSHREF(zquant_rec(LOW(r), nlev));
+ PUSHREF(zquant_rec(HIGH(r), nlev));
if (INVARSET(LEVEL(r))) {
int r2 = READREF(2), r1 = READREF(1);
@@ -2192,12 +2285,15 @@
case bddop_or: res = zor_rec(r2, r1); break;
default: throw new BDDException();
}
+ POPREF(2);
+ PUSHREF(res);
+ res = zdd_makenode(LEVEL(r), READREF(1), READREF(1));
+ POPREF(1);
} else {
res = zdd_makenode(LEVEL(r), READREF(2), READREF(1));
+ POPREF(2);
}
- POPREF(2);
-
entry.a = r;
entry.c = quantid;
entry.res = res;
@@ -2465,7 +2561,7 @@
if (numReorder == 0)
bdd_disable_reorder();
- res = quant_rec(r);
+ res = ZDD?zquant_rec(r, 0):quant_rec(r);
if (numReorder == 0)
bdd_enable_reorder();
} catch (ReorderException x) {
@@ -2478,6 +2574,7 @@
}
checkresize();
+ if (true) bdd_validate(res);
return res;
}
@@ -2504,7 +2601,7 @@
if (numReorder == 0)
bdd_disable_reorder();
- res = quant_rec(r);
+ res = ZDD?zquant_rec(r, 0):quant_rec(r);
if (numReorder == 0)
bdd_enable_reorder();
} catch (ReorderException x) {
@@ -2772,7 +2869,7 @@
void support_rec(int r, int[] support) {
- _assert(!ZDD);
+ if (VERIFY_ASSERTIONS) _assert(!ZDD);
if (r < 2)
return;
@@ -2793,7 +2890,7 @@
void zsupport_rec(int r, int lev, int[] support) {
- _assert(ZDD);
+ if (VERIFY_ASSERTIONS) _assert(ZDD);
if (!ISZERO(r)) {
while (lev != LEVEL(r)) {
@@ -3929,7 +4026,7 @@
break;
}
}
- _assert(newIndex != bddvarnum);
+ if (VERIFY_ASSERTIONS) _assert(newIndex != bddvarnum);
}
int tmp = pair.result[oldlev];
pair.result[oldlev] = pair.result[newIndex];
@@ -6295,7 +6392,11 @@
}
}
void bdd_validate(int k) {
- validate(k, -1);
+ try {
+ validate(k, -1);
+ } finally {
+ bdd_unmark(k);
+ }
}
void validate(int k, int lastLevel) {
if (k < 2) return;
@@ -6303,6 +6404,15 @@
//System.out.println("Level("+k+") = "+lev);
if (lev <= lastLevel)
throw new BDDException(lev+" <= "+lastLevel);
+ if (ZDD) {
+ if (HIGH(k) == 0)
+ throw new BDDException("HIGH("+k+")==0");
+ } else {
+ if (LOW(k) == HIGH(k))
+ throw new BDDException("LOW("+k+") == HIGH("+k+")");
+ }
+ if (MARKED(k)) return;
+ SETMARK(k);
//System.out.println("Low:");
validate(LOW(k), lev);
//System.out.println("High:");
Modified: trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java
===================================================================
--- trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java 2006-12-03 10:34:02 UTC (rev 473)
+++ trunk/JavaBDD/net/sf/javabdd/TestBDDFactory.java 2006-12-05 10:58:16 UTC (rev 474)
@@ -64,11 +64,19 @@
}
public static final void assertSame(BDDVarSet b1, BDDVarSet b2, String s) {
- assertSame(b1.toBDD(), b2.toBDD(), s);
+ if (!b1.toString().equals(b2.toString())) {
+ System.out.println("b1 = " + b1.toString());
+ System.out.println("b2 = " + b2.toString());
+ throw new InternalError(s);
+ }
}
public static final void assertSame(boolean b, BDDVarSet b1, BDDVarSet b2, String s) {
- assertSame(b, b1.toBDD(), b2.toBDD(), s);
+ if (!b) {
+ System.err.println("b1 = " + b1);
+ System.err.println("b2 = " + b2);
+ throw new InternalError(s);
+ }
}
private class TestBDD extends BDD {
BDD b1, b2;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X