[Javabdd-checkins] SF.net SVN: javabdd: [452] trunk/JavaBDD/net/sf/javabdd
Brought to you by:
joewhaley
Menu
▾
▴
[Javabdd-checkins] SF.net SVN: javabdd: [452] trunk/JavaBDD/net/sf/javabdd
|
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] |
